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

 
replaceHigherOrderInExp :: Expr -> Expr
replaceHigherOrderInExp =
  trExpr Var Lit updComb FC.Let Free Or Case Branch Typed
 where
  updComb ct qn args = case ct of
    FuncPartCall _ -> fcFailed
    ConsPartCall _ -> fcFailed
    FuncCall | qn == pre "apply" -> fcFailed
    _              -> Comb ct qn args

 no demanded arguments

 deterministic operation

 
Replace higher-order features, like occurrences of `Prelude.apply` and
partial applications, by `Prelude.failed` in an expression since they
cannot be handled by SMT. Later, occurrences of `Prelude.failed` in
SMT terms are replaced by fresh variables so that they are unspecified
values.

 ()

 referentially transparent operation

 no fixity defined

 {() |-> {trExpr}}

 replaceHigherOrderInExp

 no precedence defined

 {trExpr}

 FlatCurry.Types.Expr -> FlatCurry.Types.Expr

 operation might suspend on free variables

 possibly non-terminating

 reducible on all ground data terms