| 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 |