diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/primitives.lean | 35 | ||||
| -rw-r--r-- | compiler/Driver.ml | 34 | ||||
| -rw-r--r-- | compiler/Extract.ml | 26 | ||||
| -rw-r--r-- | compiler/Translate.ml | 14 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 35 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain.lean | 2 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 55 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 5 |
8 files changed, 150 insertions, 56 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean index 3b1d39fc..dc2314fc 100644 --- a/backends/lean/primitives.lean +++ b/backends/lean/primitives.lean @@ -1,3 +1,5 @@ +import Lean + ------------- -- PRELUDE -- ------------- @@ -10,14 +12,14 @@ inductive error where | arrayOutOfBounds: error | maximumSizeExceeded: error | panic: error -deriving Repr +deriving Repr, BEq open error inductive result (α : Type u) where | ret (v: α): result α | fail (e: error): result α -deriving Repr +deriving Repr, BEq open result @@ -48,7 +50,9 @@ instance : Pure result where def massert (b:Bool) : result Unit := if b then return () else fail assertionFailure --- Machine integers +---------------------- +-- MACHINE INTEGERS -- +---------------------- -- NOTE: we reuse the USize type from prelude.lean, because at least we know -- it's defined in an idiomatic style that is going to make proofs easy (and @@ -123,13 +127,16 @@ macro_rules #eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... -#eval USize.checked_sub 10 20 +#eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 + #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want #eval USize.sub 0 1 #eval UInt8.add 255 255 --- Vectors +------------- +-- VECTORS -- +------------- def vec (α : Type u) := { l : List α // List.length l < USize.size } @@ -176,3 +183,21 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) / -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) + +-------------------- +-- ASSERT COMMAND -- +-------------------- + +open Lean Elab Command Term Meta + +syntax (name := assert) "#assert" term: command + +@[command_elab assert] +def assertImpl : CommandElab := fun (stx: Syntax) => do + logInfo "Hello World" + +def ignore (a: Prop) (x: a) := () + +#eval ignore (2 == 2) (by simp) + +#assert (2 == 2) diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 4350c9ae..f460f73d 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -95,28 +95,19 @@ let () = " Forbid backward functions from updating the state" ); ( "-template-clauses", Arg.Set extract_template_decreases_clauses, - " Generate templates for the required decreases clauses, in a\n\ - \ dedicated file. Reauires -decreases-clauses" + " Generate templates for the required decreases clauses, in a \ + dedicated file. Implies -decreases-clauses" ); ( "-no-split-files", Arg.Clear split_files, - " Don't split the definitions between different files for types,\n\ - \ functions, etc." ); + " Don't split the definitions between different files for types, \ + functions, etc." ); ( "-no-check-inv", Arg.Clear check_invariants, - " Deactivate the invariant sanity checks performed at every step of\n\ - \ evaluation. Dramatically saves speed." ); + " Deactivate the invariant sanity checks performed at every step of \ + evaluation. Dramatically saves speed." ); ] in - (* Sanity check: -template-clauses ==> not -no-decrease-clauses *) - assert (!extract_decreases_clauses || not !extract_template_decreases_clauses); - (* Sanity check: -backward-no-state-update ==> not -no-state *) - assert ((not !backward_no_state_update) || !use_state); - (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *) - assert ( - (not !use_fuel) - || (not !extract_decreases_clauses) - && not !extract_template_decreases_clauses); let spec = Arg.align spec in let filenames = ref [] in @@ -127,6 +118,19 @@ let () = exit 1 in + if !extract_template_decreases_clauses then + extract_decreases_clauses := true; + + (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *) + assert (!extract_decreases_clauses || not !extract_template_decreases_clauses); + (* Sanity check: -backward-no-state-update ==> -state *) + assert ((not !backward_no_state_update) || !use_state); + (* Sanity check: the use of decrease clauses is not compatible with the use of fuel *) + assert ( + (not !use_fuel) + || (not !extract_decreases_clauses) + && not !extract_template_decreases_clauses); + (* Check that the user specified a backend *) let _ = match !opt_backend with diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 0207d1ea..7670c753 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1992,6 +1992,11 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx) in List.iter extract_param def.signature.inputs +let assert_backend_supports_decreases_clauses () = + match !backend with + | FStar | Lean -> () + | _ -> failwith "decreases clauses only supported for the Lean & F* backends" + (** Extract a decrease clause function template body. Only for F*. @@ -2010,7 +2015,8 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx) *) let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) (def : fun_decl) : unit = - assert (!backend = FStar); + assert_backend_supports_decreases_clauses (); + (* Retrieve the function name *) let def_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in (* Add a break before *) @@ -2022,14 +2028,16 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) * one line *) F.pp_open_hvbox fmt 0; (* Add the [unfold] keyword *) - F.pp_print_string fmt "unfold"; - F.pp_print_space fmt (); + if !backend = FStar then begin + F.pp_print_string fmt "unfold"; + F.pp_print_space fmt (); + end; (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) F.pp_open_hvbox fmt ctx.indent_incr; (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) - F.pp_print_string fmt ("let " ^ def_name); + F.pp_print_string fmt ((if !backend = FStar then "let " else "def ") ^ def_name); F.pp_print_space fmt (); (* Extract the parameters *) let space = ref true in @@ -2038,15 +2046,15 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ":"; (* Print the signature *) F.pp_print_space fmt (); - F.pp_print_string fmt "nat"; + F.pp_print_string fmt (if !backend = FStar then "nat" else "Nat"); (* Print the "=" *) F.pp_print_space fmt (); - F.pp_print_string fmt "="; + F.pp_print_string fmt (if !backend = FStar then "=" else ":="); (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_close_box fmt (); F.pp_print_space fmt (); (* Print the "admit ()" *) - F.pp_print_string fmt "admit ()"; + F.pp_print_string fmt (if !backend = FStar then "admit ()" else "sorry"); (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) F.pp_close_box fmt (); (* Close the box for the whole definition *) @@ -2128,7 +2136,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) if is_opaque then extract_fun_input_parameters_types ctx fmt def; (* [Tot] *) if has_decreases_clause then ( - assert (!backend = FStar); + assert_backend_supports_decreases_clauses (); F.pp_print_string fmt "Tot"; F.pp_print_space fmt ()); extract_ty ctx fmt has_decreases_clause def.signature.output; @@ -2137,7 +2145,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Print the decrease clause - rk.: a function with a decreases clause * is necessarily a transparent function *) if has_decreases_clause then ( - assert (!backend = FStar); + assert_backend_supports_decreases_clauses (); F.pp_print_space fmt (); (* Open a box for the decreases clause *) F.pp_open_hovbox fmt ctx.indent_incr; diff --git a/compiler/Translate.ml b/compiler/Translate.ml index b2162b20..4ca9eff2 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -353,6 +353,9 @@ type gen_config = { (** If [true], extract the opaque declarations, otherwise ignore. *) extract_state_type : bool; (** If [true], generate a definition/declaration for the state type *) + extract_globals : bool; + (** If [true], generate a definition/declaration for top-level (global) + declarations *) interface : bool; (** [true] if we generate an interface file, [false] otherwise. For now, this only impacts whether we use [val] or [assume val] for the @@ -463,8 +466,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let is_opaque = Option.is_none body.Pure.body in if - ((not is_opaque) && config.extract_transparent) - || (is_opaque && config.extract_opaque) + config.extract_globals && ( + ((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque) + ) then Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface @@ -926,6 +931,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : extract_transparent = true; extract_opaque = false; extract_state_type = false; + extract_globals = false; interface = false; test_trans_unit_functions = false; } @@ -998,12 +1004,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_fun_decls = true; + extract_globals = true; test_trans_unit_functions = !Config.test_trans_unit_functions; } in let clauses_module = if needs_clauses_module then - [ module_name ^ module_delimiter ^ "Clauses" ] + [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"] else [] in extract_file fun_config gen_ctx fun_filename crate.A.name fun_module @@ -1020,6 +1027,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : extract_transparent = true; extract_opaque = true; extract_state_type = !Config.use_state; + extract_globals = true; interface = false; test_trans_unit_functions = !Config.test_trans_unit_functions; } diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 3b1d39fc..dc2314fc 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -1,3 +1,5 @@ +import Lean + ------------- -- PRELUDE -- ------------- @@ -10,14 +12,14 @@ inductive error where | arrayOutOfBounds: error | maximumSizeExceeded: error | panic: error -deriving Repr +deriving Repr, BEq open error inductive result (α : Type u) where | ret (v: α): result α | fail (e: error): result α -deriving Repr +deriving Repr, BEq open result @@ -48,7 +50,9 @@ instance : Pure result where def massert (b:Bool) : result Unit := if b then return () else fail assertionFailure --- Machine integers +---------------------- +-- MACHINE INTEGERS -- +---------------------- -- NOTE: we reuse the USize type from prelude.lean, because at least we know -- it's defined in an idiomatic style that is going to make proofs easy (and @@ -123,13 +127,16 @@ macro_rules #eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... -#eval USize.checked_sub 10 20 +#eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 + #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want #eval USize.sub 0 1 #eval UInt8.add 255 255 --- Vectors +------------- +-- VECTORS -- +------------- def vec (α : Type u) := { l : List α // List.length l < USize.size } @@ -176,3 +183,21 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) / -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) + +-------------------- +-- ASSERT COMMAND -- +-------------------- + +open Lean Elab Command Term Meta + +syntax (name := assert) "#assert" term: command + +@[command_elab assert] +def assertImpl : CommandElab := fun (stx: Syntax) => do + logInfo "Hello World" + +def ignore (a: Prop) (x: a) := () + +#eval ignore (2 == 2) (by simp) + +#assert (2 == 2) diff --git a/tests/lean/hashmap_on_disk/HashmapMain.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean index e99d3a6f..99415d9d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain.lean @@ -1 +1 @@ -def hello := "world"
\ No newline at end of file +def hello := "world" diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index eb72cc97..0dcb6450 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,6 +3,7 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque +import HashmapMain.Clauses.Template /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k @@ -14,12 +15,18 @@ def hashmap_hash_map_allocate_slots_loop_fwd := if n > (USize.ofNatCore 0 (by intlit)) then + match h: (vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil).val with + | result.fail e => result.fail e + | result.ret slots0 => do - let slots0 <- - vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil 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 T slots n => n + decreasing_by + simp_wf + sorry + /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_fwd @@ -56,7 +63,8 @@ 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) : - result (vec (hashmap_list_t T)) + Tot (result (vec (hashmap_list_t T))) + (decreases (hashmap_hash_map_clear_slots_loop_decreases T slots i)) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -98,7 +106,10 @@ 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) : result Bool := + (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)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -115,7 +126,8 @@ 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) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_insert_in_list_loop_decreases T key value ls)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -187,7 +199,9 @@ def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) /- [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) : - result (hashmap_hash_map_t T) + Tot (result (hashmap_hash_map_t T)) + (decreases ( + hashmap_hash_map_move_elements_from_list_loop_decreases T ntable ls)) := match ls with | hashmap_list_t.HashmapListCons k v tl => @@ -208,7 +222,8 @@ def hashmap_hash_map_move_elements_from_list_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) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + Tot (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) + (decreases (hashmap_hash_map_move_elements_loop_decreases T ntable slots i)) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -283,7 +298,10 @@ def hashmap_hash_map_insert_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) : result Bool := + (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)) + := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -310,7 +328,10 @@ def hashmap_hash_map_contains_key_fwd /- [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) : result T := + (T : Type) (key : USize) (ls : hashmap_list_t T) : + Tot (result T) + (decreases (hashmap_hash_map_get_in_list_loop_decreases T key ls)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -337,7 +358,10 @@ def hashmap_hash_map_get_fwd /- [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) : result T := + (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)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -354,7 +378,8 @@ def hashmap_hash_map_get_mut_in_list_fwd /- [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) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -410,7 +435,10 @@ def hashmap_hash_map_get_mut_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) : result (Option T) := + (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)) + := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -435,7 +463,8 @@ def hashmap_hash_map_remove_from_list_fwd /- [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) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 1b8f8954..d1cd9579 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -16,11 +16,6 @@ structure hashmap_hash_map_t (T : Type) where hashmap_hash_map_slots : vec (hashmap_list_t T) -/- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : result UInt32 := - result.ret (UInt32.ofNatCore 4294967295 (by intlit)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) - /- The state type used in the state-error monad -/ axiom state : Type |