diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 93 |
1 files changed, 48 insertions, 45 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 9fbfc197..c6209cc3 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,44 +1,44 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp +open Errors open Util -open Names open Term +open Vars open Environ open Reductionops open Type_errors -open Pretype_errors open Inductive open Inductiveops open Typeops -open Evd open Arguments_renaming let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in meta_instance evd ty let constant_type_knowing_parameters env cst jl = - let paramstyp = Array.map (fun j -> j.uj_type) jl in - type_of_constant_knowing_parameters env (constant_type env cst) paramstyp + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in + type_of_constant_knowing_parameters_in env cst paramstyp -let inductive_type_knowing_parameters env ind jl = - let (mib,mip) = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> j.uj_type) jl in - Inductive.type_of_inductive_knowing_parameters env mip paramstyp +let inductive_type_knowing_parameters env (ind,u) jl = + let mspec = lookup_mind_specif env ind in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in + Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> - let (evd,s) = Evarutil.define_evar_as_sort !evdref ev in + let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -69,17 +69,17 @@ let e_judge_of_apply env evdref funj argjv = in apply_rec 1 funj.uj_type (Array.to_list argjv) -let e_check_branch_types env evdref ind cj (lfj,explft) = - if Array.length lfj <> Array.length explft then +let e_check_branch_types env evdref (ind,u) cj (lfj,explft) = + if not (Int.equal (Array.length lfj) (Array.length explft)) then error_number_branches env cj (Array.length explft); for i = 0 to Array.length explft - 1 do if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then - error_ill_formed_branch env cj.uj_val (ind,i+1) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) done -let rec max_sort l = - if List.mem InType l then InType else - if List.mem InSet l then InSet else InProp +let max_sort l = + if Sorts.List.mem InType l then InType else + if Sorts.List.mem InSet l then InSet else InProp let e_is_correct_arity env evdref c pj ind specif params = let arsign = make_arity_signature env true (make_ind_family (ind,params)) in @@ -92,10 +92,11 @@ let e_is_correct_arity env evdref c pj ind specif params = if not (Evarconv.e_cumul env evdref a1 a1') then error (); srec (push_rel (na1,None,a1) env) t ar' | Sort s, [] -> - if not (List.mem (family_of_sort s) allowed_sorts) then error () + if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + then error () | Evar (ev,_), [] -> - let s = Termops.new_sort_in_family (max_sort allowed_sorts) in - evdref := Evd.define ev (mkSort s) !evdref + let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in + evdref := Evd.define ev (mkSort s) evd | _, (_,Some _,_ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> @@ -104,13 +105,13 @@ let e_is_correct_arity env evdref c pj ind specif params = srec env pj.uj_type (List.rev arsign) let e_type_case_branches env evdref (ind,largs) pj c = - let specif = lookup_mind_specif env ind in + let specif = lookup_mind_specif env (fst ind) in let nparams = inductive_params specif in - let (params,realargs) = list_chop nparams largs in + let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in - let n = (snd specif).Declarations.mind_nrealargs_ctxt in + let n = (snd specif).Declarations.mind_nrealargs in let ty = whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in (lc, ty, univ) @@ -125,12 +126,13 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +(* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in - let specif = Global.lookup_inductive ind in + let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in - if not (List.exists ((=) ksort) sorts) then + if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env ind sorts c pj (Some(ksort,s,error_elim_explain ksort s)) @@ -195,22 +197,26 @@ let rec execute env evdref cstr = judge_of_prop_contents c | Sort (Type u) -> - judge_of_type u + judge_of_type u + + | Proj (p, c) -> + let cj = execute env evdref c in + judge_of_projection env p (Evarutil.j_nf_evar !evdref cj) | App (f,args) -> let jl = execute_array env evdref args in let j = match kind_of_term f with - | Ind ind -> + | Ind ind when Environ.template_polymorphic_pind ind env -> (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind - (jv_nf_evar !evdref jl)) - | Const cst -> + (Evarutil.jv_nf_evar !evdref jl)) + | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst - (jv_nf_evar !evdref jl)) + (Evarutil.jv_nf_evar !evdref jl)) | _ -> execute env evdref f in @@ -235,7 +241,7 @@ let rec execute env evdref cstr = let j1 = execute env evdref c1 in let j2 = execute env evdref c2 in let j2 = e_type_judgment env evdref j2 in - let _ = judge_of_cast env j1 DEFAULTcast j2 in + let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 @@ -257,40 +263,37 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) -let check env evd c t = - let evdref = ref evd in +let check env evdref c t = let j = execute env evdref c in if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type env j (nf_evar evd t) + error_actual_type env j (nf_evar !evdref t) (* Type of a constr *) let type_of env evd c = let j = execute env (ref evd) c in - (* We are outside the kernel: we take fresh universes *) - (* to avoid tactics and co to refresh universes themselves *) - Termops.refresh_universes j.uj_type + j.uj_type (* Sort of a type *) -let sort_of env evd c = - let evdref = ref evd in +let sort_of env evdref c = let j = execute env evdref c in let a = e_type_judgment env evdref j in a.utj_type (* Try to solve the existential variables by typing *) -let e_type_of env evd c = +let e_type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) - !evdref, Termops.refresh_universes j.uj_type + if refresh then + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type + else !evdref, j.uj_type -let solve_evars env evd c = - let evdref = ref evd in +let solve_evars env evdref c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) - !evdref, nf_evar !evdref c + nf_evar !evdref c let _ = Evarconv.set_solve_evars solve_evars |