|
definition:
|
reduceAsInTerm :: SMT.Term -> SMT.Term
reduceAsInTerm (SMT.TConst l) = SMT.TConst l
reduceAsInTerm (SMT.Let bs t) = SMT.Let
(map (\ (v,tm) ->
(v, reduceAsInTerm tm)) bs)
(reduceAsInTerm t)
reduceAsInTerm (SMT.Forall vs t) = SMT.Forall vs (reduceAsInTerm t)
reduceAsInTerm (SMT.Exists vs t) = SMT.Exists vs (reduceAsInTerm t)
reduceAsInTerm (SMT.Match e ps) = SMT.Match (reduceAsInTerm e)
(map (\(p,t) ->
(p, reduceAsInTerm t)) ps)
reduceAsInTerm (SMT.Annot t as) = SMT.Annot (reduceAsInTerm t) as
reduceAsInTerm (SMT.TComb f ts) = SMT.TComb (simpAs f) (map reduceAsInTerm ts)
where
simpAs qid = case qid of SMT.As n (SMT.SComb s _) | s == "Func" -> SMT.Id n
_ -> qid
|
|
demand:
|
argument 1
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
--------------------------------------------------------------------------
-- Remove As-identifiers if they are functions (for better readability):
|
|
failfree:
|
_
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{({TConst}) |-> {TConst} || ({Let}) |-> {Let} || ({Forall}) |-> {Forall} || ({Exists}) |-> {Exists} || ({Match}) |-> {Match} || ({Annot}) |-> {Annot} || ({TComb}) |-> {TComb}}
|
|
name:
|
reduceAsInTerm
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
{Annot,Exists,Forall,Let,Match,TComb,TConst}
|
|
signature:
|
Language.SMTLIB.Types.Term -> Language.SMTLIB.Types.Term
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
reducible on all ground data terms
|