CurryInfo: property-prover-2.0.0 / ESMT.addInstancesOfSig
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 |