aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml25
-rw-r--r--interp/constrarg.mli10
-rw-r--r--interp/constrexpr_ops.ml2
-rw-r--r--interp/constrextern.ml52
-rw-r--r--interp/constrintern.ml23
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/topconstr.ml6
7 files changed, 53 insertions, 67 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a7241399e0..44623f9c9a 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -22,7 +22,8 @@ let loc_of_or_by_notation f = function
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"
@@ -36,29 +37,28 @@ let wit_var = unsafe_of_type VarArgType
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_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,16 @@ 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_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";
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 fdeddd66a1..0cc111e617 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 2d48ea4d07..161fd1eb1d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -178,7 +178,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
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ba20f9fa06..5c9e80df3d 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 =
@@ -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/constrintern.ml b/interp/constrintern.ml
index 8afe630ec5..f9de8c4663 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -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) =
@@ -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/coqlib.ml b/interp/coqlib.ml
index 5ac718e3b0..b309f26cd6 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/topconstr.ml b/interp/topconstr.ml
index 1231f11555..15ac46e29e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -51,7 +51,7 @@ let ids_of_cases_indtype =
let ids_of_cases_tomatch tms =
List.fold_right
- (fun (_,(ona,indnal)) l ->
+ (fun (_,ona,indnal) l ->
Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
indnal (Option.fold_right (Loc.down_located name_cons) ona l))
tms []
@@ -120,7 +120,7 @@ let fold_constr_expr_with_binders g f n acc = function
| CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (List.fold_right 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
@@ -224,7 +224,7 @@ let map_constr_expr_with_binders g f e = function
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
let ids = ids_of_cases_tomatch a in
let po = Option.map (f (List.fold_right 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-03-09 11:51:59 +0000