Skip to content
Snippets Groups Projects
Commit 8a8e909c authored by Stoll,M. (Maximilian Stoll)'s avatar Stoll,M. (Maximilian Stoll)
Browse files

Merge branch 'parser-extension' into 'master'

Extended the GCL Parser/Lexer to also parse/lex RepBy

See merge request !1
parents 04a952d8 1bd94a5d
No related branches found
No related tags found
1 merge request!1Extended the GCL Parser/Lexer to also parse/lex RepBy
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
......@@ -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
......@@ -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 }
......
......@@ -53,4 +53,5 @@ data Token
| TBool
| TRef
| TVal
| TRepBy
deriving (Show)
\ No newline at end of file
......@@ -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.
......
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)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment