CurryInfo: contract-prover-4.0.0 / ContractProver.binding2SMT

definition: Info
 
binding2SMT :: Bool -> VerifyInfo -> (Int,TAExpr) -> TransStateM Term
binding2SMT odemanded vi (oresvar,oexp) =
  exp2smt odemanded (oresvar, simpExpr oexp)
 where
  exp2smt demanded (resvar,exp) = case exp of
    AVar _ i -> return $ if resvar==i then tTrue
                                       else tEquVar resvar (TSVar i)
    ALit _ l -> return (tEquVar resvar (lit2SMT l))
    AComb ty ct (qf,_) args ->
      if qf == pre "?" && length args == 2
        then exp2smt demanded (resvar, AOr ty (args!!0) (args!!1))
        else do
          (bs,nargs) <- normalizeArgs args
          -- TODO: select from 'bindexps' only demanded argument positions
          bindexps <- mapM (exp2smt (isPrimOp qf || optStrict (toolOpts vi))) bs
          comb2smt qf ty ct nargs bs bindexps
    ALet _ bs e -> do
      addVarTypes (map fst bs)
      bindexps <- mapM (exp2smt False) (map (\ ((i,_),ae) -> (i,ae)) bs)
      bexp <- exp2smt demanded (resvar,e)
      return (tConj (bindexps ++ [bexp]))
    AOr _ e1 e2  -> do
      bexp1 <- exp2smt demanded (resvar,e1)
      bexp2 <- exp2smt demanded (resvar,e2)
      return (tDisj [bexp1, bexp2])
    ACase _ _ e brs   -> do
      freshvar <- getFreshVar
      addVarTypes [(freshvar, annExpr e)]
      argbexp <- exp2smt demanded (freshvar,e)
      bbrs    <- mapM branch2smt (map (\b -> (freshvar,b)) brs)
      return (tConj [argbexp, tDisj bbrs])
    ATyped _ e _ -> exp2smt demanded (resvar,e)
    AFree _ _ _ -> error "Free variables not yet supported!"
   where
    comb2smt qf rtype ct nargs bs bindexps
     | qf == pre "otherwise"
       -- specific handling for the moment since the front end inserts it
       -- as the last alternative of guarded rules...
     = return (tEquVar resvar tTrue)
     | ct == ConsCall -- translate data constructor
     = return (tConj (bindexps ++
                      [tEquVar resvar
                               (TComb (cons2SMT (null nargs) False qf rtype)
                                      (map arg2smt nargs))]))
     | qf == pre "apply"
     = -- cannot translate h.o. apply: ignore it
       return tTrue
     | isPrimOp qf
     = return (tConj (bindexps ++
                      [tEquVar resvar (TComb (cons2SMT True False qf rtype)
                                             (map arg2smt nargs))]))
     | otherwise -- non-primitive operation: add contract only if demanded
     = do let targs = zip (map fst bs) (map annExpr nargs)
          precond  <- preCondExpOf vi qf targs
          postcond <- postCondExpOf vi qf (targs ++ [(resvar,rtype)])
          return
            (tConj (bindexps ++ if demanded then [precond,postcond] else []))
    
    branch2smt (cvar, (ABranch p e)) = do
      branchbexp <- exp2smt demanded (resvar,e)
      addVarTypes patvars
      return (tConj [ tEquVar cvar (pat2SMT p), branchbexp])
     where
      patvars = if isConsPattern p
                  then patArgs p
                  else []
  
    arg2smt e = case e of AVar _ i -> TSVar i
                          ALit _ l -> lit2SMT l
                          _        -> error $ "Not normalized: " ++ show e
demand: Info
 argument 3
deterministic: Info
 deterministic operation
documentation: Info
 
Translates a binding between a variable (represented by its index
in the first component) and a FlatCurry expression (second component).
The FlatCurry expression is translated into an SMT formula so that
the binding is axiomiatized as an equation between the variable
and the translated expression.
The translated expression is normalized when necessary.
For this purpose, a "fresh variable index" is passed as a state.
Moreover, the returned state contains also the types of all fresh variables.
If the first argument is `False`, the expression is not strictly demanded,
i.e., possible contracts of it (if it is a function call) are ignored.
failfree: Info
 <FAILING>
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,_,{(,)}) |-> _}
name: Info
 binding2SMT
precedence: Info
 no precedence defined
result-values: Info
 _
signature: Info
 Prelude.Bool -> VerifierState.VerifyInfo
-> (Prelude.Int, FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr)
-> Control.Monad.Trans.State.StateT TransState Prelude.IO 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