diff options
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 120 |
1 files changed, 61 insertions, 59 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 4c9b3d61..de57c50a 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -22,13 +22,11 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPself uid -> "self("^string_of_msid uid^")" - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_mbid uid - | MPself uid -> string_of_msid uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l let string_of_mp mp = @@ -38,8 +36,9 @@ let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) let prcon c = - let (mp,_,l) = repr_con c in - str(string_of_mp mp ^ "." ^ string_of_label l) + let ck = canonical_con c in + let uk = user_con c in + if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. Could be refined more... *) @@ -119,23 +118,24 @@ let is_small_constr infos = List.for_all (fun s -> is_small_sort s) infos let is_logic_constr infos = List.for_all (fun s -> is_logic_sort s) infos (* An inductive definition is a "unit" if it has only one constructor - and that all arguments expected by this constructor are - logical, this is the case for equality, conjunction of logical properties + and that all arguments expected by this constructor are + logical, this is the case for equality, conjunction of logical properties *) let is_unit constrsinfos = match constrsinfos with (* One info = One constructor *) - | [|constrinfos|] -> is_logic_constr constrinfos + | [|constrinfos|] -> is_logic_constr constrinfos | [||] -> (* type without constructors *) true | _ -> false let small_unit constrsinfos = - let issmall = array_for_all is_small_constr constrsinfos + let issmall = array_for_all is_small_constr constrsinfos and isunit = is_unit constrsinfos in issmall, isunit (* check information related to inductive arity *) let typecheck_arity env params inds = let nparamargs = rel_context_nhyps params in + let nparamdecls = rel_context_length params in let check_arity arctxt = function Monomorphic mar -> let ar = mar.mind_user_arity in @@ -154,8 +154,12 @@ let typecheck_arity env params inds = (* Arities (with params) are typed-checked here *) let arity = check_arity ar_ctxt ind.mind_arity in (* mind_nrealargs *) - if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then + let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in + if ind.mind_nrealargs <> nrealargs then failwith "bad number of real inductive arguments"; + let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in + if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then + failwith "bad length of real inductive arguments signature"; (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an @@ -273,20 +277,20 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err ntyp env0 nbpar c err = +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 match err with - | LocalNonPos kt -> + | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',Rel (kt+nbpar)))) - | LocalNotEnoughArgs kt -> - raise (InductiveError + | LocalNotEnoughArgs kt -> + raise (InductiveError (NotEnoughArgs (env,c',Rel (kt+nbpar)))) | LocalNotConstructor -> - raise (InductiveError + raise (InductiveError (NotConstructor (env,c',Rel (ntyp+nbpar)))) | LocalNonPar (n,l) -> - raise (InductiveError + raise (InductiveError (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) let failwith_non_pos n ntypes c = @@ -307,7 +311,7 @@ let failwith_non_pos_list n ntypes l = 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 + if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); let (lpar,largs') = array_chop nparams largs in let nhyps = List.length hyps in @@ -319,18 +323,18 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; - if not (array_for_all (noccur_between n ntypes) largs') then + if not (array_for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' (* Arguments of constructor: check the number of recursive parameters nrecp. - the first parameters which are constant in recursive arguments - n is the current depth, nmr is the maximum number of possible + the first parameters which are constant in recursive arguments + n is the current depth, nmr is the maximum number of possible recursive parameters *) -let check_rec_par (env,n,_,_) hyps nrecp largs = +let check_rec_par (env,n,_,_) hyps nrecp largs = let (lpar,_) = list_chop nrecp largs in - let rec find index = - function + let rec find index = + function | ([],_) -> () | (_,[]) -> failwith "number of recursive parameters cannot be greater than the number of parameters." @@ -347,14 +351,14 @@ let lambda_implicit_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 npars = 0 then +let abstract_mind_lc env ntyps npars lc = + if npars = 0 then lc - else - let make_abs = + else + let make_abs = list_tabulate - (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps - in + (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps + in Array.map (substl make_abs) lc (* [env] is the typing environment @@ -362,7 +366,7 @@ let abstract_mind_lc env ntyps npars lc = [ntypes] is the number of inductive types in the definition (i.e. range of inductives is [n; n+ntypes-1]) [lra] is the list of recursive tree of each variable - *) + *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) @@ -372,7 +376,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let env' = push_rel (Anonymous,None, hnf_prod_applist env (type_of_inductive env specif) lpar) env in - let ra_env' = + 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 *) @@ -384,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) - let rec check_pos (env, n, ntypes, ra_env as ienv) c = + let rec check_pos (env, n, ntypes, ra_env as ienv) c = let x,largs = decompose_app (whd_betadeltaiota env c) in match x with | Prod (na,b,d) -> @@ -395,7 +399,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = check_pos (ienv_push_var ienv (na, b, mk_norec)) d) | Rel k -> (try - let (ra,rarg) = List.nth ra_env (k-1) in + let (ra,rarg) = List.nth ra_env (k-1) in (match ra with Mrec _ -> check_rec_par ienv hyps nrecp largs | _ -> ()); @@ -408,9 +412,9 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = parameter, then we have an imbricated type *) if List.for_all (noccur_between n ntypes) largs then mk_norec else check_positive_imbr ienv (ind_kn, largs) - | err -> + | err -> if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + List.for_all (noccur_between n ntypes) largs then mk_norec else failwith_non_pos_list n ntypes (x::largs) @@ -419,14 +423,14 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mib.mind_nparams_rec in let (lpar,auxlargs) = - try list_chop auxnpar largs - with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in + try list_chop auxnpar largs + with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in (* If the inductive appears in the args (non params) then the definition is not positive. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then raise (IllFormedInd (LocalNonPos n)); (* We do not deal with imbricated mutual inductive types *) - let auxntyp = mib.mind_ntypes in + let auxntyp = mib.mind_ntypes in if 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 @@ -435,30 +439,30 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = 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 = + let irecargs = (* fails if the inductive type occurs non positively *) - (* when substituted *) - Array.map - (function c -> - let c' = hnf_prod_applist env' c lpar' in - check_constructors ienv' false c') - auxlcvect in + (* when substituted *) + Array.map + (function c -> + let c' = hnf_prod_applist env' c lpar' in + check_constructors ienv' false c') + auxlcvect in (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_constructors ienv check_head c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = + the ith type *) + + 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 x with - | Prod (na,b,d) -> + | Prod (na,b,d) -> assert (largs = []); - let recarg = check_pos ienv b in + 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-1) then @@ -477,7 +481,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let _,rawc = mind_extract_params lparams c in try check_constructors ienv true rawc - with IllFormedInd err -> + with IllFormedInd err -> explain_ind_err (ntypes-i) env lparams c err) indlc in mk_paths (Mrec i) irecargs @@ -500,9 +504,9 @@ let check_positivity env_ar params nrecp inds = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - check_positivity_one ienv params nrecp i mip.mind_nf_lc + check_positivity_one ienv params nrecp i mip.mind_nf_lc in - let irecargs = Array.mapi check_one inds in + let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp @@ -510,7 +514,7 @@ let check_positivity env_ar params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose msgnl (str " checking ind: " ++ prkn kn); + Flags.if_verbose msgnl (str " checking ind: " ++ pr_mind kn); (* check mind_constraints: should be consistent with env *) let env = add_constraints mib.mind_constraints env in (* check mind_record : TODO ? check #constructor = 1 ? *) @@ -535,8 +539,6 @@ let check_inductive env kn mib = (* check mind_nparams_rec: positivity condition *) check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) - if mib.mind_equiv <> None then - msg_warning (str"TODO: mind_equiv not checked"); (* Now we can add the inductive *) add_mind kn mib env |