|
definition:
|
unpoly :: [Either [FunSigTerm] SMT.Command] -> [SMT.Command]
unpoly commands =
let allsigs = map sigNameSort . concat . lefts $ commands
in concatMap (unpolyCmd allsigs) . reverse . addSigs [] . reverse $ commands
where
addSigs :: [SMT.QIdent] -> [Either [FunSigTerm] SMT.Command]
-> [Either [FunSigTerm] SMT.Command]
addSigs _ [] = []
addSigs qids (cmd:cmds) = case cmd of
Left fts ->
let (qids1,ftss) = addAllInstancesOfSigs (union (allQIdsOfSigs fts) qids)
fts
in Left ftss : addSigs qids1 cmds
Right cmd' -> cmd : addSigs (union (allQIdsOfAssert cmd') qids) cmds
-- remove remaining polymorphic signatures and rename qualified names
-- according to their sorts
unpolyCmd :: [(SMT.Ident, ([SMT.Ident],SMT.Sort))]
-> Either [FunSigTerm] SMT.Command -> [SMT.Command]
unpolyCmd sigs cmd = case cmd of
Left fts -> funSigTermsToCommands $
map rnmTermInSig (filter (\ (ps,_,_) -> null ps) fts)
Right (SMT.Assert term) -> [SMT.Assert (rnmQIdWithTInstTerm sigs term)]
Right cmd' -> [cmd']
where
rnmTermInSig (ps,sig,term) = (ps, sig, rnmQIdWithTInstTerm sigs term)
|
|
documentation:
|
--------------------------------------------------------------------------
-- Remove parametric polymorphism 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.
|