diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 44 | ||||
| -rw-r--r-- | pretyping/univdecls.ml | 7 | ||||
| -rw-r--r-- | pretyping/univdecls.mli | 2 |
3 files changed, 37 insertions, 16 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 3132d2ad53..3cc1520179 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -34,7 +34,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp) + Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with @@ -49,6 +49,30 @@ let e_assumption_of_judgment env evdref j = with Type_errors.TypeError _ | PretypeError _ -> error_assumption env !evdref j +let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = + let rec apply_rec n typ = function + | [] -> + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = + let ar = inductive_type_knowing_parameters env !evdref ind argjv in + hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } + | hj::restjl -> + match EConstr.kind !evdref (whd_all env !evdref typ) with + | Prod (_,c1,c2) -> + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + | Evar ev -> + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in + evdref := evd'; + let (_,_,c2) = destProd evd' t in + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + | _ -> + error_cant_apply_not_functional env !evdref funj argjv + in + apply_rec 1 funj.uj_type (Array.to_list argjv) + let e_judge_of_apply env evdref funj argjv = let rec apply_rec n typ = function | [] -> @@ -300,16 +324,14 @@ let rec execute env evdref cstr = | App (f,args) -> let jl = execute_array env evdref args in - let j = - match EConstr.kind !evdref f with - | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - make_judge f - (inductive_type_knowing_parameters env !evdref (ind, u) jl) - | _ -> - (* No template polymorphism *) - execute env evdref f - in - e_judge_of_apply env evdref j jl + (match EConstr.kind !evdref f with + | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> + let fj = execute env evdref f in + e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl + | _ -> + (* No template polymorphism *) + let fj = execute env evdref f in + e_judge_of_apply env evdref fj jl) | Lambda (name,c1,c2) -> let j = execute env evdref c1 in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index 3cf32d7ff0..89f1185a99 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -6,12 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open CErrors (** Local universes and constraints declarations *) type universe_decl = - (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl let default_univ_decl = let open Misctypes in @@ -34,9 +33,9 @@ let interp_univ_constraints env evd cstrs = in List.fold_left interp (evd,Univ.Constraint.empty) cstrs -let interp_univ_decl env decl = +let interp_univ_decl env decl = let open Misctypes in - let pl = decl.univdecl_instance in + let pl : lident list = decl.univdecl_instance in let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli index 0c3b749cbf..706d3a157f 100644 --- a/pretyping/univdecls.mli +++ b/pretyping/univdecls.mli @@ -8,7 +8,7 @@ (** Local universe and constraint declarations. *) type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl val default_univ_decl : universe_decl |