Skip to content
Snippets Groups Projects
Commit 43de3b37 authored by Bart Wijgers's avatar Bart Wijgers
Browse files

Add GCLAlgebra

parent 8a8e909c
No related branches found
No related tags found
No related merge requests found
......@@ -52,9 +52,10 @@ executable program-semantics
-- Modules included in this executable, other than Main.
other-modules: GCLLexer.Token
, GCLLexer.Lexer
, GCLParser.GCLAlgebra
, GCLParser.GCLDatatype
, GCLParser.Parser
, GCLLexer.Lexer
-- LANGUAGE extensions used by modules in this package.
-- other-extensions:
......
module GCLParser.GCLAlgebra
( ProgramAlgebra
, foldProgram
, idAlgebra
)
where
import GCLParser.GCLDatatype
-- | An algebra used to fold Programs.
type ProgramAlgebra pty ty vd stmt expr bo res =
( String -> [vd] -> [vd] -> stmt -> res -- Program
, String -> ty -> vd -- VarDeclaration
-- PrimitiveType
, ( pty -- PTInt
, pty -- PTBool
)
-- Type
, ( pty -> ty -- PType
, ty -- RefType
, pty -> ty -- AType
)
-- Statement
, ( stmt -- Skip
, expr -> stmt -- Assert
, expr -> stmt -- Assume
, String -> expr -> stmt -- Assign
, String -> expr -> expr -> stmt -- AAssign
, String -> expr -> stmt -- DrefAssign
, stmt -> stmt -> stmt -- Seq
, expr -> stmt -> stmt -> stmt -- IfThenElse
, expr -> stmt -> stmt -- While
, [vd] -> stmt -> stmt -- Block
, String -> stmt -> stmt -> stmt -- TryCatch
)
-- Expression
, ( String -> expr -- Var
, Int -> expr -- LitI
, Bool -> expr -- LitB
, expr -- LitNull
, expr -> expr -- Parens
, expr -> expr -> expr -- ArrayElem
, expr -> expr -- OpNeg
, bo -> expr -> expr -> expr -- BinopExpr
, String -> expr -> expr -- Forall
, expr -> expr -- SizeOf
, expr -> expr -> expr -> expr -- RepBy
, expr -> expr -> expr -> expr -- Cond
, expr -> expr -- NewStore
, String -> expr -- Dereference
)
-- BinOp
, ( bo -- And
, bo -- Or
, bo -- Implication
, bo -- LessThan
, bo -- LessThanEqual
, bo -- GreaterThan
, bo -- GreaterThanEqual
, bo -- Equal
, bo -- Minus
, bo -- Plus
, bo -- Multiply
, bo -- Divide
, bo -- Alias
)
)
-- | Folds a Program using the given algebra.
foldProgram :: ProgramAlgebra pty ty vd stmt expr bo r -> Program -> r
-- The names are relatively simple; anything in "where" starts with 'f' for fold.
-- Anything in the algebra starts with 'a' for algebra.
-- The folds have the capital letters of the type in them as long as this is unique.
-- The algebra functions have the capital letters of the types they're for,
-- followed by the capital letters of the constructors.
-- Therefore, anything in the algebra starting with at should be used in the function ft, etc.
foldProgram ( ap
, avd
, ( aptpti
, aptptb
)
, ( atpt
, atrt
, atat
)
, ( ass
, asasrt
, asasum
, asasgn
, asaa
, asda
, asseq
, asite
, asw
, asb
, astc
)
, ( aev
, aeli
, aelb
, aeln
, aep
, aeae
, aeon
, aebe
, aef
, aeso
, aerb
, aec
, aens
, aed
)
, ( aboand
, aboo
, aboi
, abolt
, abolte
, abogt
, abogte
, aboe
, abomin
, abop
, abomul
, abod
, aboa -- Alias
)
) = fp
where
fp p = ap (name p) (fvd <$> input p) (fvd <$> output p) (fs $ stmt p)
fvd (VarDeclaration s t) = avd s $ ft t
fpt PTInt = aptpti
fpt PTBool = aptptb
ft (PType pt) = atpt $ fpt pt
ft RefType = atrt
ft (AType pt) = atat $ fpt pt -- 1d array type
fs Skip = ass
fs (Assert e) = asasrt $ fe e
fs (Assume e) = asasum $ fe e
fs (Assign s e) = asasgn s $ fe e
fs (AAssign s e1 e2) = asaa s (fe e1) $ fe e2
fs (DrefAssign s e) = asda s $ fe e
fs (Seq s1 s2) = asseq (fs s1) $ fs s2
fs (IfThenElse e s1 s2) = asite (fe e) (fs s1) $ fs s2
fs (While e s) = asw (fe e) $ fs s
fs (Block decls s) = asb (fvd <$> decls) $ fs s
fs (TryCatch s s1 s2) = astc s (fs s1) $ fs s2
fe (Var s) = aev s
fe (LitI n) = aeli n
fe (LitB b) = aelb b
fe LitNull = aeln
fe (Parens e) = aep $ fe e
fe (ArrayElem e1 e2) = aeae (fe e1) $ fe e2
fe (OpNeg e) = aeon $ fe e
fe (BinopExpr op e1 e2) = aebe (fbo op) (fe e1) $ fe e2
fe (Forall s e) = aef s $ fe e
fe (SizeOf e) = aeso $ fe e
fe (RepBy e1 e2 e3) = aerb (fe e1) (fe e2) $ fe e3
fe (Cond e1 e2 e3) = aec (fe e1) (fe e2) $ fe e3
fe (NewStore e) = aens $ fe e
fe (Dereference s) = aed s
fbo And = aboand
fbo Or = aboo
fbo Implication = aboi
fbo LessThan = abolt
fbo LessThanEqual = abolte
fbo GreaterThan = abogt
fbo GreaterThanEqual = abogte
fbo Equal = aboe
fbo Minus = abomin
fbo Plus = abop
fbo Multiply = abomul
fbo Divide = abod
fbo Alias = aboa
idAlgebra :: ProgramAlgebra PrimitiveType Type VarDeclaration Stmt Expr BinOp Program
idAlgebra =
( Program
, VarDeclaration
, ( PTInt
, PTBool
)
, ( PType
, RefType
, AType
)
, ( Skip
, Assert
, Assume
, Assign
, AAssign
, DrefAssign
, Seq
, IfThenElse
, While
, Block
, TryCatch
)
, ( Var
, LitI
, LitB
, LitNull
, Parens
, ArrayElem
, OpNeg
, BinopExpr
, Forall
, SizeOf
, RepBy
, Cond
, NewStore
, Dereference
)
, ( And
, Or
, Implication
, LessThan
, LessThanEqual
, GreaterThan
, GreaterThanEqual
, Equal
, Minus
, Plus
, Multiply
, Divide
, Alias
)
)
module Main where
import GCLParser.Parser
import GCLParser.GCLAlgebra
import GCLLexer.Lexer
import System.Environment
main :: IO ()
......
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