|
definition:
|
rnmQIdWithTInst :: [(SMT.Ident, ([SMT.Ident],SMT.Sort))] -> SMT.QIdent
-> SMT.QIdent
rnmQIdWithTInst _ (SMT.Id n) = SMT.Id n
rnmQIdWithTInst sigs qid@(SMT.As n s) =
maybe qid
(\ (ps,psort) -> maybe qid
(\tsub -> SMT.As (addTInstName ps tsub n) s)
(matchSort psort s))
(lookup n sigs)
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
--------------------------------------------------------------------------
-- Rename a sorted name w.r.t. its type instance of the polymorphic function.
-- For instance,
-- (As "id" (SComb "Func" [SComb "Int" [], SComb "Int" []]))
-- will be renamed to
-- (As "id_Int" (SComb "Func" [SComb "Int" [], SComb "Int" []]))
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{Id}) |-> {Id} || (_,{As}) |-> _}
|
|
name:
|
rnmQIdWithTInst
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[(String, ([String], Language.SMTLIB.Types.Sort))]
-> Language.SMTLIB.Types.QIdent -> Language.SMTLIB.Types.QIdent
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|