diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 17 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 18 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 55 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 24 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 14 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 29 |
9 files changed, 90 insertions, 73 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 39b26a2b7..7a77d6eab 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -313,16 +313,21 @@ let rec find_row_ind = function | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) let inductive_template isevars env tmloc ind = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in + let arsign = get_full_arity_sign env ind in let hole_source = match tmloc with | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i)) | None -> fun _ -> (dummy_loc, Evd.InternalHole) in - let (evarl,_) = + let (_,evarl,_) = List.fold_right - (fun (na,ty) (evl,n) -> - (e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1) - ntys ([],1) in + (fun (na,b,ty) (subst,evarl,n) -> + match b with + | None -> + let ty' = substl subst ty in + let e = e_new_evar isevars env ~src:(hole_source n) ty' in + (e::subst,e::evarl,n+1) + | Some b -> + (b::subst,evarl,n+1)) + arsign ([],[],1) in applist (mkInd ind,List.rev evarl) let inh_coerce_to_ind isevars env ty tyi = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index ef6fccfc4..f3e3b6d2c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -48,13 +48,13 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) lift_constructor et lift_inductive_family qui ne se contentent pas de lifter les paramètres globaux *) -let mis_make_case_com depopt env sigma (ind,mib,mip) kind = +let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = let lnamespar = mib.mind_params_ctxt in let dep = match depopt with - | None -> mip.mind_sort <> (Prop Null) + | None -> inductive_sort_family mip <> InProp | Some d -> d in - if not (List.exists ((=) kind) mip.mind_kelim) then + if not (List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError (NotAllowedCaseAnalysis @@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind + mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind in (* Body of mis_make_indrec *) list_tabulate make_one_rec nrec @@ -441,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib = let make_case_com depopt env sigma ity kind = let (mib,mip) = lookup_mind_specif env ity in - mis_make_case_com depopt env sigma (ity,mib,mip) kind + mis_make_case_com depopt env sigma ity (mib,mip) kind let make_case_dep env = make_case_com (Some true) env let make_case_nodep env = make_case_com (Some false) env @@ -504,7 +504,7 @@ let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni),mibi,mipi,dep,kind) -> let id = mipi.mind_typename in - let kelim = mipi.mind_kelim in + let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) else if List.mem ni ln then raise @@ -534,7 +534,7 @@ let build_mutual_indrec env sigma = function let build_indrec env sigma ind = let (mib,mip) = lookup_mind_specif env ind in - let kind = family_of_sort mip.mind_sort in + let kind = inductive_sort_family mip in let dep = kind <> InProp in List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib) @@ -596,7 +596,7 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id id ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") @@ -617,6 +617,6 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id base ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1c290e877..737bb18ed 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -116,6 +116,10 @@ let constructor_nrealhyps env (ind,j) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) +let get_full_arity_sign env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_arity_ctxt + (* Length of arity (w/o local defs) *) let inductive_nargs env ind = @@ -196,10 +200,40 @@ let rec instantiate args c = match kind_of_term c, args with | _, [] -> c | _ -> anomaly "too short arity" +(* substitution in a signature *) + +let substnl_rel_context subst n sign = + let rec aux n = function + | d::sign -> substnl_decl subst n d :: aux (n+1) sign + | [] -> [] + in List.rev (aux n (List.rev sign)) + +let substl_rel_context subst = substnl_rel_context subst 0 + +let rec instantiate_context sign args = + let rec aux subst = function + | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args) + | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args) + | [], [] -> subst + | _ -> anomaly "Signature/instance mismatch in inductive family" + in aux [] (List.rev sign,args) + let get_arity env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let arity = mip.mind_nf_arity in - destArity (instantiate params arity) + let parsign = + (* Dynamically detect if called with an instance of recursively + uniform parameter only or also of non recursively uniform + parameters *) + let parsign = mib.mind_params_ctxt in + let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in + if List.length params = rel_context_nhyps parsign - nnonrecparams then + snd (list_chop nnonrecparams mib.mind_params_ctxt) + else + parsign in + let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in + let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in + let subst = instantiate_context parsign params in + (substl_rel_context subst arsign, Inductive.inductive_sort_family mip) (* Functions to build standard types related to inductive *) let build_dependent_constructor cs = @@ -284,12 +318,12 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) -let is_predicate_explicitly_dep env pred nodep_ar = - let rec srec env pval nodep_ar = +let is_predicate_explicitly_dep env pred arsign = + let rec srec env pval arsign = let pv' = whd_betadeltaiota env Evd.empty pval in - match kind_of_term pv', kind_of_term nodep_ar with - | Lambda (na,t,b), Prod (_,_,a') -> - srec (push_rel_assum (na,t) env) b a' + match kind_of_term pv', arsign with + | Lambda (na,t,b), (_,None,_)::arsign -> + srec (push_rel_assum (na,t) env) b arsign | Lambda (na,_,_), _ -> (* The following code has impact on the introduction names @@ -317,12 +351,11 @@ let is_predicate_explicitly_dep env pred nodep_ar = | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate" in - srec env pred nodep_ar + srec env pred arsign let is_elim_predicate_explicitly_dependent env pred indf = - let arsign,s = get_arity env indf in - let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in - is_predicate_explicitly_dep env pred glob_t + let arsign,_ = get_arity env indf in + is_predicate_explicitly_dep env pred arsign let set_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b4acaafbb..f84c95c6a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -13,6 +13,7 @@ open Term open Declarations open Environ open Evd +open Sign (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) @@ -42,8 +43,7 @@ val dest_ind_type : inductive_type -> inductive_family * constr list val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : - constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type val mkAppliedInd : inductive_type -> constr val mis_is_recursive_subset : int list -> wf_paths -> bool @@ -51,17 +51,22 @@ val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr -val mis_constr_nargs : inductive -> int array +(* Extract information from an inductive name *) + +val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -val mis_constructor_nargs_env : env -> constructor -> int +(* Return number of expected parameters and of expected real arguments *) +val inductive_nargs : env -> inductive -> int * int +val mis_constructor_nargs_env : env -> constructor -> int val constructor_nrealargs : env -> constructor -> int val constructor_nrealhyps : env -> constructor -> int -(* Return number of expected parameters and of expected real arguments *) -val inductive_nargs : env -> inductive -> int * int +val get_full_arity_sign : env -> inductive -> rel_context + +(* Extract information from an inductive family *) type constructor_summary = { cs_cstr : constructor; @@ -69,17 +74,16 @@ type constructor_summary = { cs_nargs : int; cs_args : Sign.rel_context; cs_concl_realargs : constr array; -} +} 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_arity : env -> inductive_family -> Sign.arity +val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : - env -> bool -> inductive_family -> Sign.rel_context +val make_arity_signature : 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 diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 187a8840c..386d3d5e0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -846,7 +846,7 @@ let is_arity env sigma c = match find_conclusion env sigma c with | Sort _ -> true | _ -> false - + (*************************************) (* Metas *) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 776f1313f..2fdb4148a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -118,17 +118,9 @@ let typeur sigma metamap = | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_applied_inductive env ind args = - let specif = lookup_mind_specif env ind in - let t = Inductive.type_of_inductive specif in - if is_small_inductive specif then - (* No polymorphism *) - t - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let lls = Array.map (Array.map (sort_of env')) llc in - let ls = Array.map max_inductive_sort lls in - set_inductive_level env (find_inductive_level env specif ind ls0 ls) t + let (_,mip) = lookup_mind_specif env ind in + let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + Inductive.type_of_applied_inductive env mip argtyps in type_of, sort_of, sort_family_of, type_of_applied_inductive diff --git a/pretyping/termops.ml b/pretyping/termops.ml index faf91247e..af90b91d3 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -25,7 +25,7 @@ let print_sort = function | Prop Null -> (str "Prop") | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")") -let print_sort_family = function +let pr_sort_family = function | InSet -> (str "Set") | InProp -> (str "Prop") | InType -> (str "Type") diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5ecd0b685..5bd79a8ee 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -24,7 +24,7 @@ val refresh_universes : types -> types (* printers *) val print_sort : sorts -> std_ppcmds -val print_sort_family : sorts_family -> std_ppcmds +val pr_sort_family : sorts_family -> std_ppcmds (* debug printer: do not use to display terms to the casual user... *) val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 85e75586b..8e10b0aff 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -88,14 +88,16 @@ let rec execute env evd cstr = judge_of_type u | App (f,args) -> - let j = execute env evd f in let jl = execute_array env evd args in - let (j,_) = judge_of_apply env j jl in + let j = if isInd f then (* Sort-polymorphism of inductive types *) - adjust_inductive_level env evd (destInd f) args j + judge_of_applied_inductive env (destInd f) + (jv_nf_evar (evars_of evd) jl) else - j + execute env evd f + in + fst (judge_of_apply env j jl) | Lambda (name,c1,c2) -> let j = execute env evd c1 in @@ -141,25 +143,6 @@ and execute_array env evd = Array.map (execute env evd) and execute_list env evd = List.map (execute env evd) -and adjust_inductive_level env evd ind args j = - let specif = lookup_mind_specif env ind in - if is_small_inductive specif then - (* No polymorphism *) - j - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let llj = Array.map (execute_array env' evd) llc in - let ls = - Array.map (fun lj -> - let ls = - Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj - in - max_inductive_sort ls) llj - in - let s = find_inductive_level env specif ind ls0 ls in - on_judgment_type (set_inductive_level env s) j - let mcheck env evd c t = let sigma = Evd.evars_of evd in let j = execute env evd (nf_evar sigma c) in |