diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 19 | ||||
| -rw-r--r-- | kernel/declarations.mli | 12 | ||||
| -rw-r--r-- | kernel/environ.ml | 92 | ||||
| -rw-r--r-- | kernel/environ.mli | 14 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 291 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 1 | ||||
| -rw-r--r-- | kernel/inductive.ml | 235 | ||||
| -rw-r--r-- | kernel/sign.ml | 15 | ||||
| -rw-r--r-- | kernel/sign.mli | 1 |
9 files changed, 340 insertions, 340 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index a9b8737bb7..fca3e0a50c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -31,10 +31,23 @@ type constant_body = { information). *) type recarg = - | Param of int | Norec | Mrec of int - | Imbr of inductive * (recarg list) + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +let mk_norec = Rtree.mk_node Norec [||] + +let mk_paths r recargs = + Rtree.mk_node r + (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) + +let dest_recarg p = fst (Rtree.dest_node p) + +let dest_subterms p = + let (_,cstrs) = Rtree.dest_node p in + Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs (* [mind_typename] is the name of the inductive; [mind_arity] is the arity generalized over global parameters; [mind_lc] is the list @@ -54,7 +67,7 @@ type one_inductive_body = { mind_consnames : identifier array; mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; - mind_listrec : (recarg list) array; + mind_recargs : wf_paths; } type mutual_inductive_body = { diff --git a/kernel/declarations.mli b/kernel/declarations.mli index a9b8737bb7..8a03e1cda3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -31,10 +31,16 @@ type constant_body = { information). *) type recarg = - | Param of int | Norec | Mrec of int - | Imbr of inductive * (recarg list) + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +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 (* [mind_typename] is the name of the inductive; [mind_arity] is the arity generalized over global parameters; [mind_lc] is the list @@ -54,7 +60,7 @@ type one_inductive_body = { mind_consnames : identifier array; mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; - mind_listrec : (recarg list) array; + mind_recargs : wf_paths; } type mutual_inductive_body = { diff --git a/kernel/environ.ml b/kernel/environ.ml index 7e638f5175..94303bada1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -49,16 +49,23 @@ let universes env = env.env_universes let named_context env = env.env_named_context let rel_context env = env.env_rel_context -(* Construction functions. *) +(* Access functions. *) -let named_context_app f env = - { env with - env_named_context = f env.env_named_context } +let lookup_rel n env = + Sign.lookup_rel n env.env_rel_context -let push_named_decl d = named_context_app (add_named_decl d) -let push_named_assum (id,ty) = push_named_decl (id,None,ty) -let pop_named_decl id = named_context_app (pop_named_decl id) +let lookup_named id env = + Sign.lookup_named id env.env_named_context + +let lookup_constant sp env = + Spmap.find sp env.env_globals.env_constants + +let lookup_mind sp env = + Spmap.find sp env.env_globals.env_inductives +(* Construction functions. *) + +(* Rel context *) let rel_context_app f env = { env with env_rel_context = f env.env_rel_context } @@ -77,16 +84,6 @@ let reset_rel_context env = { env with env_rel_context = empty_rel_context } - - -let fold_named_context f env ~init = - snd (Sign.fold_named_context - (fun d (env,e) -> (push_named_decl d env, f env d e)) - (named_context env) ~init:(reset_context env,init)) - -let fold_named_context_reverse f ~init env = - Sign.fold_named_context_reverse f ~init:init (named_context env) - let push_rel d = rel_context_app (add_rel_decl d) let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rel_assum (id,ty) = push_rel (id,None,ty) @@ -102,6 +99,24 @@ let fold_rel_context f env ~init = (fun d (env,e) -> (push_rel d env, f env d e)) (rel_context env) ~init:(reset_rel_context env,init)) +(* Named context *) +let named_context_app f env = + { env with + env_named_context = f env.env_named_context } + +let push_named_decl d = named_context_app (add_named_decl d) +let push_named_assum (id,ty) = push_named_decl (id,None,ty) +let pop_named_decl id = named_context_app (pop_named_decl id) + +let fold_named_context f env ~init = + snd (Sign.fold_named_context + (fun d (env,e) -> (push_named_decl d env, f env d e)) + (named_context env) ~init:(reset_context env,init)) + +let fold_named_context_reverse f ~init env = + Sign.fold_named_context_reverse f ~init:init (named_context env) + +(* Universe constraints *) let set_universes g env = if env.env_universes == g then env else { env with env_universes = g } @@ -111,7 +126,12 @@ let add_constraints c env = else { env with env_universes = merge_constraints c env.env_universes } +(* Global constants *) let add_constant sp cb env = + let _ = + try + let _ = lookup_constant sp env in failwith "already declared constant" + with Not_found -> () in let new_constants = Spmap.add sp cb env.env_globals.env_constants in let new_locals = (Constant,sp)::env.env_globals.env_locals in let new_globals = @@ -120,7 +140,12 @@ let add_constant sp cb env = env_locals = new_locals } in { env with env_globals = new_globals } +(* Mutual Inductives *) let add_mind sp mib env = + let _ = + try + let _ = lookup_mind sp env in failwith "already defined inductive" + with Not_found -> () in let new_inds = Spmap.add sp mib env.env_globals.env_inductives in let new_locals = (Inductive,sp)::env.env_globals.env_locals in let new_globals = @@ -129,20 +154,6 @@ let add_mind sp mib env = env_locals = new_locals } in { env with env_globals = new_globals } -(* Access functions. *) - -let lookup_rel n env = - Sign.lookup_rel n env.env_rel_context - -let lookup_named id env = - Sign.lookup_named id env.env_named_context - -let lookup_constant sp env = - Spmap.find sp env.env_globals.env_constants - -let lookup_mind sp env = - Spmap.find sp env.env_globals.env_inductives - (* Lookup of section variables *) let lookup_constant_variables c env = let cmap = lookup_constant c env in @@ -208,13 +219,13 @@ let keep_hyps env needed = (* Constants *) -(* Not taking opacity into account *) -let defined_constant env sp = - match (lookup_constant sp env).const_body with - Some _ -> true - | None -> false +let opaque_constant env sp = (lookup_constant sp env).const_opaque + +(* constant_type gives the type of a constant *) +let constant_type env sp = + let cb = lookup_constant sp env in + cb.const_type -(* Taking opacity into account *) type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result @@ -233,7 +244,7 @@ let constant_opt_value env cst = (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant env cst = try let _ = constant_value env cst in true - with NotEvaluableConst _ -> false + with Not_found | NotEvaluableConst _ -> false (* A local const is evaluable if it is defined and not opaque *) let evaluable_named_decl env id = @@ -252,11 +263,6 @@ let evaluable_rel_decl env n = with Not_found -> false -(* constant_type gives the type of a constant *) -let constant_type env sp = - let cb = lookup_constant sp env in - cb.const_type - (*s Modules (i.e. compiled environments). *) type compiled_env = { diff --git a/kernel/environ.mli b/kernel/environ.mli index 9a00f053ac..ecaa4d1082 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -71,14 +71,20 @@ val add_mind : (* raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> rel_declaration +val evaluable_rel_decl : env -> int -> bool + (* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) val lookup_named : variable -> env -> named_declaration +val evaluable_named_decl : env -> variable -> bool + (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) val lookup_constant : constant -> env -> constant_body +val evaluable_constant : env -> constant -> bool + (*s [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no body and [Not_found] if it does not exist in [env] *) @@ -102,14 +108,6 @@ val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context -(* A constant is defined when it has a body (theorems do) *) -val defined_constant : env -> constant -> bool -(* A constant is evaluable when delta reduction applies (theorems don't) *) -val evaluable_constant : env -> constant -> bool - -val evaluable_named_decl : env -> variable -> bool -val evaluable_rel_decl : env -> int -> bool - (*s Modules. *) type compiled_env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 746a942de9..96c2eaf987 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -27,7 +27,6 @@ open Typeops (*s Declaration. *) type one_inductive_entry = { - mind_entry_nparams : int; mind_entry_params : (identifier * local_entry) list; mind_entry_typename : identifier; mind_entry_arity : constr; @@ -90,12 +89,6 @@ let mind_check_names mie = vue since inductive and constructors are not referred to by their name, but only by the name of the inductive packet and an index. *) -(* [mind_extract_params mie] extracts the params from an inductive types - declaration, and checks that they are all present (and all the same) - for all the given types. *) - -let mind_extract_params = decompose_prod_n_assum - let mind_check_arities env mie = let check_arity id c = if not (is_arity env c) then @@ -201,7 +194,7 @@ let infer_constructor_packet env_ar params arsort vc = (* Type-check an inductive definition. Does not check positivity conditions. *) -let type_inductive env mie = +let typecheck_inductive env mie = if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration"; (* Check unicity of names *) mind_check_names mie; @@ -242,35 +235,19 @@ let type_inductive env mie = let (_,arsort) = dest_arity env full_arity in let lc = ind.mind_entry_lc in let (issmall,isunit,lc',cst') = - infer_constructor_packet env_arities params arsort lc - in - let nparams = ind.mind_entry_nparams in + infer_constructor_packet env_arities params arsort lc in let consnames = ind.mind_entry_consnames in - let ind' = (params,nparams,id,full_arity,consnames,issmall,isunit,lc') + let ind' = (params,id,full_arity,consnames,issmall,isunit,lc') in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds params_arity_list ([],cst) in - (env_arities, inds, cst) + (env_arities, Array.of_list inds, cst) (***********************************************************************) (***********************************************************************) -let all_sorts = [InProp;InSet;InType] -let impredicative_sorts = [InProp;InSet] -let logical_sorts = [InProp] - -let allowed_sorts issmall isunit = function - | Type _ -> all_sorts - | Prop Pos -> - if issmall then all_sorts - else impredicative_sorts - | Prop Null -> -(* Added InType which is derivable :when the type is unit and small *) - if isunit then - if issmall then all_sorts - else impredicative_sorts - else logical_sorts +(* Positivity *) type ill_formed_ind = | LocalNonPos of int @@ -280,6 +257,12 @@ type ill_formed_ind = exception IllFormedInd of ill_formed_ind +(* [mind_extract_params mie] extracts the params from an inductive types + declaration, and checks that they are all present (and all the same) + for all the given types. *) + +let mind_extract_params = decompose_prod_n_assum + let explain_ind_err ntyp env0 nbpar c err = let (lpar,c') = mind_extract_params nbpar c in let env = push_rel_context lpar env0 in @@ -305,7 +288,8 @@ let failwith_non_pos_vect n ntypes v = anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v" (* Check the inductive type is called with the expected parameters *) -let check_correct_par env hyps nparams ntypes n l largs = +let check_correct_par (env,n,ntypes,_) hyps l largs = + let nparams = rel_context_nhyps hyps in let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); @@ -322,7 +306,8 @@ let check_correct_par env hyps nparams ntypes n l largs = if not (array_for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' -(* This removes global parameters of the inductive types in lc *) +(* This removes global parameters of the inductive types in lc (for + nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = if npars = 0 then lc @@ -333,50 +318,58 @@ let abstract_mind_lc env ntyps npars lc = in Array.map (substl make_abs) lc +let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = + (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + +let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = + let auxntyp = 1 in + let env' = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env mi) lpar) env in + let ra_env' = + (Imbr mi,Rtree.mk_param 0) :: + List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + (* New index of the inductive types *) + let newidx = n + auxntyp in + (env', newidx, ntypes, ra_env') + (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity env ntypes hyps nparams i indlc = - let nhyps = List.length hyps in +let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = + let nparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) - let rec check_pos env n c = + let rec check_pos (env, n, ntypes, 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 (largs = []); if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n)); - check_pos (push_rel (na, None, b) env) (n+1) d + check_pos (ienv_push_var ienv (na, b, mk_norec)) d | Rel k -> - if k >= n && k<n+ntypes then begin - check_correct_par env hyps nparams ntypes n (k-n+1) largs; - Mrec(n+ntypes-k-1) - end else if List.for_all (noccur_between n ntypes) largs then - if (n-nhyps) <= k & k <= (n-1) - then Param(n-1-k) - else Norec - else - raise (IllFormedInd (LocalNonPos n)) + let (ra,rarg) = + try List.nth ra_env (k-1) + with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in + (match ra with + Mrec _ -> check_correct_par ienv hyps (k-n+1) largs + | _ -> + if not (List.for_all (noccur_between n ntypes) largs) + then raise (IllFormedInd (LocalNonPos n))); + rarg | Ind ind_sp -> - (* If the inductive type being defined or a parameter appears as + (* If the inductive type being defined appears in a parameter, then we have an imbricated type *) - if List.for_all (noccur_between n ntypes) largs then - (* If parameters are passed but occur negatively, then - the argument is considered non recursive *) - if List.for_all (noccur_between (n-nhyps) nhyps) largs - then Norec - else - try check_positive_imbr env n ind_sp largs - with IllFormedInd _ -> Norec - else check_positive_imbr env n ind_sp largs + if List.for_all (noccur_between n ntypes) largs then mk_norec + else check_positive_imbr ienv (ind_sp, largs) | err -> if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs - then Norec + then mk_norec else raise (IllFormedInd (LocalNonPos n)) (* accesses to the environment are not factorised, but does it worth it? *) - and check_positive_imbr env n mi largs = + and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mip.mind_nparams in let (lpar,auxlargs) = @@ -386,114 +379,115 @@ let check_positivity env ntypes hyps nparams i indlc = definition is not positive. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then raise (IllFormedInd (LocalNonPos n)); - (* If the inductive type appears non positively in the - parameters then the def is not positive *) - let lrecargs = List.map (check_weak_pos env n) lpar in - let auxlc = mip.mind_nf_lc in - let auxntyp = mib.mind_ntypes in (* We do not deal with imbricated mutual inductive types *) + let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); - (* The abstract imbricated inductive type with parameters substituted *) - let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in + (* The nested inductive type with parameters removed *) + let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) - let env' = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env mi) lpar) env in - let newidx = n + auxntyp in - let _ = + let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in + (* Parameters expressed in env' *) + let lpar' = List.map (lift auxntyp) lpar in + let irecargs = (* fails if the inductive type occurs non positively *) (* when substituted *) Array.map (function c -> - let c' = hnf_prod_applist env c (List.map (lift auxntyp) lpar) in - check_construct env' false newidx c') + let c' = hnf_prod_applist env' c lpar' in + check_constructors ienv' false c') auxlcvect in - Imbr(mi,lrecargs) - - (* The function check_weak_pos is exactly the same as check_pos, but - with an extra case for traversing abstractions, like in Marseille's - contribution about bisimulations: - - CoInductive strong_eq:process->process->Prop:= - str_eq:(p,q:process)((a:action)(p':process)(transition p a p')-> - (Ex [q':process] (transition q a q')/\(strong_eq p' q')))-> - ((a:action)(q':process)(transition q a q')-> - (Ex [p':process] (transition p a p')/\(strong_eq p' q')))-> - (strong_eq p q). - - Abstractions may occur in imbricated recursive ocurrences, but I am - not sure if they make sense in a form of constructor. This is why I - chose to duplicated the code. Eduardo 13/7/99. *) - (* Since Lambda can no longer occur after a product or a Ind, - I have branched the remaining cases on check_pos. HH 28/1/00 *) - - and check_weak_pos env n c = - let x = whd_betadeltaiota env c in - match kind_of_term x with - (* The extra case *) - | Lambda (na,b,d) -> - if noccur_between n ntypes b - then check_weak_pos (push_rel (na,None,b) env) (n+1) d - else raise (IllFormedInd (LocalNonPos n)) - (******************) - | _ -> check_pos env n x + (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) (* check the inductive types occur positively in the products of C, if check_head=true, also check the head corresponds to a constructor of the ith type *) - and check_construct env check_head n c = - let rec check_constr_rec env lrec n c = + and check_constructors ienv check_head c = + let rec check_constr_rec (env,n,ntypes,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) -> assert (largs = []); - let recarg = check_pos env n b in - check_constr_rec (push_rel (na, None, b) env) - (recarg::lrec) (n+1) d + let recarg = check_pos ienv b in + let ienv' = ienv_push_var ienv (na,b,mk_norec) in + check_constr_rec ienv' (recarg::lrec) d | hd -> if check_head then - if hd = Rel (n+ntypes-i) then - check_correct_par env hyps nparams ntypes n (ntypes-i+1) largs + if hd = Rel (n+ntypes-i-1) then + check_correct_par ienv hyps (ntypes-i) largs else raise (IllFormedInd LocalNotConstructor) else if not (List.for_all (noccur_between n ntypes) largs) then raise (IllFormedInd (LocalNonPos n)); List.rev lrec - in check_constr_rec env [] n c + in check_constr_rec ienv [] c in - Array.map - (fun c -> - let c = body_of_type c in - let sign, rawc = mind_extract_params nhyps c in - let env' = push_rel_context sign env in - try - check_construct env' true (1+nhyps) rawc - with IllFormedInd err -> - explain_ind_err (ntypes-i+1) env nhyps c err) - indlc + mk_paths (Mrec i) + (Array.map + (fun c -> + let c = body_of_type c in + let sign, rawc = mind_extract_params nparams c in + let env' = push_rel_context sign env in + try + check_constructors ienv true rawc + with IllFormedInd err -> + explain_ind_err (ntypes-i) env nparams c err) + indlc) + +let check_positivity env_ar inds = + let ntypes = Array.length inds in + let lra_ind = + List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in + let check_one i (params,_,_,_,_,_,lc) = + let nparams = rel_context_length params in + let ra_env = + list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in + let ienv = (env_ar, 1+nparams, ntypes, ra_env) in + check_positivity_one ienv params i lc in + Rtree.mk_rec (Array.mapi check_one inds) + + +(***********************************************************************) +(***********************************************************************) +(* Build the inductive packet *) -let is_recursive listind = - let rec one_is_rec rvec = +(* Elimination sorts *) +let is_recursive = Rtree.is_infinite +(* let rec one_is_rec rvec = List.exists (function Mrec(i) -> List.mem i listind - | Imbr(_,lvec) -> one_is_rec lvec - | Norec -> false - | Param _ -> false) rvec + | Imbr(_,lvec) -> array_exists one_is_rec lvec + | Norec -> false) rvec in array_exists one_is_rec +*) + +let all_sorts = [InProp;InSet;InType] +let impredicative_sorts = [InProp;InSet] +let logical_sorts = [InProp] -(* Check positivity of an inductive definition *) -let cci_inductive env env_ar finite inds cst = - let ntypes = List.length inds in +let allowed_sorts issmall isunit = function + | Type _ -> all_sorts + | Prop Pos -> + if issmall then all_sorts + else impredicative_sorts + | Prop Null -> +(* Added InType which is derivable :when the type is unit and small *) + if isunit then + if issmall then all_sorts + else impredicative_sorts + else logical_sorts + +let build_inductive env env_ar finite inds recargs cst = + let ntypes = Array.length inds in (* Compute the set of used section variables *) let ids = - List.fold_left - (fun acc (_,_,_,ar,_,_,_,lc) -> + Array.fold_left + (fun acc (_,_,ar,_,_,_,lc) -> Idset.union (Environ.global_vars_set env (body_of_type ar)) (Array.fold_left (fun acc c -> @@ -503,37 +497,40 @@ let cci_inductive env env_ar finite inds cst = Idset.empty inds in let hyps = keep_hyps env ids in (* Check one inductive *) - let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) = - (* Check positivity *) - let recargs = check_positivity env_ar ntypes params nparams i lc in + let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg = (* Arity in normal form *) + let nparams = rel_context_length params in let (ar_sign,ar_sort) = dest_arity env ar in let nf_ar = if isArity (body_of_type ar) then ar else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in - (* Elimination sorts *) - let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in - let kelim = allowed_sorts issmall isunit ar_sort in (* Type of constructors in normal form *) let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in let nf_lc = if nf_lc = lc then lc else nf_lc in - (* Build the inductive *) - { mind_consnames = Array.of_list cnames; - mind_typename = id; - mind_user_lc = lc; - mind_nf_lc = nf_lc; + let carities = + Array.map + (fun (args,_) -> rel_context_length args - nparams) splayed_lc in + (* Elimination sorts *) + let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in + let kelim = allowed_sorts issmall isunit ar_sort in + (* Build the inductive packet *) + { mind_typename = id; + mind_nparams = rel_context_nhyps params; + mind_params_ctxt = params; mind_user_arity = ar; mind_nf_arity = nf_ar; mind_nrealargs = rel_context_length ar_sign - nparams; mind_sort = ar_sort; mind_kelim = kelim; - mind_listrec = recargs; - mind_nparams = nparams; - mind_params_ctxt = params } - in - let packets = Array.of_list (list_map_i one_packet 1 inds) in + mind_consnames = Array.of_list cnames; + mind_user_lc = lc; + mind_nf_lc = nf_lc; + mind_recargs = recarg; + } in + let packets = array_map2 build_one_packet inds recargs in + (* Build the mutual inductive *) { mind_ntypes = ntypes; mind_finite = finite; mind_hyps = hyps; @@ -545,7 +542,9 @@ let cci_inductive env env_ar finite inds cst = (***********************************************************************) let check_inductive env mie = - (* First type the inductive definition *) - let (env_arities, inds, cst) = type_inductive env mie in - (* Then check positivity *) - cci_inductive env env_arities mie.mind_entry_finite inds cst + (* First type-check the inductive definition *) + let (env_arities, inds, cst) = typecheck_inductive env mie in + (* Then check positivity conditions *) + let recargs = check_positivity env_arities inds in + (* Build the inductive packets *) + build_inductive env env_arities mie.mind_entry_finite inds recargs cst diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7e803b11e8..532471ebcd 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -52,7 +52,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]]; *) type one_inductive_entry = { - mind_entry_nparams : int; mind_entry_params : (identifier * local_entry) list; mind_entry_typename : identifier; mind_entry_arity : constr; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b45e501eb4..d98adbb37f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -304,23 +304,21 @@ type guard_env = (* inductive of recarg of each fixpoint *) inds : inductive array; (* the recarg information of inductive family *) - recvec : recarg list array array; + recvec : wf_paths array; (* dB of variables denoting subterms *) - lst : (int * (size * recarg list array)) list; + genv : (int * (size * wf_paths)) list; } -let lookup_recargs env ind = - let (mib,mip) = lookup_mind_specif env ind in - Array.map (fun mip -> mip.mind_listrec) mib.mind_packets - let make_renv env minds recarg (_,tyi as ind) = - let mind_recvec = lookup_recargs env ind in + let (mib,mip) = lookup_mind_specif env ind in + let mind_recvec = + Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in let lcx = mind_recvec.(tyi) in { env = env; rel_min = recarg+2; inds = minds; recvec = mind_recvec; - lst = [(1,(Large,mind_recvec.(tyi)))] } + genv = [(1,(Large,mind_recvec.(tyi)))] } let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) @@ -328,26 +326,27 @@ let push_var_renv renv (x,ty) = { renv with env = push_rel (x,None,ty) renv.env; rel_min = renv.rel_min+1; - lst = map_lift_fst_n 1 renv.lst } + genv = map_lift_fst_n 1 renv.genv } 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; - lst = map_lift_fst_n n renv.lst } + genv = map_lift_fst_n 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; - lst = map_lift_fst_n n renv.lst } + genv = map_lift_fst_n n renv.genv } (* Add a variable and mark it as strictly smaller with information [spec]. *) let add_recarg renv (x,a,spec) = let renv' = push_var_renv renv (x,a) in - { renv' with lst = (1,(Strict,spec))::renv'.lst } + if spec = mk_norec then renv' + else { renv' with genv = (1,(Strict,spec))::renv'.genv } (* Fetch recursive information about a variable *) let subterm_var p renv = @@ -355,7 +354,7 @@ let subterm_var p renv = | (a,ta)::l -> if a < p then findrec l else if a = p then Some ta else None | _ -> None in - findrec renv.lst + findrec renv.genv (******************************) @@ -373,38 +372,24 @@ let subterm_var p renv = correct envs and decreasing args. *) -let lookup_subterms env (_,i as ind) = - (lookup_recargs env ind).(i) - -let imbr_recarg_expand env (sp,i as ind_sp) lrc = - let recargs = lookup_subterms env ind_sp in - let rec imbr_recarg ra = - match ra with - | Mrec(j) -> Imbr((sp,j),lrc) - | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map imbr_recarg l) - | Norec -> Norec - | Param(k) -> List.nth lrc k in - Array.map (List.map imbr_recarg) recargs +let lookup_subterms env ind = + let (_,mip) = lookup_mind_specif env ind in + mip.mind_recargs -let case_branches_specif renv = +let case_branches_specif renv spec lc = let rec crec renv lrec c = let c' = strip_outer_cast c in match lrec, kind_of_term c' with | (ra::lr,Lambda (x,a,b)) -> - let renv' = - match ra with - Mrec(i) -> add_recarg renv (x,a,renv.recvec.(i)) - | Imbr(ind_sp,lrc) -> - let lc = imbr_recarg_expand renv.env ind_sp lrc in - add_recarg renv (x,a,lc) - | _ -> push_var_renv renv (x,a) in + let renv' = add_recarg renv (x,a,ra) in crec renv' lr b | (_,LetIn (x,c,a,b)) -> crec renv lrec (subst1 c b) (* Rq: if branch is not eta-long, then the recursive information is not propagated: *) - | (_,_) -> (renv,c') - in array_map2 (crec renv) + | (_,_) -> (renv,c') in + if spec = mk_norec then Array.map (fun c -> (renv,c)) lc + else array_map2 (crec renv) (dest_subterms spec) lc (*********************************) @@ -431,74 +416,70 @@ let inductive_of_fix env recarg body = - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta) - [None] otherwise *) -let subterm_specif renv c ind = - let rec crec renv c ind = - let f,l = decompose_app (whd_betadeltaiota renv.env c) in - match kind_of_term f with - | Rel k -> subterm_var k renv - - | Case (ci,_,c,lbr) -> - if Array.length lbr = 0 - (* New: if it is built by contadiction, it is OK *) - then Some (Strict,[||]) - else - let def = Array.create (Array.length lbr) [] in - let lcv = - match crec renv c ci.ci_ind with +let rec subterm_specif renv c ind = + let f,l = decompose_app (whd_betadeltaiota renv.env c) in + match kind_of_term f with + | Rel k -> subterm_var k renv + + | Case (ci,_,c,lbr) -> + if Array.length lbr = 0 + (* New: if it is built by contadiction, it is OK *) + then Some (Strict,mk_norec) + else + let lcv = + match subterm_specif renv c ci.ci_ind with Some (_,lr) -> lr - | None -> def in - let lbr' = case_branches_specif renv lcv lbr in - let stl = - Array.map (fun (renv',br') -> crec renv' br' ind) lbr' in - let stl0 = stl.(0) in - if array_for_all (fun st -> st=stl0) stl then stl0 - (* branches do not return objects with same spec *) - else None + | None -> mk_norec in + let lbr' = case_branches_specif renv lcv lbr in + let stl = + Array.map (fun (renv',br') -> subterm_specif renv' br' ind) lbr' in + let stl0 = stl.(0) in + if array_for_all (fun st -> st=stl0) stl then stl0 + (* branches do not return objects with same spec *) + else None - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> (* when proving that the fixpoint f(x)=e is less than n, it is enough to prove that e is less than n assuming f is less than n furthermore when f is applied to a term which is strictly less than n, one may assume that x itself is strictly less than n *) - let nbfix = Array.length typarray in - let recargs = lookup_subterms renv.env ind in - (* pushing the fixpoints *) - let renv' = push_fix_renv renv recdef in - let renv' = - { renv' with lst=(nbfix-i,(Strict,recargs))::renv'.lst } in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in - (* pushing the fix parameters *) - let renv'' = push_ctxt_renv renv' sign in - let renv'' = - { renv'' with - lst = - if List.length l < nbOfAbst then renv''.lst + let nbfix = Array.length typarray in + let recargs = lookup_subterms renv.env ind in + (* pushing the fixpoints *) + let renv' = push_fix_renv renv recdef in + let renv' = + { renv' with genv=(nbfix-i,(Strict,recargs))::renv'.genv } in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + { renv'' with + genv = + if List.length l < nbOfAbst then renv''.genv else let decrarg_ind = inductive_of_fix renv''.env decrArg theBody in let theDecrArg = List.nth l decrArg in try - match crec renv theDecrArg decrarg_ind with - (Some recArgsDecrArg) -> - (1,recArgsDecrArg) :: renv''.lst - | None -> renv''.lst - with Not_found -> renv''.lst } in - crec renv'' strippedBody ind + match subterm_specif renv theDecrArg decrarg_ind with + (Some recArgsDecrArg) -> + (1,recArgsDecrArg) :: renv''.genv + | None -> renv''.genv + with Not_found -> renv''.genv } in + subterm_specif renv'' strippedBody ind - | Lambda (x,a,b) -> - assert (l=[]); - crec (push_var_renv renv (x,a)) b ind - - (* A term with metas is considered OK *) - | Meta _ -> Some (Strict,lookup_subterms renv.env ind) - (* Other terms are not subterms *) - | _ -> None - in - crec renv c ind + | Lambda (x,a,b) -> + assert (l=[]); + subterm_specif (push_var_renv renv (x,a)) b ind + + (* A term with metas is considered OK *) + | Meta _ -> Some (Strict,lookup_subterms renv.env ind) + (* Other terms are not subterms *) + | _ -> None (* Propagation of size information through Cases: if the matched object is a recursive subterm then compute the information @@ -506,9 +487,7 @@ let subterm_specif renv c ind = let spec_subterm_large renv c ind = match subterm_specif renv c ind with Some (_,lr) -> lr - | None -> - let nb = Array.length (lookup_subterms renv.env ind) in - Array.create nb [] + | None -> mk_norec (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm renv c ind = @@ -632,7 +611,7 @@ let check_one_fix renv recpos def = and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call - { renv with lst=(1,recArgsDecrArg)::renv.lst } body + { renv with genv=(1,recArgsDecrArg)::renv.genv } body else match kind_of_term body with | Lambda (x,a,b) -> @@ -707,22 +686,17 @@ exception CoFixGuardError of guard_error let anomaly_ill_typed () = anomaly "check_one_cofix: too many arguments applied to constructor" +let rec codomain_is_coind env c = + let b = whd_betadeltaiota env c in + match kind_of_term b with + | Prod (x,a,b) -> + codomain_is_coind (push_rel (x, None, a) env) b + | _ -> + (try find_coinductive env b + with Not_found -> + raise (CoFixGuardError (CodomainNotInductiveType b))) let check_one_cofix env nbfix def deftype = - let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in - match kind_of_term b with - | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b - | _ -> - (try find_coinductive env b - with Not_found -> - raise (CoFixGuardError (CodomainNotInductiveType b))) - in - let (mind, _) = codomain_is_coind env deftype in - let (sp,tyi) = mind in - let lvlra = lookup_recargs env (sp,tyi) in - let vlra = lvlra.(tyi) in let rec check_rec_call env alreadygrd n vlra t = if noccur_with_meta n nbfix t then true @@ -749,29 +723,20 @@ let check_one_cofix env nbfix def deftype = let mI = inductive_of_constructor cstr_sp in let (mib,mip) = lookup_mind_specif env mI in let _,realargs = list_chop mip.mind_nparams args in - let rec process_args_of_constr l lra = - match l with - | [] -> true - | t::lr -> - (match lra with - | [] -> anomaly_ill_typed () - | (Mrec i)::lrar -> - let newvlra = lvlra.(i) in - (check_rec_call env true n newvlra t) && - (process_args_of_constr lr lrar) - - | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> - let lc = imbr_recarg_expand env ind_sp lrc in - check_rec_call env true n lc t & - process_args_of_constr lr lrar - - | _::lrar -> - if (noccur_with_meta n nbfix t) - then (process_args_of_constr lr lrar) - else raise (CoFixGuardError - (RecCallInNonRecArgOfConstructor t))) - in (process_args_of_constr realargs lra) - + let rec process_args_of_constr = function + | (t::lr), (rar::lrar) -> + if rar = mk_norec then + if noccur_with_meta n nbfix t + then process_args_of_constr (lr, lrar) + else raise (CoFixGuardError + (RecCallInNonRecArgOfConstructor t)) + else + let spec = dest_subterms rar in + check_rec_call env true n spec t && + process_args_of_constr (lr, lrar) + | [],_ -> true + | _ -> anomaly_ill_typed () + in process_args_of_constr (realargs, lra) | Lambda (x,a,b) -> assert (args = []); @@ -808,10 +773,10 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (RecCallInCasePred c)) - | _ -> raise (CoFixGuardError NotGuardedForm) - - in - check_rec_call env false 1 vlra def + | _ -> raise (CoFixGuardError NotGuardedForm) in + let (mind, _) = codomain_is_coind env deftype in + let vlra = lookup_subterms env mind in + check_rec_call env false 1 (dest_subterms vlra) def (* The function which checks that the whole block of definitions satisfies the guarded condition *) diff --git a/kernel/sign.ml b/kernel/sign.ml index 20bd1e03a6..e1c9fbe4b0 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -20,13 +20,19 @@ type named_context = named_declaration list let empty_named_context = [] -let add_named_decl d sign = d::sign let rec lookup_named id = function | (id',_,_ as decl) :: _ when id=id' -> decl | _ :: sign -> lookup_named id sign | [] -> raise Not_found + +let add_named_decl (id,_,_ as d) sign = + try + let _ = lookup_named id sign in + failwith ("identifier "^string_of_id id^" already defined") + with _ -> d::sign + let named_context_length = List.length let pop_named_decl id = function @@ -66,6 +72,13 @@ let lookup_rel n sign = let rel_context_length = List.length +let rel_context_nhyps hyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 hyps + let fold_rel_context f l ~init:x = List.fold_right f l x let fold_rel_context_reverse f ~init:x l = List.fold_left f x l diff --git a/kernel/sign.mli b/kernel/sign.mli index 6667b598c3..a35f61d229 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -46,6 +46,7 @@ val add_rel_decl : rel_declaration -> rel_context -> rel_context val lookup_rel : int -> rel_context -> rel_declaration val rel_context_length : rel_context -> int +val rel_context_nhyps : rel_context -> int val push_named_to_rel_context : named_context -> rel_context -> rel_context |