CurryInfo: contract-prover-4.0.0 / ESMT.simpTerm

 
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]

 argument 1

 deterministic operation

 
-----------------------------------------------------------------------
A simplifier for terms:

 <FAILING>

 referentially transparent operation

 no fixity defined

 {({TConst}) |-> {TConst} || ({TSVar}) |-> {TSVar} || ({Let}) |-> _ || ({Forall}) |-> _ || ({Exists}) |-> _ || ({TComb}) |-> _}

 simpTerm

 no precedence defined

 _

 Term -> Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term