|
definition:
|
rnmQIdWithTInstTerm :: [(SMT.Ident, ([SMT.Ident],SMT.Sort))] -> SMT.Term
-> SMT.Term
rnmQIdWithTInstTerm sigs term = case term of
SMT.TConst _ -> term
SMT.TComb f args -> SMT.TComb (rnmQIdWithTInst sigs f)
(map (rnmQIdWithTInstTerm sigs) args)
SMT.Forall svs arg -> SMT.Forall svs (rnmQIdWithTInstTerm sigs arg)
SMT.Exists svs arg -> SMT.Forall svs (rnmQIdWithTInstTerm sigs arg)
SMT.Let bs e -> SMT.Let (map (\ (v,s) -> (v, rnmQIdWithTInstTerm sigs s)) bs)
(rnmQIdWithTInstTerm sigs e)
SMT.Match e ps -> SMT.Match (rnmQIdWithTInstTerm sigs e)
(map
(\(p,t) -> (p, rnmQIdWithTInstTerm sigs t)) ps)
SMT.Annot e as -> SMT.Annot (rnmQIdWithTInstTerm sigs e) as
|
|
demand:
|
argument 2
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Rename all sorted names occurring in a term w.r.t. its type instance
-- of the polymorphic function.
|
|
failfree:
|
<FAILING>
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,{TConst}) |-> {TConst} || (_,{TComb}) |-> {TComb} || (_,{Forall}) |-> {Forall} || (_,{Exists}) |-> {Forall} || (_,{Let}) |-> {Let} || (_,{Match}) |-> {Match} || (_,{Annot}) |-> {Annot}}
|
|
name:
|
rnmQIdWithTInstTerm
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
[(String, ([String], Language.SMTLIB.Types.Sort))] -> Language.SMTLIB.Types.Term
-> 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
|