Skip to content
Snippets Groups Projects
Commit bbdfccc9 authored by Jan Rochel's avatar Jan Rochel
Browse files

[e-acsl] Translate_term: inline Extlib.flatten

parent 1c7649c3
No related branches found
No related tags found
No related merge requests found
...@@ -871,37 +871,36 @@ and to_exp ~adata ?inplace kf env t = ...@@ -871,37 +871,36 @@ and to_exp ~adata ?inplace kf env t =
(Env.Logic_env.get_profile env); (Env.Logic_env.get_profile env);
let logic_env = Env.Logic_env.get env in let logic_env = Env.Logic_env.get env in
let t = Logic_normalizer.get_term t in let t = Logic_normalizer.get_term t in
let (rexp, _, _) as result = let ((rexp, _), _) as result =
Extlib.flatten Env.with_params_and_result
(Env.with_params_and_result ~rte:false
~rte:false ~f:(fun env ->
~f:(fun env -> let e, adata, env, sty, name =
let e, adata, env, sty, name = context_insensitive_term_to_exp ?inplace ~adata kf env t
context_insensitive_term_to_exp ?inplace ~adata kf env t in
in let env =
let env = if generate_rte then !translate_rte_exp_ref kf env e else env
if generate_rte then !translate_rte_exp_ref kf env e else env in
in let cast = Typing.get_cast ~logic_env t in
let cast = Typing.get_cast ~logic_env t in let name = if name = "" then None else Some name in
let name = if name = "" then None else Some name in Extlib.nest
Extlib.nest adata
adata (Typed_number.add_cast
(Typed_number.add_cast ~loc:t.term_loc
~loc:t.term_loc ?name
?name env
env kf
kf cast
cast sty
sty (Some t)
(Some t) e)
e) )
) env
env)
in in
Options.debug ~dkey ~level:4 "to_exp %a {%a} %a = %a" Options.debug ~dkey ~level:4 "to_exp %a {%a} %a = %a"
Kernel_function.pretty kf Profile.pretty (Env.Logic_env.get_profile env) Kernel_function.pretty kf Profile.pretty (Env.Logic_env.get_profile env)
Printer.pp_term t Printer.pp_exp rexp; Printer.pp_term t Printer.pp_exp rexp;
result Extlib.flatten result
let term_to_exp_without_inplace ~adata kf env t = to_exp ~adata kf env t let term_to_exp_without_inplace ~adata kf env t = to_exp ~adata kf env t
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment