aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml7
-rw-r--r--plugins/extraction/mlutil.ml8
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacinterp.ml14
-rw-r--r--plugins/micromega/zify.ml91
-rw-r--r--plugins/ssrmatching/ssrmatching.ml20
8 files changed, 93 insertions, 64 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0cad192332..ca4f5429a2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -22,7 +22,6 @@ open Reductionops
open Inductive
open Termops
open Inductiveops
-open Recordops
open Namegen
open Miniml
open Table
@@ -531,7 +530,7 @@ and extract_really_ind env kn mib =
let n = nb_default_params env sg (EConstr.of_constr ty) in
let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
in
- List.iter (Option.iter check_proj) (lookup_projections ip)
+ List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip)
with Not_found -> ()
end;
Record field_glob
@@ -1129,7 +1128,7 @@ let extract_constant env kn cb =
(match cb.const_body with
| Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
- (match Recordops.find_primitive_projection kn with
+ (match Structures.PrimitiveProjections.find_opt kn with
| None -> mk_typ (get_body c)
| Some p ->
let body = fake_match_projection env p in
@@ -1142,7 +1141,7 @@ let extract_constant env kn cb =
(match cb.const_body with
| Primitive _ | Undef _ -> warn_info (); mk_ax ()
| Def c ->
- (match Recordops.find_primitive_projection kn with
+ (match Structures.PrimitiveProjections.find_opt kn with
| None -> mk_def (get_body c)
| Some p ->
let body = fake_match_projection env p in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index da4a50b674..cfdaac710b 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -217,13 +217,13 @@ module Mlenv = struct
(* Adding a type with no [Tvar], hence no generalization needed. *)
- let push_type {env=e;free=f} t =
- { env = (0,t) :: e; free = find_free f t}
+ let push_type mle t =
+ { env = (0,t) :: mle.env; free = find_free mle.free t}
(* Adding a type with no [Tvar] nor [Tmeta]. *)
- let push_std_type {env=e;free=f} t =
- { env = (0,t) :: e; free = f}
+ let push_std_type mle t =
+ { env = (0,t) :: mle.env; free = mle.free}
end
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c7bda43465..1640bff43b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -373,11 +373,6 @@ end) = struct
end
-(* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
-(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)
-
-
let type_app_poly env env evd f args =
let evars, c = app_poly_nocheck env evd f args in
let evd', t = Typing.type_of env (goalevars evars) c in
@@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r =
let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
-(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *)
-(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
-
(** Setoid rewriting when called with "rewrite" *)
let general_s_rewrite cl l2r occs (c,l) ~new_goals =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 5e88bf7c79..f2f5fc16a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -91,6 +91,13 @@ let to_int v =
Some (out_gen (topwit wit_int) v)
else None
+let of_ident id = in_gen (topwit wit_ident) id
+
+let to_ident v =
+ if has_type v (topwit wit_ident) then
+ Some (out_gen (topwit wit_ident) v)
+ else None
+
let to_list v = prj Val.typ_list v
let to_option v = prj Val.typ_opt v
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 8ca2510459..c748fb3d1a 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -39,6 +39,8 @@ sig
val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
val of_int : int -> t
val to_int : t -> int option
+ val of_ident : Id.t -> t
+ val to_ident : t -> Id.t option
val to_list : t -> t list option
val to_option : t -> t option option
val to_pair : t -> (t * t) option
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2241e78d2..da95869abb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
| TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
- | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
+ | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
let alias = Tacenv.interp_alias s in
@@ -2148,7 +2148,8 @@ let interp_redexp env sigma r =
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
let _ =
- let eval lfun poly env sigma ty tac =
+ let eval ?loc ~poly env sigma tycon tac =
+ let lfun = GlobEnv.lfun env in
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
let tac = eval_tactic_ist ist tac in
@@ -2156,8 +2157,13 @@ let _ =
poly seems like enough to get reasonable behavior in practice
*)
let name = Id.of_string "ltac_gen" in
- let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
- (EConstr.of_constr c, sigma)
+ let sigma, ty = match tycon with
+ | Some ty -> sigma, ty
+ | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+ in
+ let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in
+ let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in
+ (j, sigma)
in
GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 61966b60c0..800dc6cee2 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -66,14 +66,36 @@ let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
let get_type_of env evd e =
Tacred.cbv_beta env evd (Retyping.get_type_of env evd e)
+(* arguments are dealt with in a second step *)
+
let rec find_option pred l =
match l with
| [] -> raise Not_found
| e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )
-(** [HConstr] is a map indexed by EConstr.t.
- It should only be used using closed terms.
- *)
+module ConstrMap = struct
+ open Names.GlobRef
+
+ type 'a t = 'a list Map.t
+
+ let add gr e m =
+ Map.update gr (function None -> Some [e] | Some l -> Some (e :: l)) m
+
+ let empty = Map.empty
+
+ let find evd h m =
+ match Map.find (fst (EConstr.destRef evd h)) m with
+ | e :: _ -> e
+ | [] -> assert false
+
+ let find_all evd h m = Map.find (fst (EConstr.destRef evd h)) m
+
+ let fold f m acc =
+ Map.fold
+ (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l)
+ m acc
+end
+
module HConstr = struct
module M = Map.Make (struct
type t = EConstr.t
@@ -81,20 +103,11 @@ module HConstr = struct
let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c')
end)
- type 'a t = 'a list M.t
-
- let lfind h m = try M.find h m with Not_found -> []
-
- let add h e m =
- let l = lfind h m in
- M.add h (e :: l) m
+ type 'a t = 'a M.t
+ let add h e m = M.add h e m
let empty = M.empty
- let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found
- let find_all = lfind
-
- let fold f m acc =
- M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc
+ let find = M.find
end
(** [get_projections_from_constant (evd,c) ]
@@ -331,7 +344,7 @@ module type Elt = sig
(** name *)
val name : string
- val table : (term_kind * decl_kind) HConstr.t ref
+ val table : (term_kind * decl_kind) ConstrMap.t ref
val cast : elt decl -> decl_kind
val dest : decl_kind -> elt decl option
@@ -346,12 +359,12 @@ module type Elt = sig
(* val arity : int*)
end
-let table = Summary.ref ~name:"zify_table" HConstr.empty
-let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty
-let specs = Summary.ref ~name:"zify_specs" HConstr.empty
-let table_cache = ref HConstr.empty
-let saturate_cache = ref HConstr.empty
-let specs_cache = ref HConstr.empty
+let table = Summary.ref ~name:"zify_table" ConstrMap.empty
+let saturate = Summary.ref ~name:"zify_saturate" ConstrMap.empty
+let specs = Summary.ref ~name:"zify_specs" ConstrMap.empty
+let table_cache = ref ConstrMap.empty
+let saturate_cache = ref ConstrMap.empty
+let specs_cache = ref ConstrMap.empty
(** Each type-class gives rise to a different table.
They only differ on how projections are extracted. *)
@@ -589,8 +602,11 @@ module MakeTable (E : Elt) = struct
let register_hint evd t elt =
match EConstr.kind evd t with
| App (c, _) ->
- E.table := HConstr.add c (Application t, E.cast elt) !E.table
- | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table
+ let gr = fst (EConstr.destRef evd c) in
+ E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+ | _ ->
+ let gr = fst (EConstr.destRef evd t) in
+ E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
let register_constr env evd c =
let c = EConstr.of_constr c in
@@ -637,7 +653,7 @@ module MakeTable (E : Elt) = struct
let pp_keys () =
let env = Global.env () in
let evd = Evd.from_env env in
- HConstr.fold
+ ConstrMap.fold
(fun _ (k, d) acc ->
match E.dest d with
| None -> acc
@@ -947,9 +963,11 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
type typed_constr = {constr : EConstr.t; typ : EConstr.t; inj : EInjT.t}
let get_injection env evd t =
- match snd (HConstr.find t !table_cache) with
- | InjTyp i -> i
- | _ -> raise Not_found
+ try
+ match snd (ConstrMap.find evd t !table_cache) with
+ | InjTyp i -> i
+ | _ -> raise Not_found
+ with DestKO -> raise Not_found
(* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *)
let arrow =
@@ -1087,7 +1105,7 @@ let declared_term env evd hd args =
| PropUnOp _ -> decomp t 1
| _ -> None )
in
- find_option match_operator (HConstr.find_all hd !table)
+ find_option match_operator (ConstrMap.find_all evd hd !table)
let rec trans_expr env evd e =
let inj = e.inj in
@@ -1099,7 +1117,7 @@ let rec trans_expr env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1243,7 +1261,7 @@ let rec trans_prop env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1262,7 +1280,7 @@ let rec trans_prop env evd e =
in
trans_binrel evd e rop a.(n - 2) a1 a.(n - 1) a2
| _ -> IProof
- with Not_found -> IProof )
+ with Not_found | DestKO -> IProof )
let trans_check_prop env evd t =
if is_prop env evd t then Some (trans_prop env evd t) else None
@@ -1359,7 +1377,7 @@ let do_let tac (h : Constr.named_declaration) =
find_option
(match_operator env evd eq
[|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
- (HConstr.find_all eq !table_cache));
+ (ConstrMap.find_all evd eq !table_cache));
tac x (EConstr.of_constr t) (EConstr.of_constr ty)
with Not_found -> Tacticals.New.tclIDTAC)
@@ -1453,12 +1471,12 @@ let rec spec_of_term env evd (senv : spec_env) t =
try (EConstr.mkVar (HConstr.find t' senv'.map), senv')
with Not_found -> (
try
- match snd (HConstr.find c !specs_cache) with
+ match snd (ConstrMap.find evd c !specs_cache) with
| UnOpSpec s | BinOpSpec s ->
let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in
register_constr senv' t' thm
| _ -> (get_name t' senv', senv')
- with Not_found -> (t', senv') )
+ with Not_found | DestKO -> (t', senv') )
let interp_pscript s =
match s with
@@ -1533,7 +1551,8 @@ let get_all_sat env evd c =
List.fold_left
(fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc)
[]
- (HConstr.find_all c !saturate_cache)
+ ( try ConstrMap.find_all evd c !saturate_cache
+ with DestKO | Not_found -> [] )
let saturate =
Proofview.Goal.enter (fun gl ->
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7774258fca..805be1fc87 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -22,7 +22,6 @@ open Vars
open Libnames
open Tactics
open Termops
-open Recordops
open Tacmach
open Glob_term
open Util
@@ -333,7 +332,8 @@ type tpattern = {
let all_ok _ _ = true
let proj_nparams c =
- try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0
+ try 1 + Structures.Structure.projection_nparams c
+ with Not_found -> 0
let isRigid c = match kind c with
| Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
@@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u =
| _ -> KpatRigid in
sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t}
-let nb_cs_proj_args pc f u =
+let nb_cs_proj_args ise pc f u =
+ let open Structures in
+ let open ValuePattern in
let na k =
- List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
+ let open CanonicalSolution in
+ let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in
+ List.length cvalue_arguments in
let nargs_of_proj t = match kind t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
@@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u =
| Prod _ -> na Prod_cs
| Sort s -> na (Sort_cs (Sorts.family s))
| Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f
- | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
+ | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f))
| _ -> -1
with Not_found -> -1
@@ -467,7 +471,7 @@ let splay_app ise =
| Cast _ | Evar _ -> loop c [| |]
| _ -> c, [| |]
-let filter_upat i0 f n u fpats =
+let filter_upat ise i0 f n u fpats =
let na = Array.length u.up_a in
if n < na then fpats else
let np = match u.up_k with
@@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats =
| KpatRigid when isRigid f -> na
| KpatFlex -> na
| KpatProj pc ->
- let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np
+ let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np
| _ -> -1 in
if np < na then fpats else
let () = if !i0 < np then i0 := n in (u, np) :: fpats
@@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
let f, a = splay_app ise c in let i0 = ref (-1) in
- let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
+ let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in
while !i0 >= 0 do
let i = !i0 in i0 := -1;
let one_match (u, np) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:45:43 +0000