From 0ddc7c1c9970ebefe5e5df84f14461d55840fc82 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 3 Oct 2024 10:10:07 -0700 Subject: [PATCH] snap --- .../generated/FStar_Algebra_Monoid.ml | 4 +- .../generated/FStar_Monotonic_Seq.ml | 14 +++---- .../generated/FStar_WellFoundedRelation.ml | 7 +--- ocaml/fstar-lib/generated/LowStar_Buffer.ml | 42 ++++--------------- .../LowStar_PrefixFreezableBuffer.ml | 5 +-- .../generated/LowStar_UninitializedBuffer.ml | 16 ++----- 6 files changed, 24 insertions(+), 64 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml index 133c0713185..e2efd9060f6 100644 --- a/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml +++ b/ocaml/fstar-lib/generated/FStar_Algebra_Monoid.ml @@ -60,10 +60,10 @@ let (embed_nat_int : Prims.nat -> Prims.int) = fun n -> n let (uu___0 : (Prims.nat, Prims.int, unit, unit, unit) monoid_morphism) = intro_monoid_morphism embed_nat_int nat_plus_monoid int_plus_monoid type 'p neg = unit -let (uu___1 : (unit, unit, unit neg, unit, unit) monoid_morphism) = +let (uu___1 : (unit, unit, unit, unit, unit) monoid_morphism) = intro_monoid_morphism (fun uu___ -> ()) conjunction_monoid disjunction_monoid -let (uu___2 : (unit, unit, unit neg, unit, unit) monoid_morphism) = +let (uu___2 : (unit, unit, unit, unit, unit) monoid_morphism) = intro_monoid_morphism (fun uu___ -> ()) disjunction_monoid conjunction_monoid type ('m, 'a, 'mult, 'act) mult_act_lemma = unit diff --git a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml index 1f8425ded08..5ee00f0e445 100644 --- a/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml +++ b/ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml @@ -9,15 +9,14 @@ let alloc_mref_seq : 'a . unit -> 'a FStar_Seq_Base.seq -> - (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows) - FStar_HyperStack_ST.m_rref + (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref = fun r -> fun init -> FStar_HyperStack_ST.ralloc () init type ('a, 'i, 'n, 'x, 'r, 'h) at_least = unit let write_at_end : 'a . unit -> - (unit, 'a FStar_Seq_Base.seq, ('a, unit, unit) grows) - FStar_HyperStack_ST.m_rref -> 'a -> unit + (unit, 'a FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref -> + 'a -> unit = fun i -> fun r -> @@ -52,16 +51,15 @@ let i_write_at_end : 'a 'p . unit -> (unit, 'a, 'p) i_seq -> 'a -> unit = type 's invariant = unit let (test0 : unit -> - (unit, Prims.nat FStar_Seq_Base.seq, (Prims.nat, unit, unit) grows) - FStar_HyperStack_ST.m_rref -> Prims.nat -> unit) + (unit, Prims.nat FStar_Seq_Base.seq, unit) FStar_HyperStack_ST.m_rref -> + Prims.nat -> unit) = fun r -> fun a -> fun k -> let h0 = FStar_HyperStack_ST.get () in FStar_HyperStack_ST.mr_witness () () () (Obj.magic a) () -let (itest : - unit -> (unit, Prims.nat, unit invariant) i_seq -> Prims.nat -> unit) = +let (itest : unit -> (unit, Prims.nat, unit) i_seq -> Prims.nat -> unit) = fun r -> fun a -> fun k -> diff --git a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml index 4aa36833970..43fc68866d2 100644 --- a/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml +++ b/ocaml/fstar-lib/generated/FStar_WellFoundedRelation.ml @@ -37,8 +37,7 @@ let default_wfr : 'a . unit -> 'a wfr_t = proof = () } type ('a, 'x1, 'x2) empty_relation = unit -let rec empty_decreaser : - 'a . 'a -> ('a, ('a, unit, unit) empty_relation, unit) acc_classical = +let rec empty_decreaser : 'a . 'a -> ('a, unit, unit) acc_classical = fun x -> let smaller y = empty_decreaser y in AccClassicalIntro smaller let empty_wfr : 'a . unit -> 'a wfr_t = fun uu___ -> @@ -48,9 +47,7 @@ let empty_wfr : 'a . unit -> 'a wfr_t = proof = () } type ('a, 'r, 'x1, 'x2) acc_relation = unit -let rec acc_decreaser : - 'a 'r . - unit -> 'a -> ('a, ('a, 'r, unit, unit) acc_relation, unit) acc_classical +let rec acc_decreaser : 'a 'r . unit -> 'a -> ('a, unit, unit) acc_classical = fun f -> fun x -> let smaller y = acc_decreaser () y in AccClassicalIntro smaller diff --git a/ocaml/fstar-lib/generated/LowStar_Buffer.ml b/ocaml/fstar-lib/generated/LowStar_Buffer.ml index 9059a9cc0cc..73d55a5a93f 100644 --- a/ocaml/fstar-lib/generated/LowStar_Buffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_Buffer.ml @@ -8,25 +8,15 @@ type 'a pointer_or_null = 'a buffer let sub : 'a . unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer - -> + ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> - unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + unit -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.msub let offset : 'a . unit -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer - -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.moffset type ('a, 'len) lbuffer = ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer let gcmalloc : @@ -34,45 +24,31 @@ let gcmalloc : unit -> unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc let malloc : 'a . unit -> unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mmalloc let alloca : 'a . unit -> 'a -> - FStar_UInt32.t -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + FStar_UInt32.t -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.malloca let alloca_of_list : 'a . unit -> - 'a Prims.list -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) LowStar_Monotonic_Buffer.mbuffer + 'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.malloca_of_list let gcmalloc_of_list : 'a . unit -> unit -> - 'a Prims.list -> - ('a, ('a, unit, unit) trivial_preorder, - ('a, unit, unit) trivial_preorder) - LowStar_Monotonic_Buffer.mbuffer + 'a Prims.list -> ('a, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.mgcmalloc_of_list type ('a, 'l) assign_list_t = 'a buffer -> unit let rec assign_list : 'a . 'a Prims.list -> 'a buffer -> unit = diff --git a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml index c0a81fdda4e..648a3cef0f8 100644 --- a/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_PrefixFreezableBuffer.ml @@ -14,10 +14,7 @@ type 'len lbuffer = buffer type ('r, 'len) malloc_pre = unit type ('h0, 'b, 'h1) alloc_post_mem_common = unit let (update_frozen_until_alloc : - (u8, (unit, unit) prefix_freezable_preorder, - (unit, unit) prefix_freezable_preorder) LowStar_Monotonic_Buffer.mbuffer - -> unit) - = + (u8, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> unit) = fun b -> LowStar_Endianness.store32_le_i b Stdint.Uint32.zero (Stdint.Uint32.of_int (4)); diff --git a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml index 24e8950e216..9a417b88559 100644 --- a/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml +++ b/ocaml/fstar-lib/generated/LowStar_UninitializedBuffer.ml @@ -10,28 +10,20 @@ type 'a pointer_or_null = 'a ubuffer let usub : 'a . unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.msub let uoffset : 'a . unit -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer -> FStar_UInt32.t -> - ('a FStar_Pervasives_Native.option, - ('a, unit, unit) initialization_preorder, - ('a, unit, unit) initialization_preorder) + ('a FStar_Pervasives_Native.option, unit, unit) LowStar_Monotonic_Buffer.mbuffer = fun uu___ -> LowStar_Monotonic_Buffer.moffset type ('a, 'i, 's) ipred = unit