Use implicit parameters in the generated code (#333)

* Update the lean toolchain

* Start computing which type parameters should be implicit/explicit

* Update the Primitives.fst file

* Update the Lean library

* Fix an issue with builtin definitions

* Update the computation of the implicit parameters

* Update the extraction

* Update the extraction of types, trait refs and trait decl refs

* Update the extraction of globals

* Regenerate some of the Lean files

* Update the extraction of aggregated arrays

* Update more Lean tests

* Update the F* test files

* Update the test proofs

* Update the Primitives.v file

* Regenerate the Coq files

* Update the Primitives.v file

* Fix minor mistakes

* Update the README

* Update the .gitignore

* Fix minor issues

* Fix a mistake in Primitives.fst

* Fix more issues

* Fix an issue with the Coq projectors

* Reformat the code

.gitignore

@@ -59,6 +59,7 @@ tests/fstar/misc/obj/
 *.d
 *Makefile.coq
 *CoqMakefile.conf
+*_CoqProject*
 
 # HOL4
 .HOLMK

README.md

@@ -35,9 +35,13 @@ You need to install OCaml, together with some packages.
 We suggest you to follow those [instructions](https://ocaml.org/docs/install.html),
 and install OPAM on the way (same instructions).
 
-We use **OCaml 4.13.1**: `opam switch create 4.13.1+options`
+Any recent version of **OCaml 4** should do. For instance, if you want to use OCaml
+4.14.2:
+```
+opam switch create 4.14.2
+```
 
-The dependencies can then be installed with the following command:
+You can then install the dependencies with the following command:
 
 ```
 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \

backends/lean/Base/Primitives/Alloc.lean

@@ -11,21 +11,21 @@ namespace boxed -- alloc.boxed
 
 namespace Box -- alloc.boxed.Box
 
-def deref (T : Type) (x : T) : Result T := ok x
-def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
+def deref {T : Type} (x : T) : Result T := ok x
+def deref_mut {T : Type} (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
 
 /-- Trait instance -/
 def coreopsDerefInst (Self : Type) :
   core.ops.deref.Deref Self := {
   Target := Self
-  deref := deref Self
+  deref := deref
 }
 
 /-- Trait instance -/
 def coreopsDerefMutInst (Self : Type) :
   core.ops.deref.DerefMut Self := {
   derefInst := coreopsDerefInst Self
-  deref_mut := deref_mut Self
+  deref_mut := deref_mut
 }
 
 end Box -- alloc.boxed.Box

backends/lean/Base/Primitives/Core.lean

@@ -58,22 +58,22 @@ def clone.CloneBool : clone.Clone Bool := {
    This acts like a swap effectively in a functional pure world.
    We return the old value of `dst`, i.e. `dst` itself.
    The new value of `dst` is `src`. -/
-@[simp] def mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
+@[simp] def mem.replace {a : Type} (dst : a) (src : a) : a × a := (dst, src)
 
 /- [core::mem::swap] -/
-@[simp] def mem.swap (T: Type) (a b: T): T × T := (b, a)
+@[simp] def mem.swap {T : Type} (a b : T): T × T := (b, a)
 
 end core
 
 /- [core::option::{core::option::Option<T>}::unwrap] -/
-@[simp] def core.option.Option.unwrap (T : Type) (x : Option T) : Result T :=
+@[simp] def core.option.Option.unwrap {T : Type} (x : Option T) : Result T :=
   Result.ofOption x Error.panic
 
 /- [core::option::Option::take] -/
-@[simp] def core.option.Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
+@[simp] def core.option.Option.take {T: Type} (self: Option T): Option T × Option T := (self, .none)
 
 /- [core::option::Option::is_none] -/
-@[simp] def core.option.Option.is_none (T: Type) (self: Option T): Bool := self.isNone
+@[simp] def core.option.Option.is_none {T: Type} (self: Option T): Bool := self.isNone
 
 /- [core::clone::Clone::clone_from]:
    Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43

backends/lean/Base/Primitives/Vec.lean

@@ -48,17 +48,16 @@ instance (α : Type u) : Inhabited (Vec α) := by
   constructor
   apply Vec.new
 
--- TODO: very annoying that the α is an explicit parameter
 @[simp]
-abbrev Vec.len (α : Type u) (v : Vec α) : Usize :=
+abbrev Vec.len {α : Type u} (v : Vec α) : Usize :=
   Usize.ofIntCore v.val.length (by constructor <;> scalar_tac)
 
 @[simp]
-theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len α v).val = v.length :=
+theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len v).val = v.length :=
   by rfl
 
 @[irreducible]
-def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
+def Vec.push {α : Type u} (v : Vec α) (x : α) : Result (Vec α)
   :=
   let nlen := List.length v.val + 1
   if h : nlen ≤ U32.max || nlen ≤ Usize.max then
@@ -72,21 +71,13 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
 
 @[pspec]
 theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.length < Usize.max) :
-  ∃ v1, v.push α x = ok v1 ∧
+  ∃ v1, v.push x = ok v1 ∧
   v1.val = v.val ++ [x] := by
   rw [push]; simp
-  split <;> simp_all <;>
+  split <;> simp_all
   scalar_tac
 
--- This shouldn't be used
-def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
-  if i.val < v.length then
-    ok ()
-  else
-    fail arrayOutOfBounds
-
--- This is actually the backward function
-def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.insert {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   if i.val < v.length then
     ok ⟨ v.val.update i.toNat x, by have := v.property; simp [*] ⟩
   else
@@ -95,19 +86,14 @@ def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
 @[pspec]
 theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.insert α i x = ok nv ∧ nv.val = v.val.update i.toNat x := by
+  ∃ nv, v.insert i x = ok nv ∧ nv.val = v.val.update i.toNat x := by
   simp [insert, *]
 
 def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.toNat with
   | none => fail .arrayOutOfBounds
   | some x => ok x
 
-/- In the theorems below: we don't always need the `∃ ..`, but we use one
-   so that `progress` introduces an opaque variable and an equality. This
-   helps control the context.
- -/
-
 @[pspec]
 theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
@@ -154,90 +140,90 @@ theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Us
   simp [h]
 
 /- [alloc::vec::Vec::index]: forward function -/
-def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+def Vec.index {T I : Type} (inst : core.slice.index.SliceIndex I (Slice T))
   (self : Vec T) (i : I) : Result inst.Output :=
   sorry -- TODO
 
 /- [alloc::vec::Vec::index_mut]: forward function -/
-def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+def Vec.index_mut {T I : Type} (inst : core.slice.index.SliceIndex I (Slice T))
   (self : Vec T) (i : I) :
   Result (inst.Output × (inst.Output → Result (Vec T))) :=
   sorry -- TODO
 
 /- Trait implementation: [alloc::vec::Vec] -/
 @[reducible]
-def Vec.coreopsindexIndexInst (T I : Type)
+def Vec.coreopsindexIndexInst {T I : Type}
   (inst : core.slice.index.SliceIndex I (Slice T)) :
   core.ops.index.Index (alloc.vec.Vec T) I := {
   Output := inst.Output
-  index := Vec.index T I inst
+  index := Vec.index inst
 }
 
 /- Trait implementation: [alloc::vec::Vec] -/
 @[reducible]
-def Vec.coreopsindexIndexMutInst (T I : Type)
+def Vec.coreopsindexIndexMutInst {T I : Type}
   (inst : core.slice.index.SliceIndex I (Slice T)) :
   core.ops.index.IndexMut (alloc.vec.Vec T) I := {
-  indexInst := Vec.coreopsindexIndexInst T I inst
-  index_mut := Vec.index_mut T I inst
+  indexInst := Vec.coreopsindexIndexInst inst
+  index_mut := Vec.index_mut inst
 }
 
 @[simp]
 theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
-  Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
+  Vec.index (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
   Vec.index_usize v i :=
   sorry
 
 @[simp]
 theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
-  Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
+  Vec.index_mut (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
   index_mut_usize v i :=
   sorry
 
 end alloc.vec
 
 /-- [alloc::slice::{@Slice<T>}::to_vec] -/
 def alloc.slice.Slice.to_vec
-  (T : Type) (cloneInst : core.clone.Clone T) (s : Slice T) : Result (alloc.vec.Vec T) :=
+  {T : Type} (cloneInst : core.clone.Clone T) (s : Slice T) : Result (alloc.vec.Vec T) :=
   -- TODO: we need a monadic map
   sorry
 
 /-- [core::slice::{@Slice<T>}::reverse] -/
-def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
+def core.slice.Slice.reverse {T : Type} (s : Slice T) : Slice T :=
   ⟨ s.val.reverse, by sorry ⟩
 
-def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
+def alloc.vec.Vec.with_capacity {T : Type} (_ : Usize) : alloc.vec.Vec T := Vec.new T
 
 /- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27
    Name pattern: alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref -/
-def alloc.vec.DerefVec.deref (T : Type) (v : Vec T) : Slice T :=
+def alloc.vec.DerefVec.deref {T : Type} (v : Vec T) : Slice T :=
   ⟨ v.val, v.property ⟩
 
 @[reducible]
-def core.ops.deref.DerefVec (T : Type) : core.ops.deref.Deref (alloc.vec.Vec T) := {
+def core.ops.deref.DerefVec {T : Type} : core.ops.deref.Deref (alloc.vec.Vec T) := {
   Target := Slice T
-  deref := fun v => ok (alloc.vec.DerefVec.deref T v)
+  deref := fun v => ok (alloc.vec.DerefVec.deref v)
 }
 
 /- [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}::deref_mut]:
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2632:4-2632:39
    Name pattern: alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, @A>>}::deref_mut -/
-def alloc.vec.DerefMutVec.deref_mut (T : Type) (v :  alloc.vec.Vec T) :
+def alloc.vec.DerefMutVec.deref_mut {T : Type} (v :  alloc.vec.Vec T) :
    Result ((Slice T) × (Slice T → Result (alloc.vec.Vec T))) :=
    ok (⟨ v.val, v.property ⟩, λ s => ok ⟨ s.val, s.property ⟩)
 
 /- Trait implementation: [alloc::vec::{(core::ops::deref::DerefMut for alloc::vec::Vec<T, A>)#10}]
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2630:0-2630:49
    Name pattern: core::ops::deref::DerefMut<alloc::vec::Vec<@Self, @>> -/
 @[reducible]
-def core.ops.deref.DerefMutVec (T : Type) :
+def core.ops.deref.DerefMutVec {T : Type} :
   core.ops.deref.DerefMut (alloc.vec.Vec T) := {
-  derefInst := core.ops.deref.DerefVec T
-  deref_mut := alloc.vec.DerefMutVec.deref_mut T
+  derefInst := core.ops.deref.DerefVec
+  deref_mut := alloc.vec.DerefMutVec.deref_mut
 }
 
-def alloc.vec.Vec.resize (T : Type) (cloneInst : core.clone.Clone T)
+def alloc.vec.Vec.resize {T : Type} (cloneInst : core.clone.Clone T)
   (v : alloc.vec.Vec T) (new_len : Usize) (value : T) : Result (alloc.vec.Vec T) := do
   if new_len.val < v.length then
     ok ⟨ v.val.resize new_len.toNat value, by scalar_tac ⟩
@@ -249,7 +235,7 @@ def alloc.vec.Vec.resize (T : Type) (cloneInst : core.clone.Clone T)
 theorem alloc.vec.Vec.resize_spec {T} (cloneInst : core.clone.Clone T)
   (v : alloc.vec.Vec T) (new_len : Usize) (value : T)
   (hClone : cloneInst.clone value = ok value) :
-  ∃ nv, alloc.vec.Vec.resize T cloneInst v new_len value = ok nv ∧
+  ∃ nv, alloc.vec.Vec.resize cloneInst v new_len value = ok nv ∧
     nv.val = v.val.resize new_len.toNat value := by
   rw [resize]
   split

compiler/AssociatedTypes.ml

@@ -82,10 +82,11 @@ let compute_norm_trait_types_from_preds (span : Meta.span option)
   in
   TraitTypeRefMap.of_list rbindings
 
-let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
-    (trait_type_constraints : trait_type_constraint list) : eval_ctx =
+let ctx_add_norm_trait_types_from_preds (span : Meta.span option)
+    (ctx : eval_ctx) (trait_type_constraints : trait_type_constraint list) :
+    eval_ctx =
   let norm_trait_types =
-    compute_norm_trait_types_from_preds (Some span) trait_type_constraints
+    compute_norm_trait_types_from_preds span trait_type_constraints
   in
   { ctx with norm_trait_types }
 
@@ -417,9 +418,9 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
   let ty = norm_ctx_normalize_ty ctx ty in
   { trait_ref; type_name; ty }
 
-let mk_norm_ctx (span : Meta.span) (ctx : eval_ctx) : norm_ctx =
+let mk_norm_ctx (span : Meta.span option) (ctx : eval_ctx) : norm_ctx =
   {
-    span = Some span;
+    span;
     norm_trait_types = ctx.norm_trait_types;
     type_decls = ctx.type_ctx.type_decls;
     fun_decls = ctx.fun_ctx.fun_decls;
@@ -430,17 +431,17 @@ let mk_norm_ctx (span : Meta.span) (ctx : eval_ctx) : norm_ctx =
     const_generic_vars = ctx.const_generic_vars;
   }
 
-let ctx_normalize_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
+let ctx_normalize_ty (span : Meta.span option) (ctx : eval_ctx) (ty : ty) : ty =
   norm_ctx_normalize_ty (mk_norm_ctx span ctx) ty
 
 (** Normalize a type and erase the regions at the same time *)
 let ctx_normalize_erase_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
-  let ty = ctx_normalize_ty span ctx ty in
+  let ty = ctx_normalize_ty (Some span) ctx ty in
   Subst.erase_regions ty
 
 let ctx_normalize_trait_type_constraint (span : Meta.span) (ctx : eval_ctx)
     (ttc : trait_type_constraint) : trait_type_constraint =
-  norm_ctx_normalize_trait_type_constraint (mk_norm_ctx span ctx) ttc
+  norm_ctx_normalize_trait_type_constraint (mk_norm_ctx (Some span) ctx) ttc
 
 (** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *)
 let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
@@ -451,7 +452,7 @@ let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
   in
   List.map
     (fun (variant_id, types) ->
-      (variant_id, List.map (ctx_normalize_ty span ctx) types))
+      (variant_id, List.map (ctx_normalize_ty (Some span) ctx) types))
     res
 
 (** Same as [type_decl_get_instantiated_field_types] but normalizes the types *)
@@ -461,15 +462,15 @@ let type_decl_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
   let types =
     Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
   in
-  List.map (ctx_normalize_ty span ctx) types
+  List.map (ctx_normalize_ty (Some span) ctx) types
 
 (** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *)
 let ctx_adt_value_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
     (adt : adt_value) (id : type_id) (generics : generic_args) : ty list =
   let types =
     Subst.ctx_adt_value_get_instantiated_field_types span ctx adt id generics
   in
-  List.map (ctx_normalize_ty span ctx) types
+  List.map (ctx_normalize_ty (Some span) ctx) types
 
 (** Same as [ctx_adt_value_get_instantiated_field_types] but normalizes the types
     and erases the regions. *)
@@ -479,7 +480,7 @@ let type_decl_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
   let types =
     Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
   in
-  let types = List.map (ctx_normalize_ty span ctx) types in
+  let types = List.map (ctx_normalize_ty (Some span) ctx) types in
   List.map Subst.erase_regions types
 
 (** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and
@@ -491,7 +492,7 @@ let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
     Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
       generics
   in
-  let types = List.map (ctx_normalize_ty span ctx) types in
+  let types = List.map (ctx_normalize_ty (Some span) ctx) types in
   List.map Subst.erase_regions types
 
 (** Same as [substitute_signature] but normalizes the types *)
@@ -507,8 +508,8 @@ let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
       sg regions_hierarchy
   in
   let { regions_hierarchy; inputs; output; trait_type_constraints } = sg in
-  let inputs = List.map (ctx_normalize_ty span ctx) inputs in
-  let output = ctx_normalize_ty span ctx output in
+  let inputs = List.map (ctx_normalize_ty (Some span) ctx) inputs in
+  let output = ctx_normalize_ty (Some span) ctx output in
   let trait_type_constraints =
     List.map
       (ctx_normalize_trait_type_constraint span ctx)