diff options
| -rw-r--r-- | kernel/indtypes.ml | 13 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | library/indrec.ml | 44 | ||||
| -rw-r--r-- | library/indrec.mli | 16 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 4 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
6 files changed, 31 insertions, 52 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 359f92d4b..ab7263503 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -23,15 +23,6 @@ let mind_check_arities env mie = in List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds -let sort_of_arity env c = - let rec sort_of ar = - match whd_betadeltaiota env Evd.empty ar with - | DOP0 (Sort s) -> s - | DOP2 (Prod, _, DLAM (_, c)) -> sort_of c - | _ -> error "not an arity" - in - sort_of c - let allowed_sorts issmall isunit = function | Type _ -> [prop;spec;types] @@ -224,10 +215,12 @@ let cci_inductive env env_ar kind nparams finite inds cst = let one_packet i (id,ar,cnames,issmall,isunit,lc) = let recargs = listrec_mconstr env_ar ntypes nparams i lc in let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in - let kelim = allowed_sorts issmall isunit (sort_of_arity env ar.body) in + let (ar_sign,ar_sort) = splay_arity env Evd.empty ar.body in + let kelim = allowed_sorts issmall isunit ar_sort in { mind_consnames = Array.of_list cnames; mind_typename = id; mind_lc = lc; + mind_nrealargs = List.length ar_sign - nparams; mind_arity = ar; mind_kelim = kelim; mind_listrec = recargs; diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 421bc937c..1e675b2c0 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,8 +14,6 @@ open Environ val mind_check_arities : env -> mutual_inductive_entry -> unit -val sort_of_arity : env -> constr -> sorts - val cci_inductive : env -> env -> path_kind -> int -> bool -> (identifier * typed_type * identifier list * bool * bool * constr) list -> diff --git a/library/indrec.ml b/library/indrec.ml index f52960cab..409018287 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -38,14 +38,9 @@ let it_lambda_name env = (* (lc is the list of the constructors of ind) *) -let mis_make_case_com depopt env sigma mispec kinds = - let sp = mispec.mis_sp in - let tyi = mispec.mis_tyi in - let cl = mispec.mis_args in +let mis_make_case_com depopt env sigma mispec kind = let nparams = mis_nparams mispec in - let mip = mispec.mis_mip in - let mind = DOPN(MutInd(sp,tyi),cl) in - let kelim = mis_kelim mispec in + let mind = mkMutInd ((mispec.mis_sp,mispec.mis_tyi),mispec.mis_args) in let t = mis_arity mispec in let (lc,lct) = mis_type_mconstructs mispec in let lnames,sort = splay_prod env sigma t in @@ -54,21 +49,22 @@ let mis_make_case_com depopt env sigma mispec kinds = | None -> (sort<>DOP0(Sort(Prop Null))) | Some d -> d in - if not (List.exists (base_sort_cmp CONV kinds) kelim) then begin + if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then begin errorlabstrm "Case analysis" [< 'sTR (if dep then "Dependent" else "Non Dependent"); - 'sTR " case analysis on sort: "; print_sort kinds; 'fNL; - 'sTR "is not allowed for inductive definition: "; print_sp sp >] + 'sTR " case analysis on sort: "; print_sort kind; 'fNL; + 'sTR "is not allowed for inductive definition: "; + print_sp mispec.mis_sp >] end; let lnamesar,lnamespar = list_chop (List.length lnames - nparams) lnames in let lgar = List.length lnamesar in let ar = hnf_prod_appvect env sigma "make_case_dep" t (rel_vect 0 nparams) in let typP = if dep then - make_arity_dep env sigma (DOP0(Sort kinds)) ar + make_arity_dep env sigma (DOP0(Sort kind)) ar (appvect (mind,rel_vect 0 nparams)) else - make_arity_nodep env sigma (DOP0(Sort kinds)) ar + make_arity_nodep env sigma (DOP0(Sort kind)) ar in let rec add_branch k = if k = nconstr then @@ -77,12 +73,9 @@ let mis_make_case_com depopt env sigma mispec kinds = (appvect (mind, (Array.append (rel_vect (nconstr+lgar+1) nparams) (rel_vect 0 lgar))), - mkMutCaseA (ci_of_mind mind) - (Rel (nconstr+lgar+2)) + mkMutCaseA (make_default_case_info mispec) + (Rel (nconstr+lgar+2)) (Rel 1) - (* (appvect (mind, - (Array.append (rel_vect (nconstr+lgar+2) nparams) - (rel_vect 1 lgar)))) *) (rel_vect (lgar+1) nconstr))) (lift_context (nconstr+1) lnamesar) else @@ -97,9 +90,9 @@ let mis_make_case_com depopt env sigma mispec kinds = in it_lambda_name env (make_lambda_string "P" typP (add_branch 0)) lnamespar -let make_case_com depopt env sigma ity kinds = +let make_case_com depopt env sigma ity kind = let mispec = lookup_mind_specif ity env in - mis_make_case_com depopt env sigma mispec kinds + mis_make_case_com depopt env sigma mispec kind let make_case_dep sigma = make_case_com (Some true) sigma let make_case_nodep sigma = make_case_com (Some false) sigma @@ -227,8 +220,7 @@ let mis_make_indrec env sigma listdepkind mispec = let recargsvec = mis_recargs mispec in let ntypes = mis_ntypes mispec in let mind_arity = mis_arity mispec in - let (lnames, ckind) = splay_prod env sigma mind_arity in - let kind = destSort ckind in + let (lnames, kind) = splay_arity env sigma mind_arity in let lnamespar = list_lastn nparams lnames in let listdepkind = if listdepkind = [] then @@ -248,10 +240,10 @@ let mis_make_indrec env sigma listdepkind mispec = in assign nrec listdepkind in - let make_one_rec p = - let makefix nbconstruct = - let rec mrec i ln ltyp ldef = function - | (mispeci,dep,_)::rest -> + let make_one_rec p = + let makefix nbconstruct = + let rec mrec i ln ltyp ldef = function + | (mispeci,dep,_)::rest -> let tyi = mispeci.mis_tyi in let mind = DOPN(MutInd (mispeci.mis_sp,tyi),mispeci.mis_args) in let (_,lct) = mis_type_mconstructs mispeci in @@ -278,7 +270,7 @@ let mis_make_indrec env sigma listdepkind mispec = (lambda_create env (appvect (mind,(Array.append (rel_vect decf nparams) (rel_vect 0 nar))), - mkMutCaseA (ci_of_mind mind) + mkMutCaseA (make_default_case_info mispec) (Rel (decf-nrec+j+1)) (Rel 1) branches)) (lift_context nrec lnames) in diff --git a/library/indrec.mli b/library/indrec.mli index f458c7a9e..9ef3df716 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -36,23 +36,23 @@ val transform_rec : env -> 'c evar_map -> (constr array) -> (constr * constr) -> constr i*) +(* val is_mutind : env -> 'a evar_map -> constr -> bool - -(* In [inductive * constr list * constr list], the second argument is - the list of global parameters and the third the list of real args *) - +*) +(* Inutilisé val pred_case_ml : env -> 'c evar_map -> bool -> constr * (inductive * constr list * constr list) -> constr array -> int * constr ->constr +*) +(* In [inductive * constr list * constr list], the second argument is + the list of global parameters and the third the list of real args *) val pred_case_ml_onebranch : env ->'c evar_map -> bool -> constr * (inductive * constr list * constr list) -> int * constr * constr -> constr +(* Obsolète ? val make_case_ml : bool -> constr -> constr -> case_info -> constr array -> constr +*) - -(*s Auxiliary functions. TODO: les déplacer ailleurs. *) - -val prod_create : env -> constr * constr -> constr diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index c3f7d8822..ec4326565 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 8c93eecd9..c31691046 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array |