Integer-indexed types

src/ecAlgTactic.ml

@@ -70,22 +70,22 @@ module Axioms = struct
          (div, (false, ty2 ty))]
 
   let subst_of_ring (cr : ring) =
-    let crcore = [(zero, cr.r_zero);
-                  (one , cr.r_one );
-                  (add , cr.r_add );
-                  (mul , cr.r_mul ); ] in
+    let crcore = [(zero, cr.r_zero.ro_op);
+                  (one , cr.r_one .ro_op);
+                  (add , cr.r_add .ro_op);
+                  (mul , cr.r_mul .ro_op); ] in
 
     let xpath  = fun x -> EcPath.pqname tmod x in
     let add    = fun subst x p -> EcSubst.add_path subst ~src:(xpath x) ~dst:p in
     let addctt = fun subst x f -> EcSubst.add_opdef subst (xpath x) ([], f) in
 
     let subst  =
-      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
+      EcSubst.add_tydef EcSubst.empty (xpath tname) ([], [], cr.r_type) in
     let subst  =
       List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in
-    let subst  = odfl subst (cr.r_opp |> omap (fun p -> add subst opp p)) in
-    let subst  = odfl subst (cr.r_sub |> omap (fun p -> add subst sub p)) in
-    let subst  = odfl subst (cr.r_exp |> omap (fun p -> add subst expr p)) in
+    let subst  = odfl subst (cr.r_opp |> omap (fun o -> add subst opp o.ro_op)) in
+    let subst  = odfl subst (cr.r_sub |> omap (fun o -> add subst sub o.ro_op)) in
+    let subst  = odfl subst (cr.r_exp |> omap (fun o -> add subst expr o.ro_op)) in
 
     let subst  =
       match cr.r_kind with
@@ -99,7 +99,7 @@ module Axioms = struct
     let subst  =
       match cr.r_embed with
       | `Direct | `Default -> subst
-      | `Embed p -> add subst embed p
+      | `Embed o -> add subst embed o.ro_op
     in
 
     subst
@@ -109,10 +109,47 @@ module Axioms = struct
     let add    = fun subst x p -> EcSubst.add_path subst ~src:(xpath x) ~dst:p in
 
     let subst = subst_of_ring cr.f_ring in
-    let subst = add subst inv cr.f_inv in
-    let subst = odfl subst (cr.f_div |> omap (fun p -> add subst div p)) in
+    let subst = add subst inv cr.f_inv.ro_op in
+    let subst = odfl subst (cr.f_div |> omap (fun o -> add subst div o.ro_op)) in
       subst
 
+  (* The op paths of an instance carry their instantiation implicitly
+     (each op records the indices/types at which it sits at the
+     carrier). The template axioms reference the ops without
+     instantiation, and [subst_of_ring] swaps paths but cannot
+     re-introduce it; so we patch the substituted axiom, tagging every
+     instance-op occurrence with its recorded targs. (If two slots
+     share one path they must also share their instantiation; the
+     first registered wins.) *)
+  let ring_op_targs (cr : ring) : EcDecl.ring_op EcPath.Mp.t =
+    let os = [cr.r_zero; cr.r_one; cr.r_add; cr.r_mul] in
+    let os = os @ List.filter_map (fun x -> x) [cr.r_opp; cr.r_sub; cr.r_exp] in
+    let os = match cr.r_embed with `Embed o -> o :: os | _ -> os in
+    List.fold_left
+      (fun m (o : EcDecl.ring_op) ->
+        if EcPath.Mp.mem o.ro_op m then m else EcPath.Mp.add o.ro_op o m)
+      EcPath.Mp.empty os
+
+  let field_op_targs (cr : field) : EcDecl.ring_op EcPath.Mp.t =
+    let os = cr.f_inv :: List.filter_map (fun x -> x) [cr.f_div] in
+    List.fold_left
+      (fun m (o : EcDecl.ring_op) ->
+        if EcPath.Mp.mem o.ro_op m then m else EcPath.Mp.add o.ro_op o m)
+      (ring_op_targs cr.f_ring) os
+
+  let inject_targs (opmap : EcDecl.ring_op EcPath.Mp.t) (f : form) =
+    let open EcAst in
+    let rec doit f =
+      match f.f_node with
+      | Fop (p, ta) when ta.indices = [] && ta.types = [] -> begin
+          match EcPath.Mp.find_opt p opmap with
+          | Some { ro_idxs = []; ro_tys = []; _ } | None -> f
+          | Some o ->
+              f_op_r p { indices = o.ro_idxs; types = o.ro_tys } (f_ty f)
+        end
+      | _ -> f_map (fun ty -> ty) doit f
+    in doit f
+
   (* FIXME: should use operators inlining when available *)
   let get cr env axs =
     let subst  =
@@ -121,10 +158,16 @@ module Axioms = struct
       | `Field cr -> subst_of_field cr
     in
 
