From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- checker/inductive.ml | 93 +++++++++++++++++++++++++++++++++----------------- checker/inductive.mli | 4 +-- checker/safe_typing.ml | 2 +- 3 files changed, 64 insertions(+), 35 deletions(-) (limited to 'checker') 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; -- cgit v1.2.3