aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml3
-rw-r--r--pretyping/constr_matching.ml32
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/glob_ops.ml3
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/pretyping.ml23
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/reductionops.ml10
-rw-r--r--pretyping/univdecls.ml64
-rw-r--r--pretyping/univdecls.mli19
11 files changed, 119 insertions, 51 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1cc072a2a2..260cd04446 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,6 @@
open CErrors
open Util
open Pp
-open Flags
open Names
open Libnames
open Globnames
@@ -387,7 +386,7 @@ let add_coercion_in_graph (ic,source,target) =
old_inheritance_graph
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
- if is_ambig && not !quiet then
+ if is_ambig && not !Flags.quiet then
Feedback.msg_info (message_ambig !ambig_paths)
type coercion = {
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 886cfd880f..ca7f633dc5 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -90,7 +90,8 @@ let rec build_lambda sigma vars ctx m = match vars with
let pre, suf = List.chop (pred n) ctx in
let (na, t, suf) = match suf with
| [] -> assert false
- | (_, na, t) :: suf -> (na, t, suf)
+ | (_, id, t) :: suf ->
+ (Name id, t, suf)
in
(** Check that the abstraction is legal by generating a transitive closure of
its dependencies. *)
@@ -126,11 +127,11 @@ let rec build_lambda sigma vars ctx m = match vars with
mkRel 1 ::
List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
in
- let map i (id, na, c) =
+ let map i (na, id, c) =
let i = succ i in
let subst = List.skipn i subst in
let subst = List.map (fun c -> Vars.lift (- i) c) subst in
- (id, na, substl subst c)
+ (na, id, substl subst c)
in
let pre = List.mapi map pre in
let pre = List.filter_with clear pre in
@@ -150,11 +151,10 @@ let rec build_lambda sigma vars ctx m = match vars with
let rec extract_bound_aux k accu frels ctx = match ctx with
| [] -> accu
-| (na1, na2, _) :: ctx ->
+| (na, _, _) :: ctx ->
if Int.Set.mem k frels then
- begin match na1 with
+ begin match na with
| Name id ->
- let () = assert (match na2 with Anonymous -> false | Name _ -> true) in
let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
| Anonymous -> raise PatternMatchingFailure
@@ -167,13 +167,21 @@ let extract_bound_vars frels ctx =
let dummy_constr = EConstr.mkProp
let make_renaming ids = function
-| (Name id, Name _, _) ->
+| (Name id, _, _) ->
begin
try EConstr.mkRel (List.index Id.equal id ids)
with Not_found -> dummy_constr
end
| _ -> dummy_constr
+let push_binder na1 na2 t ctx =
+ let id2 = match na2 with
+ | Name id2 -> id2
+ | Anonymous ->
+ let avoid = List.map pi2 ctx in
+ Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
+ (na1, id2, t) :: ctx
+
let to_fix (idx, (nas, cs, ts)) =
let inj = EConstr.of_constr in
(idx, (nas, Array.map inj cs, Array.map inj ts))
@@ -306,19 +314,19 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
sorec ctx env subst c1 c2
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
- sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
+ sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
- sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
+ sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
+ sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2
| PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
+ sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -327,7 +335,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
let n = Context.Rel.length ctx_b2 in
let n' = Context.Rel.length ctx_b2' in
if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
- let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in
+ let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = push_binder Anonymous na t l in
let ctx_br = List.fold_left f ctx ctx_b2 in
let ctx_br' = List.fold_left f ctx ctx_b2' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1eb22cdb81..5e14307418 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -460,8 +460,11 @@ and detype_r d flags avoid env sigma t =
in GVar (Id.of_string s))
| Meta n ->
(* Meta in constr are not user-parsable and are mapped to Evar *)
- (* using numbers to be unparsable *)
- GEvar (Id.of_string ("M" ^ string_of_int n), [])
+ if n = Constr_matching.special_meta then
+ (* Using a dash to be unparsable *)
+ GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+ else
+ GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), [])
| Var id ->
(try let _ = Global.lookup_named id in GRef (VarRef id, None)
with Not_found -> GVar id)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index c40a24e3b7..e1576b9713 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -234,7 +234,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
let acc = Option.fold_left (f v') acc rtntypopt in
List.fold_left fold_pattern acc pl
| GLetTuple (nal,rtntyp,b,c) ->
- f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
+ f (List.fold_right (Name.fold_right g) nal v)
+ (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
| GIf (c,rtntyp,b1,b2) ->
f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
| GRec (_,idl,bll,tyl,bv) ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 88ca9b5ca8..b31ee03d8c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -397,8 +397,8 @@ let get_arity env ((ind,u),params) =
mib.mind_params_ctxt
else begin
assert (Int.equal nparams mib.mind_nparams_rec);
- let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
- snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+ let nnonrecparamdecls = mib.mind_nparams - mib.mind_nparams_rec in
+ snd (Termops.context_chop nnonrecparamdecls mib.mind_params_ctxt)
end in
let parsign = Vars.subst_instance_context u parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 79d2c3333b..ea1f2de539 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -222,18 +222,6 @@ let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
| None -> new_univ_level_variable ?loc univ_rigid evd
| Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
-let interp_sort ?loc evd = function
- | GProp -> evd, Prop Null
- | GSet -> evd, Prop Pos
- | GType n ->
- let evd, u = interp_universe ?loc evd n in
- evd, Type u
-
-let interp_elimination_sort = function
- | GProp -> InProp
- | GSet -> InSet
- | GType _ -> InType
-
type inference_hook = env -> evar_map -> evar -> evar_map * constr
type inference_flags = {
@@ -1103,15 +1091,6 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with
| GHole (knd, naming, None) ->
let loc = loc_of_glob_constr c in
- let rec is_Type c = match EConstr.kind !evdref c with
- | Sort s ->
- begin match ESorts.kind !evdref s with
- | Type _ -> true
- | Prop _ -> false
- end
- | Cast (c, _, _) -> is_Type c
- | _ -> false
- in
(match valcon with
| Some v ->
let s =
@@ -1119,7 +1098,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
| Sort s -> ESorts.kind sigma s
- | Evar ev when is_Type (existential_type sigma ev) ->
+ | Evar ev when is_Type sigma (existential_type sigma ev) ->
evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
| _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7395e94a09..5822f5add5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,7 +18,6 @@ open Evd
open EConstr
open Glob_term
open Evarutil
-open Misctypes
(** An auxiliary function for searching for fixpoint guard indexes *)
@@ -119,9 +118,6 @@ val ise_pretype_gen :
(** To embed constr in glob_constr *)
-val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
-val interp_elimination_sort : glob_sort -> sorts_family
-
val register_constr_interp0 :
('r, 'g, 't) Genarg.genarg_type ->
(unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c8b3307d76..d04dcb8e3b 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -29,3 +29,4 @@ Indrec
Cases
Pretyping
Unification
+Univdecls
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3563235434..2aa2f90131 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1438,17 +1438,13 @@ let sigma_univ_state =
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
(** FIXME *)
- let open Universes in
- let x = EConstr.Unsafe.to_constr x in
- let y = EConstr.Unsafe.to_constr y in
try
- let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in
let b, sigma =
let ans =
if pb == Reduction.CUMUL then
- Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+ EConstr.leq_constr_universes sigma x y
else
- Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+ EConstr.eq_constr_universes sigma x y
in
let ans = match ans with
| None -> None
@@ -1462,6 +1458,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
in
if b then sigma, true
else
+ 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
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
new file mode 100644
index 0000000000..d7c42d03af
--- /dev/null
+++ b/pretyping/univdecls.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Nameops
+open CErrors
+open Pp
+
+(** Local universes and constraints declarations *)
+type universe_decl =
+ (Id.t Loc.located 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 open Misctypes in
+ let u_of_id x =
+ match x with
+ | Misctypes.GProp -> Loc.tag Univ.Level.prop
+ | GSet -> Loc.tag Univ.Level.set
+ | GType None | GType (Some (_, Anonymous)) ->
+ user_err ~hdr:"interp_constraint"
+ (str "Cannot declare constraints on anonymous universes")
+ | GType (Some (loc, Name id)) ->
+ try loc, Evd.universe_of_name evd (Id.to_string id)
+ with Not_found ->
+ user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id)
+ in
+ let interp (evd,cstrs) (u, d, u') =
+ let lloc, ul = u_of_id u and rloc, u'l = u_of_id 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" (str "Universe inconsistency" (* TODO *))
+ in
+ List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+ let open Misctypes in
+ let pl = 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;
+ 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
new file mode 100644
index 0000000000..0c3b749cbf
--- /dev/null
+++ b/pretyping/univdecls.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Local universe and constraint declarations. *)
+type universe_decl =
+ (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val default_univ_decl : universe_decl
+
+val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr ->
+ Evd.evar_map * universe_decl
+
+val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option ->
+ Evd.evar_map * universe_decl
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:48:25 +0000