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