WIP lots of stuff

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