From 296faec482d17f9bfdc419f79ed565ecd8035e60 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 7 Feb 2002 16:07:34 +0000 Subject: petit nettoyage de kernel/inductive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 12 ++++--- pretyping/cases.mli | 2 +- pretyping/detyping.ml | 65 ++++++++++++++++++------------------ pretyping/detyping.mli | 9 +++-- pretyping/indrec.ml | 82 ++++++++++++++++++++++------------------------ pretyping/inductiveops.ml | 49 ++++++++++++++++----------- pretyping/inductiveops.mli | 29 ++++++++++------ pretyping/pretyping.ml | 27 ++++++++------- pretyping/retyping.ml | 2 +- pretyping/termops.ml | 20 +++++------ pretyping/termops.mli | 8 ++--- 11 files changed, 165 insertions(+), 140 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4d8c03d3e..41d6941a9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -92,7 +92,8 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr = in crec env (List.rev cstr.cs_args,recargs) -let branch_scheme env isevars isrec ((ind,params) as indf) = +let branch_scheme env isevars isrec indf = + let (ind,params) = dest_ind_family indf in let (mib,mip) = Inductive.lookup_mind_specif env ind in let cstrs = get_constructors env indf in if isrec then @@ -139,7 +140,7 @@ exception NotInferable of ml_case_error let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = - let (ind,params) = indf in + let (ind,params) = dest_ind_family indf in let (mib,mip) = Inductive.lookup_mind_specif env ind in let recargs = mip.mind_listrec in if Array.length recargs = 0 then raise (NotInferable MlCaseAbsurd); @@ -449,12 +450,12 @@ let unify_tomatch_with_patterns isevars env typ = function try IsInd (typ,find_rectype env (evars_of isevars) typ) (* will try to coerce later in check_and_adjust_constructor.. *) - with Induc -> + with Not_found -> NotInd (None,typ)) (* error will be detected in check_all_variables *) | None -> try IsInd (typ,find_rectype env (evars_of isevars) typ) - with Induc -> NotInd (None,typ) + with Not_found -> NotInd (None,typ) let coerce_row typing_fun isevars env cstropt tomatch = let j = typing_fun empty_tycon env tomatch in @@ -939,7 +940,8 @@ let abstract_conclusion typ cs = let (sign,p) = decompose_prod_n n typ in lam_it p sign -let infer_predicate loc env isevars typs cstrs ((mis,_) as indf) = +let infer_predicate loc env isevars typs cstrs indf = + let (mis,_) = dest_ind_family indf in (* Il faudra substituer les isevars a un certain moment *) if Array.length cstrs = 0 then (* "TODO4-3" *) error "Inference of annotation for empty inductive types not implemented" diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 45694a01b..287e78f76 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -33,7 +33,7 @@ exception PatternMatchingError of env * pattern_matching_error (*s Used for old cases in pretyping *) val branch_scheme : - env -> evar_defs -> bool -> inductive * constr list -> constr array + env -> evar_defs -> bool -> inductive_family -> constr array type ml_case_error = | MlCaseAbsurd diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 111e5a514..5300f1f9b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -166,39 +166,39 @@ let computable p k = -let lookup_name_as_renamed ctxt t s = +let lookup_name_as_renamed env t s = let rec lookup avoid env_names n c = match kind_of_term c with | Prod (name,_,c') -> - (match concrete_name avoid env_names name c' with + (match concrete_name env avoid env_names name c' with | (Some id,avoid') -> if id=s then (Some n) else lookup avoid' (add_name (Name id) env_names) (n+1) c' | (None,avoid') -> lookup avoid' env_names (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match concrete_name avoid env_names name c' with + (match concrete_name env avoid env_names name c' with | (Some id,avoid') -> if id=s then (Some n) else lookup avoid' (add_name (Name id) env_names) (n+1) c' | (None,avoid') -> lookup avoid' env_names (n+1) (pop c')) | Cast (c,_) -> lookup avoid env_names n c | _ -> None - in lookup (ids_of_named_context ctxt) empty_names_context 1 t + in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t -let lookup_index_as_renamed t n = +let lookup_index_as_renamed env t n = let rec lookup n d c = match kind_of_term c with | Prod (name,_,c') -> - (match concrete_name [] empty_names_context name c' with + (match concrete_name env [] empty_names_context name c' with (Some _,_) -> lookup n (d+1) c' | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match concrete_name [] empty_names_context name c' with + (match concrete_name env [] empty_names_context name c' with | (Some _,_) -> lookup n (d+1) c' | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c') | Cast (c,_) -> lookup n d c | _ -> None in lookup n 1 t -let rec detype avoid env t = +let rec detype tenv avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with @@ -212,23 +212,26 @@ let rec detype avoid env t = | Sort (Prop c) -> RSort (dummy_loc,RProp c) | Sort (Type u) -> RSort (dummy_loc,RType (Some u)) | Cast (c1,c2) -> - RCast(dummy_loc,detype avoid env c1,detype avoid env c2) - | Prod (na,ty,c) -> detype_binder BProd avoid env na ty c - | Lambda (na,ty,c) -> detype_binder BLambda avoid env na ty c - | LetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c + RCast(dummy_loc,detype tenv avoid env c1, + detype tenv avoid env c2) + | Prod (na,ty,c) -> detype_binder tenv BProd avoid env na ty c + | Lambda (na,ty,c) -> detype_binder tenv BLambda avoid env na ty c + | LetIn (na,b,_,c) -> detype_binder tenv BLetIn avoid env na b c | App (f,args) -> - RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args) + RApp (dummy_loc,detype tenv avoid env f, + array_map_to_list (detype tenv avoid env) args) | Const sp -> RRef (dummy_loc, ConstRef sp) | Evar (ev,cl) -> let f = REvar (dummy_loc, ev) in - RApp (dummy_loc, f, List.map (detype avoid env) (Array.to_list cl)) + RApp (dummy_loc, f, + List.map (detype tenv avoid env) (Array.to_list cl)) | Ind ind_sp -> RRef (dummy_loc, IndRef ind_sp) | Construct cstr_sp -> RRef (dummy_loc, ConstructRef cstr_sp) | Case (annot,p,c,bl) -> let synth_type = synthetize_type () in - let tomatch = detype avoid env c in + let tomatch = detype tenv avoid env c in let indsp = annot.ci_ind in let considl = annot.ci_pp_info.cnames in let k = annot.ci_pp_info.ind_nargs in @@ -237,11 +240,11 @@ let rec detype avoid env t = if synth_type & computable p k & considl <> [||] then None else - Some (detype avoid env p) in + Some (detype tenv avoid env p) in let constructs = Array.init (Array.length considl) (fun i -> (indsp,i+1)) in let eqnv = - array_map3 (detype_eqn avoid env) constructs consnargsl bl in + array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in let eqnl = Array.to_list eqnv in let tag = if PrintingLet.active (indsp,consnargsl) then @@ -253,10 +256,10 @@ let rec detype avoid env t = in RCases (dummy_loc,tag,pred,[tomatch],eqnl) - | Fix (nvn,recdef) -> detype_fix avoid env (RFix nvn) recdef - | CoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef + | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef + | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef -and detype_fix avoid env fixkind (names,tys,bodies) = +and detype_fix tenv avoid env fixkind (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left (fun (avoid, env, l) na -> @@ -264,11 +267,11 @@ and detype_fix avoid env fixkind (names,tys,bodies) = (id::avoid, add_name (Name id) env, id::l)) (avoid, env, []) names in RRec(dummy_loc,fixkind,Array.of_list (List.rev lfi), - Array.map (detype avoid env) tys, - Array.map (detype def_avoid def_env) bodies) + Array.map (detype tenv avoid env) tys, + Array.map (detype tenv def_avoid def_env) bodies) -and detype_eqn avoid env constr construct_nargs branch = +and detype_eqn tenv avoid env constr construct_nargs branch = let make_pat x avoid env b ids = if not (force_wildcard ()) or (dependent (mkRel 1) b) then let id = next_name_away_with_default "x" x avoid in @@ -280,7 +283,7 @@ and detype_eqn avoid env constr construct_nargs branch = if n=0 then (dummy_loc, ids, [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - detype avoid env b) + detype tenv avoid env b) else match kind_of_term b with | Lambda (x,_,b) -> @@ -305,15 +308,15 @@ and detype_eqn avoid env constr construct_nargs branch = in buildrec [] [] avoid env construct_nargs branch -and detype_binder bk avoid env na ty c = +and detype_binder tenv bk avoid env na ty c = let na',avoid' = - if bk = BLetIn then concrete_let_name avoid env na c + if bk = BLetIn then concrete_let_name tenv avoid env na c else - match concrete_name avoid env na c with + match concrete_name tenv avoid env na c with | (Some id,l') -> (Name id), l' | (None,l') -> Anonymous, l' in - let r = detype avoid' (add_name na' env) c in + let r = detype tenv avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dummy_loc, na',detype [] env ty, r) - | BLambda -> RLambda (dummy_loc, na',detype [] env ty, r) - | BLetIn -> RLetIn (dummy_loc, na',detype [] env ty, r) + | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r) + | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r) + | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index f787da2ba..44992725f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -17,15 +17,14 @@ open Rawterm open Termops (*i*) -(* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *) +(* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *) (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *) -val detype : identifier list -> names_context -> constr -> rawconstr +val detype : env -> identifier list -> names_context -> constr -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) -val lookup_name_as_renamed : - named_context -> constr -> identifier -> int option -val lookup_index_as_renamed : constr -> int -> int option +val lookup_name_as_renamed : env -> constr -> identifier -> int option +val lookup_index_as_renamed : env -> constr -> int -> int option val force_wildcard : unit -> bool diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index d52c7f643..cb51cecaf 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -59,13 +59,13 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind = (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) let env' = push_rel_context lnamespar env in - let indf = (ind, extended_rel_list 0 lnamespar) in + let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in let constrs = get_constructors env indf in let rec add_branch env k = if k = Array.length mip.mind_consnames then let nbprod = k+1 in - let indf = (ind,extended_rel_list nbprod lnamespar) in + let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in let lnamesar,_ = get_arity env indf in let ci = make_default_case_info env ind in it_mkLambda_or_LetIn_name env' @@ -103,7 +103,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind = * on it with which predicate and which recursive function. *) -let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = +let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let make_prod = make_prod_dep dep in let nparams = List.length vargs in let process_pos env depK pk = @@ -120,7 +120,8 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = let (_,realargs) = list_chop nparams largs in let base = applist (lift i pk,realargs) in if depK then - mkApp (base, [|applist (mkRel (i+1),extended_rel_list 0 sign)|]) + Reduction.beta_appvect + base [|applist (mkRel (i+1),extended_rel_list 0 sign)|] else base | _ -> assert false @@ -133,12 +134,11 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = let (optionpos,rest) = match recargs with | [] -> None,[] - | Param _ :: rest -> (None,rest) - | Norec :: rest -> (None,rest) + | Mrec j :: rest when is_rec -> (depPvect.(j),rest) | Imbr _ :: rest -> Options.if_verbose warning "Ignoring recursive call"; (None,rest) - | Mrec j :: rest -> (depPvect.(j),rest) + | _ :: rest -> (None, rest) in (match optionpos with | None -> @@ -167,7 +167,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in let params = List.map (lift i) vargs in let co = applist (mkConstruct cs.cs_cstr,params@realargs) in - mkApp (c, [|co|]) + Reduction.beta_appvect c [|co|] else c in let nhyps = List.length cs.cs_args in @@ -258,9 +258,10 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let nctyi = Array.length mipi.mind_consnames in (* nb constructeurs du type *) - (* arity in the context P1..P_nrec f1..f_nbconstruct *) + (* arity in the context of the fixpoint, i.e. + P1..P_nrec f1..f_nbconstruct *) let args = extended_rel_list (nrec+nbconstruct) lnamespar in - let indf = (indi,args) in + let indf = make_ind_family(indi,args) in let lnames,_ = get_arity env indf in let nar = mipi.mind_nrealargs in @@ -268,8 +269,11 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let dect = nar+nrec+nbconstruct in let vecfi = rel_vect (dect+1-i-nctyi) nctyi in - let args = extended_rel_list (decf+1) lnamespar in - let constrs = get_constructors env (indi,args) in + (* constructors in context of the Cases expr, i.e. + P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) + let args' = extended_rel_list (decf+1) lnamespar in + let indf' = make_ind_family(indi,args') in + let constrs = get_constructors env indf' in let branches = array_map3 (make_rec_branch_arg env sigma (nparams,depPvec,nar+1)) @@ -277,8 +281,6 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let j = (match depPvec.(tyi) with | Some (_,c) when isRel c -> destRel c | _ -> assert false) in - let args = extended_rel_list (nrec+nbconstruct) lnamespar in - let indf = (indi,args) in let deftyi = it_mkLambda_or_LetIn_name env (lambda_create env @@ -325,7 +327,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let indf = (indi, vargs) in let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in let p_0 = - type_rec_branch dep env sigma (vargs,depPvec,i+j) tyi cs recarg + type_rec_branch + true dep env sigma (vargs,depPvec,i+j) tyi cs recarg in mkLambda_string "f" p_0 (onerec (push_rel (Anonymous,None,p_0) env) (j+1)) @@ -398,8 +401,9 @@ let instanciate_type_indrec_scheme sort npars term = match kind_of_term elim with | Prod (n,t,c) -> if np = 0 then - let t' = change_sort_arity sort t - in mkProd (n, t', c), mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) + let t' = change_sort_arity sort t in + mkProd (n, t', c), + mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else let c',term' = drec (np-1) c in mkProd (n, t, c'), mkLambda (n, t, term') @@ -451,38 +455,32 @@ let build_indrec env sigma ind = (* To handle old Case/Match syntax in Pretyping *) (***********************************) -(* To interpret the Match operator *) +(* To interpret Case and Match operators *) -(* TODO: check that we can drop universe constraints ? *) -let type_mutind_rec env sigma (IndType (indf,realargs) as indt) pj c = +let type_rec_branches recursive env sigma indt pj c = + let IndType (indf,realargs) = indt in let p = pj.uj_val in let (ind,params) = dest_ind_family indf in let tyi = snd ind in let (mib,mip) = lookup_mind_specif env ind in - if mis_is_recursive_subset [tyi] mip then - let (dep,_) = find_case_dep_nparams env (c,pj) indf in - let init_depPvec i = if i = tyi then Some(dep,p) else None in - let depPvec = Array.init mib.mind_ntypes init_depPvec in - let vargs = Array.of_list params in - let constructors = get_constructors env indf in - let recargs = mip.mind_listrec in - let lft = array_map2 (type_rec_branch dep env sigma (params,depPvec,0) tyi) - constructors recargs in - (lft, - if dep then applist(p,realargs@[c]) - else applist(p,realargs) ) - else + let is_rec = recursive && mis_is_recursive_subset [tyi] mip in + let dep = is_dependent_elimination env pj.uj_type indf in + let init_depPvec i = if i = tyi then Some(dep,p) else None in + let depPvec = Array.init mib.mind_ntypes init_depPvec in + let vargs = Array.of_list params in + let constructors = get_constructors env indf in + let recargs = mip.mind_listrec in + let lft = + array_map2 + (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi) + constructors recargs in + (lft, + if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) + else Reduction.beta_appvect p (Array.of_list realargs)) +(* Non recursive case. Pb: does not deal with unification let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in (p,ra) - -let type_rec_branches recursive env sigma indt pj c = - if recursive then - type_mutind_rec env sigma indt pj c - else - let IndType((ind,params),rargs) = indt in - let (p,ra,_) = type_case_branches env (ind,params@rargs) pj c in - (p,ra) - +*) (*s Eliminations. *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 6bf4813c2..cb1e7d3ee 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -190,19 +190,17 @@ let build_branch_type env dep p cs = (**************************************************) -exception Induc - let extract_mrectype t = let (t, l) = decompose_app t in match kind_of_term t with | Ind ind -> (ind, l) - | _ -> raise Induc + | _ -> raise Not_found let find_mrectype env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) - | _ -> raise Induc + | _ -> raise Not_found let find_rectype env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in @@ -211,7 +209,7 @@ let find_rectype env sigma c = let (mib,mip) = Inductive.lookup_mind_specif env ind in let (par,rargs) = list_chop mip.mind_nparams l in IndType((ind, par),rargs) - | _ -> raise Induc + | _ -> raise Not_found let find_inductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in @@ -219,7 +217,7 @@ let find_inductive env sigma c = | Ind ind when (fst (Inductive.lookup_mind_specif env ind)).mind_finite -> (ind, l) - | _ -> raise Induc + | _ -> raise Not_found let find_coinductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in @@ -227,28 +225,27 @@ let find_coinductive env sigma c = | Ind ind when not (fst (Inductive.lookup_mind_specif env ind)).mind_finite -> (ind, l) - | _ -> raise Induc + | _ -> raise Not_found (***********************************************) (* find appropriate names for pattern variables. Useful in the Case tactic. *) -let is_dep_arity env kelim predty t = - let rec srec (pt,t) = +let is_dep_arity env kelim predty nodep_ar = + let rec srec pt nodep_ar = let pt' = whd_betadeltaiota env Evd.empty pt in - let t' = whd_betadeltaiota env Evd.empty t in - match kind_of_term pt', kind_of_term t' with - | Prod (_,a1,a2), Prod (_,a1',a2') -> srec (a2,a2') + match kind_of_term pt', kind_of_term nodep_ar with + | Prod (_,a1,a2), Prod (_,a1',a2') -> srec a2 a2' | Prod (_,a1,a2), _ -> true | _ -> false in - srec (predty,t) + srec predty nodep_ar -let is_dep env predty (ind,args) = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let params = fst (list_chop mip.mind_nparams args) in +let is_dependent_elimination env predty indf = + let (ind,params) = indf in + let (_,mip) = Inductive.lookup_mind_specif env ind in let kelim = mip.mind_kelim in - let arsign,s = get_arity env (ind,params) in + let arsign,s = get_arity env indf in let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in is_dep_arity env kelim predty glob_t @@ -261,17 +258,29 @@ let set_pattern_names env ind brv = let (_,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map - (fun c -> List.length (fst (decompose_prod c)) - mip.mind_nparams) + (fun c -> + rel_context_length (fst (decompose_prod_assum c)) - + mip.mind_nparams) mip.mind_nf_lc in array_map2 (set_names env) arities brv let type_case_branches_with_names env indspec pj c = + let (ind,args) = indspec in let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in - if is_dep env pj.uj_type indspec then - (set_pattern_names env (fst indspec) lbrty, conclty) + let (mib,mip) = Inductive.lookup_mind_specif env ind in + let params = fst (list_chop mip.mind_nparams args) in + if is_dependent_elimination env pj.uj_type (ind,params) then + (set_pattern_names env ind lbrty, conclty) else (lbrty, conclty) +(* Type of Case predicates *) +let arity_of_case_predicate env (ind,params) dep k = + let arsign,_ = get_arity env (ind,params) in + let mind = build_dependent_inductive env (ind,params) in + let concl = if dep then mkArrow mind (mkSort k) else mkSort k in + it_mkProd_or_LetIn concl arsign + (***********************************************) (* Guard condition *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 09c81c7d7..b807c2d7f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -15,9 +15,9 @@ open Environ open Evd (* An inductive type with its parameters *) -type inductive_family = inductive * constr list -val make_ind_family : 'a * 'b -> 'a * 'b -val dest_ind_family : 'a * 'b -> 'a * 'b +type inductive_family +val make_ind_family : inductive * constr list -> inductive_family +val dest_ind_family : inductive_family -> inductive * constr list val liftn_inductive_family : int -> int -> inductive_family -> inductive_family val lift_inductive_family : int -> inductive_family -> inductive_family val substnl_ind_family : @@ -49,23 +49,31 @@ val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : inductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_constructors : - env -> inductive * constr list -> constructor_summary array -val get_arity : env -> inductive * constr list -> Sign.arity +val get_arity : env -> inductive_family -> Sign.arity +val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr -val build_dependent_inductive : env -> inductive * constr list -> constr +val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : - env -> bool -> inductive * constr list -> Sign.rel_context -val make_arity : env -> bool -> inductive * constr list -> sorts -> types + env -> bool -> inductive_family -> Sign.rel_context +val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types -exception Induc +(* Raise Not_found if not given an valid inductive type *) val extract_mrectype : constr -> inductive * constr list val find_mrectype : env -> evar_map -> constr -> inductive * constr list val find_rectype : env -> evar_map -> constr -> inductive_type val find_inductive : env -> evar_map -> constr -> inductive * constr list val find_coinductive : env -> evar_map -> constr -> inductive * constr list +(********************) +(* Determines if a case predicate type corresponds to dependent elimination *) +val is_dependent_elimination : + env -> types -> inductive_family -> bool + +(* Builds the case predicate arity (dependent or not) *) +val arity_of_case_predicate : + env -> inductive_family -> bool -> sorts -> types + val type_case_branches_with_names : env -> inductive * constr list -> unsafe_judgment -> constr -> types array * types @@ -73,4 +81,5 @@ val make_case_info : env -> inductive -> case_style option -> pattern_source array -> case_info val make_default_case_info : env -> inductive -> case_info +(********************) val control_only_guard : env -> types -> unit diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d28db7510..11ddc43cd 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,7 +43,8 @@ let lift_context n l = let transform_rec loc env sigma (pj,c,lf) indt = let p = pj.uj_val in - let ((ind,params) as indf,realargs) = dest_ind_type indt in + let (indf,realargs) = dest_ind_type indt in + let (ind,params) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let mI = mkInd ind in let recargs = mip.mind_listrec in @@ -54,9 +55,8 @@ let transform_rec loc env sigma (pj,c,lf) indt = (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in error_number_branches_loc loc env sigma cj nconstr); if mis_is_recursive_subset [tyi] mip then - let (dep,_) = - find_case_dep_nparams env - (nf_evar sigma c, j_nf_evar sigma pj) indf in + let dep = + is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in let depFvec = Array.init mib.mind_ntypes init_depFvec in (* build now the fixpoint *) @@ -322,10 +322,16 @@ let rec pretype tycon env isevars lvar lmeta = function let cj = pretype empty_tycon env isevars lvar lmeta c in let (IndType (indf,realargs) as indt) = try find_rectype env (evars_of isevars) cj.uj_type - with Induc -> + with Not_found -> error_case_not_inductive_loc loc env (evars_of isevars) cj in - let pj = match po with - | Some p -> pretype empty_tycon env isevars lvar lmeta p + let (dep,pj) = match po with + | Some p -> + let pj = pretype empty_tycon env isevars lvar lmeta p in + let dep = is_dependent_elimination env pj.uj_type indf in + let ar = + arity_of_case_predicate env indf dep (Type (new_univ())) in + let _ = the_conv_x_leq env isevars pj.uj_type ar in + (dep, pj) | None -> (* get type information from type of branches *) let expbr = Cases.branch_scheme env isevars isrec indf in @@ -337,7 +343,8 @@ let rec pretype tycon env isevars lvar lmeta = function (* may be Type while Prop or Set would be expected *) match tycon with | Some pred -> - Retyping.get_judgment_of env (evars_of isevars) pred + (false, + Retyping.get_judgment_of env (evars_of isevars) pred) | None -> let sigma = evars_of isevars in error_cant_find_case_type_loc loc env sigma cj.uj_val @@ -355,13 +362,11 @@ let rec pretype tycon env isevars lvar lmeta = function Retyping.get_type_of env (evars_of isevars) pred in let pj = { uj_val = pred; uj_type = pty } in let _ = option_app (the_conv_x_leq env isevars pred) tycon - in pj + in (false,pj) with Cases.NotInferable _ -> findtype (i+1) in findtype 0 in let pj = j_nf_evar (evars_of isevars) pj in - let (dep,_) = find_case_dep_nparams env (cj.uj_val,pj) indf in - let pj = if dep then pj else let n = List.length realargs in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a87354d65..2380b94c8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -70,7 +70,7 @@ let typeur sigma metamap = (* TODO: could avoid computing the type of branches *) let i = try find_rectype env (type_of env c) - with Induc -> anomaly "type_of: Bad recursive type" in + with Not_found -> anomaly "type_of: Bad recursive type" in let pj = { uj_val = p; uj_type = type_of env p } in let (_,ty,_) = type_case_branches env i pj c in ty diff --git a/pretyping/termops.ml b/pretyping/termops.ml index e861ebbe4..790abaa43 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -638,25 +638,25 @@ let occur_rel p env id = try lookup_name_of_rel p env = Name id with Not_found -> false (* Unbound indice : may happen in debug *) -let occur_id env id0 c = +let occur_id env nenv id0 c = let rec occur n c = match kind_of_term c with | Var id when id=id0 -> raise Occur | Const sp when basename sp = id0 -> raise Occur | Ind ind_sp - when basename (path_of_inductive (Global.env()) ind_sp) = id0 -> + when basename (path_of_inductive env ind_sp) = id0 -> raise Occur | Construct cstr_sp - when basename (path_of_constructor (Global.env()) cstr_sp) = id0 -> + when basename (path_of_constructor env cstr_sp) = id0 -> raise Occur - | Rel p when p>n & occur_rel (p-n) env id0 -> raise Occur + | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur | _ -> iter_constr_with_binders succ occur n c in try occur 1 c; false with Occur -> true -let next_name_not_occuring name l env_names t = +let next_name_not_occuring env name l env_names t = let rec next id = - if List.mem id l or occur_id env_names id t then next (lift_ident id) + if List.mem id l or occur_id env env_names id t then next (lift_ident id) else id in match name with @@ -664,16 +664,16 @@ let next_name_not_occuring name l env_names t = | Anonymous -> id_of_string "_" (* Remark: Anonymous var may be dependent in Evar's contexts *) -let concrete_name l env_names n c = +let concrete_name env l env_names n c = if n = Anonymous & not (dependent (mkRel 1) c) then (None,l) else - let fresh_id = next_name_not_occuring n l env_names c in + let fresh_id = next_name_not_occuring env n l env_names c in let idopt = if dependent (mkRel 1) c then (Some fresh_id) else None in (idopt, fresh_id::l) -let concrete_let_name l env_names n c = - let fresh_id = next_name_not_occuring n l env_names c in +let concrete_let_name env l env_names n c = + let fresh_id = next_name_not_occuring env n l env_names c in (Name fresh_id, fresh_id::l) let global_vars env ids = Idset.elements (global_vars_set env ids) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2a3e8b29c..e47570f47 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -126,15 +126,15 @@ val names_of_rel_context : env -> names_context (* sets of free identifiers *) type used_idents = identifier list val occur_rel : int -> name list -> identifier -> bool -val occur_id : name list -> identifier -> constr -> bool +val occur_id : env -> name list -> identifier -> constr -> bool val next_name_not_occuring : - name -> identifier list -> name list -> constr -> identifier + env -> name -> identifier list -> name list -> constr -> identifier val concrete_name : - identifier list -> name list -> name -> + env -> identifier list -> name list -> name -> constr -> identifier option * identifier list val concrete_let_name : - identifier list -> name list -> + env -> identifier list -> name list -> name -> constr -> name * identifier list val global_vars : env -> constr -> identifier list val rename_bound_var : env -> identifier list -> types -> types -- cgit v1.2.3