From 19e5c09f478d073dda2d17e94754d12716f63469 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Tue, 24 Sep 2024 09:54:26 +0200
Subject: [PATCH] internals: user-defined rules can be headed by a projection

---
 src/ecEnv.ml       | 20 ++++++++++++--------
 src/ecEnv.mli      |  2 +-
 src/ecReduction.ml |  8 ++++++--
 src/ecTheory.ml    |  2 +-
 src/ecTheory.mli   |  2 +-
 5 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index 240cd56850..fb11e65a9e 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -117,17 +117,20 @@ type env_norm = {
 type red_topsym = [
   | `Path of path
   | `Tuple
+  | `Proj of int
 ]
 
 module Mrd = EcMaps.Map.Make(struct
   type t = red_topsym
 
+  let to_comparable (p : t) =
+    match p with
+    | `Path p -> `Path p.p_tag
+    | `Tuple  -> `Tuple
+    | `Proj i -> `Proj i
+
   let compare (p1 : t) (p2 : t) =
-    match p1, p2 with
-    | `Path p1, `Path p2 ->  EcPath.p_compare p1 p2
-    | `Tuple  , `Tuple   ->  0
-    | `Tuple  , `Path _  -> -1
-    | `Path _ , `Tuple   ->  1
+    Stdlib.compare (to_comparable p1) (to_comparable p2)
 end)
 
 (* -------------------------------------------------------------------- *)
@@ -1451,11 +1454,12 @@ module Reduction = struct
   let add_rule ((_, rule) : path * rule option) (db : mredinfo) =
     match rule with None -> db | Some rule ->
 
-    let p =
+    let p : topsym =
       match rule.rl_ptn with
       | Rule (`Op p, _)   -> `Path (fst p)
-      | Rule (`Tuple, _) -> `Tuple
-      | Var _ | Int _    -> assert false in
+      | Rule (`Tuple, _)  -> `Tuple
+      | Rule (`Proj i, _) -> `Proj i
+      | Var _ | Int _     -> assert false in
 
     Mrd.change (fun rls ->
       let { ri_priomap } =
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index e86cf773e5..5d73b3bd15 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -404,7 +404,7 @@ end
 (* -------------------------------------------------------------------- *)
 module Reduction : sig
   type rule   = EcTheory.rule
-  type topsym = [ `Path of path | `Tuple ]
+  type topsym = [ `Path of path | `Tuple | `Proj of int]
 
   val add1 : path * rule_option * rule option -> env -> env
   val add  : ?import:import -> (path * rule_option * rule option) list -> env -> env
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index d6fb0c8a1d..5e83cd1ee2 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -717,11 +717,12 @@ let eta_expand bd f ty =
 let reduce_user_gen simplify ri env hyps f =
   if not ri.user then raise nohead;
 
-  let p =
+  let p : EcEnv.Reduction.topsym =
     match f.f_node with
     | Fop (p, _)
     | Fapp ({ f_node = Fop (p, _) }, _) -> `Path p
     | Ftuple _   -> `Tuple
+    | Fproj (_, i) -> `Proj i
     | _ -> raise nohead in
 
   let rules = EcEnv.Reduction.get p env in
@@ -1660,6 +1661,8 @@ module User = struct
             R.Rule (`Op (p, tys), List.map rule args)
         | { f_node = Ftuple args }, [] ->
             R.Rule (`Tuple, List.map rule args)
+        | { f_node = Fproj (target, i) }, [] ->
+            R.Rule (`Proj i, [rule target])
         | { f_node = Fint i }, [] ->
             R.Int i
         | { f_node = Flocal x }, [] ->
@@ -1684,7 +1687,8 @@ module User = struct
                       | { ty_node = Tvar a } -> Sid.add a ltyvars
                       | _ as ty -> ty_fold doit ltyvars ty in doit)
                   cst.cst_ty_vs tys
-              | `Tuple -> cst.cst_ty_vs in
+              | `Tuple -> cst.cst_ty_vs
+              | `Proj _ -> cst.cst_ty_vs in
             let cst = {cst with cst_ty_vs = ltyvars } in
             List.fold_left doit cst args
 
diff --git a/src/ecTheory.ml b/src/ecTheory.ml
index 3e2065112e..0d39c8d21d 100644
--- a/src/ecTheory.ml
+++ b/src/ecTheory.ml
@@ -59,7 +59,7 @@ and rule_pattern =
   | Var  of EcIdent.t
 
 and top_rule_pattern =
-  [`Op of (EcPath.path * EcTypes.ty list) | `Tuple]
+  [`Op of (EcPath.path * EcTypes.ty list) | `Tuple | `Proj of int]
 
 and rule = {
   rl_tyd   : EcDecl.ty_params;
diff --git a/src/ecTheory.mli b/src/ecTheory.mli
index 9e239bd411..472928561f 100644
--- a/src/ecTheory.mli
+++ b/src/ecTheory.mli
@@ -56,7 +56,7 @@ and rule_pattern =
   | Var  of EcIdent.t
 
 and top_rule_pattern =
-  [`Op of (EcPath.path * EcTypes.ty list) | `Tuple]
+  [`Op of (EcPath.path * EcTypes.ty list) | `Tuple | `Proj of int]
 
 and rule = {
   rl_tyd   : EcDecl.ty_params;