| definition: |
simpTerm :: Term -> Term
simpTerm (TConst l) = TConst l
simpTerm (TSVar v) = TSVar v
simpTerm (Let bs t) = if null bs then t'
else Let bs' t'
where bs' = map (\ (v,tm) -> (v, simpTerm tm)) bs
t' = simpTerm t
simpTerm (Forall vs t) = if null vs then t' else Forall vs t'
where t' = simpTerm t
simpTerm (Exists vs t) = if null vs then t' else Exists vs t'
where t' = simpTerm t
simpTerm (TComb f ts)
| qidName f == "/=" && length ts == 2
= simpTerm (TComb (Id "not") [TComb (Id "=") ts])
| f == Id "apply" && not (null ts')
= case head ts' of TComb s' ts0 -> TComb s' (ts0 ++ tail ts')
_ -> fts
| f == Id "not"
= case ts' of [TComb s' [ts0]] -> if s' == f then ts0 else fts
_ -> fts
| f == Id "and"
= case filter (/= tTrue) ts' of
[] -> tTrue
cjs -> if tFalse `elem` cjs
then tFalse
else TComb f (concatMap joinSame cjs)
| f == Id "or"
= case filter (/= tFalse) ts' of
[] -> tFalse
djs -> if tTrue `elem` djs
then tTrue
else TComb f (concatMap joinSame djs)
| otherwise = fts
where
ts' = map simpTerm ts
fts = TComb f ts'
joinSame arg = case arg of 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} || ({TSVar}) |-> {TSVar} || ({Let}) |-> _ || ({Forall}) |-> _ || ({Exists}) |-> _ || ({TComb}) |-> _}
|
| name: |
simpTerm |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Term -> Term |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |