diff options
| -rw-r--r-- | compiler/Extract.ml | 61 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 84 |
2 files changed, 107 insertions, 38 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index f45b9b58..eb96cd48 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2258,14 +2258,16 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* [Tot] *) if has_decreases_clause then ( assert_backend_supports_decreases_clauses (); - F.pp_print_string fmt "Tot"; - F.pp_print_space fmt ()); + if !backend = FStar then begin + F.pp_print_string fmt "Tot"; + F.pp_print_space fmt () + end); extract_ty ctx fmt has_decreases_clause def.signature.output; (* Close the box for the return type *) F.pp_close_box fmt (); (* Print the decrease clause - rk.: a function with a decreases clause * is necessarily a transparent function *) - if has_decreases_clause then ( + if has_decreases_clause && !backend = FStar then ( assert_backend_supports_decreases_clauses (); F.pp_print_space fmt (); (* Open a box for the decreases clause *) @@ -2339,6 +2341,59 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) print_decl_end_delimiter fmt kind; (* Close the outer box for the definition *) F.pp_close_box fmt (); + (* Termination clause *) + 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 + (* 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_print_string fmt "termination_by"; + F.pp_open_hvbox fmt ctx.indent_incr; + F.pp_print_space fmt (); + F.pp_print_string fmt def_name; + F.pp_print_space fmt (); + Collections.List.iter_link + (F.pp_print_space fmt) + (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body)) + vars; + F.pp_print_space fmt (); + F.pp_print_string fmt "=>"; + F.pp_close_box fmt (); + F.pp_open_hbox fmt (); + F.pp_print_space fmt (); + F.pp_print_string fmt terminates_name; + F.pp_print_space fmt (); + List.iter + (fun (p : type_var) -> + let pname = ctx_get_type_var p.index ctx in + F.pp_print_string fmt pname; + F.pp_print_space fmt ()) + def.signature.type_params; + List.iter + (fun v -> + F.pp_print_string fmt (ctx_get_var v ctx_body); + F.pp_print_space fmt ()) + vars; + F.pp_close_box fmt (); + F.pp_close_box fmt (); + + let decreases_name = ctx_get_decreases_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_print_string fmt "decreasing_by"; + F.pp_print_space fmt (); + F.pp_open_hvbox fmt ctx.indent_incr; + F.pp_print_string fmt decreases_name; + F.pp_print_space fmt (); + Collections.List.iter_link + (F.pp_print_space fmt) + (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body)) + vars; + F.pp_close_box fmt (); + F.pp_close_box fmt () + end; (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 29ed735f..6cdc6bd8 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -11,8 +11,7 @@ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_loop_fwd (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : - Tot (result (vec (hashmap_list_t T))) - (decreases (hashmap_hash_map_allocate_slots_loop_decreases T slots n)) + (result (vec (hashmap_list_t T))) := if n > (USize.ofNatCore 0 (by intlit)) then @@ -22,6 +21,8 @@ def hashmap_hash_map_allocate_slots_loop_fwd let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots +termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => hashmap_hash_map_allocate_slots_loop_terminates T slots n +decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_fwd @@ -58,8 +59,7 @@ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ def hashmap_hash_map_clear_slots_loop_fwd_back (T : Type) (slots : vec (hashmap_list_t T)) (i : USize) : - Tot (result (vec (hashmap_list_t T))) - (decreases (hashmap_hash_map_clear_slots_loop_decreases T slots i)) + (result (vec (hashmap_list_t T))) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -71,6 +71,8 @@ def hashmap_hash_map_clear_slots_loop_fwd_back hashmap_list_t.HashmapListNil hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 else result.ret slots +termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => hashmap_hash_map_clear_slots_loop_terminates T slots i +decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ def hashmap_hash_map_clear_slots_fwd_back @@ -102,8 +104,7 @@ def hashmap_hash_map_len_fwd /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - Tot (result Bool) - (decreases (hashmap_hash_map_insert_in_list_loop_decreases T key value ls)) + (result Bool) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -112,6 +113,9 @@ def hashmap_hash_map_insert_in_list_loop_fwd else hashmap_hash_map_insert_in_list_loop_fwd T key value tl | hashmap_list_t.HashmapListNil => result.ret true +termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => + hashmap_hash_map_insert_in_list_loop_terminates T key value ls +decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_fwd @@ -121,8 +125,7 @@ def hashmap_hash_map_insert_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - Tot (result (hashmap_list_t T)) - (decreases (hashmap_hash_map_insert_in_list_loop_decreases T key value ls)) + (result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -136,6 +139,9 @@ def hashmap_hash_map_insert_in_list_loop_back let l := hashmap_list_t.HashmapListNil result.ret (hashmap_list_t.HashmapListCons key value l) +termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => + hashmap_hash_map_insert_in_list_loop_terminates T key value ls +decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_back @@ -195,9 +201,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap_hash_map_move_elements_from_list_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - Tot (result (hashmap_hash_map_t T)) - (decreases ( - hashmap_hash_map_move_elements_from_list_loop_decreases T ntable ls)) + (result (hashmap_hash_map_t T)) := match ls with | hashmap_list_t.HashmapListCons k v tl => @@ -206,6 +210,13 @@ def hashmap_hash_map_insert_no_resize_fwd_back hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl | hashmap_list_t.HashmapListNil => result.ret ntable + termination_by + hashmap_hash_map_move_elements_from_list_loop_fwd_back + ntable + ls + => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls + decreasing_by + hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap_hash_map_move_elements_from_list_fwd_back @@ -218,9 +229,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back def hashmap_hash_map_move_elements_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) : - Tot (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) - (decreases ( - hashmap_hash_map_move_elements_loop_decreases T ntable slots i)) + (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -237,6 +246,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back let slots0 <- vec_index_mut_back (hashmap_list_t T) slots i l0 hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) + termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => + hashmap_hash_map_move_elements_loop_terminates T ntable slots i + decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ def hashmap_hash_map_move_elements_fwd_back @@ -294,11 +306,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : - Tot (result Bool) - (decreases ( - hashmap_hash_map_contains_key_in_list_loop_decreases T key ls)) - := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result Bool) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -306,6 +314,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret false + termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => + hashmap_hash_map_contains_key_in_list_loop_terminates T key ls + decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_fwd @@ -325,10 +336,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : - Tot (result T) - (decreases (hashmap_hash_map_get_in_list_loop_decreases T key ls)) - := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result T) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -336,6 +344,8 @@ def hashmap_hash_map_insert_no_resize_fwd_back else hashmap_hash_map_get_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.fail error.panic + termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls + decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_fwd @@ -355,10 +365,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : - Tot (result T) - (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) - := + (T : Type) (ls : hashmap_list_t T) (key : USize) : (result T) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -366,6 +373,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key | hashmap_list_t.HashmapListNil => result.fail error.panic + termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key + decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_fwd @@ -375,8 +385,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_back (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - Tot (result (hashmap_list_t T)) - (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) + (result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -388,6 +397,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back result.ret (hashmap_list_t.HashmapListCons ckey cvalue l) | hashmap_list_t.HashmapListNil => result.fail error.panic + termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => + hashmap_hash_map_get_mut_in_list_loop_terminates T ls key ret0 + decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key ret0 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_back @@ -434,10 +446,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : - Tot (result (Option T)) - (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) - := + (T : Type) (key : USize) (ls : hashmap_list_t T) : (result (Option T)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -453,6 +462,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back else hashmap_hash_map_remove_from_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret Option.none + termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => + hashmap_hash_map_remove_from_list_loop_terminates T key ls + decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_fwd @@ -462,8 +474,7 @@ def hashmap_hash_map_insert_no_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_back (T : Type) (key : USize) (ls : hashmap_list_t T) : - Tot (result (hashmap_list_t T)) - (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) + (result (hashmap_list_t T)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => @@ -483,6 +494,9 @@ def hashmap_hash_map_insert_no_resize_fwd_back | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil + termination_by hashmap_hash_map_remove_from_list_loop_back key ls => + hashmap_hash_map_remove_from_list_loop_terminates T key ls + decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_back |