aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml9
-rw-r--r--engine/eConstr.mli27
-rw-r--r--engine/evarutil.ml7
-rw-r--r--engine/namegen.ml33
-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.ml31
-rw-r--r--engine/termops.mli12
10 files changed, 79 insertions, 65 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 521d6b707d..981f9454e4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -73,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
@@ -668,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 6a144be6b3..25ceffbd04 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -109,9 +109,9 @@ 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
@@ -124,7 +124,8 @@ 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
@@ -139,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
@@ -179,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
@@ -197,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
@@ -213,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 5c2b480db4..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
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 46fdf08e10..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
@@ -155,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"
@@ -176,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
@@ -457,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 9c4b64b60d..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
@@ -1353,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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:30:09 +0000