aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml88
-rw-r--r--interp/constrexpr_ops.mli12
-rw-r--r--interp/constrextern.ml8
-rw-r--r--interp/constrintern.ml7
-rw-r--r--interp/constrintern.mli24
-rw-r--r--interp/notation.ml4
-rw-r--r--interp/notation_ops.ml1
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/stdarg.mli1
9 files changed, 62 insertions, 85 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 53c97f6b6b..a592b4cff8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -303,83 +303,51 @@ let add_name_in_env env n =
let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
-let expand_pattern_binders mkC bl c =
- let rec loop bl c =
+let expand_binders mkC loc bl c =
+ let rec loop loc bl c =
match bl with
- | [] -> ([], [], c)
+ | [] -> ([], c)
| b :: bl ->
- let (env, bl, c) = loop bl c in
match b with
- | CLocalDef (n, _, _) ->
+ | CLocalDef ((loc1,_) as n, oty, b) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let env = add_name_in_env env n in
- (env, b :: bl, c)
- | CLocalAssum (nl, _, _) ->
+ (env, CLetIn (loc,n,oty,b,c))
+ | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let env = List.fold_left add_name_in_env env nl in
- (env, b :: bl, c)
- | CLocalPattern (loc, p, ty) ->
+ (env, mkC loc (nl,bk,t) c)
+ | CLocalAssum ([],_,_) -> loop loc bl c
+ | CLocalPattern (loc1, p, ty) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let ni = Hook.get fresh_var env c in
- let id = (loc, Name ni) in
- let b =
- CLocalAssum
- ([id], Default Explicit,
- match ty with
+ let id = (loc1, Name ni) in
+ let ty = match ty with
| Some ty -> ty
- | None -> CHole (loc, None, IntroAnonymous, None))
+ | None -> CHole (loc1, None, IntroAnonymous, None)
in
- let e = CRef (Libnames.Ident (loc, ni), None) in
+ let e = CRef (Libnames.Ident (loc1, ni), None) in
let c =
CCases
(loc, LetPatternStyle, None, [(e,None,None)],
- [(loc, [(loc,[p])], mkC loc bl c)])
+ [(loc1, [(loc1,[p])], c)])
in
- (ni :: env, [b], c)
+ (ni :: env, mkC loc ([id],Default Explicit,ty) c)
in
- let (_, bl, c) = loop bl c in
- (bl, c)
+ let (_, c) = loop loc bl c in
+ c
let mkCProdN loc bll c =
- let rec loop loc bll c =
- match bll with
- | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
- | CLocalDef ((loc1,_) as id,b,t) :: bll ->
- CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
- | [] -> c
- | CLocalAssum ([],_,_) :: bll -> loop loc bll c
- | CLocalPattern (loc,p,ty) :: bll -> assert false
- in
- let (bll, c) = expand_pattern_binders loop bll c in
- loop loc bll c
+ let mk loc b c = CProdN (loc,[b],c) in
+ expand_binders mk loc bll c
let mkCLambdaN loc bll c =
- let rec loop loc bll c =
- match bll with
- | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
- | CLocalDef ((loc1,_) as id,b,t) :: bll ->
- CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
- | [] -> c
- | CLocalAssum ([],_,_) :: bll -> loop loc bll c
- | CLocalPattern (loc,p,ty) :: bll -> assert false
- in
- let (bll, c) = expand_pattern_binders loop bll c in
- loop loc bll c
-
-let rec abstract_constr_expr c = function
- | [] -> c
- | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl)
- | CLocalAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
- (abstract_constr_expr c bl)
- | CLocalPattern _::_ -> assert false
-
-let rec prod_constr_expr c = function
- | [] -> c
- | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl)
- | CLocalAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
- (prod_constr_expr c bl)
- | CLocalPattern _::_ -> assert false
+ let mk loc b c = CLambdaN (loc,[b],c) in
+ expand_binders mk loc bll c
+
+(* Deprecated *)
+let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
+let prod_constr_expr c bl = mkCProdN (local_binders_loc bl) bl c
let coerce_reference_to_id = function
| Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 45e3a19bc8..f6d97e107d 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -49,19 +49,19 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-
val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [abstract_constr_expr], with location *)
val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [prod_constr_expr], with location *)
+(** @deprecated variant of mkCLambdaN *)
+val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+
+(** @deprecated variant of mkCProdN *)
+val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+
val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
-val expand_pattern_binders :
- (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) ->
- local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr
(** {6 Destructors}*)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5bf49b7334..59b8b4e5b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -975,6 +975,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* Not "goal_concl_style" means do alpha-conversion avoiding only *)
(* those goal/section/rel variables that occurs in the subterm under *)
(* consideration; see namegen.ml for further details *)
+ let t = EConstr.of_constr t in
let avoid = if goal_concl_style then ids_of_context env else [] in
let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
@@ -987,6 +988,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
extern_constr_gen lax goal_concl_style None env sigma t
let extern_type goal_concl_style env sigma t =
+ let t = EConstr.of_constr t in
let avoid = if goal_concl_style then ids_of_context env else [] in
let r = Detyping.detype goal_concl_style avoid env sigma t in
extern_glob_type (vars_of_env env) r
@@ -1065,14 +1067,16 @@ let rec glob_of_pat env sigma = function
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
in
GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
- | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *)
- | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c)
+ | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
+ | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
| PSort s -> GSort (loc,s)
let extern_constr_pattern env sigma pat =
extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
let extern_rel_context where env sigma sign =
+ let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
+ let where = Option.map EConstr.of_constr where in
let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8fe6ce85e8..d75487ecf3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1831,7 +1831,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(add_name match_acc (loc,x)) ((loc,x)::var_acc)
| (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
let fresh =
- Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in
+ Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
canonize_args t tt (fresh::forbidden_names)
((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
| _ -> assert false in
@@ -1925,7 +1925,7 @@ let extract_ids env =
let scope_of_type_kind = function
| IsType -> Notation.current_type_scope_name ()
- | OfType typ -> compute_type_scope typ
+ | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ)
| WithoutTypeConstraint -> None
let empty_ltac_sign = {
@@ -2004,7 +2004,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen env evdref ~impls (OfType typ) c
+ interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c
let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
interp_constr_evars_gen env evdref IsType ~impls c
@@ -2064,6 +2064,7 @@ let intern_context global_level env impl_env binders =
user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
let interp_rawcontext_evars env evdref k bl =
+ let open EConstr in
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index e45de25887..758d4e650b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -99,7 +99,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env ->
constr_expr -> constr Evd.in_evar_universe_context
val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
- constr_expr -> types -> constr Evd.in_evar_universe_context
+ constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context
val interp_type : env -> evar_map -> ?impls:internalization_env ->
constr_expr -> types Evd.in_evar_universe_context
@@ -107,32 +107,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env ->
(** Main interpretation function expecting all postponed problems to
be resolved, but possibly leaving evars. *)
-val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr
(** Accepting unresolved evars *)
val interp_constr_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> constr
+ ?impls:internalization_env -> constr_expr -> EConstr.constr
val interp_casted_constr_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> types -> constr
+ ?impls:internalization_env -> constr_expr -> types -> EConstr.constr
val interp_type_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> types
+ ?impls:internalization_env -> constr_expr -> EConstr.types
(** Accepting unresolved evars and giving back the manual implicit arguments *)
val interp_constr_evars_impls : env -> evar_map ref ->
?impls:internalization_env -> constr_expr ->
- constr * Impargs.manual_implicits
+ EConstr.constr * Impargs.manual_implicits
val interp_casted_constr_evars_impls : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> types ->
- constr * Impargs.manual_implicits
+ ?impls:internalization_env -> constr_expr -> EConstr.types ->
+ EConstr.constr * Impargs.manual_implicits
val interp_type_evars_impls : env -> evar_map ref ->
?impls:internalization_env -> constr_expr ->
- types * Impargs.manual_implicits
+ EConstr.types * Impargs.manual_implicits
(** Interprets constr patterns *)
@@ -151,14 +151,14 @@ val interp_reference : ltac_sign -> reference -> glob_constr
val interp_binder : env -> evar_map -> Name.t -> constr_expr ->
types Evd.in_evar_universe_context
-val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
+val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types
(** Interpret contexts: returns extended env and context *)
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
env -> evar_map ref -> local_binder_expr list ->
- internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
+ internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -175,7 +175,7 @@ val interp_context_evars :
val locate_reference : Libnames.qualid -> Globnames.global_reference
val is_global : Id.t -> bool
-val construct_reference : Context.Named.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
val global_reference : Id.t -> constr
val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
diff --git a/interp/notation.ml b/interp/notation.ml
index 66d3c91859..90ac7f7296 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -585,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int =
cl_typ_ord
let compute_scope_class t =
- let (cl,_,_) = find_class_type Evd.empty t in
+ let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in
cl
module ScopeClassOrd =
@@ -615,7 +615,7 @@ let find_scope_class_opt = function
(* Special scopes associated to arguments of a global reference *)
let rec compute_arguments_classes t =
- match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
+ match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
| Prod (_,t,u) ->
let cl = try Some (compute_scope_class t) with Not_found -> None in
cl :: compute_arguments_classes u
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 59625426f0..8b4fadb5a0 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -442,6 +442,7 @@ let notation_constr_of_glob_constr nenv a =
(* Substitution of kernel names, avoiding a list of bound identifiers *)
let notation_constr_of_constr avoiding t =
+ let t = EConstr.of_constr t in
let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
let nenv = {
ninterp_var_type = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a4d4f40277..1565ba4a92 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -107,7 +107,9 @@ let constr_key c =
let revert_reserved_type t =
try
+ let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
+ let t = EConstr.of_constr t in
let t = Detyping.detype false [] (Global.env()) Evd.empty t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index af3a734627..113fe40ba7 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -11,6 +11,7 @@
open Loc
open Names
open Term
+open EConstr
open Libnames
open Globnames
open Genredexpr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:08:10 +0000