Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

3 files changed, 64 insertions, 35 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index a300af79..fcd69f26 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -429,7 +429,7 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
 let make_renv env minds recarg (kn,tyi) =
@@ -440,7 +440,7 @@ let make_renv env minds recarg (kn,tyi) =
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    genv = [Subterm(Large,mind_recvec.(tyi))] }
+    genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] }
 
 let push_var renv (x,ty,spec) =
   { renv with
@@ -452,30 +452,30 @@ let assign_var_spec renv (i,spec) =
   { renv with genv = list_assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
-  push_var renv (x,ty,Not_subterm)
+  push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
 
 (* Fetch recursive information about a variable p *)
 let subterm_var p renv =
-  try List.nth renv.genv (p-1)
+  try Lazy.force (List.nth renv.genv (p-1))
   with Failure _ | Invalid_argument _ -> Not_subterm
 
 (* Add a variable and mark it as strictly smaller with information [spec]. *)
 let add_subterm renv (x,a,spec) =
-  push_var renv (x,a,spec_of_tree spec)
+  push_var renv (x,a,lazy (spec_of_tree (Lazy.force spec)))
 
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { renv with
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { renv with
     env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 
 (******************************)
@@ -499,12 +499,44 @@ let lookup_subterms env ind =
 
 (*********************************)
 
+let match_trees t1 t2 =
+  let v1 = dest_subterms t1 in
+  let v2 = dest_subterms t2 in
+  array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2
+
+(* In {match c as z in ind y_s return P with |C_i x_s => t end}
+   [branches_specif renv c_spec ind] returns an array of x_s specs given
+   c_spec the spec of c. *)
+let branches_specif renv c_spec ind =
+  let (_,mip) = lookup_mind_specif renv.env ind in
+  let car = 
+    (* We fetch the regular tree associated to the inductive of the match.
+       This is just to get the number of constructors (and constructor
+       arities) that fit the match branches without forcing c_spec.
+       Note that c_spec might be more precise than [v] below, because of
+       nested inductive types. *)
+    let v = dest_subterms mip.mind_recargs in
+      Array.map List.length v in
+    Array.mapi
+      (fun i nca -> (* i+1-th cstructor has arity nca *)
+	 let lvra = lazy 
+	   (match Lazy.force c_spec with
+		Subterm (_,t) when match_trees mip.mind_recargs t ->
+		  let vra = Array.of_list (dest_subterms t).(i) in
+		  assert (nca = Array.length vra);
+		  Array.map spec_of_tree vra
+	      | Dead_code -> Array.create nca Dead_code
+	      | _ -> Array.create nca Not_subterm) in
+	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+      car
+
 (* Propagation of size information through Cases: if the matched
    object is a recursive subterm then compute the information
    associated to its own subterms.
    Rq: if branch is not eta-long, then the recursive information
    is not propagated to the missing abstractions *)
 let case_branches_specif renv c_spec ind lbr =
+  let vlrec = branches_specif renv c_spec ind in
   let rec push_branch_args renv lrec c =
     match lrec with
         ra::lr ->
@@ -516,17 +548,9 @@ let case_branches_specif renv c_spec ind lbr =
             | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
                 (renv,c'))
       | [] -> (renv, c) in
-  match c_spec with
-      Subterm (_,t) ->
-        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Dead_code ->
-        let t = dest_subterms (lookup_subterms renv.env ind) in
-        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
+  assert (Array.length vlrec = Array.length lbr);
+  array_map2 (push_branch_args renv) vlrec lbr
+ 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
@@ -541,14 +565,11 @@ let rec subterm_specif renv t =
     | Rel k -> subterm_var k renv
 
     | Case (ci,_,c,lbr) ->
-        if Array.length lbr = 0 then Dead_code
-        else
-          let c_spec = subterm_specif renv c in
-          let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
-          let stl  =
-            Array.map (fun (renv',br') -> subterm_specif renv' br')
-              lbr_spec in
-          subterm_spec_glb stl
+        let lbr_spec = case_subterm_specif renv ci c lbr in
+        let stl  =
+          Array.map (fun (renv',br') -> subterm_specif renv' br')
+            lbr_spec in
+        subterm_spec_glb stl
 
     | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
 (* when proving that the fixpoint f(x)=e is less than n, it is enough
@@ -571,7 +592,8 @@ let rec subterm_specif renv t =
               let renv' =
                 (* Why Strict here ? To be general, it could also be
                    Large... *)
-                assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
+                assign_var_spec renv'
+		  (nbfix-i, Lazy.lazy_from_val (Subterm(Strict,recargs))) in
               let decrArg = recindxs.(i) in
               let theBody = bodies.(i)   in
               let nbOfAbst = decrArg+1 in
@@ -582,7 +604,7 @@ let rec subterm_specif renv t =
                 if List.length l < nbOfAbst then renv''
                 else
                   let theDecrArg  = List.nth l decrArg in
-	          let arg_spec    = subterm_specif renv theDecrArg in
+	          let arg_spec    = lazy_subterm_specif renv theDecrArg in
                   assign_var_spec renv'' (1, arg_spec) in
 	      subterm_specif renv'' strippedBody)
 
@@ -596,7 +618,15 @@ let rec subterm_specif renv t =
     (* Other terms are not subterms *)
     | _ -> Not_subterm
 
+and lazy_subterm_specif renv t =
+  lazy (subterm_specif renv t)
 
+and case_subterm_specif renv ci c lbr =
+  if Array.length lbr = 0 then [||]
+  else
+    let c_spec = lazy_subterm_specif renv c in
+    case_branches_specif renv c_spec ci.ci_ind lbr
+ 
 (* Check term c can be applied to one of the mutual fixpoints. *)
 let check_is_subterm renv c =
   match subterm_specif renv c with
@@ -611,7 +641,7 @@ let error_illegal_rec_call renv fx arg =
   let (_,le_vars,lt_vars) =
     List.fold_left
       (fun (i,le,lt) sbt ->
-        match sbt with
+        match Lazy.force sbt with
             (Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
           | (Subterm(Large,_)) -> (i+1, i::le, lt)
           | _ -> (i+1, le ,lt))
@@ -665,8 +695,7 @@ let check_one_fix renv recpos def =
             List.iter (check_rec_call renv) (c_0::p::l);
             (* compute the recarg information for the arguments of
                each branch *)
-            let c_spec = subterm_specif renv c_0 in
-            let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
+            let lbr = case_subterm_specif renv ci c_0 lrest in
             Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
@@ -694,7 +723,7 @@ let check_one_fix renv recpos def =
                 (fun j body ->
                   if i=j then
                     let theDecrArg  = List.nth l decrArg in
-	            let arg_spec = subterm_specif renv theDecrArg in
+	            let arg_spec = lazy_subterm_specif renv theDecrArg in
 	            check_nested_fix_body renv' (decrArg+1) arg_spec body
                   else check_rec_call renv' body)
                 bodies
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 2708c2d8..d44d1556 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -77,9 +77,9 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
 val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec -> inductive ->
+val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive ->
   constr array -> (guard_env * constr) array
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 9c82285b..07718a09 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -131,7 +131,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+let unsafe_import file (dp,mb,depends,engmt) digest =
 (*  if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;