From 08ade6176cd14817dc581a2a03b393cbfb5f02a9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias <e+git@x80.org> Date: Mon, 27 May 2024 13:12:32 +0200 Subject: [PATCH] [serlib] [ltac2] Fix wrong piercing creating havoc. This broke in #18432, creating a segfault. cc https://github.com/ejgallego/coq-serapi/issues/82 --- serlib/plugins/ltac2/ser_tac2expr.ml | 93 +++++++++++++++------------- tests/genarg/dune | 7 +++ tests/genarg/ltac2.v | 5 ++ 3 files changed, 61 insertions(+), 44 deletions(-) create mode 100644 tests/genarg/ltac2.v diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml index b087580d..65eb5a41 100644 --- 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 index f1253f9e..f3326f1a 100644 --- 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 new file mode 100644 index 00000000..011f4ea6 --- /dev/null +++ b/tests/genarg/ltac2.v @@ -0,0 +1,5 @@ +From Ltac2 Require Import Ltac2. + +Goal True /\ True. + split; exact I. +Qed.