Add basic WLP calculation

The WLP of a subset of statements in the language can now be calculated.
This needs to be extended, but it gives a basic idea of what we can do.

I made new types for the logical expressions (and the mathematical
expression in them) rather than reusing the datatype within the
language. I feel that there's a benefit to separating these, showing
when we're talking about the programs and when we're talking about the
wlp and its calculation and the like. However, this does increase the
amount of types we use. I think the benefit outweighs the cost of having
extra types, but I also feel like we should discuss this :)

examples/id

+id ( x : int | y : int ) {
+    assume x > 0;
+    y := x;
+    assert y > 0
+}
+

program-semantics.cabal

@@ -56,6 +56,9 @@ executable program-semantics
                        , GCLParser.GCLAlgebra
                        , GCLParser.GCLDatatype 
                        , GCLParser.Parser
+                       , WLP.LogicalExpression
+                       , WLP.MathExpression
+                       , WLP.WLPCalculator
 
   -- LANGUAGE extensions used by modules in this package.
   -- other-extensions:

src/Main.hs

@@ -7,6 +7,9 @@ import GCLLexer.Lexer
 
 import System.Environment
 
+import WLP.LogicalExpression
+import WLP.WLPCalculator
+
 main :: IO ()
 main = do
     [fp] <- getArgs
@@ -14,3 +17,10 @@ main = do
     let tokens = lexer file
     let parsed = parseGCL tokens
     putStrLn (show parsed)
+    case parsed of
+      Left xs -> return ()
+      Right program -> do
+        -- We gotta turn the AST into a logical formula based on the wlp
+        let wlpFormula = foldProgram programToWLPAlgebra program
+        putStrLn . show $ wlpFormula
+

src/WLP/LogicalExpression.hs

+module WLP.LogicalExpression
+  ( LogicalExpression(..)
+  , replace
+  )
+where
+
+import WLP.MathExpression (MathExpression, replaceInExpr)
+
+data LogicalExpression
+  = Constant Bool
+  | Variable String
+  | Expression MathExpression
+  | Not LogicalExpression
+  | LogicalExpression :/\: LogicalExpression
+  | LogicalExpression :\/: LogicalExpression
+  | LogicalExpression :=>: LogicalExpression
+  | LogicalExpression :<=>: LogicalExpression
+
+instance Show LogicalExpression where
+  show (Constant x)   = show x
+  show (Variable s)   = s
+  show (Expression e) = "(" ++ show e ++ ")"
+  show (Not le)       = "!" ++ show le
+
+  show (e1 :/\: e2)   = "(" ++ show e1 ++ ") /\\ (" ++ show e2 ++ ")"
+  show (e1 :\/: e2)   = "(" ++ show e1 ++ ") \\/ (" ++ show e2 ++ ")"
+  show (e1 :=>: e2)   = "(" ++ show e1 ++  ") => (" ++ show e2 ++ ")"
+  show (e1 :<=>: e2)  = "(" ++ show e1 ++ ") <=> (" ++ show e2 ++ ")"
+
+-- | Substitutes the variable given by the string with the value given in the expression.
+replace :: String -> MathExpression -> LogicalExpression -> LogicalExpression
+replace _   _ x@(Constant _) = x
+replace var e x@(Variable v) = if v == var then Expression e else x
+replace var e x@(Expression expr) = Expression $ replaceInExpr var e expr
+replace var e x@(e1 :/\: e2) = replace var e e1 :/\: replace var e e2
+replace var e x@(e1 :\/: e2) = replace var e e1 :/\: replace var e e2
+replace var e x@(e1 :=>: e2) = replace var e e1 :=>: replace var e e2
+replace var e x@(e1 :<=>: e2) = replace var e e1 :<=>: replace var e e2
+

src/WLP/MathExpression.hs

