aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml40
-rw-r--r--interp/constrarg.mli10
-rw-r--r--interp/constrexpr_ops.ml7
-rw-r--r--interp/constrextern.ml54
-rw-r--r--interp/constrextern.mli3
-rw-r--r--interp/constrintern.ml29
-rw-r--r--interp/constrintern.mli5
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/genintern.ml14
-rw-r--r--interp/topconstr.ml10
10 files changed, 78 insertions, 96 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index d9c60a18bf..b093d92e73 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -19,10 +19,8 @@ let loc_of_or_by_notation f = function
| AN c -> f c
| ByNotation (loc,s,_) -> loc
-let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
- Obj.magic t
-
-let wit_int_or_var = unsafe_of_type IntOrVarArgType
+let wit_int_or_var =
+ Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var"
let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
Genarg.make0 None "intropattern"
@@ -30,35 +28,37 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
Genarg.make0 None "tactic"
-let wit_ident = unsafe_of_type IdentArgType
+let wit_ident =
+ Genarg.make0 None "ident"
-let wit_var = unsafe_of_type VarArgType
+let wit_var =
+ Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var"
let wit_ref = Genarg.make0 None "ref"
-let wit_quant_hyp = unsafe_of_type QuantHypArgType
-
-let wit_genarg = unsafe_of_type GenArgType
+let wit_quant_hyp = Genarg.make0 None "quant_hyp"
let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
Genarg.make0 None "sort"
-let wit_constr = unsafe_of_type ConstrArgType
+let wit_constr =
+ Genarg.make0 None "constr"
-let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+let wit_constr_may_eval =
+ Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
let wit_uconstr = Genarg.make0 None "uconstr"
-let wit_open_constr = unsafe_of_type OpenConstrArgType
+let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr"
-let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
+let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings"
-let wit_bindings = unsafe_of_type BindingsArgType
+let wit_bindings = Genarg.make0 None "bindings"
let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
Genarg.make0 None "hyp_location_flag"
-let wit_red_expr = unsafe_of_type RedExprArgType
+let wit_red_expr = Genarg.make0 None "redexpr"
let wit_clause_dft_concl =
Genarg.make0 None "clause_dft_concl"
@@ -66,9 +66,19 @@ let wit_clause_dft_concl =
(** Register location *)
let () =
+ register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
register_name0 wit_ref "Constrarg.wit_ref";
+ register_name0 wit_ident "Constrarg.wit_ident";
+ register_name0 wit_var "Constrarg.wit_var";
register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";
+ register_name0 wit_constr "Constrarg.wit_constr";
register_name0 wit_uconstr "Constrarg.wit_uconstr";
+ register_name0 wit_open_constr "Constrarg.wit_open_constr";
+ register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
+ register_name0 wit_red_expr "Constrarg.wit_red_expr";
register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
+ register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
+ register_name0 wit_bindings "Constrarg.wit_bindings";
+ register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index ebef1ada5b..e1a5f4d7c9 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
(** {5 Additional generic arguments} *)
-val wit_int_or_var : int or_var uniform_genarg_type
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
@@ -38,8 +38,6 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type
-
val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
@@ -52,17 +50,17 @@ val wit_constr_may_eval :
val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
val wit_open_constr :
- (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
+ (constr_expr, glob_constr_and_expr, constr) genarg_type
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
- constr with_bindings Evd.sigma) genarg_type
+ constr with_bindings delayed_open) genarg_type
val wit_bindings :
(constr_expr bindings,
glob_constr_and_expr bindings,
- constr bindings Evd.sigma) genarg_type
+ constr bindings delayed_open) genarg_type
val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 1644700268..9c577034e8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
Option.equal Int.equal proj1 proj2 &&
constr_expr_eq e1 e2 &&
List.equal args_eq al1 al2
- | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+ | CRecord (_, l1), CRecord (_, l2) ->
let field_eq (r1, e1) (r2, e2) =
eq_reference r1 r2 && constr_expr_eq e1 e2
in
- Option.equal constr_expr_eq e1 e2 &&
List.equal field_eq l1 l2
| CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
(** Don't care about the case_style *)
@@ -178,7 +177,7 @@ and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
constr_expr_eq a1 a2
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
constr_expr_eq e1 e2 &&
Option.equal (eq_located Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
@@ -238,7 +237,7 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
- | CRecord (loc,_,_) -> loc
+ | CRecord (loc,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9df8f9c233..70a35c6132 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp =
exception Expl
-let params_implicit n impl =
- let rec aux n impl =
- if n == 0 then true
- else match impl with
- | [] -> false
- | imp :: impl when is_status_implicit imp -> aux (pred n) impl
- | _ -> false
- in aux n impl
-
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
let explicitize loc inctx impl (cf,f) args =
@@ -689,7 +680,7 @@ let rec extern inctx scopes vars r =
| head :: tail -> ip q locs' tail
((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
in
- CRecord (loc, None, List.rev (ip projs locals args []))
+ CRecord (loc, List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
extern_app loc inctx
@@ -721,26 +712,29 @@ let rec extern inctx scopes vars r =
(cases_predicate_names tml) vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
- let na' = match na,tm with
- | Anonymous, GVar (_, id) ->
- begin match rtntypopt with
- | None -> None
- | Some ntn ->
- if occur_glob_constr id ntn then
- Some (Loc.ghost, Anonymous)
- else None
- end
- | Anonymous, _ -> None
- | Name id, GVar (_,id') when Id.equal id id' -> None
- | Name _, _ -> Some (Loc.ghost,na) in
- (sub_extern false scopes vars tm,
- (na',Option.map (fun (loc,ind,nal) ->
- let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
- let fullargs =
- if !Flags.in_debugger then args else
- Notation_ops.add_patterns_for_params ind args in
- extern_ind_pattern_in_scope scopes vars ind fullargs
- ) x))) tml in
+ let na' = match na,tm with
+ | Anonymous, GVar (_, id) ->
+ begin match rtntypopt with
+ | None -> None
+ | Some ntn ->
+ if occur_glob_constr id ntn then
+ Some (Loc.ghost, Anonymous)
+ else None
+ end
+ | Anonymous, _ -> None
+ | Name id, GVar (_,id') when Id.equal id id' -> None
+ | Name _, _ -> Some (Loc.ghost,na) in
+ (sub_extern false scopes vars tm,
+ na',
+ Option.map (fun (loc,ind,nal) ->
+ let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+ let fullargs =
+ if !Flags.in_debugger then args else
+ Notation_ops.add_patterns_for_params ind args in
+ extern_ind_pattern_in_scope scopes vars ind fullargs
+ ) x))
+ tml
+ in
let eqns = List.map (extern_eqn inctx scopes vars) eqns in
CCases (loc,sty,rtntypopt',tml,eqns)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index bf1f529c67..f617faa38a 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Termops
open Environ
open Libnames
@@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
- rel_context -> local_binder list
+ Context.Rel.t -> local_binder list
(** Printing options *)
val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a7b1bb4128..964ed05140 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -101,7 +101,7 @@ let global_reference id =
let construct_reference ctx id =
try
- Term.mkVar (let _ = Context.lookup_named id ctx in id)
+ Term.mkVar (let _ = Context.Named.lookup id ctx in id)
with Not_found ->
global_reference id
@@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
str "variable " ++ pr_id id ++ str " should be bound to a term.")
else
(* Is [id] a goal or section variable *)
- let _ = Context.lookup_named id namedctx in
+ let _ = Context.Named.lookup id namedctx in
try
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
@@ -698,19 +698,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
(* [id] a goal variable *)
GVar (loc,id), [], [], []
-let proj_impls r impls =
- let env = Global.env () in
- let f (x, l) = x, projection_implicits env r l in
- List.map f impls
-
-let proj_scopes n scopes =
- List.skipn_at_least n scopes
-
-let proj_impls_scopes p impls scopes =
- match p with
- | Some (r, n) -> proj_impls r impls, proj_scopes n scopes
- | None -> impls, scopes
-
let find_appl_head_data c =
match c with
| GRef (loc,ref,_) as x ->
@@ -1386,7 +1373,7 @@ let internalize globalenv env allow_patvar lvar c =
let (env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in
+ let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, (env',rbl) =
@@ -1492,7 +1479,7 @@ let internalize globalenv env allow_patvar lvar c =
apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
- | CRecord (loc, _, fs) ->
+ | CRecord (loc, fs) ->
let cargs =
sort_fields true loc fs
(fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l)
@@ -1506,7 +1493,7 @@ let internalize globalenv env allow_patvar lvar c =
intern env app
end
| CCases (loc, sty, rtnpo, tms, eqns) ->
- let as_in_vars = List.fold_left (fun acc (_,(na,inb)) ->
+ let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x)
(Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na)
inb) Id.Set.empty tms in
@@ -1542,7 +1529,7 @@ let internalize globalenv env allow_patvar lvar c =
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
(* "in" is None so no match to add *)
- let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in
+ let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(Loc.ghost,na') in
@@ -1551,7 +1538,7 @@ let internalize globalenv env allow_patvar lvar c =
intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
- let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *)
+ let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(Loc.ghost,na') in
@@ -1628,7 +1615,7 @@ let internalize globalenv env allow_patvar lvar c =
let rhs' = intern {env with ids = env_ids} rhs in
(loc,eqn_ids,pl,rhs')) pll
- and intern_case_item env forbidden_names_for_gen (tm,(na,t)) =
+ and intern_case_item env forbidden_names_for_gen (tm,na,t) =
(*the "match" part *)
let tm' = intern env tm in
(* the "as" part *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 22cf910b22..73ecc437dd 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Evd
open Environ
open Libnames
@@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
env -> evar_map ref -> local_binder list ->
- internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ internalization_env * ((env * Context.Rel.t) * 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) -> *)
@@ -178,7 +177,7 @@ val interp_context_evars :
val locate_reference : Libnames.qualid -> Globnames.global_reference
val is_global : Id.t -> bool
-val construct_reference : named_context -> Id.t -> constr
+val construct_reference : Context.Named.t -> Id.t -> constr
val global_reference : Id.t -> constr
val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 9e5173815e..23bcddaea2 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -87,7 +87,7 @@ let check_required_library d =
*)
(* or failing ...*)
errorlabstrm "Coqlib.check_required_library"
- (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 47b7173587..d6bfd347ff 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -37,20 +37,16 @@ module Subst = Register (SubstObj)
let intern = Intern.obj
let register_intern0 = Intern.register0
-let generic_intern ist v =
- let unpacker wit v =
- let (ist, v) = intern wit ist (raw v) in
- (ist, in_gen (glbwit wit) v)
- in
- unpack { unpacker; } v
+let generic_intern ist (GenArg (Rawwit wit, v)) =
+ let (ist, v) = intern wit ist v in
+ (ist, in_gen (glbwit wit) v)
(** Substitution functions *)
let substitute = Subst.obj
let register_subst0 = Subst.register0
-let generic_substitute subs v =
- let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in
- unpack { unpacker; } v
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+ in_gen (glbwit wit) (substitute wit subs v)
let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc8e697ea4..8293f7f88d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -71,7 +71,7 @@ let ids_of_cases_indtype p =
let ids_of_cases_tomatch tms =
List.fold_right
- (fun (_,(ona,indnal)) l ->
+ (fun (_, ona, indnal) l ->
Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
indnal
(Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
@@ -111,11 +111,11 @@ let fold_constr_expr_with_binders g f n acc = function
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
acc
- | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+ | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
| CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
- let acc = List.fold_left (f n) acc (List.map fst al) in
+ let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
List.fold_right (fun (loc,patl,rhs) acc ->
let ids = ids_of_pattern_list patl in
f (Id.Set.fold g ids n) acc rhs) bl acc
@@ -213,14 +213,14 @@ let map_constr_expr_with_binders g f e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CRef _ as x -> x
- | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
+ | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
| CCases (loc,sty,rtnpo,a,bl) ->
let bl = List.map (fun (loc,patl,rhs) ->
let ids = ids_of_pattern_list patl in
(loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
let ids = ids_of_cases_tomatch a in
let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
- CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+ CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:39:04 +0000