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