CurryInfo: verify-non-fail-2.0.0 / Verify.WithSMT.exp2SMT

definition: Info
 
exp2SMT :: Maybe Term -> Expr -> Maybe Term
exp2SMT lhs exp = case exp of
  Var i          -> Just $ makeRHS (TSVar i)
  Lit l          -> Just $ makeRHS (lit2SMT l)
  Comb _ qf args -> mapM (exp2SMT Nothing) args >>= comb2SMT qf
  Case _ e bs -> do t <- exp2SMT Nothing e
                    bts <- mapM branch2SMT bs
                    return $ makeRHS (Match t bts)
  FC.Let bs e -> do tbs <- mapM (\(v,be) -> do t <- exp2SMT Nothing be
                                               return (v,t))
                                bs
                    t <- exp2SMT lhs e
                    return $ tLet tbs t
  Free _ _    -> Nothing --error "exp2SMT: Free"
  Typed e te  -> case e of
    Comb _ qf args | all isTyped args
       -> mapM (exp2SMT Nothing) args >>=
          return . makeRHS .
            TComb (As (transOpName qf)
                      (type2sort (foldr FuncType te (map exprType args))))
    _  -> exp2SMT lhs e
  Or    e1 e2 -> do t1 <- exp2SMT lhs e1
                    t2 <- exp2SMT lhs e2
                    return $ tDisj [t1,t2]
 where
  comb2SMT qf targs
    | qf `elem` map pre ["chr", "ord"] && length targs == 1
    = return $ makeRHS (head targs) -- chars are integers --> no conversion
    | otherwise
    = return $ makeRHS (tComb (transOpName qf) targs)

  makeRHS rhs = maybe rhs (\l -> tEqu l rhs) lhs

  branch2SMT (Branch (LPattern _) _) = Nothing -- literal patterns not supported
  branch2SMT (Branch (Pattern qf vs) e) = do
    t <- exp2SMT lhs e
    return (PComb (Id (transOpName qf)) vs, t)
demand: Info
 argument 2
deterministic: Info
 deterministic operation
documentation: Info
 
Translates a (Boolean) 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.
failfree: Info
 <FAILING>
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,{Var}) |-> _ || (_,{Lit}) |-> _ || (_,{Comb}) |-> _ || (_,{Case}) |-> _ || (_,{Let}) |-> _ || (_,{Free}) |-> {Nothing} || (_,{Typed}) |-> _ || (_,{Or}) |-> _}
name: Info
 exp2SMT
precedence: Info
 no precedence defined
result-values: Info
 _
signature: Info
 Prelude.Maybe Verify.ESMT.Term -> FlatCurry.Types.Expr
-> Prelude.Maybe Verify.ESMT.Term
solution-complete: Info
 operation might suspend on free variables
terminating: Info
 possibly non-terminating
totally-defined: Info
 possibly non-reducible on same data term