From a1d98a90938e7c4aa84c4f02176f3a7b7b9f8bf2 Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 29 Oct 2017 21:42:55 +0100
Subject: [PATCH] Lexer for z3 models
---
src/ModelParser/Lexer.x | 54 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)
create mode 100644 src/ModelParser/Lexer.x
diff --git a/src/ModelParser/Lexer.x b/src/ModelParser/Lexer.x
new file mode 100644
index 0000000..dfda4b4
--- /dev/null
+++ b/src/ModelParser/Lexer.x
@@ -0,0 +1,54 @@
+{
+module ModelParser.Lexer where
+
+import Numeric
+}
+
+%wrapper "basic"
+
+$ident = [0-9a-zA-Z!\._]
+$value = [0-9a-f]
+
+tokens :-
+ $white+ ;
+ "->" { \s -> Tarrow }
+ "{" { \s -> Tbopen }
+ "}" { \s -> Tbclose }
+ "(" { \s -> Tpopen }
+ ")" { \s -> Tpclose }
+ "_" { \s -> Tunderscore }
+ "else" { \s -> Telse}
+ "as-array" { \s -> Tasarray }
+ "BitVec" { \s -> Tbitvec }
+ "as" { \s -> Tas }
+ "const" { \s -> Tconst }
+ "true" { \s -> Tbool True }
+ "false" { \s -> Tbool False }
+ "#x"$value+ { \s -> Tvalue (parseHex s) }
+ $ident+ { \s -> Tident s }
+{
+
+data Token = Tarrow
+ | Tbopen
+ | Tbclose
+ | Tpopen
+ | Tpclose
+ | Tunderscore
+ | Telse
+ | Tasarray
+ | Tbitvec
+ | Tas
+ | Tconst
+ | Tvalue Int
+ | Tbool Bool
+ | Tident String
+ deriving (Eq, Show)
+
+parseHex :: String -> Int
+parseHex ('#' : 'x' : value) = let [(n, "")] = readHex value in n
+
+model1 = "a.null -> false\nj -> #x00000000\ni -> #x00000000\na.length -> #x00000001"
+model2 = "a.length -> #x00000001\na.null -> true\ni!0 -> #x00000000\na -> (_ as-array k!1)\nk!1 -> {\n #x00000000\n}"
+model3 = "a.length -> #x00000003\ni!0 -> #x00000001\na -> (_ as-array k!1)\nk!1 -> {\n #x00000002 -> #x00000001\n #x00000001 -> #x00000000\n else -> #x00000001\n}"
+
+}
\ No newline at end of file
--
GitLab