Commit 0c898266 authored by Michael Hanus's avatar Michael Hanus
Browse files

Small refactorings

parent c91b98f7
--- Test for verification with user-defined lists.
data MyList = Nil | Cons Int MyList
isNull :: MyList -> Bool
isNull Nil = True
isNull (Cons _ _) = False
--- Defining head on these lists:
head :: MyList -> Int
head (Cons x _) = x
head'nonfail xs = not (isNull xs)
main :: Int
main = head (Cons 1 Nil)
......@@ -53,27 +53,12 @@ fun2SMT (AFunc qn _ _ texp rule) =
lhs = tComb (transOpName qn) (map (TSVar . fst) vs)
-- Since basic arithmetic operations are represented in FlatCurry
-- via access to class dictionaries and `apply` operations,
-- this operations transforms them into standard function calls
-- so that they can be translated into SMT formulas.
simpArith :: TAExpr -> TAExpr
simpArith exp = case exp of
AComb _ FuncCall (qf,_) args | qf == pre "apply" && isComb (head args)
-> -- "defunctionalization": if the first argument is a
-- combination, append the second argument to its arguments
case map simpArith args of -- TODO: correct typing!
[AComb ty ct bn bas, barg2] | isPrimOp (fst bn)
-> AComb ty ct bn (bas++[barg2])
_ -> exp -- no translation possible
_ -> exp
-- Translates a typed FlatCurry expression into an SMT expression.
-- If the first argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
exp2SMT :: Maybe Term -> TAExpr -> Term
exp2SMT lhs exp = case simpArith exp of
exp2SMT lhs exp = case exp of
AVar _ i -> makeRHS (TSVar i)
ALit _ l -> makeRHS (lit2smt l)
AComb _ ct (qn,ftype) args ->
......
......@@ -565,13 +565,6 @@ pred2SMT exp = case simpExpr exp of
returnS (tEqu barg
(sortedConst "nil"
(polytype2sort (typeOfVar tstate arg))))
| qf == pre "apply" && ar == 2 && isComb (head args)
= -- "defunctionalization": if the first argument is a
-- combination, append the second argument to its arguments
mapS pred2SMT args `bindS` \bargs ->
case bargs of
[TComb bn bas, barg2] -> returnS (TComb bn (bas++[barg2]))
_ -> returnS (tComb (show exp) []) -- no translation possible
| qf == pre "apply"
= -- cannot translate h.o. apply: replace it by new variable
getS `bindS` \ts ->
......@@ -762,7 +755,6 @@ testBoolCase brs =
Still to be done:
- consider encapsulated search
- type-specialize polymorphic operations when axiomatizing them in SMT
Verified system libraries:
......@@ -778,19 +770,4 @@ Verified system libraries:
Prelude Char Either ErrorState Integer Maybe State ShowS
Version without type classes:
- Prelude
- AnsiCodes
- Either
- ErrorState
- Integer
- Maybe
- State
- Nat
- ShowS
- Socket
- Array
- Char
-}
......@@ -29,6 +29,7 @@ simpProg = updProgExps simpExpr
--- case otherwise of { True -> e1 ; False -> e2 } ==> e1
--- * simplify application of `Prelude.$`:
--- f $ e ==> f e
--- * simplify `Prelude.apply` for partially applied first arguments
simpExpr :: TAExpr -> TAExpr
simpExpr exp = case exp of
AVar _ _ -> exp
......@@ -43,25 +44,29 @@ simpExpr exp = case exp of
AFree ty vs e -> AFree ty vs (simpExpr e)
where
simpComb ty ct (qf, qt) args
-- simplify application of `Prelude.$`:
| qf == pre "$" && length args == 2
-- simplify application of `Prelude.apply` to partially applied functions:
| qf == pre "apply" && length args == 2
= case head args of
AComb _ (FuncPartCall n) qft1 fargs ->
AComb ty (if n==1 then FuncCall else FuncPartCall (n-1)) qft1
(fargs ++ [args!!1])
_ -> AComb ty ct (qf,qt) args
simpComb ty (if n==1 then FuncCall else FuncPartCall (n-1)) qft1
(fargs ++ [args!!1])
_ -> moreSimpComb (AComb ty ct (qf,qt) args)
-- inline application of `Prelude.$`:
| qf == pre "$"
= simpComb ty ct (pre "apply", qt) args
-- simplify equality instance on lists:
| ct == FuncCall && qf == pre "_impl#==#Prelude.Eq#[]"
= AComb ty ct (pre "==", dropArgTypes 1 qt {- TODO: remove first type arg -} )
(tail args)
= AComb ty ct (pre "==", dropArgTypes 1 qt) (tail args)
-- simplify equal class calls:
| otherwise
= simpArithExp (simpClassEq (AComb ty ct (qf,qt) args))
= moreSimpComb (AComb ty ct (qf,qt) args)
moreSimpComb e = simpArithExp (simpClassEq e)
simpBranch (ABranch p e) = ABranch p (simpExpr e)
isOtherwise e = case e of AComb _ _ (qf,_) _ -> qf == pre "otherwise"
_ -> False
_ -> False
trueBranch brs =
maybe (error "simpExpr: Branch with True pattern does not exist!")
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment