| definition: |
addInstancesOfSig :: [SMT.QIdent] -> [FunSigTerm] -> FunSigTerm
-> ([SMT.QIdent], [FunSigTerm])
addInstancesOfSig allqids allsigs fts@(ps, (FunSig fn ss rs), _) =
addSigInsts allqids
where
addSigInsts :: [SMT.QIdent] -> ([SMT.QIdent], [FunSigTerm])
addSigInsts [] = ([],[])
addSigInsts (qid:qids) =
let (qids1,sigs1) = addSigInsts qids
in case qid of
SMT.As n s | n==fn -> (qids1, sigInstForType s ++ sigs1)
_ -> (qid : qids1, sigs1)
sigInstForType s =
maybe []
(\tsub -> let rnm = toTInstName fn ps tsub
in if rnm fn `elem` map nameOfSig allsigs
then []
else [(rnmDefSig rnm (substDefSig tsub fts))])
(matchSort (sigTypeAsSort ss rs) s)
|
| demand: |
arguments 1 3 |
| deterministic: |
deterministic operation |
| documentation: |
-- Adds to a given (polymorphic) define-sig element all its type instances -- required by qualified identifiers occurring in the first argument -- provided that it does not already occur in the sig elements -- contained in the second argument. -- The list of unused qualified identifiers is also returned. |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,_,{(,,)}) |-> {(,)}}
|
| name: |
addInstancesOfSig |
| precedence: |
no precedence defined |
| result-values: |
{(,)}
|
| signature: |
[Language.SMTLIB.Types.QIdent] -> [([String], FunSig, Language.SMTLIB.Types.Term)] -> ([String], FunSig, Language.SMTLIB.Types.Term) -> ([Language.SMTLIB.Types.QIdent], [([String], FunSig, 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 |