Revert "fix(proofs-lib/fstar): make type implicits on typeclasses"

This reverts commit 253fb96.

Author: Lucas Franceschino

proof-libs/fstar/core/Alloc.Vec.fst

@@ -30,8 +30,8 @@ let from_elem #a (item: a) (len: usize) = Seq.create (v len) item
 
 open Rust_primitives.Hax
 open Core.Ops.Index
-instance update_at_tc_array t n: update_at_tc #(t_Vec t ()) #(int_t n) = {
-  super_index = FStar.Tactics.Typeclasses.solve <: t_Index #(t_Vec t ()) #(int_t n);
+instance update_at_tc_array t n: update_at_tc (t_Vec t ()) (int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Vec t ()) (int_t n);
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 

proof-libs/fstar/core/Core.Clone.fst

@@ -1,11 +1,11 @@
 module Core.Clone
 
-class t_Clone #self = {
+class t_Clone self = {
   f_clone: x:self -> r:self {x == r}
 }
 
 (** Everything is clonable *)
-instance clone_all (t: Type): t_Clone #t = {
+instance clone_all (t: Type): t_Clone t = {
   f_clone = (fun x -> x);
 }
 

proof-libs/fstar/core/Core.Cmp.fsti

@@ -1,11 +1,11 @@
 module Core.Cmp
 open Rust_primitives
 
-class min_tc #t = {
+class min_tc t = {
   min: t -> t -> t
 }
 
