aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml14
-rw-r--r--engine/eConstr.mli30
-rw-r--r--engine/evarutil.ml9
-rw-r--r--engine/evd.ml6
-rw-r--r--engine/namegen.ml34
-rw-r--r--engine/namegen.mli12
-rw-r--r--engine/nameops.ml6
-rw-r--r--engine/nameops.mli3
-rw-r--r--engine/proofview.ml4
-rw-r--r--engine/termops.ml34
-rw-r--r--engine/termops.mli12
-rw-r--r--engine/uState.ml15
-rw-r--r--engine/univGen.ml5
-rw-r--r--engine/univMinim.ml3
14 files changed, 109 insertions, 78 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8756ebfdf2..981f9454e4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -48,9 +48,10 @@ type 'a puniverses = 'a * EInstance.t
let in_punivs a = (a, EInstance.empty)
+let mkSProp = of_kind (Sort (ESorts.make Sorts.sprop))
let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
let mkSet = of_kind (Sort (ESorts.make Sorts.set))
-let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u)))
+let mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u)))
let mkRel n = of_kind (Rel n)
let mkVar id = of_kind (Var id)
let mkMeta n = of_kind (Meta n)
@@ -72,7 +73,8 @@ let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
let mkFix f = of_kind (Fix f)
let mkCoFix f = of_kind (CoFix f)
let mkProj (p, c) = of_kind (Proj (p, c))
-let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
+let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
let mkInt i = of_kind (Int i)
let mkRef (gr,u) = let open GlobRef in match gr with
@@ -81,6 +83,8 @@ let mkRef (gr,u) = let open GlobRef in match gr with
| ConstructRef c -> mkConstructU (c,u)
| VarRef x -> mkVar x
+let type1 = mkSort Sorts.type1
+
let applist (f, arg) = mkApp (f, Array.of_list arg)
let applistc f arg = mkApp (f, Array.of_list arg)
@@ -665,9 +669,9 @@ let mkLambda_or_LetIn decl c =
| LocalAssum (na,t) -> mkLambda (na, t, c)
| LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
-let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
-let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
-let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
+let mkNamedProd id typ c = mkProd (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLambda id typ c = mkLambda (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (map_annot Name.mk_name id, c1, t, Vars.subst_var id.binder_name c2)
let mkNamedProd_or_LetIn decl c =
let open Context.Named.Declaration in
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2f4cf7d5d0..25ceffbd04 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -104,13 +104,14 @@ val mkVar : Id.t -> t
val mkMeta : metavariable -> t
val mkEvar : t pexistential -> t
val mkSort : Sorts.t -> t
+val mkSProp : t
val mkProp : t
val mkSet : t
val mkType : Univ.Universe.t -> t
val mkCast : t * cast_kind * t -> t
-val mkProd : Name.t * t * t -> t
-val mkLambda : Name.t * t * t -> t
-val mkLetIn : Name.t * t * t * t -> t
+val mkProd : Name.t Context.binder_annot * t * t -> t
+val mkLambda : Name.t Context.binder_annot * t * t -> t
+val mkLetIn : Name.t Context.binder_annot * t * t * t -> t
val mkApp : t * t array -> t
val mkConst : Constant.t -> t
val mkConstU : Constant.t * EInstance.t -> t
@@ -123,11 +124,14 @@ val mkConstructUi : (inductive * EInstance.t) * int -> t
val mkCase : case_info * t * t * t array -> t
val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
-val mkArrow : t -> t -> t
+val mkArrow : t -> Sorts.relevance -> t -> t
+val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkRef : GlobRef.t * EInstance.t -> t
+val type1 : t
+
val applist : t * t list -> t
val applistc : t -> t list -> t
@@ -136,9 +140,9 @@ val mkLambda_or_LetIn : rel_declaration -> t -> t
val it_mkProd_or_LetIn : t -> rel_context -> t
val it_mkLambda_or_LetIn : t -> rel_context -> t
-val mkNamedLambda : Id.t -> types -> constr -> constr
-val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
-val mkNamedProd : Id.t -> types -> types -> types
+val mkNamedLambda : Id.t Context.binder_annot -> types -> constr -> constr
+val mkNamedLetIn : Id.t Context.binder_annot -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t Context.binder_annot -> types -> types -> types
val mkNamedLambda_or_LetIn : named_declaration -> types -> types
val mkNamedProd_or_LetIn : named_declaration -> types -> types
@@ -176,9 +180,9 @@ val destMeta : Evd.evar_map -> t -> metavariable
val destVar : Evd.evar_map -> t -> Id.t
val destSort : Evd.evar_map -> t -> ESorts.t
val destCast : Evd.evar_map -> t -> t * cast_kind * t
-val destProd : Evd.evar_map -> t -> Name.t * types * types
-val destLambda : Evd.evar_map -> t -> Name.t * types * t
-val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
+val destProd : Evd.evar_map -> t -> Name.t Context.binder_annot * types * types
+val destLambda : Evd.evar_map -> t -> Name.t Context.binder_annot * types * t
+val destLetIn : Evd.evar_map -> t -> Name.t Context.binder_annot * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t pexistential
@@ -194,7 +198,7 @@ val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
val decompose_app : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)
-val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_lam : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t
(** Pops lambda abstractions and letins until there are no more, skipping casts. *)
val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
@@ -210,10 +214,10 @@ val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
@raise UserError if the term doesn't have enough lambdas/letins. *)
val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
-val compose_lam : (Name.t * t) list -> t -> t
+val compose_lam : (Name.t Context.binder_annot * t) list -> t -> t
val to_lambda : Evd.evar_map -> int -> t -> t
-val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_prod : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t
val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t
val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 840c14b241..96beb72a56 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -11,6 +11,7 @@
open CErrors
open Util
open Names
+open Context
open Constr
open Environ
open Evd
@@ -781,13 +782,13 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
in
NamedDecl.fold_constr fold decl accu
| Some cache ->
- let id = NamedDecl.get_id decl in
+ let id = NamedDecl.get_annot decl in
let r =
- try Id.Map.find id cache.cache
+ try Id.Map.find id.binder_name cache.cache
with Not_found ->
(* Dummy value *)
let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
- let () = cache.cache <- Id.Map.add id r cache.cache in
+ let () = cache.cache <- Id.Map.add id.binder_name r cache.cache in
r
in
let (decl', evs) = !r in
@@ -836,7 +837,7 @@ let occur_evar_upto sigma n c =
let judge_of_new_Type evd =
let open EConstr in
let (evd', s) = new_univ_variable univ_rigid evd in
- (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) })
+ (evd', { uj_val = mkType s; uj_type = mkType (Univ.super s) })
let subterm_source evk ?where (loc,k) =
let evk = match k with
diff --git a/engine/evd.ml b/engine/evd.ml
index dd2be29bd9..b89222cf8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -898,7 +898,7 @@ let new_univ_variable ?loc ?name rigid evd =
let new_sort_variable ?loc ?name rigid d =
let (d', u) = new_univ_variable ?loc rigid ?name d in
- (d', Type u)
+ (d', Sorts.sort_of_univ u)
let add_global_univ d u =
{ d with universes = UState.add_global_univ d.universes u }
@@ -962,10 +962,10 @@ let normalize_universe_instance evd l =
let normalize_sort evars s =
match s with
- | Prop | Set -> s
+ | SProp | Prop | Set -> s
| Type u ->
let u' = normalize_universe evars u in
- if u' == u then s else Type u'
+ if u' == u then s else Sorts.sort_of_univ u'
(* FIXME inefficient *)
let set_eq_sort env d s1 s2 =
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ef4108c22..10ece55a63 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -18,6 +18,7 @@ open Util
open Names
open Term
open Constr
+open Context
open Environ
open EConstr
open Vars
@@ -117,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
| Const _ | Ind _ | Construct _ | Var _ as c ->
Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
- Some (match lna.(i) with Name id -> id | _ -> assert false)
+ Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
| Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
in
hdrec c
@@ -136,6 +137,7 @@ let lowercase_first_char id = (* First character of a constr *)
s ^ Unicode.lowercase_first_char s'
let sort_hdchar = function
+ | SProp -> "P"
| Prop -> "P"
| Set -> "S"
| Type _ -> "T"
@@ -154,12 +156,12 @@ let hdchar env sigma c =
| Rel n ->
(if n<=k then "p" (* the initial term is flexible product/function *)
else
- try match lookup_rel (n-k) env with
- | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id
- | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
+ try match let d = lookup_rel (n-k) env in get_name d, get_type d with
+ | Name id, _ -> lowercase_first_char id
+ | Anonymous, t -> hdrec 0 (lift (n-k) t)
with Not_found -> "y")
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
- let id = match lna.(i) with Name id -> id | _ -> assert false in
+ let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
lowercase_first_char id
| Evar _ (* We could do better... *)
| Meta _ | Case (_, _, _, _) -> "y"
@@ -175,18 +177,20 @@ let named_hd env sigma a = function
| Anonymous -> Name (Id.of_string (hdchar env sigma a))
| x -> x
-let mkProd_name env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b)
-let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b)
+let mkProd_name env sigma (n,a,b) = mkProd (map_annot (named_hd env sigma a) n, a, b)
+let mkLambda_name env sigma (n,a,b) = mkLambda (map_annot (named_hd env sigma a) n, a, b)
let lambda_name = mkLambda_name
let prod_name = mkProd_name
-let prod_create env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b)
-let lambda_create env sigma (a,b) = mkLambda (named_hd env sigma a Anonymous, a, b)
+let prod_create env sigma (r,a,b) =
+ mkProd (make_annot (named_hd env sigma a Anonymous) r, a, b)
+let lambda_create env sigma (r,a,b) =
+ mkLambda (make_annot (named_hd env sigma a Anonymous) r, a, b)
let name_assumption env sigma = function
- | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t)
- | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t)
+ | LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env sigma t) na, t)
+ | LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env sigma c) na, c, t)
let name_context env sigma hyps =
snd
@@ -456,13 +460,13 @@ let rename_bound_vars_as_displayed sigma avoid env c =
| Prod (na,c1,c2) ->
let na',avoid' =
compute_displayed_name_in sigma
- (RenamingElsewhereFor (env,c2)) avoid na c2 in
- mkProd (na', c1, rename avoid' (na' :: env) c2)
+ (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
+ mkProd ({na with binder_name=na'}, c1, rename avoid' (na' :: env) c2)
| LetIn (na,c1,t,c2) ->
let na',avoid' =
compute_displayed_let_name_in sigma
- (RenamingElsewhereFor (env,c2)) avoid na c2 in
- mkLetIn (na',c1,t, rename avoid' (na' :: env) c2)
+ (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
+ mkLetIn ({na with binder_name=na'},c1,t, rename avoid' (na' :: env) c2)
| Cast (c,k,t) -> mkCast (rename avoid env c, k,t)
| _ -> c
in
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 3722cbed24..240fd8fa81 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -44,15 +44,15 @@ val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
val named_hd : env -> evar_map -> types -> Name.t -> Name.t
val head_name : evar_map -> types -> Id.t option
-val mkProd_name : env -> evar_map -> Name.t * types * types -> types
-val mkLambda_name : env -> evar_map -> Name.t * types * constr -> constr
+val mkProd_name : env -> evar_map -> Name.t Context.binder_annot * types * types -> types
+val mkLambda_name : env -> evar_map -> Name.t Context.binder_annot * types * constr -> constr
(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> evar_map -> Name.t * types * types -> types
-val lambda_name : env -> evar_map -> Name.t * types * constr -> constr
+val prod_name : env -> evar_map -> Name.t Context.binder_annot * types * types -> types
+val lambda_name : env -> evar_map -> Name.t Context.binder_annot * types * constr -> constr
-val prod_create : env -> evar_map -> types * types -> constr
-val lambda_create : env -> evar_map -> types * constr -> constr
+val prod_create : env -> evar_map -> Sorts.relevance * types * types -> constr
+val lambda_create : env -> evar_map -> Sorts.relevance * types * constr -> constr
val name_assumption : env -> evar_map -> rel_declaration -> rel_declaration
val name_context : env -> evar_map -> rel_context -> rel_context
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 15e201347c..2047772cfe 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -132,6 +132,7 @@ sig
val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
val get_id : t -> Id.t
val pick : t -> t -> t
+ val pick_annot : t Context.binder_annot -> t Context.binder_annot -> t Context.binder_annot
val cons : t -> Id.t list -> Id.t list
val to_option : Name.t -> Id.t option
@@ -176,6 +177,11 @@ struct
| Name _ -> na1
| Anonymous -> na2
+ let pick_annot na1 na2 =
+ let open Context in
+ match na1.binder_name with
+ | Name _ -> na1 | Anonymous -> na2
+
let cons na l =
match na with
| Anonymous -> l
diff --git a/engine/nameops.mli b/engine/nameops.mli
index a5308904f5..0e75fed045 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -84,6 +84,9 @@ module Name : sig
(** [pick na na'] returns [Anonymous] if both names are [Anonymous].
Pick one of [na] or [na'] otherwise. *)
+ val pick_annot : Name.t Context.binder_annot -> Name.t Context.binder_annot ->
+ Name.t Context.binder_annot
+
val cons : Name.t -> Id.t list -> Id.t list
(** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index a725444e81..2d693e0259 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -876,9 +876,9 @@ module Progress = struct
let eq_named_declaration d1 d2 =
match d1, d2 with
| LocalAssum (i1,t1), LocalAssum (i2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
+ Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
| LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
- Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
+ Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
&& eq_constr sigma1 sigma2 t1 t2
| _ ->
false
diff --git a/engine/termops.ml b/engine/termops.ml
index 2f766afaa6..8e12c9be88 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -15,6 +15,7 @@ open Names
open Nameops
open Term
open Constr
+open Context
open Vars
open Environ
@@ -115,8 +116,8 @@ let pr_decl env sigma (decl,ok) =
let open NamedDecl in
let print_constr = print_kconstr in
match decl with
- | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
- | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
+ | LocalAssum ({binder_name=id},_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
+ | LocalDef ({binder_name=id},c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
print_constr env sigma c ++ str (if ok then ")" else "}")
let pr_evar_source env sigma = function
@@ -248,8 +249,8 @@ let pr_evar_universe_context ctx =
let print_env_short env sigma =
let print_constr = print_kconstr in
let pr_rel_decl = function
- | RelDecl.LocalAssum (n,_) -> Name.print n
- | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
+ | RelDecl.LocalAssum (n,_) -> Name.print n.binder_name
+ | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n.binder_name ++ str " := "
++ print_constr env sigma (EConstr.of_constr b) ++ str ")"
in
let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
@@ -459,9 +460,10 @@ let push_named_rec_types (lna,typarray,_) env =
let ctxt =
Array.map2_i
(fun i na t ->
- match na with
- | Name id -> LocalAssum (id, lift i t)
- | Anonymous -> anomaly (Pp.str "Fix declarations must be named."))
+ let id = map_annot (function
+ | Name id -> id
+ | Anonymous -> anomaly (Pp.str "Fix declarations must be named.")) na
+ in LocalAssum (id, lift i t))
lna typarray in
Array.fold_left
(fun e assum -> push_named assum e) env ctxt
@@ -469,14 +471,11 @@ let push_named_rec_types (lna,typarray,_) env =
let lookup_rel_id id sign =
let open RelDecl in
let rec lookrec n = function
- | [] ->
- raise Not_found
- | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
- lookrec (n + 1) l
- | LocalAssum (Name id', t) :: l ->
- if Names.Id.equal id' id then (n,None,t) else lookrec (n + 1) l
- | LocalDef (Name id', b, t) :: l ->
- if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
+ | [] -> raise Not_found
+ | decl :: l ->
+ if Names.Name.equal (Name id) (get_name decl)
+ then (n, get_value decl, get_type decl)
+ else lookrec (n+1) l
in
lookrec 1 sign
@@ -1098,7 +1097,8 @@ let is_template_polymorphic_ind env sigma f =
let base_sort_cmp pb s0 s1 =
match (s0,s1) with
- | Prop, Prop | Set, Set | Type _, Type _ -> true
+ | SProp, SProp | Prop, Prop | Set, Set | Type _, Type _ -> true
+ | SProp, _ | _, SProp -> false
| Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
| Set, Prop | Type _, Prop | Type _, Set -> false
@@ -1352,7 +1352,7 @@ let compact_named_context sign =
let clear_named_body id env =
let open NamedDecl in
let aux _ = function
- | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
+ | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named (LocalAssum (id',t))
| d -> push_named d in
fold_named_context aux env ~init:(reset_context env)
diff --git a/engine/termops.mli b/engine/termops.mli
index dea59e9efc..1dd9941c5e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -23,9 +23,9 @@ val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
(** about contexts *)
-val push_rel_assum : Name.t * types -> env -> env
-val push_rels_assum : (Name.t * Constr.types) list -> env -> env
-val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env
+val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
+val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
+val push_named_rec_types : Name.t Context.binder_annot array * Constr.types array * 'a -> env -> env
val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
(** Associates the contents of an identifier in a [rel_context]. Raise
@@ -40,8 +40,8 @@ val rel_list : int -> int -> constr list
(** iterators/destructors on terms *)
val mkProd_or_LetIn : rel_declaration -> types -> types
val mkProd_wo_LetIn : rel_declaration -> types -> types
-val it_mkProd : types -> (Name.t * types) list -> types
-val it_mkLambda : constr -> (Name.t * types) list -> constr
+val it_mkProd : types -> (Name.t Context.binder_annot * types) list -> types
+val it_mkLambda : constr -> (Name.t Context.binder_annot * types) list -> constr
val it_mkProd_or_LetIn : types -> rel_context -> types
val it_mkProd_wo_LetIn : types -> rel_context -> types
val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
@@ -246,7 +246,7 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
(** other signature iterators *)
val process_rel_context : (rel_declaration -> env -> env) -> env -> env
-val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
+val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t Context.binder_annot * 't) list
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 77d1896683..6f4f40e2c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -37,18 +37,25 @@ type t =
uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
uctx_weak_constraints : UPairSet.t
}
-
+
+let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+
let empty =
{ uctx_names = UNameMap.empty, LMap.empty;
uctx_local = ContextSet.empty;
uctx_seff_univs = LSet.empty;
uctx_univ_variables = LMap.empty;
uctx_univ_algebraic = LSet.empty;
- uctx_universes = UGraph.initial_universes;
- uctx_initial_universes = UGraph.initial_universes;
+ uctx_universes = initial_sprop_cumulative;
+ uctx_initial_universes = initial_sprop_cumulative;
uctx_weak_constraints = UPairSet.empty; }
+let elaboration_sprop_cumul =
+ Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+ ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
+
let make u =
+ let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
{ empty with
uctx_universes = u; uctx_initial_universes = u}
@@ -710,7 +717,7 @@ let universe_of_name uctx s =
UNameMap.find s (fst uctx.uctx_names)
let update_sigma_env uctx env =
- let univs = Environ.universes env in
+ let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
let eunivs =
{ uctx with uctx_initial_universes = univs;
uctx_universes = univs }
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 40c4c909fe..c310331b15 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -28,7 +28,7 @@ let fresh_level () =
(* TODO: remove *)
let new_univ () = Univ.Universe.make (fresh_level ())
let new_Type () = mkType (new_univ ())
-let new_Type_sort () = Type (new_univ ())
+let new_Type_sort () = sort_of_univ (new_univ ())
let fresh_instance auctx =
let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
@@ -128,11 +128,12 @@ let type_of_reference env r =
let type_of_global t = type_of_reference (Global.env ()) t
let fresh_sort_in_family = function
+ | InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
| InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
- Type (Univ.Universe.make u), ContextSet.singleton u
+ sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
let new_sort_in_family sf =
fst (fresh_sort_in_family sf)
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1619ac3d34..46ff6340b4 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -268,6 +268,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
module UPairs = OrderedType.UnorderedPair(Univ.Level)
module UPairSet = Set.Make (UPairs)
+(* TODO check is_small/sprop *)
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
(* Keep the Prop/Set <= i constraints separate for minimization *)
@@ -275,7 +276,7 @@ let normalize_context_set g ctx us algs weak =
Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
in
let smallles = if get_set_minimization ()
- then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+ then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
else Constraint.empty
in
let csts, partition =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 10:24:26 +0000