internals: user-defined rules can be headed by a projection

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 } =

src/ecEnv.mli

@@ -402,7 +402,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

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
 

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;

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;