-instance min_inttype (#t:inttype): min_tc #(int_t t) = {
+instance min_inttype (#t:inttype): min_tc (int_t t) = {
   min = fun a b -> if a <. b then a else b
 }
 
@@ -14,26 +14,26 @@ type t_Ordering =
   | Ordering_Equal : t_Ordering
   | Ordering_Greater : t_Ordering
 
-class t_Ord (#v_Self: Type) = {
+class t_Ord (v_Self: Type) = {
   f_cmp:v_Self -> v_Self -> t_Ordering;
   // f_max:v_Self -> v_Self -> v_Self;
   // f_min:v_Self -> v_Self -> v_Self;
   // f_clamp:v_Self -> v_Self -> v_Self -> v_Self
 }
 
-class t_PartialEq (#v_Self: Type) (#v_Rhs: Type) = {
+class t_PartialEq (v_Self: Type) (v_Rhs: Type) = {
   // __constraint_1069563329_t_PartialEq:t_PartialEq v_Self v_Rhs;
   f_eq:v_Self -> v_Rhs -> bool;
   f_ne:v_Self -> v_Rhs -> bool
 }
 
-instance all_eq (a: eqtype): t_PartialEq #a #a = {
+instance all_eq (a: eqtype): t_PartialEq a a = {
   f_eq = (fun x y -> x = y);
   f_ne = (fun x y -> x <> y);
 }
 
-class t_PartialOrd (#v_Self: Type) (#v_Rhs: Type) = {
-  __constraint_Rhs_t_PartialEq:t_PartialEq #v_Self #v_Rhs;
+class t_PartialOrd (v_Self: Type) (v_Rhs: Type) = {
+  __constraint_Rhs_t_PartialEq:t_PartialEq v_Self v_Rhs;
   // __constraint_Rhs_t_PartialOrd:t_PartialOrd v_Self v_Rhs;
   f_partial_cmp:v_Self -> v_Rhs -> Core.Option.t_Option t_Ordering;
   // f_lt:v_Self -> v_Rhs -> bool;
@@ -47,7 +47,7 @@ type t_Reverse t = | Reverse of t
 let impl__then x y = x
 
 [@FStar.Tactics.Typeclasses.tcinstance]
-val ord_u64: t_Ord #u64
+val ord_u64: t_Ord u64
 
 [@FStar.Tactics.Typeclasses.tcinstance]
-val ord_reverse t {| t_Ord #t |}: t_Ord #(t_Reverse t)
+val ord_reverse t {| t_Ord t |}: t_Ord (t_Reverse t)

proof-libs/fstar/core/Core.Convert.fst

@@ -2,13 +2,13 @@
 module Core.Convert
 open Rust_primitives
 
-class try_into_tc #self #t = {
+class try_into_tc self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
   f_try_into: self -> Core.Result.t_Result t f_Error
 }
 
-instance impl_6 (t: Type0) (len: usize): try_into_tc #(t_Slice t) #(t_Array t len) = {
+instance impl_6 (t: Type0) (len: usize): try_into_tc (t_Slice t) (t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t) -> 
     if Core.Slice.impl__len s = len
@@ -18,26 +18,26 @@ instance impl_6 (t: Type0) (len: usize): try_into_tc #(t_Slice t) #(t_Array t le
 }
 
 
-instance impl_6_refined (t: Type0) (len: usize): try_into_tc #(s: t_Slice t {Core.Slice.impl__len s == len}) #(t_Array t len) = {
+instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core.Slice.impl__len s == len}) (t_Array t len) = {
   f_Error = Core.Array.t_TryFromSliceError;
   f_try_into = (fun (s: t_Slice t {Core.Slice.impl__len s == len}) -> 
     Core.Result.Result_Ok (s <: t_Array t len)
   )
 }
 
-class t_Into #self #t = {
+class t_Into self t = {
   f_into_pre: self -> bool;
   f_into_post: self -> t -> bool;
   f_into: self -> t;
 }
 
-class t_From #self #t = {
+class t_From self t = {
   f_from_pre: t -> bool;
   f_from_post: t -> self -> bool;
   f_from: t -> self;
 }
 
-class t_TryFrom #self #t = {
+class t_TryFrom self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
   f_try_from_pre: t -> bool;
@@ -47,26 +47,26 @@ class t_TryFrom #self #t = {
 
 instance integer_into
   (t:inttype) (t':inttype { minint t >= minint t' /\ maxint t <= maxint t' })
-  : t_From #(int_t t') #(int_t t)
+  : t_From (int_t t') (int_t t)
   = {
       f_from_pre = (fun _ -> true);
       f_from_post = (fun _ _ -> true);
       f_from = (fun (x: int_t t) -> Rust_primitives.Integers.cast #t #t' x);
     }
 
-instance into_from_from a b {| t_From #a #b |}: t_Into #b #a = {
+instance into_from_from a b {| t_From a b |}: t_Into b a = {
   f_into_pre = (fun _ -> true);
   f_into_post = (fun _ _ -> true);
   f_into = (fun x -> f_from x)
 }
 
-instance from_id a: t_From #a #a = {
+instance from_id a: t_From a a = {
   f_from_pre = (fun _ -> true);
   f_from_post = (fun _ _ -> true);
   f_from = (fun x -> x)
 }
 
-class t_AsRef #self #t = {
+class t_AsRef self t = {
   f_as_ref_pre: self -> bool;
   f_as_ref_post: self -> t -> bool;
   f_as_ref: self -> t;

proof-libs/fstar/core/Core.Default.fsti

@@ -1,5 +1,5 @@
 module Core.Default
 
-class t_Default (#t: Type0) = {
+class t_Default (t: Type0) = {
   v_default: unit -> t;
 }

proof-libs/fstar/core/Core.Fmt.fsti

@@ -6,7 +6,7 @@ val t_Error: Type0
 type t_Result = Core.Result.t_Result unit t_Error
 
 val t_Formatter: Type0
-class t_Display #t_Self = {
+class t_Display t_Self = {
   f_fmt_pre: t_Self -> Core.Fmt.t_Formatter -> bool;
   f_fmt_post: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) -> bool;
   f_fmt: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error)

proof-libs/fstar/core/Core.Iter.Traits.Collect.fst

@@ -1,14 +1,14 @@
 module Core.Iter.Traits.Collect
 
-class into_iterator #self = {
+class into_iterator self = {
   f_IntoIter: Type0;
   // f_Item: Type0;
   f_into_iter: self -> f_IntoIter;
 }
 
-let t_IntoIterator #self = into_iterator #self
+let t_IntoIterator = into_iterator
 
-unfold instance impl t {| Core.Iter.Traits.Iterator.iterator #t |}: into_iterator #t = {
+unfold instance impl t {| Core.Iter.Traits.Iterator.iterator t |}: into_iterator t = {
   f_IntoIter = t;
   f_into_iter = id;
 }

proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst

@@ -28,7 +28,7 @@ unfold type t_all self item
 //   f_enumerate: t_enumerate self;
 // }
 
-class iterator (#self: Type u#0): Type u#1 = {
+class iterator (self: Type u#0): Type u#1 = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Item: Type0;
   f_next:      self -> self * option f_Item;

proof-libs/fstar/core/Core.Iter.fsti

@@ -9,18 +9,18 @@ open Core.Iter.Traits.Iterator
 (**** Enumerate *)
 (** This lives in this file for cyclic dependencies reasons. *)
 
-val iterator_enumerate_contains it (i: iterator #it)
+val iterator_enumerate_contains it (i: iterator it)
   : t_contains (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item)
-val iterator_enumerate_fold it (i: iterator #it)
+val iterator_enumerate_fold it (i: iterator it)
   : t_fold (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item) (iterator_enumerate_contains it i)
 val iterator_enumerate_enumerate it
   : t_enumerate (Core.Iter.Adapters.Enumerate.t_Enumerate it)
-val iterator_enumerate_all it (i: iterator #it)
+val iterator_enumerate_all it (i: iterator it)
   : t_all (Core.Iter.Adapters.Enumerate.t_Enumerate it) (usize * i.f_Item)
 val iterator_enumerate_step_by it
   : t_step_by (Core.Iter.Adapters.Enumerate.t_Enumerate it)
 
-instance iterator_enumerate it {| i: iterator #it |}: iterator #(Core.Iter.Adapters.Enumerate.t_Enumerate it) = 
+instance iterator_enumerate it {| i: iterator it |}: iterator (Core.Iter.Adapters.Enumerate.t_Enumerate it) = 
   let open Core.Iter.Adapters.Enumerate in
   {
     f_Item = (usize * i.f_Item);
@@ -43,20 +43,20 @@ instance iterator_enumerate it {| i: iterator #it |}: iterator #(Core.Iter.Adapt
 (**** Step_by *)
 (** This lives in this file for cyclic dependencies reasons. *)
 
-val iterator_step_by_contains it (i: iterator #it)
+val iterator_step_by_contains it (i: iterator it)
   : t_contains (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
-val iterator_step_by_fold it (i: iterator #it)
+val iterator_step_by_fold it (i: iterator it)
   : t_fold (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item (iterator_step_by_contains it i)
-val iterator_step_by_next it (i: iterator #it)
+val iterator_step_by_next it (i: iterator it)
   : t_next (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
 val iterator_step_by_enumerate it
   : t_enumerate (Core.Iter.Adapters.Step_by.t_StepBy it)
-val iterator_step_by_all it (i: iterator #it)
+val iterator_step_by_all it (i: iterator it)
   : t_all (Core.Iter.Adapters.Step_by.t_StepBy it) i.f_Item
 val iterator_step_by_step_by it
   : t_step_by (Core.Iter.Adapters.Step_by.t_StepBy it)
 
-unfold instance iterator_step_by it {| i: iterator #it |}: iterator #(Core.Iter.Adapters.Step_by.t_StepBy it) = 
+unfold instance iterator_step_by it {| i: iterator it |}: iterator (Core.Iter.Adapters.Step_by.t_StepBy it) = 
   let open Core.Iter.Adapters.Enumerate in
   {
     f_Item = i.f_Item;
@@ -81,7 +81,7 @@ val iterator_slice_enumerate (t: eqtype): t_enumerate (t_Slice t)
 val iterator_slice_step_by (t: eqtype): t_step_by (t_Slice t)
 val iterator_slice_all (t: eqtype): t_all (t_Slice t) t
 
-instance iterator_slice (t: eqtype): iterator #(t_Slice t) = {
+instance iterator_slice (t: eqtype): iterator (t_Slice t) = {
   f_Item = t;
   f_next = iterator_slice_next t;
   // size_hint = (fun s -> Some (Rust_primitives.Arrays.length s));
@@ -103,7 +103,7 @@ val iterator_array_enumerate (t: eqtype) len: t_enumerate (t_Array t len)
 val iterator_array_step_by (t: eqtype) len: t_step_by (t_Array t len)
 val iterator_array_all (t: eqtype) len: t_all (t_Array t len) t
 
-instance iterator_array (t: eqtype) len: iterator #(t_Array t len) = {
+instance iterator_array (t: eqtype) len: iterator (t_Array t len) = {
   f_Item = t;
   f_next = iterator_array_next t len;
   // size_hint = (fun (_s: t_Array t len) -> Some len);

proof-libs/fstar/core/Core.Marker.fst

@@ -1,19 +1,19 @@
 module Core.Marker
 
-class t_Sized (#h: Type) = {
+class t_Sized (h: Type) = {
   dummy_field: unit
 }
 
 (** we consider everything to be sized *)
-instance t_Sized_all t: t_Sized #t = {
+instance t_Sized_all t: t_Sized t = {
   dummy_field = ()
 }
 
-class t_Copy (#h: Type) = {
+class t_Copy (h: Type) = {
   dummy_copy_field: unit
 }
 
 (** we consider everything to be copyable *)
-instance t_Copy_all t: t_Copy #t = {
+instance t_Copy_all t: t_Copy t = {
   dummy_copy_field = ()
 }

proof-libs/fstar/core/Core.Num.fsti

@@ -47,50 +47,50 @@ val impl__usize__leading_zeros: usize -> u32
 
 open Core.Ops.Arith
 unfold instance add_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
-  : t_AddAssign #(x: int_t t {phi1 x}) #(y: int_t t {phi2 y}) = {
+  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
     f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x +. y));
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num_lhs_refined t ($phi1: int_t t -> bool)
-  : t_AddAssign #(x: int_t t {phi1 x}) #(y: int_t t) = {
+  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t) = {
     f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x +. y));
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num_rhs_refined t ($phi1: int_t t -> bool)
-  : t_AddAssign #(x: int_t t) #(y: int_t t {phi1 y}) = {
+  : t_AddAssign (x: int_t t) (y: int_t t {phi1 y}) = {
     f_add_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 unfold instance add_assign_num t
-  : t_AddAssign #(x: int_t t) #(y: int_t t) = {
+  : t_AddAssign (x: int_t t) (y: int_t t) = {
     f_add_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
     f_add_assign_post = (fun x y r -> x +. y = r);
     f_add_assign = (fun x y -> x +. y);
   }
 
 unfold instance sub_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
-  : t_SubAssign #(x: int_t t {phi1 x}) #(y: int_t t {phi2 y}) = {
+  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
     f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x -. y));
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num_lhs_refined t ($phi1: int_t t -> bool)
-  : t_SubAssign #(x: int_t t {phi1 x}) #(y: int_t t) = {
+  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t) = {
     f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x -. y));
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num_rhs_refined t ($phi1: int_t t -> bool)
-  : t_SubAssign #(x: int_t t) #(y: int_t t {phi1 y}) = {
+  : t_SubAssign (x: int_t t) (y: int_t t {phi1 y}) = {
     f_sub_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);
   }
 unfold instance sub_assign_num t
-  : t_SubAssign #(x: int_t t) #(y: int_t t) = {
+  : t_SubAssign (x: int_t t) (y: int_t t) = {
     f_sub_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
     f_sub_assign_post = (fun x y r -> x -. y = r);
     f_sub_assign = (fun x y -> x -. y);