From 07abaef2027a1c58a8e4f9e9d9c7d554ad924187 Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 5 Nov 2017 14:56:46 +0100
Subject: [PATCH] Separate Model structure from parser
---
.gitignore | 2 ++
src/ModelParser/Model.hs | 14 ++++++++++++++
src/ModelParser/Parser.y | 18 ++++--------------
src/SimpleFormulaChecker.hs | 1 +
4 files changed, 21 insertions(+), 14 deletions(-)
create mode 100644 src/ModelParser/Model.hs
diff --git a/.gitignore b/.gitignore
index 5678842..35ad64d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,5 @@ tests/org/
*.hi
*.o
.DS_Store
+/src/ModelParser/Lexer.hs
+/src/ModelParser/Parser.hs
diff --git a/src/ModelParser/Model.hs b/src/ModelParser/Model.hs
new file mode 100644
index 0000000..0e5cfd0
--- /dev/null
+++ b/src/ModelParser/Model.hs
@@ -0,0 +1,14 @@
+module ModelParser.Model where
+
+data FuncInst = InstInt Int Int
+ | InstElse Int
+ deriving (Show, Read, Eq)
+
+data ModelVal = BoolVal Bool
+ | IntVal Int
+ | ArrayRef String -- TODO: immediately forward to ArrayFunc?
+ | ArrayAsConst Int -- TODO: parse to InstElse?
+ | ArrayFunc [FuncInst]
+ deriving (Show, Read, Eq)
+
+type Z3Model = [(String, ModelVal)]
\ No newline at end of file
diff --git a/src/ModelParser/Parser.y b/src/ModelParser/Parser.y
index 20b05a7..c9b1576 100644
--- a/src/ModelParser/Parser.y
+++ b/src/ModelParser/Parser.y
@@ -1,7 +1,8 @@
{
-module ModelParser.Parser where
+module ModelParser.Parser (parseModel) where
import ModelParser.Lexer
+import ModelParser.Model
}
%name happyParseTokens
@@ -46,22 +47,11 @@ FuncEntry : value "->" value { InstInt $1 $3 }
| value { InstElse $1 }
{
-data FuncInst = InstInt Int Int
- | InstElse Int
- deriving (Show, Read, Eq)
-
-data ModelVal = BoolVal Bool
- | IntVal Int
- | ArrayRef String -- TODO: immediately forward to ArrayFunc?
- | ArrayAsConst Int -- TODO: parse to InstElse?
- | ArrayFunc [FuncInst]
- deriving (Show, Read, Eq)
-
-type Z3Model = [(String, ModelVal)]
parseError :: [Token] -> a
-parseError t = error $ "Parse error" ++ show t
+parseError t = error $ "Model parse error " ++ show t
parseModel :: String -> Z3Model
parseModel = happyParseTokens . alexScanTokens
+
}
\ No newline at end of file
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 778ddef..fae4e58 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -18,6 +18,7 @@ import LogicIR.Backend.Pretty
import LogicIR.Backend.Null
import ModelParser.Parser
+import ModelParser.Model
import Control.Monad.Trans (liftIO)
--
GitLab