diff options
| -rw-r--r-- | kernel/indtypes.ml | 20 | ||||
| -rw-r--r-- | kernel/inductive.ml | 169 | ||||
| -rw-r--r-- | kernel/inductive.mli | 3 | ||||
| -rw-r--r-- | lib/rtree.ml | 20 | ||||
| -rw-r--r-- | lib/rtree.mli | 2 |
5 files changed, 175 insertions, 39 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f79d16c02f..6e87a04446 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -431,24 +431,6 @@ if Int.equal nmr 0 then 0 else | _ -> k) in find 0 (n-1) (lpar,List.rev hyps) -let lambda_implicit_lift n a = - let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in - let implicit_sort = mkType (Universe.make level) in - let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in - iterate lambda_implicit n (lift n a) - -(* This removes global parameters of the inductive types in lc (for - nested inductive types only ) *) -let abstract_mind_lc env ntyps npars lc = - if Int.equal npars 0 then - lc - else - let make_abs = - List.init ntyps - (function i -> lambda_implicit_lift npars (mkRel (i+1))) - in - Array.map (substl make_abs) lc - (* [env] is the typing environment [n] is the dB of the last inductive type [ntypes] is the number of inductive types in the definition @@ -538,7 +520,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let auxntyp = mib.mind_ntypes in if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) - let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in + let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 24763b79e2..edaec5ff4f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -493,6 +493,23 @@ type subterm_spec = let eq_wf_paths = Rtree.equal Declareops.eq_recarg +let pp_recarg = function + | Norec -> Pp.str "Norec" + | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) + | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) + +let pp_wf_paths = Rtree.pp_tree pp_recarg + +let inter_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> Some r1 +| Mrec i1, Mrec i2 +| Imbr i1, Imbr i2 +| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None +| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| _ -> None + +let inter_wf_paths = Rtree.inter inter_recarg Norec + let spec_of_tree t = if eq_wf_paths t mk_norec then Not_subterm @@ -506,9 +523,15 @@ let subterm_spec_glb init = | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> - if eq_wf_paths t1 t2 then Subterm (size_glb a1 a2, t1) - (* branches do not return objects with same spec *) - else Not_subterm in + Pp.msg_info (Pp.str "t1 = "); + Pp.msg_info (pp_wf_paths t1); + Pp.msg_info (Pp.str "t2 = "); + Pp.msg_info (pp_wf_paths t2); + let r = inter_wf_paths t1 t2 in + Pp.msg_info (Pp.str "r = "); + Pp.msg_info (pp_wf_paths r); + Subterm (size_glb a1 a2, r) + in Array.fold_left glb2 init type guard_env = @@ -572,7 +595,6 @@ let lookup_subterms env ind = let (_,mip) = lookup_mind_specif env ind in mip.mind_recargs - let match_inductive ind ra = match ra with | (Mrec i | Imbr i) -> eq_ind ind i @@ -594,7 +616,7 @@ let branches_specif renv c_spec ci = Array.mapi (fun i nca -> (* i+1-th cstructor has arity nca *) let lvra = lazy - (match Lazy.force c_spec with + (match Lazy.force c_spec with (* TODO: is this check necessary? *) Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) -> let vra = Array.of_list (dest_subterms t).(i) in assert (Int.equal nca (Array.length vra)); @@ -610,13 +632,122 @@ let check_inductive_codomain env p = let i,l' = decompose_app (whd_betadeltaiota env s) in isInd i +(* The following functions are almost duplicated from indtypes.ml, except +that they carry here a poorer environment (containing less information). *) +let ienv_push_var (env, lra) (x,a,ra) = +(push_rel (x,None,a) env, (Norec,ra)::lra) + +let ienv_push_inductive (env, ra_env) ((mi,u),lpar) = + let specif = (lookup_mind_specif env mi, u) in + let env' = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env specif) lpar) env in + let ra_env' = + (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: + List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + (* New index of the inductive types *) + (env', ra_env') + +let rec ienv_decompose_prod (env,_ as ienv) n c = + if Int.equal n 0 then (ienv,c) else + let c' = whd_betadeltaiota env c in + match kind_of_term c' with + Prod(na,a,b) -> + let ienv' = ienv_push_var ienv (na,a,mk_norec) in + ienv_decompose_prod ienv' (n-1) b + | _ -> assert false + +let lambda_implicit_lift n a = + let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in + let implicit_sort = mkType (Universe.make level) in + let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in + iterate lambda_implicit n (lift n a) + +(* This removes global parameters of the inductive types in lc (for + nested inductive types only ) *) +let abstract_mind_lc ntyps npars lc = + if Int.equal npars 0 then + lc + else + let make_abs = + List.init ntyps + (function i -> lambda_implicit_lift npars (mkRel (i+1))) + in + Array.map (substl make_abs) lc + +(* [get_recargs_approx ind args] builds an approximation of the recargs tree for ind, +knowing args. All inductive types appearing in the type of constructors are +considered as nested. 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 ind args = + let rec build_recargs (env, ra_env as ienv) 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)) d + | Rel k -> + (* Free variable are allowed and assigned Norec *) + (try snd (List.nth ra_env (k-1)) + with Failure _ | Invalid_argument _ -> mk_norec) + | Ind ind_kn -> + (* We always consider that we have a potential nested inductive type *) + build_recargs_nested ienv (ind_kn, largs) + | err -> + mk_norec + + and build_recargs_nested (env,ra_env as ienv) ((mi,u), largs) = + let (mib,mip) = lookup_mind_specif env mi in + let auxnpar = mib.mind_nparams_rec in + let nonrecpar = mib.mind_nparams - auxnpar in + let (lpar,auxlargs) = List.chop auxnpar largs in + let auxntyp = mib.mind_ntypes in + (* The nested inductive type with parameters removed *) + let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in + (* Extends the environment with a variable corresponding to + the inductive def *) + let (env',_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in + (* Parameters expressed in env' *) + let lpar' = List.map (lift auxntyp) lpar in + let irecargs = + Array.map + (function c -> + let c' = hnf_prod_applist env' c lpar' in + (* skip non-recursive parameters *) + let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in + build_recargs_constructors ienv' c') + auxlcvect + in +(* let irecargs = Array.map snd irecargs_nmr in *) + (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) + + and build_recargs_constructors ienv c = + let rec recargs_constr_rec (env,ra_env as ienv) 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 b in + let ienv' = ienv_push_var ienv (na,b,mk_norec) in + recargs_constr_rec ienv' (recarg::lrec) d + | hd -> + List.rev lrec + in recargs_constr_rec ienv [] c + in + (* starting with ra_env = [] seems safe because any unbounded Rel will be + assigned Norec *) + build_recargs_nested (env,[]) (ind, args) + + let get_codomain_tree env p = let absctx, ar = dest_lam_assum env p in (* TODO: reduce or preserve lets? *) let arctx, s = dest_prod_assum env ar in (* TODO: check number of prods *) - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_betadeltaiota env s) in match kind_of_term i with | Ind i -> - let (_,mip) = lookup_mind_specif env i in Subterm(Strict,mip.mind_recargs) + let recargs = get_recargs_approx env i args in Subterm(Strict,recargs) | _ -> Not_subterm (* [subterm_specif renv t] computes the recursive structure of [t] and @@ -685,7 +816,7 @@ let rec subterm_specif renv stack t = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in - let spec,stack' = extract_stack stack in + let spec,stack' = extract_stack renv a stack in subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) @@ -701,9 +832,9 @@ and stack_element_specif = function |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h |SArg x -> x -and extract_stack = function - | [] -> Lazy.lazy_from_val Not_subterm , [] - | h::t -> stack_element_specif h, t +and extract_stack renv a = function + | [] -> Lazy.lazy_from_val Not_subterm , [] + | h::t -> stack_element_specif h, t (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm x = @@ -739,21 +870,23 @@ let filter_stack_domain env ci p stack = match stack, kind_of_term t with | elt :: stack', Prod (n,a,c0) -> let d = (n,None,a) in - let ty, _ = decompose_app a in (* TODO: reduce a? *) + let ty, args = decompose_app a in (* TODO: reduce a? *) let elt = match kind_of_term ty with - | Ind i -> - let (_,mip) = lookup_mind_specif env i in + | Ind ind -> let spec' = stack_element_specif elt in (* TODO: this is recomputed each time*) (match (Lazy.force spec') with (* TODO: are we forcing too much? *) | Not_subterm -> elt - | Subterm(_,path) -> - if eq_wf_paths path mip.mind_recargs then elt - else (SArg (lazy Not_subterm))) (* TODO: intersection *) + | Subterm(s,path) -> + let recargs = get_recargs_approx env ind args in + let path = inter_wf_paths path recargs in + SArg (lazy (Subterm(s,path)))) (* TODO: not really an SArg *) + (* TODO: what if Dead_code above? *) | _ -> (SArg (lazy Not_subterm)) in elt :: filter_stack (push_rel d env) c0 stack' + | [], _ -> [] (* TODO: remove after debugging *) | _,_ -> List.fold_right (fun _ l -> SArg (lazy Not_subterm) :: l) stack [] (* TODO: is it correct to empty the stack instead? *) in @@ -856,7 +989,7 @@ let check_one_fix renv recpos def = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in check_rec_call renv [] a ; - let spec, stack' = extract_stack stack in + let spec, stack' = extract_stack renv a stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 497c064172..05b0248b9e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -135,3 +135,6 @@ type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec +val lambda_implicit_lift : int -> Constr.constr -> Term.constr + +val abstract_mind_lc : int -> Int.t -> Constr.constr array -> Constr.constr array diff --git a/lib/rtree.ml b/lib/rtree.ml index 5806ebd000..3c900d0b4d 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -145,8 +145,24 @@ let equal cmp t t' = (** Deprecated alias *) let eq_rtree = equal -(** Tests if a given tree is infinite, i.e. has an branch of infinite length. - This correspond to a cycle when visiting the expanded tree. +(* Intersection of rtrees of same arity *) +let rec inter interlbl def t t' = + match t, t' with + | Param (i,j), Param (i',j') -> + assert (Int.equal i i' && Int.equal j j'); t + | Node (x, a), Node (x', a') -> + (match interlbl x x' with + | None -> mk_node def [||] + | Some x'' -> Node (x'', Array.map2 (inter interlbl def) a a')) + | Rec (i, a), Rec (i', a') -> + if Int.equal i i' then Rec(i, Array.map2 (inter interlbl def) a a') + else mk_node def [||] + | Rec _, _ -> inter interlbl def (expand t) t' + | _ , Rec _ -> inter interlbl def t (expand t') + | _ -> assert false + +(** Tests if a given tree is infinite, i.e. has a branch of infinite length. + This corresponds to a cycle when visiting the expanded tree. We use a specific comparison to detect already seen trees. *) let is_infinite cmp t = diff --git a/lib/rtree.mli b/lib/rtree.mli index c3ec3a0c51..b1cfc35bcc 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -66,6 +66,8 @@ val equiv : then by logical equivalence [Rtree.equiv eq eq] *) val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool +val inter : ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t + (** Iterators *) val map : ('a -> 'b) -> 'a t -> 'b t |