aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml29
-rw-r--r--pretyping/evarconv.ml119
-rw-r--r--pretyping/evarconv.mli6
-rw-r--r--pretyping/glob_ops.ml16
-rw-r--r--pretyping/glob_ops.mli4
-rw-r--r--pretyping/glob_term.ml14
-rw-r--r--pretyping/pretyping.ml117
-rw-r--r--pretyping/pretyping.mli3
8 files changed, 155 insertions, 153 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a12a832f76..402a6f6ed3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) =
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
-(* TODO use some algebraic type with a case for unnamed univs so we
- can cleanly detype them. NB: this corresponds to a hack in
- Pretyping.interp_universe_level_name to convert Foo.xx strings into
- universes. *)
-let hack_qualid_of_univ_level sigma l =
- match Termops.reference_of_level sigma l with
- | Some qid -> qid
- | None ->
- let path = String.split_on_char '.' (Univ.Level.to_string l) in
- let path = List.rev_map Id.of_string_soft path in
- Libnames.qualid_of_dirpath (DirPath.make path)
+let detype_level_name sigma l =
+ if Univ.Level.is_sprop l then GSProp else
+ if Univ.Level.is_prop l then GProp else
+ if Univ.Level.is_set l then GSet else
+ match UState.id_of_level (Evd.evar_universe_context sigma) l with
+ | Some id -> GLocalUniv (CAst.make id)
+ | None -> GUniv l
let detype_universe sigma u =
- let fn (l, n) =
- let s =
- if Univ.Level.is_prop l then GProp else
- if Univ.Level.is_set l then GSet else
- GType (hack_qualid_of_univ_level sigma l) in
- (s, n) in
- List.map fn (Univ.Universe.repr u)
+ List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
let detype_sort sigma = function
| SProp -> UNamed [GSProp,0]
@@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn
(* Main detyping function *)
let detype_level sigma l =
- let l = hack_qualid_of_univ_level sigma l in
- UNamed (GType l)
+ UNamed (detype_level_name sigma l)
let detype_instance sigma l =
let l = EInstance.kind sigma l in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cdf2922516..d0b724b755 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -448,6 +448,58 @@ let compare_cumulative_instances evd variances u u' =
Success evd
| Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
+let compare_heads env evd ~nargs term term' =
+ let check_strict evd u u' =
+ let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+ try Success (Evd.add_constraints evd cstrs)
+ with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+ in
+ match EConstr.kind evd term, EConstr.kind evd term' with
+ | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
+ if Int.equal nargs 1 && Environ.is_array_type env c
+ then
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ check_strict evd u u'
+ | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+ | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
+ let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+ if not (Int.equal nargs needed)
+ then check_strict evd u u'
+ else
+ compare_cumulative_instances evd variances u u'
+ end
+ | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+ | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+ when Names.Construct.CanOrd.equal cons cons' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_variance with
+ | None -> check_strict evd u u'
+ | Some variances ->
+ let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+ if not (Int.equal nargs needed)
+ then check_strict evd u u'
+ else
+ Success (compare_constructor_instances evd u u')
+ end
+ | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
+ | _, _ -> anomaly (Pp.str "")
+
+
let conv_fun f flags on_types =
let typefn env evd pbty term1 term2 =
let flags = { (default_flags env) with
@@ -556,65 +608,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
else evar_eqappr_x flags env' evd CONV out2 out1
in
let rigids env evd sk term sk' term' =
- let check_strict evd u u' =
- let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
- try Success (Evd.add_constraints evd cstrs)
- with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
- in
- let compare_heads evd =
- match EConstr.kind evd term, EConstr.kind evd term' with
- | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
- if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c
- then
- let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
- compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
- else
- let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
- check_strict evd u u'
- | Const _, Const _ -> UnifFailure (evd, NotSameHead)
- | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
- if EInstance.is_empty u && EInstance.is_empty u' then Success evd
- else
- let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
- let mind = Environ.lookup_mind mi env in
- let open Declarations in
- begin match mind.mind_variance with
- | None -> check_strict evd u u'
- | Some variances ->
- let nparamsaplied = Stack.args_size sk in
- let nparamsaplied' = Stack.args_size sk' in
- let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
- if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
- then check_strict evd u u'
- else
- compare_cumulative_instances evd variances u u'
- end
- | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
- | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
- when Names.Construct.CanOrd.equal cons cons' ->
- if EInstance.is_empty u && EInstance.is_empty u' then Success evd
- else
- let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
- let mind = Environ.lookup_mind mi env in
- let open Declarations in
- begin match mind.mind_variance with
- | None -> check_strict evd u u'
- | Some variances ->
- let nparamsaplied = Stack.args_size sk in
- let nparamsaplied' = Stack.args_size sk' in
- let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
- if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
- then check_strict evd u u'
- else
- Success (compare_constructor_instances evd u u')
- end
- | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
- | _, _ -> anomaly (Pp.str "")
- in
- ise_and evd [(fun i ->
- try compare_heads i
- with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
- (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
+ let nargs = Stack.args_size sk in
+ let nargs' = Stack.args_size sk' in
+ if not (Int.equal nargs nargs') then UnifFailure (evd, NotSameArgSize)
+ else
+ ise_and evd [(fun i ->
+ try compare_heads env i ~nargs term term'
+ with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+ (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')]
in
let consume on_left (_, skF as apprF) (_,skM as apprM) i =
if not (Stack.is_empty skF && Stack.is_empty skM) then
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a5a8d1f916..be03ced7eb 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -84,6 +84,12 @@ val check_conv_record : env -> evar_map ->
(constr Stack.t * constr Stack.t) * constr *
(int option * constr)
+(** Compares two constants/inductives/constructors unifying their universes.
+ It required the number of arguments applied to the c/i/c in order to decided
+ the kind of check it must perform. *)
+val compare_heads : env -> evar_map ->
+ nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result
+
(** Try to solve problems of the form ?x[args] = c by second-order
matching, using typing to select occurrences *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f42c754ef5..86d2cc78e0 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with
| GSProp, GSProp
| GProp, GProp
| GSet, GSet -> true
- | GType u1, GType u2 -> Libnames.qualid_eq u1 u2
- | (GSProp|GProp|GSet|GType _), _ -> false
+ | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2
+ | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2
+ | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2
+ | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false
exception ComplexSort
@@ -60,19 +62,23 @@ let glob_sort_family = let open Sorts in function
| UNamed [GSet,0] -> InSet
| _ -> raise ComplexSort
-let glob_sort_expr_eq f u1 u2 =
+let map_glob_sort_gen f = function
+ | UNamed l -> UNamed (f l)
+ | UAnonymous _ as x -> x
+
+let glob_sort_gen_eq f u1 u2 =
match u1, u2 with
| UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
| UNamed l1, UNamed l2 -> f l1 l2
| (UNamed _ | UAnonymous _), _ -> false
let glob_sort_eq u1 u2 =
- glob_sort_expr_eq
+ glob_sort_gen_eq
(List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
u1 u2
let glob_level_eq u1 u2 =
- glob_sort_expr_eq glob_sort_name_eq u1 u2
+ glob_sort_gen_eq glob_sort_name_eq u1 u2
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 6da8173dce..5ad1a207f3 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,8 +11,12 @@
open Names
open Glob_term
+val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen
+
(** Equalities *)
+val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool
+
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a49c8abe26..a957bc0fcd 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -26,17 +26,23 @@ type glob_sort_name =
| GSProp (** representation of [SProp] literal *)
| GProp (** representation of [Prop] level *)
| GSet (** representation of [Set] level *)
- | GType of Libnames.qualid (** representation of a [Type] level *)
+ | GUniv of Univ.Level.t
+ | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *)
+ | GRawUniv of Univ.Level.t
+ (** Hack for funind, DO NOT USE
-type 'a glob_sort_expr =
+ Note that producing the similar Constrexpr.CRawType for printing
+ is OK, just don't try to reinterp it. *)
+
+type 'a glob_sort_gen =
| UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
| UNamed of 'a
(** levels, occurring in universe instances *)
-type glob_level = glob_sort_name glob_sort_expr
+type glob_level = glob_sort_name glob_sort_gen
(** sort expressions *)
-type glob_sort = (glob_sort_name * int) list glob_sort_expr
+type glob_sort = (glob_sort_name * int) list glob_sort_gen
type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b70ff20e32..9dbded75ba 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -130,53 +130,32 @@ let is_strict_universe_declarations =
(** Miscellaneous interpretation functions *)
-let interp_known_universe_level_name evd qid =
- try
- let open Libnames in
- if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
- else raise Not_found
- with Not_found ->
- let qid = Nametab.locate_universe qid in
- Univ.Level.make qid
-
-let interp_universe_level_name evd qid =
- try evd, interp_known_universe_level_name evd qid
+let universe_level_name evd ({CAst.v=id} as lid) =
+ try evd, Evd.universe_of_name evd id
with Not_found ->
- if Libnames.qualid_is_ident qid then (* Undeclared *)
- let id = Libnames.qualid_basename qid in
- if not (is_strict_universe_declarations ()) then
- new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
- else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared universe: " ++ Id.print id))
- else
- let dp, i = Libnames.repr_qualid qid in
- let num =
- try int_of_string (Id.to_string i)
- with Failure _ ->
- user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
- in
- let level = Univ.Level.(make (UGlobal.make dp num)) in
- let evd =
- try Evd.add_global_univ evd level
- with UGraph.AlreadyDeclared -> evd
- in evd, level
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd
+ else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name"
+ (Pp.(str "Undeclared universe: " ++ Id.print id))
-let interp_sort_name sigma = function
+let sort_name sigma = function
| GSProp -> sigma, Univ.Level.sprop
| GProp -> sigma, Univ.Level.prop
| GSet -> sigma, Univ.Level.set
- | GType l -> interp_universe_level_name sigma l
+ | GUniv u -> sigma, u
+ | GRawUniv u ->
+ (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u
+ | GLocalUniv l -> universe_level_name sigma l
-let interp_sort_info ?loc evd l =
+let sort_info ?loc evd l =
List.fold_left (fun (evd, u) (l,n) ->
- let evd', u' = interp_sort_name evd l in
+ let evd', u' = sort_name evd l in
let u' = Univ.Universe.make u' in
let u' = match n with
| 0 -> u'
| 1 -> Univ.Universe.super u'
| n ->
- user_err ?loc ~hdr:"interp_universe"
+ user_err ?loc ~hdr:"sort_info"
(Pp.(str "Cannot interpret universe increment +" ++ int n))
in (evd', Univ.sup u u'))
(evd, Univ.Universe.type0m) l
@@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id =
(*************************************************************************)
(* Main pretyping function *)
-let interp_known_glob_level ?loc evd = function
+let known_universe_level_name evd lid =
+ try Evd.universe_of_name evd lid.CAst.v
+ with Not_found ->
+ let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in
+ Univ.Level.make u
+
+let known_glob_level evd = function
| GSProp -> Univ.Level.sprop
| GProp -> Univ.Level.prop
| GSet -> Univ.Level.set
- | GType qid ->
- try interp_known_universe_level_name evd qid
+ | GUniv u -> u
+ | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.")
+ | GLocalUniv lid ->
+ try known_universe_level_name evd lid
with Not_found ->
- user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
+ user_err ?loc:lid.CAst.loc ~hdr:"known_level_info"
+ (str "Undeclared universe " ++ Id.print lid.CAst.v)
-let interp_glob_level ?loc evd : glob_level -> _ = function
+let glob_level ?loc evd : glob_level -> _ = function
| UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
- | UNamed s -> interp_sort_name evd s
+ | UNamed s -> sort_name evd s
-let interp_instance ?loc evd l =
+let instance ?loc evd l =
let evd, l' =
List.fold_left
(fun (evd, univs) l ->
- let evd, l = interp_glob_level ?loc evd l in
+ let evd, l = glob_level ?loc evd l in
(evd, l :: univs)) (evd, [])
l
in
@@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us =
let evd, instance =
match us with
| None -> evd, None
- | Some l -> interp_instance ?loc evd l
+ | Some l -> instance ?loc evd l
in
Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
@@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us =
let sigma, ty = type_of !!env sigma c in
sigma, make_judge c ty
-let interp_sort ?loc evd : glob_sort -> _ = function
+let sort ?loc evd : glob_sort -> _ = function
| UAnonymous {rigid} ->
let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in
evd, Univ.Universe.make l
- | UNamed l -> interp_sort_info ?loc evd l
+ | UNamed l -> sort_info ?loc evd l
let judge_of_sort ?loc evd s =
let judge =
@@ -469,11 +457,22 @@ let pretype_sort ?loc sigma s =
| UNamed [GProp,0] -> sigma, judge_of_prop
| UNamed [GSet,0] -> sigma, judge_of_set
| _ ->
- let sigma, s = interp_sort ?loc sigma s in
+ let sigma, s = sort ?loc sigma s in
judge_of_sort ?loc sigma s
-let new_type_evar env sigma loc =
- new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let new_typed_evar env sigma ?naming ~src tycon =
+ match tycon with
+ | Some ty ->
+ let sigma, c = new_evar env sigma ~src ?naming ty in
+ sigma, c, ty
+ | None ->
+ let sigma, ty = new_type_evar env sigma ~src in
+ let sigma, c = new_evar env sigma ~src ?naming ty in
+ let evk = fst (destEvar sigma c) in
+ let ido = Evd.evar_ident evk sigma in
+ let src = (fst src,Evar_kinds.EvarType (ido,evk)) in
+ let sigma = update_source sigma (fst (destEvar sigma ty)) src in
+ sigma, c, ty
let mark_obligation_evar sigma k evc =
match k with
@@ -636,13 +635,9 @@ struct
discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma =
- let sigma, ty =
- match tycon with
- | Some ty -> sigma, ty
- | None -> new_type_evar env sigma loc in
let k = Evar_kinds.MatchingVar kind in
- let sigma, uj_val = new_evar env sigma ~src:(loc,k) ty in
- sigma, { uj_val; uj_type = ty }
+ let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) tycon in
+ sigma, { uj_val; uj_type }
let pretype_hole self (k, naming, ext) =
fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -653,19 +648,15 @@ struct
| IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
| IntroAnonymous -> IntroAnonymous
| IntroFresh id -> IntroFresh (interp_ltac_id env id) in
- let sigma, ty =
- match tycon with
- | Some ty -> sigma, ty
- | None -> new_type_evar env sigma loc in
- let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
+ let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) ~naming tycon in
let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
- sigma, { uj_val; uj_type = ty }
+ sigma, { uj_val; uj_type }
| Some arg ->
let sigma, ty =
match tycon with
| Some ty -> sigma, ty
- | None -> new_type_evar env sigma loc in
+ | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
sigma, { uj_val = c; uj_type = ty }
@@ -1144,7 +1135,7 @@ struct
| None ->
let sigma, p = match tycon with
| Some ty -> sigma, ty
- | None -> new_type_evar env sigma loc
+ | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.CasesType false)
in
sigma, it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar sigma pred in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb4a6e273..5668098fe6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option
val clear_bidirectionality_hint : GlobRef.t -> unit
-val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
- glob_sort_name -> Univ.Level.t
+val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t
(** An auxiliary function for searching for fixpoint guard indexes *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:57:22 +0000