| definition: |
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)
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{({TConst}) |-> _ || ({TSVar}) |-> _ || ({TComb}) |-> _ || ({Let}) |-> _ || ({Forall}) |-> _ || ({Exists}) |-> _ || ({Match}) |-> _}
|
| name: |
elimFailedInTerm |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Verify.ESMT.Term -> Control.Monad.Trans.State.StateT TransApplyState Data.Functor.Identity.Identity Verify.ESMT.Term |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |