CurryInfo: verify-non-fail-2.0.0 / Verify.ESMT.unpoly
definition: 
|
unpoly :: [Command] -> [Command]
unpoly commands =
let allsigs = map sigNameSort (allSigs commands)
in map (unpolyCmd allsigs) . reverse . addSigs [] . reverse $ commands
where
addSigs _ [] = []
addSigs qids (cmd:cmds) = case cmd of
DefineSigsRec fts ->
let (qids1,ftss) = addAllInstancesOfSigs (union (allQIdsOfSigs fts) qids)
fts
in DefineSigsRec ftss : addSigs qids1 cmds
_ -> cmd : addSigs (union (allQIdsOfAssert cmd) qids) cmds
-- rename qualified names according to their sorts
unpolyCmd sigs cmd = case cmd of
DefineSigsRec fts -> DefineSigsRec $ map rnmTermInSig fts
Assert term -> Assert (rnmQIdWithTInstTerm sigs term)
_ -> cmd
where
rnmTermInSig (ps,sig,term) = (ps, sig, rnmQIdWithTInstTerm sigs term)
|
|
demand:
|
no demanded arguments |
|
deterministic:
|
deterministic operation |
|
documentation:
|
----------------------------------------------------------------------- Remove parametric polymorphism (supported by `DefineSigsRec`) in an SMT script. First, for all QIdents occurring in assertions, their type-instantiated signatures are added. Then, for all QIdents occurring in these added operations, their type-instantiated signatures are added and so forth, until nothing needs to be added. Finally, the type-instantiated signatures are renamed. |
|
failfree:
|
<FAILING> |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{(_) |-> _}
|
|
name:
|
unpoly |
|
precedence:
|
no precedence defined |
|
result-values:
|
_ |
|
signature:
|
[Command] -> [Command] |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
possibly non-terminating |
|
totally-defined:
|
possibly non-reducible on same data term |