Do not store recursive trees anymore in inductive blocks.

This data is now useless as it can be recovered from the compiled automaton.

Author: ppedrot

checker/checkInductive.ml

@@ -174,7 +174,7 @@ let check_same_record r1 r2 = match r1, r2 with
 let check_packet mind ind
     { mind_typename; mind_arity_ctxt; mind_user_arity; mind_record; mind_sort; mind_consnames; mind_user_lc;
       mind_nrealargs; mind_nrealdecls; mind_squashed; mind_nf_lc;
-      mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_automaton; mind_relevance;
+      mind_consnrealargs; mind_consnrealdecls; mind_automaton; mind_relevance;
       mind_relies_on_indices_not_mattering; mind_nb_constant; mind_nb_args; mind_reloc_tbl } =
   let check = check mind in
 
@@ -196,7 +196,6 @@ let check_packet mind ind
   check "mind_consnrealargs" (Array.equal Int.equal ind.mind_consnrealargs mind_consnrealargs);
   check "mind_consnrealdecls" (Array.equal Int.equal ind.mind_consnrealdecls mind_consnrealdecls);
 
-  check "mind_recargs" (Rtree.equal eq_recarg ind.mind_recargs mind_recargs);
   check "mind_automaton" (Rtree.Automaton.equal eq_recarg ind.mind_automaton mind_automaton);
 
   check "mind_relevant" (Sorts.relevance_equal ind.mind_relevance mind_relevance);

checker/values.ml

@@ -430,14 +430,6 @@ let v_recarg_type = v_sum "recarg_type" 0
 let v_recarg = v_sum "recarg" 1 (* Norec *)
   [|[|v_recarg_type|] (* Mrec *)|]
 
-let v_wfp =
-  fix (fun v_wfp ->
-  v_sum_c ("wf_paths",0,
-    [|[|v_int;v_int|]; (* Rtree.Param *)
-      [|v_recarg;v_array (v_array v_wfp)|]; (* Rtree.Node *)
-      [|v_int;v_array v_wfp|] (* Rtree.Rec *)
-    |]))
-
 let v_automaton =
   v_tuple "automaton"
     [|v_int; v_array (v_pair v_recarg (v_array (v_array v_int)))|]
@@ -463,7 +455,6 @@ let v_one_ind = v_tuple "one_inductive_body"
     v_array (v_pair v_rctxt v_constr);
     v_array v_int;
     v_array v_int;
-    v_wfp;
     v_automaton;
     v_relevance;
     v_bool;

kernel/declarations.mli

