CurryInfo: property-prover-2.0.0 / ESMT.simpTerm

 
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]

 argument 1

 deterministic operation

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

 <FAILING>

 referentially transparent operation

 no fixity defined

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

 simpTerm

 no precedence defined

 _

 Language.SMTLIB.Types.Term -> Language.SMTLIB.Types.Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term