Merge pull request #387 from Yann-Leray/rewrite-rules

rocq-archive · Feb 21, 2024 · e25a10c · e25a10c
2 parents da086de + a021ed8
commit e25a10c
Show file tree

Hide file tree

Showing 5 changed files with 49 additions and 2 deletions.
diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml
@@ -33,6 +33,8 @@ module Mod_subst   = Ser_mod_subst
 module Opaqueproof = Ser_opaqueproof
 module Vmemitcodes = Ser_vmemitcodes
 module Retroknowledge = Ser_retroknowledge
+module Uint63  = Ser_uint63
+module Float64 = Ser_float64
 
 type template_arity =
   [%import: Declarations.template_arity]
@@ -87,8 +89,8 @@ type universes =
   [%import: Declarations.universes]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('a, 'b) constant_def =
-  [%import: ('a, 'b) Declarations.constant_def]
+type ('a, 'b, 'c) constant_def =
+  [%import: ('a, 'b, 'c) Declarations.constant_def]
   [@@deriving sexp,yojson,hash,compare]
 
 type typing_flags =
@@ -145,6 +147,35 @@ type mutual_inductive_body =
   [@with Context.section_context := Context.Named.t;]]
   [@@deriving sexp,yojson,hash,compare]
 
+type instance_mask =
+  [%import: UVars.Instance.mask]
+  [@@deriving sexp,yojson,hash,compare]
+
+type 'a head_pattern =
+  [%import: 'a Declarations.head_pattern
+    [@with sort_pattern := Sorts.pattern]]
+  [@@deriving sexp,yojson,hash,compare]
+
+type pattern_elimination =
+  [%import: Declarations.pattern_elimination]
+  [@@deriving sexp,yojson,hash,compare]
+
+and head_elimination =
+  [%import: Declarations.head_elimination]
+  [@@deriving sexp,yojson,hash,compare]
+
+and pattern_argument =
+  [%import: Declarations.pattern_argument]
+  [@@deriving sexp,yojson,hash,compare]
+
+type rewrite_rule =
+  [%import: Declarations.rewrite_rule]
+  [@@deriving sexp,yojson,hash,compare]
+
+type rewrite_rules_body =
+  [%import: Declarations.rewrite_rules_body]
+  [@@deriving sexp,yojson,hash,compare]
+
 type ('ty,'a) functorize =
   [%import: ('ty, 'a) Declarations.functorize]
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli
@@ -89,6 +89,9 @@ type recursivity_kind = Declarations.recursivity_kind
 type mutual_inductive_body = Declarations.mutual_inductive_body
   [@@deriving sexp,yojson,hash,compare]
 
+type rewrite_rule = Declarations.rewrite_rule
+  [@@deriving sexp,yojson,hash,compare]
+
 type 'a module_alg_expr = 'a Declarations.module_alg_expr
   [@@deriving sexp,yojson,hash,compare]
 

diff --git a/serlib/ser_entries.ml b/serlib/ser_entries.ml
@@ -95,6 +95,10 @@ type primitive_entry =
   [%import: Entries.primitive_entry]
   [@@deriving sexp]
 
+type symbol_entry =
+  [%import: Entries.symbol_entry]
+  [@@deriving sexp]
+
 type constant_entry =
   [%import: Entries.constant_entry]
   [@@deriving sexp]

diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml
@@ -62,6 +62,14 @@ type relevance =
   [%import: Sorts.relevance]
   [@@deriving sexp,yojson,hash,compare]
 
+open Sexplib.Std
+open Ppx_hash_lib.Std.Hash.Builtin
+open Ppx_compare_lib.Builtin
+
+type pattern =
+  [%import: Sorts.pattern]
+  [@@deriving sexp,yojson,hash,compare]
+
 module QConstraint = struct
   type kind =
     [%import: Sorts.QConstraint.kind]

diff --git a/serlib/ser_sorts.mli b/serlib/ser_sorts.mli
@@ -17,6 +17,7 @@ include SerType.SJHC with type t = Sorts.t
 
 type family = Sorts.family [@@deriving sexp,yojson,hash,compare]
 type relevance = Sorts.relevance [@@deriving sexp,yojson,hash,compare]
+type pattern = Sorts.pattern [@@deriving sexp,yojson,hash,compare]
 
 module QVar : sig
   include SerType.SJHC with type t = Sorts.QVar.t