CurryInfo: verify-non-fail-2.0.0 / Verify.WithSMT.elimFailedInTerm

 
elimFailedInTerm :: Term -> TAState Term
elimFailedInTerm t = case t of
  TConst _      -> return t
  TSVar _       -> return t
  TComb (As n srt) [] | n == "Prelude_failed"
    -> do st <- get
          let fv = tsFreshVarIndex st
              fvt = (fv, srt) -- sort is type of `failed`
          put st { tsFreshVarIndex = tsFreshVarIndex st + 1
                 , tsNewVars = fvt : tsNewVars st }
          return (TSVar fv)
  TComb qid ts  -> mapM elimFailedInTerm ts >>= return . TComb qid
  SMT.Let bs bt -> do trbs <- mapM (elimFailedInTerm . snd) bs
                      trbt <- elimFailedInTerm bt
                      return $ SMT.Let (zip (map fst bs) trbs) trbt
  Forall vs te  -> elimFailedInTerm te >>= return . Forall vs
  Exists vs te  -> elimFailedInTerm te >>= return . Exists vs
  Match mt brs  -> do trmt <- elimFailedInTerm mt
                      trbs <- mapM (elimFailedInTerm . snd) brs
                      return $ Match trmt (zip (map fst brs) trbs)

 argument 1

 deterministic operation

 _

 referentially transparent operation

 no fixity defined

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

 elimFailedInTerm

 no precedence defined

 _

 Verify.ESMT.Term
-> Control.Monad.Trans.State.StateT TransApplyState Data.Functor.Identity.Identity Verify.ESMT.Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term