CurryInfo: contract-prover-4.0.0 / Curry2SMT.exp2SMT

 
exp2SMT :: TAExpr -> Term
exp2SMT exp = case exp of
  AVar _ i -> TSVar i
  ALit _ l -> lit2SMT l
  AComb _ ct (qn,ftype) args ->
    -- TODO: reason about condition `not (null args)`
    TComb (cons2SMT (ct /= ConsCall || not (null args)) True qn ftype)
          (map exp2SMT args)
  ACase _ _ e brs -> let be = exp2SMT e
                     in branches2SMT be brs
  ALet   _ bs e -> Let (map (\ ((v,_),be) -> (v, exp2SMT be)) bs)
                       (exp2SMT e)
  ATyped _ e _ -> exp2SMT e
  AFree  _ fvs e -> Forall (map (\ (v,t) -> SV v (polytype2psort t)) fvs)
                           (exp2SMT e)
  AOr    _ e1 e2 -> tDisj [exp2SMT e1, exp2SMT e2]
 where
  branches2SMT _  [] = error "branches2SMT: empty branch list"
  branches2SMT be [ABranch p e] = branch2SMT be p e
  branches2SMT be (ABranch p e : brs@(_:_)) =
    tComb "ite" [patternTest p be, --tEqu be (pat2SMT p),
                 branch2SMT be p e,
                 branches2SMT be brs]
  
  branch2SMT _  (ALPattern _ _) e = exp2SMT e
  branch2SMT be (APattern _ (qf,_) ps) e = case ps of
    [] -> exp2SMT e
    _  -> Let (map (\ (s,v) -> (v, tComb s [be]))
                   (zip (selectors qf) (map fst ps)))
              (exp2SMT e)

 argument 1

 deterministic operation

 
Translates a typed FlatCurry expression into an SMT expression.

 _

 referentially transparent operation

 no fixity defined

 {({AVar}) |-> {TSVar} || ({ALit}) |-> {TConst} || ({AComb}) |-> {TComb} || ({ACase}) |-> _ || ({ALet}) |-> {Let} || ({ATyped}) |-> _ || ({AFree}) |-> {Forall} || ({AOr}) |-> _}

 exp2SMT

 no precedence defined

 _

 FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr -> ESMT.Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term