diff --git a/examples/memberOf b/examples/memberOf new file mode 100644 index 0000000000000000000000000000000000000000..624fa1495f47a2378ffaa1f63815a9c0e8fd9151 --- /dev/null +++ b/examples/memberOf @@ -0,0 +1,13 @@ +memberOf ( x : int , a :[] int | found : bool ) { + assume #a >= N && #a >=0 + && ( exists k :: 0 <= k && k <# a && a [ k ]= x ) ; + var k : int { + k := 0 ; + found := false ; + while k <# a do { + if a [ k ]= x then found := true else skip ; + k := k +1 + } + }; + assert found +} \ No newline at end of file diff --git a/program-semantics.cabal b/program-semantics.cabal index 89fc831a31bc132a20be04bc2e0f9ff1151a20d9..ab972795b835b802bb3e1ae089d86df5c9a68740 100644 --- a/program-semantics.cabal +++ b/program-semantics.cabal @@ -51,14 +51,18 @@ executable program-semantics main-is: Main.hs -- Modules included in this executable, other than Main. - -- other-modules: + other-modules: GCLLexer.Token + , GCLParser.GCLDatatype + , GCLParser.Parser + , GCLLexer.Lexer -- LANGUAGE extensions used by modules in this package. -- other-extensions: -- Other library packages from which modules are imported. - build-depends: base >=4.11 && <4.12 + build-depends: base >=4.11 , z3 + , array -- Directories containing source files. hs-source-dirs: src @@ -66,3 +70,5 @@ executable program-semantics -- Base language which the package is written in. default-language: Haskell2010 + build-tools: happy, alex + diff --git a/src/GCLLexer/Lexer.x b/src/GCLLexer/Lexer.x index bb13ab96a534382ac8ad36f083de6d037c49efc0..37fafdffa42a247b61d895d02f9c6eb528c88c51 100644 --- a/src/GCLLexer/Lexer.x +++ b/src/GCLLexer/Lexer.x @@ -65,6 +65,7 @@ tokens :- "bool" {\s -> TBool } "true" {\s -> TBoolValue True } "false" {\s -> TBoolValue False } + "repby" {\s -> TRepBy } $digit+ {\s -> TIntValue (read s) } $alpha [$alpha $digit \_ \']* {\s -> TIdent s } diff --git a/src/GCLLexer/Token.hs b/src/GCLLexer/Token.hs index 5c79e2e43af4ce4fd3c5adfd5b3c5a717fdea2af..bd65f61d5cc060162319009c64db79c9a434c6ee 100644 --- a/src/GCLLexer/Token.hs +++ b/src/GCLLexer/Token.hs @@ -53,4 +53,5 @@ data Token | TBool | TRef | TVal + | TRepBy deriving (Show) \ No newline at end of file diff --git a/src/GCLParser/Parser.y b/src/GCLParser/Parser.y index caed2b6b5b798f8e815d5a11cc738db44f482790..807fa454851c3f8fa09ebd9e4d4023544580e137 100644 --- a/src/GCLParser/Parser.y +++ b/src/GCLParser/Parser.y @@ -66,6 +66,7 @@ import Debug.Trace null { TNull } val { TVal } alias { TAlias } + repby { TRepBy } %left implication @@ -172,6 +173,7 @@ PExpr :: { Expr } | new popen PExpr pclose { NewStore $3 } | null { LitNull } | identifier dot val { Dereference $1 } + | PExpr popen PExpr repby PExpr pclose { RepBy $1 $3 $5 } -- I suppress the introduction of fresh name here. You should decide it yourself. diff --git a/src/Main.hs b/src/Main.hs index 65ae4a05d5db90794a0f769fd667e23df74f67e2..4d7da1b9acf6b273e76731b7140be6eab0236c6d 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,4 +1,13 @@ module Main where +import GCLParser.Parser +import GCLLexer.Lexer +import System.Environment + main :: IO () -main = putStrLn "Hello, Haskell!" +main = do + [fp] <- getArgs + file <- readFile fp + let tokens = lexer file + let parsed = parseGCL tokens + putStrLn (show parsed)