Merge branch 'main' into handle-cyclic-module-dependencies

hacspec · Oct 2, 2024 · d20b769 · d20b769
2 parents f1d09dc + bfcd974
commit d20b769
Show file tree

Hide file tree

Showing 18 changed files with 180 additions and 74 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -362,10 +362,8 @@ struct
 
   let pgeneric_param_as_argument span : generic_param -> C.AST.argument =
     function
-    | { ident; kind = GPType { default }; _ } ->
-        C.AST.Explicit
-          ( C.AST.Ident ident.name,
-            match default with Some t -> pty span t | None -> C.AST.WildTy )
+    | { ident; kind = GPType; _ } ->
+        C.AST.Explicit (C.AST.Ident ident.name, C.AST.WildTy)
     | _ -> Error.unimplemented ~details:"Coq: TODO: generic_params" span
 
   let rec pitem (e : item) : C.AST.decl list =

diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -1322,11 +1322,10 @@ struct
         SSP.AST.Implicit
           ( SSP.AST.Ident (plocal_ident ident),
             match kind with
-            | GPType { default = Some t } -> pty span t
             | GPConst { typ = t } ->
                 SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])"
                   (pty span t)
-            | GPType { default = None } -> SSP.AST.WildTy
+            | GPType -> SSP.AST.WildTy
             | _ -> . )
 
   let pgeneric_constraints_as_argument span :

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -13,6 +13,7 @@ include
       include On.Construct_base
       include On.Quote
       include On.Dyn
+      include On.Unsafe
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -42,8 +43,7 @@ module SubtypeToInputLanguage
              and type for_index_loop = Features.Off.for_index_loop
              and type state_passing_loop = Features.Off.state_passing_loop
              and type match_guard = Features.Off.match_guard
-             and type trait_item_default = Features.Off.trait_item_default
-             and type unsafe = Features.Off.unsafe) =
+             and type trait_item_default = Features.Off.trait_item_default) =
 struct
   module FB = InputLanguage
 
@@ -59,6 +59,7 @@ struct
         include Features.SUBTYPE.On.Macro
         include Features.SUBTYPE.On.Quote
         include Features.SUBTYPE.On.Dyn
+        include Features.SUBTYPE.On.Unsafe
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -680,7 +681,7 @@ struct
       let ident = plocal_ident p.ident in
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
-      | GPType { default = _ } -> { kind = Implicit; typ = F.type0_term; ident }
+      | GPType -> { kind = Implicit; typ = F.type0_term; ident }
       | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =
@@ -1718,8 +1719,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 
 module TransformToInputLanguage =
   [%functor_application
-  Phases.Reject.Unsafe(Features.Rust)
-  |> Phases.Reject.RawOrMutPointer
+    Phases.Reject.RawOrMutPointer(Features.Rust)
   |> Phases.Transform_hax_lib_inline
   |> Phases.Specialize
   |> Phases.Drop_sized_trait

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -365,7 +365,7 @@ functor
 
     and generic_param_kind =
       | GPLifetime of { witness : F.lifetime }
-      | GPType of { default : ty option }
+      | GPType
       | GPConst of { typ : ty }
 
     and generic_constraint =