Merge pull request #4175 from FStarLang/gebner_rm_dup_dyn

gebner · web-flow · commit 0cb31e9d4085 · 2026-04-07T15:55:52.000-07:00
Replace FStarC.Dyn with FStar.Dyn
diff --git a/mk/plugins.mk b/mk/plugins.mk
@@ -13,6 +13,7 @@ EXTRACT += --extract -FStar.Ghost
 EXTRACT += --extract -FStar.Heap
 EXTRACT += --extract -FStar.Bytes
 EXTRACT += --extract -FStar.Char
+EXTRACT += --extract -FStar.Dyn
 EXTRACT += --extract -FStar.Exn
 EXTRACT += --extract -FStar.Float
 EXTRACT += --extract -FStar.Int16
diff --git a/pulse/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst b/pulse/src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst
@@ -180,7 +180,7 @@ let parse_extension_lang (contents:string) (r:FStarC.Range.range)
           Qualifier Irreducible::quals@attrs
         in
         let d =
-          let open FStarC.Dyn in
+          let open FStar.Dyn in
           DeclToBeDesugared {
             lang_name="pulse";
             blob=mkdyn d;
@@ -226,11 +226,11 @@ let desugar_pulse (env:TcEnv.env)
 module S = FStarC.Syntax.Syntax
 let desugar_pulse_decl_callback
       (env:DsEnv.env)
-      (blob:FStarC.Dyn.dyn)
+      (blob:FStar.Dyn.dyn)
       (lids:list lident)
       (rng:R.range)
 : ML (list FStarC.Syntax.Syntax.sigelt')
-= let d = D.desugar_decl (D.mk_env env) (FStarC.Dyn.undyn blob) 0 in
+= let d = D.desugar_decl (D.mk_env env) (FStar.Dyn.undyn blob) 0 in
   match fst d with
   | Inr None ->
     //All errors were logged via the error API, just stop.
diff --git a/src/basic/FStarC.Dyn.fsti b/src/basic/FStarC.Dyn.fsti
diff --git a/src/extraction/FStarC.Extraction.Krml.fst b/src/extraction/FStarC.Extraction.Krml.fst
@@ -814,7 +814,7 @@ and translate_expr' env e: ML expr =
   // We recognize certain distinguished names from [FStar.HST] and other
   // modules, and translate them into built-in Karamel constructs
   | MLE_App({expr=MLE_TApp ({ expr = MLE_Name p }, [t])}, [arg])
-    when string_of_mlpath p = "FStarC.Dyn.undyn" ->
+    when string_of_mlpath p = "FStar.Dyn.undyn" ->
       ECast (translate_expr env arg, translate_type env t)
   | MLE_App({expr=MLE_TApp ({ expr = MLE_Name p }, _)}, _)
     when string_of_mlpath p = "Prims.admit" ->
diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fsti b/src/extraction/FStarC.Extraction.ML.Modul.fsti
@@ -23,9 +23,9 @@ open FStarC.Extraction.ML.UEnv
 val iface : Type0
 
 type extension_sigelt_extractor =
-  uenv -> sigelt -> FStarC.Dyn.dyn -> ML (either (list mlmodule1) string)
+  uenv -> sigelt -> FStar.Dyn.dyn -> ML (either (list mlmodule1) string)
 type extension_sigelt_iface_extractor =
-  uenv -> sigelt -> FStarC.Dyn.dyn -> ML (either (uenv & iface) string)
+  uenv -> sigelt -> FStar.Dyn.dyn -> ML (either (uenv & iface) string)
 
 type extension_extractor = {
    extract_sigelt : extension_sigelt_extractor;
diff --git a/src/parser/FStarC.Parser.AST.fsti b/src/parser/FStarC.Parser.AST.fsti
@@ -244,11 +244,11 @@ type dep_scan_callbacks = {
 
 type to_be_desugared = {
   lang_name: string;
-  blob: FStarC.Dyn.dyn;
+  blob: FStar.Dyn.dyn;
   idents: list ident;
-  to_string: FStarC.Dyn.dyn -> ML string;
-  eq: FStarC.Dyn.dyn -> FStarC.Dyn.dyn -> ML bool;
-  dep_scan: dep_scan_callbacks -> FStarC.Dyn.dyn -> ML unit
+  to_string: FStar.Dyn.dyn -> ML string;
+  eq: FStar.Dyn.dyn -> FStar.Dyn.dyn -> ML bool;
+  dep_scan: dep_scan_callbacks -> FStar.Dyn.dyn -> ML unit
 }
 
 type decl' =
diff --git a/src/reflection/FStarC.Reflection.V2.Builtins.fst b/src/reflection/FStarC.Reflection.V2.Builtins.fst
@@ -44,7 +44,7 @@ module EMB   = FStarC.Syntax.Embeddings
 module N     = FStarC.TypeChecker.Normalize
 open FStarC.VConfig
 
-open FStarC.Dyn
+open FStar.Dyn
 
 (* This file provides implementation for reflection primitives in F*.
  *
diff --git a/src/reflection/FStarC.Reflection.V2.Embeddings.fst b/src/reflection/FStarC.Reflection.V2.Embeddings.fst
@@ -34,7 +34,7 @@ module SS      = FStarC.Syntax.Subst
 module U       = FStarC.Syntax.Util
 
 open FStarC.Reflection.V2.Builtins //needed for inspect_fv, but that feels wrong
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.Syntax.Embeddings.AppEmb
 open FStarC.Class.Monad
 
diff --git a/src/reflection/FStarC.Reflection.V2.NBEEmbeddings.fst b/src/reflection/FStarC.Reflection.V2.NBEEmbeddings.fst
@@ -22,7 +22,7 @@ open FStarC.Syntax.Syntax
 open FStarC.TypeChecker.NBETerm
 open FStarC.Order
 open FStarC.Errors
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.Reflection.V2.Constants
 
 module Env     = FStarC.TypeChecker.Env
@@ -59,7 +59,7 @@ let mk_emb' x y fv = mk_emb x y (fun () -> mkFV fv [] []) (fun () -> fv_as_emb_t
 
 let mk_lazy cb obj ty kind : ML t =
     let li = {
-          blob = FStarC.Dyn.mkdyn obj
+          blob = FStar.Dyn.mkdyn obj
         ; lkind = kind
         ; ltyp = ty
         ; rng = Range.dummyRange
@@ -75,7 +75,7 @@ let e_bv =
     let unembed_bv cb (t:t) : ML (option bv) =
         match t.nbe_t with
         | Lazy (Inl {blob=b; lkind=Lazy_bv}, _) ->
-            Some <| FStarC.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             Err.log_issue0 Err.Warning_NotEmbedded (Format.fmt1 "Not an embedded bv: %s" (t_to_string t));
             None
@@ -89,7 +89,7 @@ let e_namedv =
     let unembed_namedv cb (t:t) : ML (option namedv) =
         match t.nbe_t with
         | Lazy (Inl {blob=b; lkind=Lazy_namedv}, _) ->
-            Some <| FStarC.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             Err.log_issue0 Err.Warning_NotEmbedded (Format.fmt1 "Not an embedded namedv: %s" (t_to_string t));
             None
@@ -330,7 +330,7 @@ let unlazy_as_t k t : ML _ =
     match t.nbe_t with
     | Lazy (Inl {lkind=k'; blob=v}, _)
         when k =? k' ->
-      FStarC.Dyn.undyn v
+      FStar.Dyn.undyn v
     | _ ->
       failwith "Not a Lazy of the expected kind (NBE)"
 
diff --git a/src/syntax/FStarC.Syntax.Syntax.fst b/src/syntax/FStarC.Syntax.Syntax.fst
@@ -23,7 +23,7 @@ open FStarC
 open FStarC.Range
 open FStarC.Ident
 open FStarC.Const
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.VConfig
 
 open FStarC.Class.Ord
diff --git a/src/syntax/FStarC.Syntax.Syntax.fsti b/src/syntax/FStarC.Syntax.Syntax.fsti
@@ -21,7 +21,7 @@ open FStarC
 open FStarC.Effect
 open FStarC.Range.Type
 open FStarC.Ident
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.Const
 open FStarC.VConfig
 
diff --git a/src/syntax/FStarC.Syntax.Util.fst b/src/syntax/FStarC.Syntax.Util.fst
@@ -23,7 +23,7 @@ open FStarC.Range
 open FStarC.Syntax
 open FStarC.Syntax.Syntax
 open FStarC.Const
-open FStarC.Dyn
+open FStar.Dyn
 module U = FStarC.Util
 module List = FStarC.List
 module PC = FStarC.Parser.Const
diff --git a/src/syntax/FStarC.Syntax.Util.fsti b/src/syntax/FStarC.Syntax.Util.fsti
@@ -23,7 +23,7 @@ open FStarC.Range.Type
 open FStarC.Syntax
 open FStarC.Syntax.Syntax
 open FStarC.Const
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.Syntax.Subst
 
 open FStarC.Class.Show
diff --git a/src/tactics/FStarC.Tactics.Embedding.fst b/src/tactics/FStarC.Tactics.Embedding.fst
@@ -156,7 +156,7 @@ let fv_as_emb_typ fv = S.ET_app (show fv.fv_name, [])
 let e_ref_proofstate_nbe =
     let embed_ref_proofstate _cb (ps:ref_proofstate) : ML NBETerm.t =
         let li = { lkind = Lazy_ref_proofstate
-                 ; blob = FStarC.Dyn.mkdyn ps
+                 ; blob = FStar.Dyn.mkdyn ps
                  ; ltyp = fstar_tactics_ref_proofstate.t
                  ; rng = Range.dummyRange }
         in
@@ -166,7 +166,7 @@ let e_ref_proofstate_nbe =
     let unembed_ref_proofstate _cb (t:NBETerm.t) : ML (option ref_proofstate) =
         match NBETerm.nbe_t_of_t t with
         | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_ref_proofstate}, _) ->
-            Some <| FStarC.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
           if !Options.debug_embedding then
             Err.log_issue0
@@ -184,7 +184,7 @@ let e_ref_proofstate_nbe =
 let e_proofstate_nbe =
     let embed_proofstate _cb (ps:proofstate) : ML NBETerm.t =
         let li = { lkind = Lazy_proofstate
-                 ; blob = FStarC.Dyn.mkdyn ps
+                 ; blob = FStar.Dyn.mkdyn ps
                  ; ltyp = fstar_tactics_proofstate.t
                  ; rng = Range.dummyRange }
         in
@@ -194,7 +194,7 @@ let e_proofstate_nbe =
     let unembed_proofstate _cb (t:NBETerm.t) : ML (option proofstate) =
         match NBETerm.nbe_t_of_t t with
         | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_proofstate}, _) ->
-            Some <| FStarC.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
           if !Options.debug_embedding then
             Err.log_issue0
@@ -212,7 +212,7 @@ let e_proofstate_nbe =
 let e_goal_nbe =
     let embed_goal _cb (ps:goal) : ML NBETerm.t =
         let li = { lkind = Lazy_goal
-                 ; blob = FStarC.Dyn.mkdyn ps
+                 ; blob = FStar.Dyn.mkdyn ps
                  ; ltyp = fstar_tactics_goal.t
                  ; rng = Range.dummyRange }
         in
@@ -222,7 +222,7 @@ let e_goal_nbe =
     let unembed_goal _cb (t:NBETerm.t) : ML (option goal) =
         match NBETerm.nbe_t_of_t t with
         | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_goal}, _) ->
-            Some <| FStarC.Dyn.undyn b
+            Some <| FStar.Dyn.undyn b
         | _ ->
             if !Options.debug_embedding then
               Err.log_issue0 Err.Warning_NotEmbedded (Format.fmt1 "Not an embedded NBE goal: %s" (NBETerm.t_to_string t));
@@ -505,7 +505,7 @@ let e_tref #a =
 let e_tref_nbe #a =
   let embed_tref _cb (r:tref a) : ML NBETerm.t =
     let li = { lkind = Lazy_tref
-             ; blob = FStarC.Dyn.mkdyn r
+             ; blob = FStar.Dyn.mkdyn r
              ; ltyp = t_tref
              ; rng = Range.dummyRange }
     in
@@ -515,7 +515,7 @@ let e_tref_nbe #a =
   let unembed_tref _cb (t:NBETerm.t) : ML (option (tref a)) =
     match NBETerm.nbe_t_of_t t with
     | NBETerm.Lazy (Inl {blob=b; lkind = Lazy_tref}, _) ->
-      Some <| FStarC.Dyn.undyn b
+      Some <| FStar.Dyn.undyn b
     | _ ->
       if !Options.debug_embedding then
         Err.log_issue0
diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti
@@ -27,7 +27,7 @@ open FStarC.Ident
 
 module S = FStarC.Syntax.Syntax
 
-type extension_tosyntax_decl_t = env -> FStarC.Dyn.dyn -> lids:list lident -> Range.t -> ML (list sigelt')
+type extension_tosyntax_decl_t = env -> FStar.Dyn.dyn -> lids:list lident -> Range.t -> ML (list sigelt')
 val register_extension_tosyntax (lang_name:string) (cb:extension_tosyntax_decl_t) : ML unit
 
 (* Return a list of wildcard patterns (implicit or explicit as needed)
diff --git a/src/typechecker/FStarC.TypeChecker.NBETerm.fst b/src/typechecker/FStarC.TypeChecker.NBETerm.fst
@@ -301,7 +301,7 @@ let lazy_embed (et:unit -> ML emb_typ) (x:'a) (f:unit -> ML t) : ML t =
     if !Options.eager_embedding
     then f()
     else let thunk = Thunk.mk f in
-         let li = FStarC.Dyn.mkdyn x, et () in
+         let li = FStar.Dyn.mkdyn x, et () in
          mk_t <| Lazy (Inr li, thunk)
 
 let lazy_unembed (et:unit -> ML emb_typ) (x:t) (f:t -> ML (option 'a)) : ML (option 'a) =
@@ -319,7 +319,7 @@ let lazy_unembed (et:unit -> ML emb_typ) (x:t) (f:t -> ML (option 'a)) : ML (opt
                                 (show et')
            in
            res
-      else let a = FStarC.Dyn.undyn b in
+      else let a = FStar.Dyn.undyn b in
            let _ = if !Options.debug_embedding
                    then Format.print1 "Unembed cancelled for %s\n"
                                      (show (et ()))
@@ -336,7 +336,7 @@ let lazy_unembed_lazy_kind (#a:Type) (k:lazy_kind) (x:t) : ML (option a) =
   match x.nbe_t with
   | Lazy (Inl li, _) ->
     if li.lkind = k
-    then Some (FStarC.Dyn.undyn li.blob)
+    then Some (FStar.Dyn.undyn li.blob)
     else None
   | _ -> None
 
diff --git a/src/typechecker/FStarC.TypeChecker.Primops.Array.fst b/src/typechecker/FStarC.TypeChecker.Primops.Array.fst
@@ -105,7 +105,7 @@ let ops : list primitive_step =
                                                       [NBETerm.as_arg l]))))
          (fun  universes elt_t (l, lst) ->
             let blob = FStar.ImmutableArray.Base.of_list #NBETerm.t lst in
-            Some (universes, elt_t, (l, FStarC.Dyn.mkdyn blob)))
+            Some (universes, elt_t, (l, FStar.Dyn.mkdyn blob)))
          univs args
     in
     (  PC.immutable_array_of_list_lid, 2, 1,
@@ -130,19 +130,19 @@ let ops : list primitive_step =
           (fun r universes elt_t (l, lst) ->
             //The actual primitive step computing the IA.t blob
              let blob = FStar.ImmutableArray.Base.of_list #term lst in
-             Some (universes, elt_t, (l, FStarC.Dyn.mkdyn blob))),
+             Some (universes, elt_t, (l, FStar.Dyn.mkdyn blob))),
        nbe_of_list)
   in
   let arg1_as_elt_t (x:arg) : option term = Some (fst x) in
-  let arg2_as_blob (x:arg) : ML (option FStarC.Dyn.dyn) =
+  let arg2_as_blob (x:arg) : ML (option FStar.Dyn.dyn) =
       //try_unembed_simple an arg as a IA.t blob if the emb_typ
       //of the lkind tells us it has the right type
       match (SS.compress (fst x)).n with
       | Tm_lazy {blob=blob; lkind=Lazy_embedding (ET_app(head, _), _)}
         when head=Ident.string_of_lid PC.immutable_array_t_lid -> Some blob
       | _ -> None
   in
-  let arg2_as_blob_nbe (x:NBETerm.arg) : option FStarC.Dyn.dyn =
+  let arg2_as_blob_nbe (x:NBETerm.arg) : option FStar.Dyn.dyn =
       //try_unembed_simple an arg as a IA.t blob if the emb_typ
       //tells us it has the right type
       let open FStarC.TypeChecker.NBETerm in
@@ -153,8 +153,8 @@ let ops : list primitive_step =
   in
   let length_op =
     let embed_int (r:Range.t) (i:int) : ML term = embed_simple r i in
-    let run_op (blob:FStarC.Dyn.dyn) : ML (option int) =
-        Some (BU.array_length #term (FStarC.Dyn.undyn blob))
+    let run_op (blob:FStar.Dyn.dyn) : ML (option int) =
+        Some (BU.array_length #term (FStar.Dyn.undyn blob))
     in
     let nbe_length : nbe_interp_t =
       fun _cbs univs args ->
@@ -180,15 +180,15 @@ let ops : list primitive_step =
            arg2_as_blob_nbe //2nd arg is an `IA.t NBEterm.t` blob
            NBETerm.arg_as_int
            (fun tm -> tm) //In this case, the result is a NBE.t, so embedding is the identity
-           (fun _universes _t blob i  -> Some (BU.array_index #NBETerm.t (FStarC.Dyn.undyn blob) i))
+           (fun _universes _t blob i  -> Some (BU.array_index #NBETerm.t (FStar.Dyn.undyn blob) i))
            univs args
     in
     (PC.immutable_array_index_lid, 3, 1,
        mixed_ternary_op arg1_as_elt_t //1st arg of index is the type
                         arg2_as_blob //2nd arg is the `IA.t term` blob
                         arg_as_int //3rd arg is an int
                         (fun r tm -> tm) //the result is just a term, so the embedding is the identity
-                        (fun r _universes _t blob i -> Some (BU.array_index #term (FStarC.Dyn.undyn blob) i)),
+                        (fun r _universes _t blob i -> Some (BU.array_index #term (FStar.Dyn.undyn blob) i)),
        nbe_index)
   in
   let s1 = as_primitive_step true of_list_op in
diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst
@@ -29,7 +29,7 @@ open FStarC.Syntax.Syntax
 open FStarC.Syntax.Subst
 open FStarC.Syntax.Util
 open FStarC.Const
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.TypeChecker.Rel
 
 open FStarC.Class.Show
diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst
@@ -31,7 +31,7 @@ open FStarC.Syntax.Syntax
 open FStarC.Ident
 open FStarC.Syntax.Subst
 open FStarC.Syntax
-open FStarC.Dyn
+open FStar.Dyn
 open FStarC.Class.Show
 open FStarC.Class.PP
 open FStarC.Class.Monoid
diff --git a/stage0/ulib/ml/app/FStar_Dyn.ml b/stage0/ulib/ml/app/FStar_Dyn.ml
diff --git a/ulib/ml/app/FStar_Dyn.ml b/ulib/ml/app/FStar_Dyn.ml

Original file line number	Diff line number	Diff line change
`@@ -44,7 +44,7 @@ module EMB = FStarC.Syntax.Embeddings`
`44`	`44`	`module N = FStarC.TypeChecker.Normalize`
`45`	`45`	`open FStarC.VConfig`
`46`	`46`
`47`		`-open FStarC.Dyn`
	`47`	`+open FStar.Dyn`
`48`	`48`
`49`	`49`	`(* This file provides implementation for reflection primitives in F*.`
`50`	`50`	`*`