CurryInfo: verify-non-fail-2.0.0 / Verify.ESMT.rnmQIdWithTInst
definition: 
|
rnmQIdWithTInst :: [(Ident, ([Ident],Sort))] -> QIdent -> QIdent
rnmQIdWithTInst _ (Id n) = Id n
rnmQIdWithTInst sigs qid@(As n s) =
maybe qid
(\ (ps,psort) -> maybe qid
(\tsub -> 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], Sort))] -> QIdent -> QIdent |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
possibly non-terminating |
|
totally-defined:
|
possibly non-reducible on same data term |