+    let opmap =
+      match cr with
+      | `Ring  cr -> ring_op_targs  cr
+      | `Field cr -> field_op_targs cr
+    in
+
     let for1 axname =
       let ax = EcEnv.Ax.by_path (EcPath.pqname tmod axname) env in
-        assert (ax.ax_tparams = [] && is_axiom ax.ax_kind);
-        (axname, EcSubst.subst_form subst ax.ax_spec)
+        assert (ax.ax_tparams.tyvars = [] && ax.ax_tparams.idxvars = [] && is_axiom ax.ax_kind);
+        (axname, inject_targs opmap (EcSubst.subst_form subst ax.ax_spec))
     in
       List.map for1 axs
 

src/ecAlgebra.ml

@@ -73,9 +73,11 @@ end
 type eq = form * form
 
 (* -------------------------------------------------------------------- *)
-let rapp r op args =
+let rapp r (op : EcDecl.ring_op) args =
   let opty = toarrow (List.map f_ty args) r.r_type in
-    f_app (f_op op [] opty) args r.r_type
+  let indices = if op.ro_idxs = [] then None else Some op.ro_idxs in
+  let tyargs  = if op.ro_tys  = [] then None else Some op.ro_tys  in
+    f_app (f_op op.ro_op ?indices ?tyargs opty) args r.r_type
 
 let rzero r = rapp r r.r_zero []
 let rone  r = rapp r r.r_one  []
@@ -150,35 +152,41 @@ let emb_fone  r = emb_rone  r.f_ring
 
 (* -------------------------------------------------------------------- *)
 type cringop = [`Zero | `One | `Add | `Opp | `Sub | `Mul | `Exp | `OfInt]
-type cring   = ring * (cringop Mp.t)
+type cring   = ring * ((cringop * EcDecl.ring_op) Mp.t)
 
 (* -------------------------------------------------------------------- *)
 type cfieldop = [cringop | `Inv | `Div]
-type cfield   = field * (cfieldop Mp.t)
+type cfield   = field * ((cfieldop * EcDecl.ring_op) Mp.t)
 
 (* -------------------------------------------------------------------- *)
+(* Recognition is keyed by op path, then checked against the slot's
+   recorded instantiation: an occurrence of the same path at OTHER
+   indices/types is not this ring's operator. *)
 let cring_of_ring (r : ring) : cring =
   let cr = [(r.r_zero, `Zero);
             (r.r_one , `One );
             (r.r_add , `Add );
             (r.r_mul , `Mul );]
   in
 
-  let cr = List.fold_left (fun m (p, op) -> Mp.add p op m) Mp.empty cr in
-  let cr = odfl cr (r.r_opp |> omap (fun p -> Mp.add p `Opp cr)) in
-  let cr = odfl cr (r.r_sub |> omap (fun p -> Mp.add p `Sub cr)) in
-  let cr = odfl cr (r.r_exp |> omap (fun p -> Mp.add p `Exp cr)) in
+  let radd (o : EcDecl.ring_op) tag m = Mp.add o.ro_op (tag, o) m in
+  let cr = List.fold_left (fun m (o, tag) -> radd o tag m) Mp.empty cr in
+  let cr = odfl cr (r.r_opp |> omap (fun o -> radd o `Opp cr)) in
+  let cr = odfl cr (r.r_sub |> omap (fun o -> radd o `Sub cr)) in
+  let cr = odfl cr (r.r_exp |> omap (fun o -> radd o `Exp cr)) in
   let cr = r.r_embed |>
-      (function (`Direct | `Default) -> cr | `Embed p -> Mp.add p `OfInt cr) in
+      (function (`Direct | `Default) -> cr | `Embed o -> radd o `OfInt cr) in
     (r, cr)
 
 let ring_of_cring (cr:cring) = fst cr
 
 (* -------------------------------------------------------------------- *)
 let cfield_of_field (r : field) : cfield =
-  let cr = (snd (cring_of_ring r.f_ring) :> cfieldop Mp.t) in
-  let cr = Mp.add r.f_inv `Inv cr in
-  let cr = odfl cr (r.f_div |> omap (fun p -> Mp.add p `Div cr)) in
+  let cr =
+    (snd (cring_of_ring r.f_ring) :> (cfieldop * EcDecl.ring_op) Mp.t) in
+  let cr = Mp.add r.f_inv.ro_op (`Inv, r.f_inv) cr in
+  let cr =
+    odfl cr (r.f_div |> omap (fun o -> Mp.add o.ro_op (`Div, o) cr)) in
     (r, cr)
 
 let field_of_cfield (cr:cfield) : field = fst cr
