Merge pull request #413 from ejgallego/fix_ltac2_piercing

[serlib] [ltac2] Fix wrong piercing creating havoc.
rocq-archive · May 28, 2024 · cfa66f2 · cfa66f2
2 parents 8619fae + 08ade61
commit cfa66f2
Show file tree

Hide file tree

Showing 3 changed files with 61 additions and 44 deletions.
diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml
@@ -66,6 +66,10 @@ type raw_quant_typedef =
   [%import: Ltac2_plugin.Tac2expr.raw_quant_typedef]
   [@@deriving sexp,yojson,hash,compare]
 
+type 'a glb_typexpr =
+  [%import: 'a Ltac2_plugin.Tac2expr.glb_typexpr]
+  [@@deriving sexp,yojson,hash,compare]
+
 type atom =
   [%import: Ltac2_plugin.Tac2expr.atom]
   [@@deriving sexp,yojson,hash,compare]
@@ -97,46 +101,6 @@ type tacref =
   [%import: Ltac2_plugin.Tac2expr.tacref]
   [@@deriving sexp,yojson,hash,compare]
 
-module ObjS = struct type t = Obj.t let name = "Obj.t" end
-module Obj = SerType.Opaque(ObjS)
-
-module T2ESpec = struct
-  type t = Ltac2_plugin.Tac2expr.raw_tacexpr_r
-  open Ltac2_plugin.Tac2expr
-  type _t =
-    | CTacAtm of atom
-    | CTacRef of tacref or_relid
-    | CTacCst of ltac_constructor or_tuple or_relid
-    | CTacFun of raw_patexpr list * raw_tacexpr
-    | CTacApp of raw_tacexpr * raw_tacexpr list
-    | CTacSyn of (raw_patexpr * raw_tacexpr) list * Names.KerName.t
-    | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
-    | CTacCnv of raw_tacexpr * raw_typexpr
-    | CTacSeq of raw_tacexpr * raw_tacexpr
-    | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
-    | CTacCse of raw_tacexpr * raw_taccase list
-    | CTacRec of raw_tacexpr option * raw_recexpr
-    | CTacPrj of raw_tacexpr * ltac_projection or_relid
-    | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-    | CTacExt of int * Obj.t
-
-  and raw_tacexpr = _t CAst.t
-  and raw_taccase =
-  [%import: Ltac2_plugin.Tac2expr.raw_taccase]
-  and raw_recexpr =
-  [%import: Ltac2_plugin.Tac2expr.raw_recexpr]
-  [@@deriving sexp,yojson,hash,compare]
-
-end
-
-module T2E = Serlib.SerType.Pierce(T2ESpec)
-type raw_tacexpr_r = T2E.t
-  [@@deriving sexp,yojson,hash,compare]
-
-type raw_tacexpr =
-  [%import: Ltac2_plugin.Tac2expr.raw_tacexpr]
-  [@@deriving sexp,yojson,hash,compare]
-
 type ml_tactic_name =
   [%import: Ltac2_plugin.Tac2expr.ml_tactic_name]
   [@@deriving sexp,yojson,hash,compare]
@@ -145,10 +109,6 @@ type sexpr =
   [%import: Ltac2_plugin.Tac2expr.sexpr]
   [@@deriving sexp,yojson,hash,compare]
 
-type strexpr =
-  [%import: Ltac2_plugin.Tac2expr.strexpr]
-  [@@deriving sexp,yojson,hash,compare]
-
 type ctor_indx =
   [%import: Ltac2_plugin.Tac2expr.ctor_indx]
   [@@deriving sexp,yojson,hash,compare]
@@ -169,6 +129,9 @@ type 'a open_match =
   [%import: 'a Ltac2_plugin.Tac2expr.open_match]
   [@@deriving sexp,yojson,hash,compare]
 
+module ObjS = struct type t = Obj.t let name = "Obj.t" end
+module Obj = SerType.Opaque(ObjS)
+
 module GT2ESpec = struct
   type t = Ltac2_plugin.Tac2expr.glb_tacexpr
   open Ltac2_plugin.Tac2expr
@@ -195,3 +158,45 @@ end
 module GT2E = Serlib.SerType.Pierce(GT2ESpec)
 type glb_tacexpr = GT2E.t
   [@@deriving sexp,yojson,hash,compare]
+
+module T2ESpec = struct
+  type t = Ltac2_plugin.Tac2expr.raw_tacexpr_r
+  open Ltac2_plugin.Tac2expr
+  type _t =
+    | CTacAtm of atom
+    | CTacRef of tacref or_relid
+    | CTacCst of ltac_constructor or_tuple or_relid
+    | CTacFun of raw_patexpr list * raw_tacexpr
+    | CTacApp of raw_tacexpr * raw_tacexpr list
+    | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t
+    | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * Names.KerName.t
+    | CTacCnv of raw_tacexpr * raw_typexpr
+    | CTacSeq of raw_tacexpr * raw_tacexpr
+    | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
+    | CTacCse of raw_tacexpr * raw_taccase list
+    | CTacRec of raw_tacexpr option * raw_recexpr
+    | CTacPrj of raw_tacexpr * ltac_projection or_relid
+    | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+    | CTacExt of int * Obj.t
+    | CTacGlb of int * (Names.lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
+
+  and raw_tacexpr = _t CAst.t
+  and raw_taccase =
+  [%import: Ltac2_plugin.Tac2expr.raw_taccase]
+  and raw_recexpr =
+  [%import: Ltac2_plugin.Tac2expr.raw_recexpr]
+  [@@deriving sexp,yojson,hash,compare]
+
+end
+
+module T2E = Serlib.SerType.Pierce(T2ESpec)
+type raw_tacexpr_r = T2E.t
+  [@@deriving sexp,yojson,hash,compare]
+
+type raw_tacexpr =
+  [%import: Ltac2_plugin.Tac2expr.raw_tacexpr]
+  [@@deriving sexp,yojson,hash,compare]
+
+type strexpr =
+  [%import: Ltac2_plugin.Tac2expr.strexpr]
+  [@@deriving sexp,yojson,hash,compare]
diff --git a/tests/genarg/dune b/tests/genarg/dune
@@ -166,3 +166,10 @@
  (alias runtest)
  (deps (:input primitives.v))
  (action (run ./test_roundtrip %{input})))
+
+; Disabled until we implement ltac2 extension serialization
+;
+; (rule
+;  (alias runtest)
+;  (deps (:input ltac2.v))
+;  (action (run ./test_roundtrip %{input})))
diff --git a/tests/genarg/ltac2.v b/tests/genarg/ltac2.v
@@ -0,0 +1,5 @@
+From Ltac2 Require Import Ltac2.
+
+Goal True /\ True.
+  split; exact I.
+Qed.