From 61b477aada38f25dfc24ec09e453454f62df234e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 6 Aug 2014 18:15:55 -0400
Subject: Relax a bit the guard condition.

My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.

The following (cooked-up) example illustrates this:

Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.

Inductive tree := Node : list tree tree -> tree.

Lemma foo : tree = tree. exact eq_refl. Qed.

Fixpoint id (t : tree) :=
  match t with
  | Node l =>
    let l := match foo in (_ = T) return list tree T with eq_refl => l end
    in
    match l with
    | nil  => Node (nil _ _)
    | cons x tl => Node (cons _ _ (id x) tl)
    end
  end.

is accepted, but changing tree to:

Inductive tree := Node : list tree tree -> tree.
with tree2 := .

made id be rejected after the optimization.

The same problem occurred in Paco, and is now fixed.

Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.
---
 kernel/inductive.ml | 40 +++++++++++++++++-----------------------
 1 file changed, 17 insertions(+), 23 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 802e232c7a..6ddddeb05d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -633,12 +633,12 @@ nested types should be traversed, pruning the tree otherwise. This code is very
 close to check_positive in indtypes.ml, but does no positivy check and does not
 compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
-  let rec build_recargs (env, ra_env as ienv) otree c =
+  let rec build_recargs (env, ra_env as ienv) tree c =
     let x,largs = decompose_app (whd_betadeltaiota env c) in
     match kind_of_term x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
-       build_recargs (ienv_push_var ienv (na, b, mk_norec)) otree d
+       build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d
     | Rel k ->
        (* Free variables are allowed and assigned Norec *)
        (try snd (List.nth ra_env (k-1))
@@ -646,13 +646,9 @@ let get_recargs_approx env tree ind args =
     | Ind ind_kn ->
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
-       begin match otree with
-	     | Some tree ->
-		begin match dest_recarg tree with
-		      | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
-				    build_recargs_nested ienv tree (ind_kn, largs)
-		      | _ -> mk_norec
-		end
+       begin match dest_recarg tree with
+	     | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+			   build_recargs_nested ienv tree (ind_kn, largs)
 	     | _ -> mk_norec
        end
     | err ->
@@ -672,10 +668,12 @@ let get_recargs_approx env tree ind args =
     let (env',_ as ienv') = ienv_push_inductive ienv ((mind,u),lpar) in
     (* Parameters expressed in env' *)
     let lpar' = List.map (lift auxntyp) lpar in
-    (* In case of mutual inductive types, no need to keep the tree since nested
-       mutual inductive types are not supported. *)
-    let otree =
-      if Int.equal auxntyp 1 then Some (dest_subterms tree) else None
+    (* In case of mutual inductive types, we use the recargs tree which was
+    computed statically. This is fine because nested inductive types with
+    mutually recursive containers are not supported. *)
+    let trees =
+      if Int.equal auxntyp 1 then [|dest_subterms tree|]
+      else Array.map (fun mip -> dest_subterms mip.mind_recargs) mib.mind_packets
     in
     let mk_irecargs j specif =
       (* The nested inductive type with parameters removed *)
@@ -685,10 +683,7 @@ let get_recargs_approx env tree ind args =
 	 let c' = hnf_prod_applist env' c lpar' in
 	 (* skip non-recursive parameters *)
 	 let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in
-	 let otree =
-	   match otree with None -> None | Some tree -> Some tree.(k)
-	 in
-	 build_recargs_constructors ienv' otree c')
+	 build_recargs_constructors ienv' trees.(j).(k) c')
 	auxlcvect
       in
       mk_paths (Imbr (mind,j)) paths
@@ -696,21 +691,20 @@ let get_recargs_approx env tree ind args =
     let irecargs = Array.mapi mk_irecargs mib.mind_packets in
     (Rtree.mk_rec irecargs).(i)
 
-  and build_recargs_constructors ienv otrees c =
-    let rec recargs_constr_rec (env,ra_env as ienv) otrees lrec c =
+  and build_recargs_constructors ienv trees c =
+    let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
       let x,largs = decompose_app (whd_betadeltaiota env c) in
 	match kind_of_term x with
 
           | Prod (na,b,d) ->
 	     let () = assert (List.is_empty largs) in
-             let recarg = build_recargs ienv (Option.map List.hd otrees) b in
+             let recarg = build_recargs ienv (List.hd trees) b in
              let ienv' = ienv_push_var ienv (na,b,mk_norec) in
-	     let otrees = Option.map List.tl otrees in
-             recargs_constr_rec ienv' otrees (recarg::lrec) d
+             recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d
           | hd ->
              List.rev lrec
     in
-    recargs_constr_rec ienv otrees [] c
+    recargs_constr_rec ienv trees [] c
   in
   (* starting with ra_env = [] seems safe because any unbounded Rel will be
   assigned Norec *)
-- 
cgit v1.2.3