diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 15 | ||||
| -rw-r--r-- | pretyping/nativenorm.mli | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 4 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 18 | ||||
| -rw-r--r-- | pretyping/vnorm.mli | 1 |
10 files changed, 20 insertions, 46 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c6c397135a..af2877d34f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1006,21 +1006,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let are_canonical_instances args1 args2 env = - let n1 = Array.length args1 in - let n2 = Array.length args2 in - let rec aux n = function - | (id,_,c)::sign - when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) -> - aux (n+1) sign - | [] -> - let rec aux2 n = - Int.equal n n1 || - (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1)) - in aux2 n - | _ -> false in - Int.equal n1 n2 && aux 0 (named_context env) - let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 0352038385..286cb2e079 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -8,7 +8,6 @@ open Term open Environ open Evd -open Nativelambda (** This module implements normalization by evaluation to OCaml code *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6d9ed9a30c..84beaa9e3c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -46,7 +46,7 @@ open Misctypes type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; @@ -443,26 +443,12 @@ let new_type_evar env evdref loc = univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref in e -let get_projection env cst = - let cb = lookup_constant cst env in - match cb.Declarations.const_proj with - | Some {Declarations.proj_ind = mind; proj_npars = n; - proj_arg = m; proj_type = ty} -> - (cst,mind,n,m,ty) - | None -> raise Not_found - let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let is_GHole = function - | GHole _ -> true - | _ -> false - -let evars = ref Id.Map.empty - let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f8587d01cd..8b76816ab2 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; @@ -152,5 +152,5 @@ val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t -> + (types -> env -> evar_map -> unbound_ltac_var_map -> Genarg.glob_generic_argument -> constr * evar_map) Hook.t diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7fde7b7ac4..af48654015 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -299,7 +299,7 @@ let check_and_decompose_canonical_structure ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in + let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 5195784a4c..55bce23089 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -221,7 +221,6 @@ val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_prod_assum : env -> evar_map -> constr -> Context.Rel.t * constr -val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { mP : constr; (** the result type *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 48911a5a9f..31e75e5508 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -940,8 +940,6 @@ let matches_head env sigma c t = | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) | _ -> raise Constr_matching.PatternMatchingFailure -let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false - (** FIXME: Specific function to handle projections: it ignores what happens on the parameters. This is a temporary fix while rewrite etc... are not up to equivalence of the projection and its eta expanded form. @@ -1055,10 +1053,6 @@ let unfold env sigma name = else error (string_of_evaluable_ref env name^" is opaque.") -let is_projection env = function - | EvalVarRef _ -> false - | EvalConstRef c -> Environ.is_projection c env - (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences. diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c4f22987f7..5595c3cdc2 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -435,7 +435,7 @@ let instance_constructor (cl,u) args = | None -> true | Some _ -> false in - let lenpars = List.length (List.filter filter (snd cl.cl_context)) in + let lenpars = List.count filter (snd cl.cl_context) in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2f9803b62f..11ad7bfdf5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -143,8 +143,13 @@ let e_judge_of_cast env evdref cj k tj = { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type } -(* The typing machine without information, without universes but with - existential variables. *) +let enrich_env env evdref = + let penv = Environ.pre_env env in + let penv' = Pre_env.({ penv with env_stratification = + { penv.env_stratification with env_universes = Evd.universes !evdref } }) in + Environ.env_of_pre_env penv' + +(* The typing machine with universes and existential variables. *) (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) @@ -263,6 +268,7 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) let check env evdref c t = + let env = enrich_env env evdref in 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 !evdref t) @@ -270,12 +276,15 @@ let check env evdref c t = (* Type of a constr *) let unsafe_type_of env evd c = - let j = execute env (ref evd) c in + let evdref = ref evd in + let env = enrich_env env evdref in + let j = execute env evdref c in j.uj_type (* Sort of a type *) let sort_of env evdref c = + let env = enrich_env env evdref in let j = execute env evdref c in let a = e_type_judgment env evdref j in a.utj_type @@ -284,6 +293,7 @@ let sort_of env evdref c = let type_of ?(refresh=false) env evd c = let evdref = ref evd in + let env = enrich_env env evdref in let j = execute env evdref c in (* side-effect on evdref *) if refresh then @@ -291,6 +301,7 @@ let type_of ?(refresh=false) env evd c = else !evdref, j.uj_type let e_type_of ?(refresh=false) env evdref c = + let env = enrich_env env evdref in let j = execute env evdref c in (* side-effect on evdref *) if refresh then @@ -300,6 +311,7 @@ let e_type_of ?(refresh=false) env evdref c = else j.uj_type let solve_evars env evdref c = + let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) nf_evar !evdref c diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 9421b2d859..b75fe7c928 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -8,7 +8,6 @@ open Term open Environ -open Evd (** {6 Reduction functions } *) val cbv_vm : env -> constr -> types -> constr |