CurryInfo: contract-prover-4.0.0 / Curry2SMT.constructorTest
definition: 
|
constructorTest :: Bool -> QName -> Term -> TypeExpr -> Term
constructorTest withpoly qn be vartype
| qn == pre "[]"
= tEqu be (sortedConst "nil"
((if withpoly then polytype2psort else polytype2sort) vartype))
| qn `elem` map pre ["[]","True","False","LT","EQ","GT","Nothing"]
= tEqu be (tComb (transOpName qn) [])
| qn `elem` map pre ["Just","Left","Right"]
= tComb ("is-" ++ snd qn) [be]
| otherwise
= tComb ("is-" ++ transOpName qn) [be]
|
|
demand:
|
argument 2 |
|
deterministic:
|
deterministic operation |
|
documentation:
|
Translates a constructor name and a term into an SMT formula implementing a test on the term for this constructor. If the first argument is true, parametric sorts are used (i.e., we translate a polymorphic function), otherwise type variables are translated into the sort `TVar`. |
|
failfree:
|
(_, _, _, _) |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{(_,_,_,_) |-> {TComb}}
|
|
name:
|
constructorTest |
|
precedence:
|
no precedence defined |
|
result-values:
|
{TComb}
|
|
signature:
|
Prelude.Bool -> (String, String) -> ESMT.Term -> FlatCurry.Types.TypeExpr -> ESMT.Term |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
possibly non-terminating |
|
totally-defined:
|
possibly non-reducible on same data term |