| definition: |
simpTerm :: SMT.Term -> SMT.Term
simpTerm (SMT.TConst l) = SMT.TConst l
simpTerm (SMT.Let bs t) = if null bs then t'
else SMT.Let bs' t'
where bs' = map (\ (v,tm) -> (v, simpTerm tm)) bs
t' = simpTerm t
simpTerm (SMT.Forall vs t) = if null vs then t' else SMT.Forall vs t'
where t' = simpTerm t
simpTerm (SMT.Exists vs t) = if null vs then t' else SMT.Exists vs t'
where t' = simpTerm t
simpTerm (SMT.Match e ps) = SMT.Match (simpTerm e)
(map (\(p,t) -> (p, simpTerm t)) ps)
simpTerm (SMT.Annot t as) = SMT.Annot (simpTerm t) as
simpTerm (SMT.TComb f ts)
| unqual f == "/=" && length ts == 2
= simpTerm (SMT.TComb (SMT.Id "not") [SMT.TComb (SMT.Id "=") ts])
| f == SMT.Id "apply" && not (null ts')
= case head ts' of SMT.TComb s' ts0 -> SMT.TComb s' (ts0 ++ tail ts')
_ -> fts
| f == SMT.Id "not"
= case ts' of [SMT.TComb s' [ts0]] -> if s' == f then ts0 else fts
_ -> fts
| f == SMT.Id "and"
= case filter (/= true) ts' of
[] -> true
cjs -> if false `elem` cjs
then false
else SMT.TComb f (concatMap joinSame cjs)
| f == SMT.Id "or"
= case filter (/= false) ts' of
[] -> false
djs -> if true `elem` djs
then true
else SMT.TComb f (concatMap joinSame djs)
| otherwise = fts
where
ts' = map simpTerm ts
fts = SMT.TComb f ts'
joinSame arg = case arg of SMT.TComb f' args | f==f' -> args
_ -> [arg]
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| documentation: |
-------------------------------------------------------------------------- -- A simplifier for terms: |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{({TConst}) |-> {TConst} || ({Let}) |-> _ || ({Forall}) |-> _ || ({Exists}) |-> _ || ({Match}) |-> {Match} || ({Annot}) |-> {Annot} || ({TComb}) |-> _}
|
| name: |
simpTerm |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
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 |