| definition: |
constructorTest :: Bool -> QName -> SMT.Term -> TypeExpr -> SMT.Term
constructorTest withpoly qn be vartype
| qn == pre "[]"
= be =% (sortedConst "nil"
((if withpoly then polytype2psort else polytype2sort) vartype))
| qn `elem` map pre ["[]","True","False","LT","EQ","GT","Nothing"]
= 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) -> Language.SMTLIB.Types.Term -> FlatCurry.Types.TypeExpr -> Language.SMTLIB.Types.Term |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |