diff options
author | Jonathan Protzenko | 2023-01-30 19:02:48 -0800 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | b54d983914ad8f380ca474fd3fece66770fc21cd (patch) | |
tree | 0617ae0341ecfb82960fed1da971e5d82496f195 /compiler | |
parent | 1ffe67501674a2ec2caa623913324bee665aa43a (diff) |
Don't need extra variables for the decreases clauses
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Extract.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index eb96cd48..64069cb0 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2130,6 +2130,7 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter) F.pp_print_space fmt (); (* Tuple of the arguments *) let vars = List.map (fun (v: var) -> v.id) def_body.inputs in + if List.length vars = 1 then F.pp_print_string fmt (ctx_get_var (List.hd vars) ctx_body) else begin @@ -2345,12 +2346,17 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) if has_decreases_clause && !backend = Lean then begin let def_body = Option.get def.body in let vars = List.map (fun (v: var) -> v.id) def_body.inputs in + let num_fwd_inputs = + def.signature.info.num_fwd_inputs_with_fuel_with_state + in + let vars = Collections.List.prefix num_fwd_inputs vars in + (* terminates_by *) let terminates_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in F.pp_print_break fmt 0 0; - F.pp_open_hvbox fmt ctx.indent_incr; + F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "termination_by"; - F.pp_open_hvbox fmt ctx.indent_incr; + F.pp_open_hovbox fmt 0; F.pp_print_space fmt (); F.pp_print_string fmt def_name; F.pp_print_space fmt (); @@ -2361,7 +2367,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "=>"; F.pp_close_box fmt (); - F.pp_open_hbox fmt (); + F.pp_open_hovbox fmt 0; F.pp_print_space fmt (); F.pp_print_string fmt terminates_name; F.pp_print_space fmt (); |