@@ -192,10 +200,14 @@ let toring hyps ((r, cr) : cring) (rmap : RState.rstate) (form : form) =
   let rec doit form =
     let o, args = destr_app form in
     match o.f_node with
-    | Fop (op, _) -> begin
+    | Fop (op, ta) -> begin
         match Mp.find_opt op cr with
         | None -> abstract form
-        | Some op -> begin
+        | Some (_, ro)
+            when not (List.all2 EcAst.tindex_equal ta.indices ro.ro_idxs
+                      && List.all2 ty_equal ta.types ro.ro_tys) ->
+          abstract form
+        | Some (op, _) -> begin
           match op,args with
           | `Zero, []           -> PEc c0
           | `One , []           -> PEc c1
@@ -255,10 +267,14 @@ let tofield hyps ((r, cr) : cfield) (rmap : RState.rstate) (form : form) =
   let rec doit form =
     let o, args = destr_app form in
     match o.f_node with
-    | Fop(op, _) -> begin
+    | Fop(op, ta) -> begin
         match Mp.find_opt op cr with
         | None -> abstract form
-        | Some op -> begin
+        | Some (_, ro)
+            when not (List.all2 EcAst.tindex_equal ta.indices ro.ro_idxs
+                      && List.all2 ty_equal ta.types ro.ro_tys) ->
+          abstract form
+        | Some (op, _) -> begin
           match op,args with
           | `Zero, []           -> FEc c0
           | `One , []           -> FEc c1

src/ecAlgebra.mli

@@ -16,7 +16,7 @@ module RState : sig
 end
 
 (* -------------------------------------------------------------------- *)
-val rapp   : ring -> EcPath.path -> form list -> form
+val rapp   : ring -> EcDecl.ring_op -> form list -> form
 val rzero  : ring -> form
 val rone   : ring -> form
 val radd   : ring -> form -> form -> form

src/ecAlphaInvHashtbl.ml

@@ -5,8 +5,9 @@
    The hash is invariant under the renaming of bound variables: a bound
    occurrence is hashed by the de-Bruijn *level* of its binder (an
    integer, intrinsically stable) rather than by its name, so
-   alpha-equivalent formulas hash equal. Free variables, operators and
-   types are stable under alpha-renaming and are hashed as-is.
+   alpha-equivalent formulas hash equal. Free variables, operators
+   (with their type and index instantiations) and types are stable
+   under alpha-renaming and are hashed as-is.
 
    The hash traverses the whole formula, but is memoized on the hash-cons
    tag ([f_tag]) of every subformula reached with no binder in scope: each
@@ -78,7 +79,7 @@ let hash_memo (memo : (int, int) Hashtbl.t) (f0 : form) : int =
       combine 3 (pv_hash pv)
     | Fglob (mp, _m) -> combine 4 (id_hash mp)
     | Fop (p, tys) ->
-      combine 5 (combine_list (EcPath.p_hash p) (List.map ty_hash tys))
+      combine 5 (targ_hash (EcPath.p_hash p) tys)
     | Fif (c, t, f) -> combine 6 (combine_list 0 [hash e c; hash e t; hash e f])
     | Fmatch (c, bs, ty) ->
       combine 7 (combine_list (ty_hash ty) (hash e c :: List.map (hash e) bs))