+module WLP.MathExpression
+  ( MathExpression(..)
+  , replaceInExpr
+  )
+where
+
+import Prelude hiding (GT, LT, EQ)
+
+data MathExpression
+  = Constant Int
+  | Variable String
+  | Add MathExpression MathExpression
+  | Sub MathExpression MathExpression
+  | Mul MathExpression MathExpression
+  | Div MathExpression MathExpression
+  | GT  MathExpression MathExpression
+  | LT  MathExpression MathExpression
+  | EQ  MathExpression MathExpression
+  | GTE MathExpression MathExpression
+  | LTE MathExpression MathExpression
+
+instance Show MathExpression where
+  show (Constant n) = show n
+  show (Variable s) = s
+  show (Add e1 e2)  = "(" ++ show e1 ++ " + "  ++ show e2 ++ ")"
+  show (Sub e1 e2)  = "(" ++ show e1 ++ " - "  ++ show e2 ++ ")"
+  show (Mul e1 e2)  = "(" ++ show e1 ++ " * "  ++ show e2 ++ ")"
+  show (Div e1 e2)  = "(" ++ show e1 ++ " / "  ++ show e2 ++ ")"
+  show (GT  e1 e2)  = "(" ++ show e1 ++ " > "  ++ show e2 ++ ")"
+  show (LT  e1 e2)  = "(" ++ show e1 ++ " < "  ++ show e2 ++ ")"
+  show (EQ  e1 e2)  = "(" ++ show e1 ++ " = "  ++ show e2 ++ ")"
+  show (GTE e1 e2)  = "(" ++ show e1 ++ " >= " ++ show e2 ++ ")"
+  show (LTE e1 e2)  = "(" ++ show e1 ++ " <= " ++ show e2 ++ ")"
+
+replaceInExpr :: String -> MathExpression -> MathExpression -> MathExpression
+replaceInExpr _   _      x@(Constant _) = x
+replaceInExpr var newVal x@(Variable s) = if var == s then newVal else x
+replaceInExpr var newVal x@(Add e1 e2)  = Add (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(Sub e1 e2)  = Sub (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(Mul e1 e2)  = Mul (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(Div e1 e2)  = Div (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(GT e1 e2)  = GT (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(LT e1 e2)  = LT (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(EQ e1 e2)  = EQ (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(GTE e1 e2)  = GTE (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+replaceInExpr var newVal x@(LTE e1 e2)  = LTE (replaceInExpr var newVal e1) (replaceInExpr var newVal e2)
+

src/WLP/WLPCalculator.hs

+module WLP.WLPCalculator
+  ( programToWLPAlgebra
+  )
+where
+
+import GCLParser.GCLAlgebra
+
+import WLP.LogicalExpression as LE
+import WLP.MathExpression as ME
+
+type BinOp = (MathExpression -> MathExpression -> MathExpression)
+
+-- type ProgramAlgebra pty ty vd stmt expr bo res
+programToWLPAlgebra :: ProgramAlgebra () () () (LogicalExpression -> LogicalExpression) MathExpression BinOp LogicalExpression
+programToWLPAlgebra =
+  ( program
+  , variableDeclaration
+  , ( ptInt
+    , ptBool
+    )
+  , ( ptype
+    , reftype
+    , arraytype
+    )
+  , ( 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
+    )
+  )
+
+  where
+    program s i o stmt  = stmt $ LE.Constant True
+    variableDeclaration = undefined
+    ptInt               = undefined
+    ptBool              = undefined
+    ptype               = undefined
+    reftype             = undefined
+    arraytype           = undefined
+    skip                = \le -> le
+    assert me           = \le -> Expression me :/\: le
+    assume me           = \le -> Expression me :\/: le
+    assign var e        = \le -> replace var e le
+    aassign             = undefined
+    drefassign          = undefined
+    seq s1 s2           = \le -> s1 (s2 le)
+    ifthenelse g s1 s2  = \le -> (Expression g :/\: s1 le) :\/: (Not (Expression g) :/\: s2 le)
+    while               = undefined
+    block               = undefined
+    trycatch            = undefined
+    var                 = ME.Variable
+    liti                = ME.Constant
+    litb                = undefined
+    litnull             = undefined
+    parens              = undefined
+    arrayelem           = undefined
+    opneg               = undefined
+    binopexpr op e1 e2  = op e1 e2
+    forall              = undefined
+    sizeof              = undefined
+    repby               = undefined
+    cond                = undefined
+    newstore            = undefined
+    dereference         = undefined
+    and                 = undefined
+    or                  = undefined
+    implication         = undefined
+    lessthan            = ME.LT
+    lessthanequal       = ME.LTE
+    greaterthan         = ME.GT
+    greaterthanequal    = ME.GTE
+    equal               = ME.EQ
+    minus               = ME.Sub
+    plus                = ME.Add
+    multiply            = ME.Mul
+    divide              = ME.Div
+    alias               = undefined
+