module Language.Dove.ACL2
( acl2
, check
, check'
) where
import qualified Language.ACL2 as A
import Language.Dove.Syntax
check :: Expr -> IO Bool
check a = check' a >>= return . fst
check' :: Expr -> IO (Bool, String)
check' a = A.check' [A.thm $ acl2 a]
acl2 :: Expr -> A.Expr
acl2 a = case a of
Var a -> A.var a
ForAll _ a -> expr a
Let a b c -> A.let' [(a, expr b)] $ expr c
If a b c -> A.if' (expr a) (expr b) (expr c)
Unit -> A.nil
Bool a -> if a then A.t else A.nil
Integer a -> A.lit $ show a
Comment _ a -> expr a
Array a -> A.list $ map expr a
ArrayAppend a b -> A.append (expr a) (expr b)
ArrayProject a b -> A.nth (expr b) (expr a)
ArrayUpdate a b c -> A.updateNth (expr a) (expr b) (expr c)
Record a -> A.list [ A.cons (A.string a) (expr b) | (a, b) <- a ]
RecordOverlay a b -> A.append (expr a) (expr b)
RecordProject a b -> A.cdr $ A.assoc (A.string b) (expr a)
UniOp op a -> case op of
Not -> A.not' $ expr a
Length -> A.len $ expr a
Negate -> 0 (expr a)
Abs -> A.if' (expr a A.>=. 0) (expr a) (0 (expr a))
Signum -> A.if' (expr a A.>. 0) 1 $ A.if' (expr a A.<. 0) (1) 0
IsArray -> A.consp $ expr a
IsInt -> A.integerp $ expr a
BinOp op a b -> op' (expr a) (expr b)
where
op' = case op of
And -> A.and'
Or -> A.or'
Implies -> A.implies
Eq -> A.equal
Lt -> (A.<.)
Le -> (A.<=.)
Gt -> (A.>.)
Ge -> (A.>=.)
Add -> (+)
Sub -> ()
Mul -> (*)
Mod -> A.mod'
where
expr = acl2