Fix comparison of fixpoints

Do take recursive calls (i.e. the fixpoints names) into
account.

Author: strub

src/ecDecl.ml

@@ -25,11 +25,17 @@ and ty_body = [
   | `Concrete of EcTypes.ty
   | `Abstract of Sp.t
   | `Datatype of ty_dtype
-  | `Record   of EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
+  | `Record   of ty_record
 ]
 
+and ty_record =
+  EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
+
+and ty_dtype_ctor =
+  EcSymbols.symbol * EcTypes.ty list
+
 and ty_dtype = {
-  tydt_ctors   : (EcSymbols.symbol * EcTypes.ty list) list;
+  tydt_ctors   : ty_dtype_ctor list;
   tydt_schelim : EcCoreFol.form;
   tydt_schcase : EcCoreFol.form;
 }
@@ -87,6 +93,7 @@ and prbody =
   | PR_Ind   of prind
 
 and opfix = {
+  opf_recp     : EcPath.path;
   opf_args     : (EcIdent.t * EcTypes.ty) list;
   opf_resty    : EcTypes.ty;
   opf_struct   : int list * int;

src/ecDecl.mli

@@ -21,13 +21,19 @@ and ty_body = [
   | `Concrete of EcTypes.ty
   | `Abstract of Sp.t
   | `Datatype of ty_dtype
-  | `Record   of form * (EcSymbols.symbol * EcTypes.ty) list
+  | `Record   of ty_record
 ]
 
+and ty_record =
+  EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
+
+and ty_dtype_ctor =
+  EcSymbols.symbol * EcTypes.ty list
+
 and ty_dtype = {
-  tydt_ctors   : (EcSymbols.symbol * EcTypes.ty list) list;
-  tydt_schelim : form;
-  tydt_schcase : form;
+  tydt_ctors   : ty_dtype_ctor list;
+  tydt_schelim : EcCoreFol.form;
+  tydt_schcase : EcCoreFol.form;
 }
 
 val tydecl_as_concrete : tydecl -> EcTypes.ty option
@@ -60,6 +66,7 @@ and prbody =
   | PR_Ind   of prind
 
 and opfix = {
+  opf_recp     : EcPath.path;
   opf_args     : (EcIdent.t * EcTypes.ty) list;
   opf_resty    : EcTypes.ty;
   opf_struct   : int list * int;

src/ecPrinting.ml

@@ -620,7 +620,7 @@ let pp_modtype1 (ppe : PPEnv.t) fmt mty =
 
 (* -------------------------------------------------------------------- *)
 let pp_local (ppe : PPEnv.t) fmt x =
-  Format.fprintf fmt "%s" (PPEnv.local_symb ppe x)
+  Format.fprintf fmt "%s" (EcIdent.tostring x)
 
 (* -------------------------------------------------------------------- *)
 let pp_local ?fv (ppe : PPEnv.t) fmt x =

src/ecScope.ml

@@ -1143,6 +1143,7 @@ module Op = struct
       | `Plain e  -> Some (OP_Plain (fs e))
       | `Fix opfx ->
           Some (OP_Fix {
+            opf_recp     = EcPath.pqname (EcEnv.root eenv) (EcIdent.name opfx.EHI.mf_name);
             opf_args     = opfx.EHI.mf_args;
             opf_resty    = opfx.EHI.mf_codom;
             opf_struct   = (opfx.EHI.mf_recs, List.length opfx.EHI.mf_args);

src/ecSection.ml

@@ -853,6 +853,7 @@ let generalize_opdecl to_gen prefix (name, operator) =
               let (l,i) = opfix.opf_struct in
               (List.map (fun i -> i + nb_extra) l, i + nb_extra) in
             OP_Fix {
+                opf_recp     = opfix.opf_recp;
                 opf_args     = extra_a @ opfix.opf_args;
                 opf_resty    = opfix.opf_resty;
                 opf_struct;

src/ecSubst.ml

@@ -899,7 +899,8 @@ and subst_op_body (s : subst) (bd : opbody) =
   | OP_Fix opfix ->
       let (es, args) = fresh_elocals s opfix.opf_args in
 
-      OP_Fix { opf_args     = args;
+      OP_Fix { opf_recp     = subst_path s opfix.opf_recp;
+               opf_args     = args;
                opf_resty    = subst_ty s opfix.opf_resty;
                opf_struct   = opfix.opf_struct;
                opf_branches = subst_branches es opfix.opf_branches; }

src/ecSubst.mli

@@ -42,6 +42,7 @@ val freshen_type : (ty_params * ty) -> (ty_params * ty)
 val subst_theory  : subst -> theory -> theory
 val subst_ax      : subst -> axiom -> axiom
 val subst_op      : subst -> operator -> operator
+val subst_op_body : subst -> opbody -> opbody
 val subst_tydecl  : subst -> tydecl -> tydecl
 val subst_tc      : subst -> typeclass -> typeclass
 val subst_theory  : subst -> theory -> theory