| 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
-- remove remaining polymorphic signatures and rename qualified names
-- according to their sorts
unpolyCmd sigs cmd = case cmd of
DefineSigsRec fts -> DefineSigsRec $ map rnmTermInSig
(filter (\ (ps,_,_) -> null ps) 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 |