@@ -248,9 +248,7 @@ type one_inductive_body = {
     mind_consnrealdecls : int array;
  (** Length of the signature of the constructors (with let, w/o params) *)
 
-    mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
-
-    mind_automaton : recarg Rtree.Automaton.t; (** Minimal automaton generated from the above *)
+    mind_automaton : recarg Rtree.Automaton.t; (** Minimal automaton generated from the inductive tree *)
 
     mind_relevance : Sorts.relevance;
     (* XXX this is redundant with mind_sort, is it actually worth keeping? *)

kernel/declareops.ml

@@ -218,12 +218,6 @@ let dest_subterms p =
   assert (match ra with Norec -> false | _ -> true);
   Array.map Array.to_list cstrs
 
-let recarg_length p j =
-  let (_,cstrs) = Rtree.dest_node p in
-  Array.length cstrs.(j-1)
-
-let subst_wf_paths subst p = Rtree.Smart.map (subst_recarg subst) p
-
 let subst_automaton subst a =
   Rtree.Automaton.map (fun r -> subst_recarg subst r) a
 
@@ -251,7 +245,6 @@ let subst_mind_packet subst mbp =
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_squashed = mbp.mind_squashed;
-    mind_recargs = subst_wf_paths subst mbp.mind_recargs (*wf_paths*);
     mind_automaton = subst_automaton subst mbp.mind_automaton;
     mind_relevance = mbp.mind_relevance;
     mind_relies_on_indices_not_mattering = mbp.mind_relies_on_indices_not_mattering;

kernel/declareops.mli

@@ -51,9 +51,6 @@ val mk_norec : wf_paths
 val mk_paths : recarg -> wf_paths list array -> wf_paths
 val dest_recarg : wf_paths -> recarg
 val dest_subterms : wf_paths -> wf_paths list array
-val recarg_length : wf_paths -> int -> int
-
-val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 

kernel/discharge.ml

@@ -155,7 +155,6 @@ let cook_one_ind info cache ~params ~ntypes mip =
     mind_nf_lc;
     mind_consnrealargs = mip.mind_consnrealargs;
     mind_consnrealdecls = mip.mind_consnrealdecls;
-    mind_recargs = mip.mind_recargs;
     mind_automaton = mip.mind_automaton;
     mind_relevance = lift_relevance info mip.mind_relevance;
     mind_relies_on_indices_not_mattering = mip.mind_relies_on_indices_not_mattering;

kernel/indtypes.ml

@@ -561,7 +561,6 @@ let build_inductive env ~sec_univs names prv univs template variance
         mind_consnrealargs = consnrealargs;
         mind_user_lc = lc;
         mind_nf_lc = nf_lc;
-        mind_recargs = recarg;
         mind_automaton = automaton;
         mind_relevance;
         mind_relies_on_indices_not_mattering = relies_on_indices_not_mattering;

plugins/funind/gen_principle.ml

@@ -1109,8 +1109,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
             in
             if
               infos.is_general
-              || Rtree.is_infinite Declareops.eq_recarg
-                   graph_def.Declarations.mind_recargs
+              || Inductiveops.mis_is_recursive graph_def
             then
               let eq_lemma = match infos.equation_lemma with
               | None -> CErrors.anomaly (Pp.str "Cannot find equation lemma.")

pretyping/inductiveops.ml

@@ -15,7 +15,6 @@ open EConstr
 open Vars
 open Context
 open Declarations
-open Declareops
 open Environ
 open Reductionops
 open Context.Rel.Declaration
@@ -116,24 +115,22 @@ let dest_subterms p = match Rtree.Kind.kind p with
 | Rtree.Kind.Var _ -> assert false
 
 let mis_is_recursive mip =
-  let one_is_rec rvec =
-    Array.exists (fun ra ->
-      match dest_recarg ra with
-        | Mrec (RecArgInd ind) -> true
-        | Mrec (RecArgPrim _) | Norec -> false
-    ) rvec
-    in
-  Array.exists one_is_rec (dest_subterms @@ Rtree.Kind.make mip.mind_recargs)
+  let ra = mip.mind_automaton in
+  let trans = Rtree.Automaton.transitions ra (Rtree.Automaton.initial ra) in
+  let check tr = match Rtree.Automaton.data ra tr with Mrec _ -> true | Norec -> false in
+  Array.exists (fun v -> Array.exists check v) trans
 
 let mis_is_nested kn mib =
   Array.exists (fun mip ->
+    let ra = mip.mind_automaton in
+    let trans = Rtree.Automaton.transitions ra (Rtree.Automaton.initial ra) in
     Array.exists (fun rvec ->
-      Array.exists (fun ra ->
-        match dest_recarg ra with
+      Array.exists (fun tr ->
+        match Rtree.Automaton.data ra tr with
         | Mrec (RecArgInd (kni, _)) -> not @@ MutInd.CanOrd.equal kn kni
         | Mrec (RecArgPrim _) | Norec -> false
       ) rvec
-    ) (dest_subterms @@ Rtree.Kind.make mip.mind_recargs)
+    ) trans
   ) mib.mind_packets
 
 let mis_nf_constructor_type ((_,j),u) (mib,mip) =
@@ -239,12 +236,6 @@ let constructor_alltags env (ind,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
 
-let constructor_has_local_defs env (indsp,j) =
-  let (mib,mip) = Inductive.lookup_mind_specif env indsp in
-  let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
-  let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
-  not (Int.equal l1 l2)
-
 let inductive_has_local_defs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in

pretyping/inductiveops.mli

@@ -123,7 +123,6 @@ val inductive_alltags : env -> inductive -> bool list
 val constructor_alltags : env -> constructor -> bool list
 
 (** Is there local defs in params or args ? *)
-val constructor_has_local_defs : env -> constructor -> bool
 val inductive_has_local_defs : env -> inductive -> bool
 
 val constant_sorts_below : UnivGen.QualityOrSet.t -> UnivGen.QualityOrSet.t list