aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml20
-rw-r--r--pretyping/constr_matching.ml20
-rw-r--r--pretyping/constrexpr.ml153
-rw-r--r--pretyping/evarconv.ml11
-rw-r--r--pretyping/evarsolve.ml15
-rw-r--r--pretyping/genredexpr.ml66
-rw-r--r--pretyping/inductiveops.ml6
-rw-r--r--pretyping/miscops.ml21
-rw-r--r--pretyping/miscops.mli6
-rw-r--r--pretyping/nativenorm.mli2
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/pretyping.mllib4
-rw-r--r--pretyping/redops.ml44
-rw-r--r--pretyping/redops.mli15
-rw-r--r--pretyping/reductionops.ml20
-rw-r--r--pretyping/reductionops.mli8
-rw-r--r--pretyping/typeclasses_errors.ml4
-rw-r--r--pretyping/typeclasses_errors.mli4
-rw-r--r--pretyping/unification.ml94
-rw-r--r--pretyping/univdecls.ml52
-rw-r--r--pretyping/univdecls.mli21
21 files changed, 121 insertions, 477 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ee7c39982..1edce17bd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -574,7 +574,7 @@ let dependent_decl sigma a =
let rec dep_in_tomatch sigma n = function
| (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l
- | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l
+ | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l
| [] -> false
let dependencies_in_rhs sigma nargs current tms eqns =
@@ -1704,9 +1704,11 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
List.map_i
(fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
(rel_context extenv) in
- let rel_filter =
- List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u
- || Int.Set.mem (destRel !evdref a) depvl) inst in
+ let map a = match EConstr.kind !evdref a with
+ | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl
+ | _ -> true
+ in
+ let rel_filter = List.map map inst in
let named_filter =
List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
(named_context extenv) in
@@ -1848,7 +1850,7 @@ let build_inversion_problem loc env sigma tms t =
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
let s' = Retyping.get_sort_of env sigma t in
- let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
+ let sigma, s = Evd.new_sort_variable univ_flexible sigma in
let sigma = Evd.set_leq_sort env sigma s' s in
let evdref = ref sigma in
let pb =
@@ -1937,8 +1939,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match EConstr.kind sigma tm with
- | Rel n when dependent sigma tm c
- && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
+ | Rel n when Int.equal signlen 1 && not (noccurn sigma n c)
+ (* The term to match is not of a dependent type itself *) ->
((n, len) :: subst, len - signlen)
| Rel n when signlen > 1 (* The term is of a dependent type,
maybe some variable in its type appears in the tycon. *) ->
@@ -1949,13 +1951,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_left
(fun (subst, len) arg ->
match EConstr.kind sigma arg with
- | Rel n when dependent sigma arg c ->
+ | Rel n when not (noccurn sigma n c) ->
((n, len) :: subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent sigma tm c && List.for_all (isRel sigma) realargs
+ if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs
then (n, len) :: subst else subst
in (subst, pred len))
| _ -> (subst, len - signlen))
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 22da5315f..2bc603a90 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -59,7 +59,7 @@ let warn_meta_collision =
strbrk " and a metavariable of same name.")
-let constrain sigma n (ids, m) (names, terms as subst) =
+let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) =
let open EConstr in
try
let (ids', m') = Id.Map.find n terms in
@@ -67,19 +67,21 @@ let constrain sigma n (ids, m) (names, terms as subst) =
else raise PatternMatchingFailure
with Not_found ->
let () = if Id.Map.mem n names then warn_meta_collision n in
- (names, Id.Map.add n (ids, m) terms)
+ (names_seen, Id.Map.add n (ids, m) terms)
-let add_binders na1 na2 binding_vars (names, terms as subst) =
+let add_binders na1 na2 binding_vars ((names,seen), terms as subst) =
match na1, na2 with
| Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
if Id.Map.mem id1 names then
let () = Glob_ops.warn_variable_collision id1 in
- (names, terms)
+ subst
else
+ let id2 = Namegen.next_ident_away id2 seen in
let names = Id.Map.add id1 id2 names in
+ let seen = Id.Set.add id2 seen in
let () = if Id.Map.mem id1 terms then
warn_meta_collision id1 in
- (names, terms)
+ ((names,seen), terms)
| _ -> subst
let rec build_lambda sigma vars ctx m = match vars with
@@ -413,13 +415,15 @@ let matches_core env sigma allow_bound_rels
| PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure
in
- sorec [] env (Id.Map.empty, Id.Map.empty) pat c
+ sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
let matches_core_closed env sigma pat c =
let names, subst = matches_core env sigma false pat c in
- (names, Id.Map.map snd subst)
+ (fst names, Id.Map.map snd subst)
-let extended_matches env sigma = matches_core env sigma true
+let extended_matches env sigma pat c =
+ let (names,_), subst = matches_core env sigma true pat c in
+ names, subst
let matches env sigma pat c =
snd (matches_core_closed env sigma (Id.Set.empty,pat) c)
diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
deleted file mode 100644
index 1443dfb51..000000000
--- a/pretyping/constrexpr.ml
+++ /dev/null
@@ -1,153 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-open Libnames
-open Misctypes
-open Decl_kinds
-
-(** {6 Concrete syntax for terms } *)
-
-(** [constr_expr] is the abstract syntax tree produced by the parser *)
-
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
-
-type ident_decl = lident * universe_decl_expr option
-type name_decl = lname * universe_decl_expr option
-
-type notation = string
-
-type explicitation =
- | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
- | ExplByName of Id.t
-
-type binder_kind =
- | Default of binding_kind
- | Generalized of binding_kind * binding_kind * bool
- (** Inner binding, outer bindings, typeclass-specific flag
- for implicit generalization of superclasses *)
-
-type abstraction_kind = AbsLambda | AbsPi
-
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-
-(** Representation of integer literals that appear in Coq scripts.
- We now use raw strings of digits in base 10 (big-endian), and a separate
- sign flag. Note that this representation is not unique, due to possible
- multiple leading zeros, and -0 = +0 *)
-
-type sign = bool
-type raw_natural_number = string
-
-type prim_token =
- | Numeral of raw_natural_number * sign
- | String of string
-
-type instance_expr = Glob_term.glob_level list
-
-type cases_pattern_expr_r =
- | CPatAlias of cases_pattern_expr * lname
- | CPatCstr of reference
- * cases_pattern_expr list option * cases_pattern_expr list
- (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
- | CPatAtom of reference option
- | CPatOr of cases_pattern_expr list
- | CPatNotation of notation * cases_pattern_notation_substitution
- * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
- (notation n applied with substitution l1)
- applied to arguments l2 *)
- | CPatPrim of prim_token
- | CPatRecord of (reference * cases_pattern_expr) list
- | CPatDelimiters of string * cases_pattern_expr
- | CPatCast of cases_pattern_expr * constr_expr
-and cases_pattern_expr = cases_pattern_expr_r CAst.t
-
-and cases_pattern_notation_substitution =
- cases_pattern_expr list * (** for constr subterms *)
- cases_pattern_expr list list (** for recursive notations *)
-
-and constr_expr_r =
- | CRef of reference * instance_expr option
- | CFix of lident * fix_expr list
- | CCoFix of lident * cofix_expr list
- | CProdN of local_binder_expr list * constr_expr
- | CLambdaN of local_binder_expr list * constr_expr
- | CLetIn of lname * constr_expr * constr_expr option * constr_expr
- | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
- | CApp of (proj_flag * constr_expr) *
- (constr_expr * explicitation CAst.t option) list
- | CRecord of (reference * constr_expr) list
-
- (* representation of the "let" and "match" constructs *)
- | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *)
- * constr_expr option (* return-clause *)
- * case_expr list
- * branch_expr list (* branches *)
-
- | CLetTuple of lname list * (lname option * constr_expr option) *
- constr_expr * constr_expr
- | CIf of constr_expr * (lname option * constr_expr option)
- * constr_expr * constr_expr
- | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
- | CPatVar of patvar
- | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
- | CSort of Glob_term.glob_sort
- | CCast of constr_expr * constr_expr cast_type
- | CNotation of notation * constr_notation_substitution
- | CGeneralization of binding_kind * abstraction_kind option * constr_expr
- | CPrim of prim_token
- | CDelimiters of string * constr_expr
- | CProj of reference * constr_expr
-and constr_expr = constr_expr_r CAst.t
-
-and case_expr = constr_expr (* expression that is being matched *)
- * lname option (* as-clause *)
- * cases_pattern_expr option (* in-clause *)
-
-and branch_expr =
- (cases_pattern_expr list list * constr_expr) CAst.t
-
-and fix_expr =
- lident * (lident option * recursion_order_expr) *
- local_binder_expr list * constr_expr * constr_expr
-
-and cofix_expr =
- lident * local_binder_expr list * constr_expr * constr_expr
-
-and recursion_order_expr =
- | CStructRec
- | CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-
-(* Anonymous defs allowed ?? *)
-and local_binder_expr =
- | CLocalAssum of lname list * binder_kind * constr_expr
- | CLocalDef of lname * constr_expr * constr_expr option
- | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
-
-and constr_notation_substitution =
- constr_expr list * (** for constr subterms *)
- constr_expr list list * (** for recursive notations *)
- cases_pattern_expr list * (** for binders *)
- local_binder_expr list list (** for binder lists (recursive notations) *)
-
-type constr_pattern_expr = constr_expr
-
-(** Concrete syntax for modules and module types *)
-
-type with_declaration_ast =
- | CWith_Module of Id.t list CAst.t * qualid CAst.t
- | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
-
-type module_ast_r =
- | CMident of qualid
- | CMapply of module_ast * module_ast
- | CMwith of module_ast * with_declaration_ast
-and module_ast = module_ast_r CAst.t
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 062136ff5..6d08f66c1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
let ground_test =
if is_ground_term evd term1 && is_ground_term evd term2 then (
let e =
- try
- let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
- env evd term1 term2
- in
- if b then Success evd
- else UnifFailure (evd, ConversionFailed (env,term1,term2))
- with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+ match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+ | Some evd -> Success evd
+ | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
+ | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
in
match e with
| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7eaff078..aefae1ecc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -525,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t =
match Option.List.map map l with
| Some l ->
begin match find_unification_pattern_args env evd l t with
- | Some _ as x when not (dependent evd (mkMeta m) t) -> x
+ | Some _ as x when not (occur_metavariable evd m t) -> x
| _ -> None
end
| None ->
@@ -1068,8 +1068,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
let rhs = expand_vars_in_term env evd rhs in
- let filter =
- restrict_upon_filter evd evk
+ let filter a = match EConstr.kind evd a with
+ | Rel n -> not (noccurn evd n rhs)
+ | Var id ->
+ local_occur_var evd id rhs
+ || List.exists (fun (id', _) -> Id.equal id id') sols
+ | _ -> true
+ in
+ let filter = restrict_upon_filter evd evk filter argsv in
(* Keep only variables that occur in rhs *)
(* This is not safe: is the variable is a local def, its body *)
(* may contain references to variables that are removed, leading to *)
@@ -1077,9 +1083,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
(* that says that the body is hidden. Note that expand_vars_in_term *)
(* expands only rels and vars aliases, not rels or vars bound to an *)
(* arbitrary complex term *)
- (fun a -> not (isRel evd a || isVar evd a)
- || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols)
- argsv in
let filter = closure_of_filter evd evk filter in
let candidates = extract_candidates sols in
match candidates with
diff --git a/pretyping/genredexpr.ml b/pretyping/genredexpr.ml
deleted file mode 100644
index 80697461a..000000000
--- a/pretyping/genredexpr.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Reduction expressions *)
-
-(** The parsing produces initially a list of [red_atom] *)
-
-type 'a red_atom =
- | FBeta
- | FMatch
- | FFix
- | FCofix
- | FZeta
- | FConst of 'a list
- | FDeltaBut of 'a list
-
-(** This list of atoms is immediately converted to a [glob_red_flag] *)
-
-type 'a glob_red_flag = {
- rBeta : bool;
- rMatch : bool;
- rFix : bool;
- rCofix : bool;
- rZeta : bool;
- rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
- rConst : 'a list
-}
-
-(** Generic kinds of reductions *)
-
-type ('a,'b,'c) red_expr_gen =
- | Red of bool
- | Hnf
- | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
- | Cbv of 'b glob_red_flag
- | Cbn of 'b glob_red_flag
- | Lazy of 'b glob_red_flag
- | Unfold of 'b Locus.with_occurrences list
- | Fold of 'a list
- | Pattern of 'a Locus.with_occurrences list
- | ExtraRedExpr of string
- | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
- | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
-
-type ('a,'b,'c) may_eval =
- | ConstrTerm of 'a
- | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of Misctypes.lident * 'a
- | ConstrTypeOf of 'a
-
-open Libnames
-open Constrexpr
-open Misctypes
-
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-
-type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 8e3c33ff7..b1ab2d2b7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -629,6 +629,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
env evdref scl ar.template_level (ctx,ar.template_param_levels) in
!evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
+let type_of_projection_constant env (p,u) =
+ let pb = lookup_projection p env in
+ Vars.subst_instance_constr u pb.proj_type
+
let type_of_projection_knowing_arg env sigma p c ty =
let c = EConstr.Unsafe.to_constr c in
let IndType(pars,realargs) =
@@ -637,7 +641,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
in
let (_,u), pars = dest_ind_family pars in
- substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u))
+ substl (c :: List.rev pars) (type_of_projection_constant env (p,u))
(***********************************************)
(* Guard condition *)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1b536bfda..1697e54ab 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,7 +10,6 @@
open Util
open Misctypes
-open Genredexpr
(** Mapping [cast_type] *)
@@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
| _ -> false
-(** Mapping [red_expr_gen] *)
-
-let map_flags f flags =
- { flags with rConst = List.map f flags.rConst }
-
-let map_occs f (occ,e) = (occ,f e)
-
-let map_red_expr_gen f g h = function
- | Fold l -> Fold (List.map f l)
- | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
- | Simpl (flags,occs_o) ->
- Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
- | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
- | Cbv flags -> Cbv (map_flags g flags)
- | Lazy flags -> Lazy (map_flags g flags)
- | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
- | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
- | Cbn flags -> Cbn (map_flags g flags)
- | ExtraRedExpr _ | Red _ | Hnf as x -> x
-
(** Mapping bindings *)
let map_explicit_bindings f l =
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 1d4504541..6a84fb9eb 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Misctypes
-open Genredexpr
(** Mapping [cast_type] *)
@@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
val intro_pattern_naming_eq :
intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
- ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
-
(** Mapping bindings *)
val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 67b7a2a40..4997d0bf0 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr
(** Conversion with inference of universe constraints *)
val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool
+ evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92f87ab95..b2507b5f2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
if not (occur_existential !evdref cty || occur_existential !evdref tval) then
- let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
else user_err ?loc (str "Cannot check cast with vm: " ++
@@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
begin
- let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
end
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c48decdb0..3d9b5d3cf 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -16,13 +16,10 @@ Evarsolve
Recordops
Evarconv
Typing
-Constrexpr
-Genredexpr
Miscops
Glob_term
Ltac_pretype
Glob_ops
-Redops
Pattern
Patternops
Constr_matching
@@ -37,4 +34,3 @@ Indrec
Cases
Pretyping
Unification
-Univdecls
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
deleted file mode 100644
index 90c3bdfae..000000000
--- a/pretyping/redops.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Genredexpr
-
-let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
-
-let make_red_flag l =
- let rec add_flag red = function
- | [] -> red
- | FBeta :: lf -> add_flag { red with rBeta = true } lf
- | FMatch :: lf -> add_flag { red with rMatch = true } lf
- | FFix :: lf -> add_flag { red with rFix = true } lf
- | FCofix :: lf -> add_flag { red with rCofix = true } lf
- | FZeta :: lf -> add_flag { red with rZeta = true } lf
- | FConst l :: lf ->
- if red.rDelta then
- CErrors.user_err Pp.(str
- "Cannot set both constants to unfold and constants not to unfold");
- add_flag { red with rConst = union_consts red.rConst l } lf
- | FDeltaBut l :: lf ->
- if red.rConst <> [] && not red.rDelta then
- CErrors.user_err Pp.(str
- "Cannot set both constants to unfold and constants not to unfold");
- add_flag
- { red with rConst = union_consts red.rConst l; rDelta = true }
- lf
- in
- add_flag
- {rBeta = false; rMatch = false; rFix = false; rCofix = false;
- rZeta = false; rDelta = false; rConst = []}
- l
-
-
-let all_flags =
- {rBeta = true; rMatch = true; rFix = true; rCofix = true;
- rZeta = true; rDelta = true; rConst = []}
diff --git a/pretyping/redops.mli b/pretyping/redops.mli
deleted file mode 100644
index 285931ecd..000000000
--- a/pretyping/redops.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Genredexpr
-
-val make_red_flag : 'a red_atom list -> 'a glob_red_flag
-
-val all_flags : 'a glob_red_flag
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6fde86837..7fb1a0a57 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
(** FIXME *)
try
- let b, sigma =
- let ans =
- if pb == Reduction.CUMUL then
+ let ans = match pb with
+ | Reduction.CUMUL ->
EConstr.leq_constr_universes env sigma x y
- else
+ | Reduction.CONV ->
EConstr.eq_constr_universes env sigma x y
in
let ans = match ans with
@@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
in
match ans with
- | None -> false, sigma
- | Some sigma -> true, sigma
- in
- if b then sigma, true
- else
+ | Some sigma -> ans
+ | None ->
let x = EConstr.Unsafe.to_constr x in
let y = EConstr.Unsafe.to_constr y in
let sigma' =
conv_fun pb ~l2r:false sigma ts
env (sigma, sigma_univ_state) x y in
- sigma', true
+ Some sigma'
with
- | Reduction.NotConvertible -> sigma, false
- | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
+ | Reduction.NotConvertible -> None
+ | Univ.UniverseInconsistency _ when catch_incon -> None
| e when is_anomaly e -> report_anomaly e
let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ad280d9f3..9256fa7ce 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con
otherwise returns false in that case.
*)
val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state ->
- env -> evar_map -> constr -> constr -> evar_map * bool
+ env -> evar_map -> constr -> constr -> evar_map option
(** Conversion with inference of universe constraints *)
val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool) -> unit
+ evar_map option) -> unit
val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool
+ evar_map option
(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
@@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *)
val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
(Constr.constr, evar_map) Reduction.generic_conversion_function) ->
?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
- evar_map -> constr -> constr -> evar_map * bool
+ evar_map -> constr -> constr -> evar_map option
(** {6 Special-Purpose Reduction Functions } *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 89c5d7e7b..a1ac53c73 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,7 +12,6 @@
open Names
open EConstr
open Environ
-open Constrexpr
(*i*)
type contexts = Parameters | Properties
@@ -20,7 +19,6 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
exception TypeClassError of env * typeclass_error
@@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err))
let not_a_class env c = typeclass_error env (NotAClass c)
let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
-
-let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 4aabc0aee..1003f2ae1 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -11,14 +11,12 @@
open Names
open EConstr
open Environ
-open Constrexpr
type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
exception TypeClassError of env * typeclass_error
@@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a
val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
-
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 62bee5a36..a8a4003dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -579,16 +579,16 @@ let constr_cmp pb env sigma flags t u =
in
match cstrs with
| Some cstrs ->
- begin try Evd.add_universe_constraints sigma cstrs, true
- with Univ.UniverseInconsistency _ -> sigma, false
+ begin try Some (Evd.add_universe_constraints sigma cstrs)
+ with Univ.UniverseInconsistency _ -> None
| Evd.UniversesDiffer ->
if is_rigid_head sigma flags t then
- try Evd.add_universe_constraints sigma (force_eqs cstrs), true
- with Univ.UniverseInconsistency _ -> sigma, false
- else sigma, false
+ try Some (Evd.add_universe_constraints sigma (force_eqs cstrs))
+ with Univ.UniverseInconsistency _ -> None
+ else None
end
| None ->
- sigma, false
+ None
let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
@@ -623,9 +623,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
| None -> sigma
| Some n ->
if is_ground_term sigma m && is_ground_term sigma n then
- let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in
- if b then sigma
- else error_cannot_unify env sigma (m,n)
+ match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
+ | Some sigma -> sigma
+ | None -> error_cannot_unify env sigma (m,n)
else sigma
@@ -698,7 +698,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
else sigma,(k2,cM,stM)::metasubst,evarsubst
| Meta k, _
- when not (dependent sigma cM cN) (* helps early trying alternatives *) ->
+ when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
@@ -718,7 +718,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Meta k
- when not (dependent sigma cN cM) (* helps early trying alternatives *) ->
+ when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
@@ -740,11 +740,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Evar (evk,_ as ev), Evar (evk',_)
when not (Evar.Set.mem evk flags.frozen_evars)
&& Evar.equal evk evk' ->
- let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
- if b then
- sigma',metasubst,evarsubst
- else
+ begin match constr_cmp cv_pb env sigma flags cM cN with
+ | Some sigma ->
+ sigma, metasubst, evarsubst
+ | None ->
sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ end
| Evar (evk,_ as ev), _
when not (Evar.Set.mem evk flags.frozen_evars)
&& not (occur_evar sigma evk cN) ->
@@ -837,6 +838,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
with ex when precatchable_exception ex ->
reduce curenvnb pb opt substn cM cN)
+ | Fix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(_,tl2,bl2)) when
+ Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 ->
+ (try
+ let opt' = {opt with at_top = true; with_types = false} in
+ let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
+ Array.fold_left2 (unirec_rec curenvnb' CONV opt')
+ (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
+ with ex when precatchable_exception ex ->
+ reduce curenvnb pb opt substn cM cN)
+
+ | CoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(_,tl2,bl2)) when
+ Int.equal i1 i2 ->
+ (try
+ let opt' = {opt with at_top = true; with_types = false} in
+ let curenvnb' = Array.fold_right2 (fun na t -> push (na,t)) lna1 tl1 curenvnb in
+ Array.fold_left2 (unirec_rec curenvnb' CONV opt')
+ (Array.fold_left2 (unirec_rec curenvnb CONV opt') substn tl1 tl2) bl1 bl2
+ with ex when precatchable_exception ex ->
+ reduce curenvnb pb opt substn cM cN)
+
| App (f1,l1), _ when
(isMeta sigma f1 && use_metas_pattern_unification sigma flags nb l1
|| use_evars_pattern_unification flags && isAllowedEvar sigma flags f1) ->
@@ -922,9 +943,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
- let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
- if b then (sigma', metas, evars)
- else
+ match constr_cmp cv_pb env sigma flags cM cN with
+ | Some sigma -> (sigma, metas, evars)
+ | None ->
try reduce curenvnb pb opt substn cM cN
with ex when precatchable_exception ex ->
let (f1,l1) =
@@ -981,12 +1002,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
(* Renounce, maybe metas/evars prevents typing *) sigma
else sigma
in
- let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
- if b then Some (sigma, metasubst, evarsubst)
- else
- if is_ground_term sigma m1 && is_ground_term sigma n1 then
- error_cannot_unify curenv sigma (cM,cN)
- else None
+ match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
+ | Some sigma ->
+ Some (sigma, metasubst, evarsubst)
+ | None ->
+ if is_ground_term sigma m1 && is_ground_term sigma n1 then
+ error_cannot_unify curenv sigma (cM,cN)
+ else None
in
match res with
| Some substn -> substn
@@ -1089,11 +1111,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
then
None
else
- let sigma, b = match flags.modulo_conv_on_closed_terms with
+ let ans = match flags.modulo_conv_on_closed_terms with
| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
| _ -> constr_cmp cv_pb env sigma flags m n in
- if b then Some sigma
- else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ match ans with
+ | Some sigma -> ans
+ | None ->
+ if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some (cv_id, cv_k), (dl_id, dl_k) ->
Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
| None,(dl_id, dl_k) ->
@@ -1391,7 +1415,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
and mimick_undefined_evar evd flags hdc nargs sp =
let ev = Evd.find_undefined evd sp in
- let sp_env = Global.env_of_context ev.evar_hyps in
+ let sp_env = Global.env_of_context (evar_filtered_hyps ev) in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
@@ -1500,7 +1524,8 @@ let indirectly_dependent sigma c d decls =
it is needed otherwise, as e.g. when abstracting over "2" in
"forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
way to see that the second hypothesis depends indirectly over 2 *)
- List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
+ let open Context.Named.Declaration in
+ List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
@@ -1582,8 +1607,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
let merge_fun c1 c2 =
match c1, c2 with
| Some (evd,c1,x), Some (_,c2,_) ->
- let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
- if b then Some (evd, c1, x) else raise (NotUnifiable None)
+ begin match infer_conv ~pb:CONV env evd c1 c2 with
+ | Some evd -> Some (evd, c1, x)
+ | None -> raise (NotUnifiable None)
+ end
| Some _, None -> c1
| None, Some _ -> c2
| None, None -> None in
@@ -1900,10 +1927,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
let typp = Typing.meta_type evd' p in
let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
- let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
- if not b then
+ match infer_conv ~pb:CUMUL env evd' predtyp typp with
+ | None ->
error_wrong_abstraction_type env evd'
(Evd.meta_name evd p) pred typp predtyp;
+ | Some evd' ->
w_merge env false flags.merge_unify_flags
(evd',[p,pred,(Conv,TypeProcessed)],[])
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
deleted file mode 100644
index 8864be576..000000000
--- a/pretyping/univdecls.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open CErrors
-
-(** Local universes and constraints declarations *)
-type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let default_univ_decl =
- let open Misctypes in
- { univdecl_instance = [];
- univdecl_extensible_instance = true;
- univdecl_constraints = Univ.Constraint.empty;
- univdecl_extensible_constraints = true }
-
-let interp_univ_constraints env evd cstrs =
- let interp (evd,cstrs) (u, d, u') =
- let ul = Pretyping.interp_known_glob_level evd u in
- let u'l = Pretyping.interp_known_glob_level evd u' in
- let cstr = (ul,d,u'l) in
- let cstrs' = Univ.Constraint.add cstr cstrs in
- try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
- evd, cstrs'
- with Univ.UniverseInconsistency e ->
- user_err ~hdr:"interp_constraint"
- (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
- in
- List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
- let open Misctypes in
- let pl : lident list = decl.univdecl_instance in
- let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
- let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
- let decl = { univdecl_instance = pl;
- univdecl_extensible_instance = decl.univdecl_extensible_instance;
- univdecl_constraints = cstrs;
- univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
- in evd, decl
-
-let interp_univ_decl_opt env l =
- match l with
- | None -> Evd.from_env env, default_univ_decl
- | Some decl -> interp_univ_decl env decl
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
deleted file mode 100644
index 305d045b1..000000000
--- a/pretyping/univdecls.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Local universe and constraint declarations. *)
-type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-val default_univ_decl : universe_decl
-
-val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
- Evd.evar_map * universe_decl
-
-val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
- Evd.evar_map * universe_decl
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 07:07:26 +0000