aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/matching.ml12
-rw-r--r--pretyping/matching.mli14
-rw-r--r--tactics/class_tactics.ml438
-rw-r--r--tactics/tacinterp.ml56
4 files changed, 76 insertions, 44 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 217398a6d..4beaf5282 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -252,13 +252,20 @@ let matches c p = snd (matches_core_closed None true c p)
let special_meta = (-1)
+type 'a matching_result =
+ { m_sub : bound_ident_map * patvar_map;
+ m_ctx : 'a;
+ m_nxt : unit -> 'a matching_result }
+
+let mkresult s c n = { m_sub=s; m_ctx=c; m_nxt=n }
+
(* Tells if it is an authorized occurrence and if the instance is closed *)
let authorized_occ partial_app closed pat c mk_ctx next =
try
let sigma = matches_core_closed None partial_app pat c in
if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
then next ()
- else sigma, mk_ctx (mkMeta special_meta), next
+ else mkresult sigma (mk_ctx (mkMeta special_meta)) next
with
PatternMatchingFailure -> next ()
@@ -330,9 +337,6 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
try_sub_match_rec [] lc in
aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
-type subterm_matching_result =
- (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
-
let match_subterm pat c = sub_match pat c
let match_appsubterm pat c = sub_match ~partial_app:true pat c
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 9b412692c..273c4d061 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -50,27 +50,29 @@ val is_matching : constr_pattern -> constr -> bool
val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
(** The type of subterm matching results: a substitution + a context
- (whose hole is denoted with [special_meta]) + a continuation that
+ (whose hole is denoted here with [special_meta]) + a continuation that
either returns the next matching subterm or raise PatternMatchingFailure *)
-type subterm_matching_result =
- (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+type 'a matching_result =
+ { m_sub : bound_ident_map * patvar_map;
+ m_ctx : 'a;
+ m_nxt : unit -> 'a matching_result }
(** [match_subterm n pat c] returns the substitution and the context
corresponding to the first **closed** subterm of [c] matching [pat], and
a continuation that looks for the next matching subterm.
It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_subterm : constr_pattern -> constr -> subterm_matching_result
+val match_subterm : constr_pattern -> constr -> constr matching_result
(** [match_appsubterm pat c] returns the substitution and the context
corresponding to the first **closed** subterm of [c] matching [pat],
considering application contexts as well. It also returns a
continuation that looks for the next matching subterm.
It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
+val match_appsubterm : constr_pattern -> constr -> constr matching_result
(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
val match_subterm_gen : bool (** true = with app context *) ->
- constr_pattern -> constr -> subterm_matching_result
+ constr_pattern -> constr -> constr matching_result
(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
against [pat] taking partial subterms into consideration *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d411a28c4..1fc013496 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -217,6 +217,16 @@ type auto_result = autogoal list sigma
type atac = auto_result tac
+(* Some utility types to avoid the need of -rectypes *)
+
+type 'a optionk =
+ | Nonek
+ | Somek of 'a * 'a optionk fk
+
+type ('a,'b) optionk2 =
+ | Nonek2
+ | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+
let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
let cty = Evarutil.nf_evar sigma cty in
let rec iscl env ty =
@@ -408,21 +418,23 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
(Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
else true
in
- let fk'' =
+ let fk'' =
if not needs_backtrack then
- (if !typeclasses_debug then msg_debug (str"no backtrack on " ++ pr_ev s gl ++
- str " after " ++ Lazy.force info.auto_last_tac); fk)
- else fk'
+ (if !typeclasses_debug then
+ msg_debug (str"no backtrack on " ++ pr_ev s gl ++
+ str " after " ++ Lazy.force info.auto_last_tac);
+ fk)
+ else fk'
in aux s' (gls'::acc) fk'' gls)
fk {it = (gl,info); sigma = s})
- | [] -> Some (List.rev acc, s, fk)
+ | [] -> Somek2 (List.rev acc, s, fk)
in fun {it = gls; sigma = s} fk ->
let rec aux' = function
- | None -> fk ()
- | Some (res, s', fk') ->
+ | Nonek2 -> fk ()
+ | Somek2 (res, s', fk') ->
let goals' = List.concat res in
sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ()))
- in aux' (aux s [] (fun () -> None) gls)
+ in aux' (aux s [] (fun () -> Nonek2) gls)
let then_tac (first : atac) (second : atac) : atac =
{ skft = fun sk fk -> first.skft (then_list second sk) fk }
@@ -430,12 +442,12 @@ let then_tac (first : atac) (second : atac) : atac =
let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
t.skft (fun x _ -> Some x) (fun _ -> None) gl
-type run_list_res = (auto_result * run_list_res fk) option
+type run_list_res = auto_result optionk
let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
- (then_list t (fun x fk -> Some (x, fk)))
+ (then_list t (fun x fk -> Somek (x, fk)))
gl
- (fun _ -> None)
+ (fun _ -> Nonek)
let fail_tac : atac =
{ skft = fun sk fk _ -> fk () }
@@ -465,8 +477,8 @@ let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs ev
let get_result r =
match r with
- | None -> None
- | Some (gls, fk) -> Some (gls.sigma,fk)
+ | Nonek -> None
+ | Somek (gls, fk) -> Some (gls.sigma,fk)
let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
match evars_to_goals p evm with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2ed054ea1..215dee837 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1672,6 +1672,11 @@ let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
+type 'a extended_matching_result =
+ { e_ctx : 'a;
+ e_sub : bound_ident_map * extended_patvar_map;
+ e_nxt : unit -> 'a extended_matching_result }
+
(* Tries to match one hypothesis pattern with a list of hypotheses *)
let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
let get_id_couple id = function
@@ -1683,27 +1688,34 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
let lmeta = extended_matches t hyp in
(try
let lmeta = verify_metas_coherence gl lmatch lmeta in
- ([],lmeta,(fun () -> raise PatternMatchingFailure))
+ { e_ctx = [];
+ e_sub = lmeta;
+ e_nxt = fun () -> raise PatternMatchingFailure }
with
- | Not_coherent_metas -> raise PatternMatchingFailure);
+ | Not_coherent_metas -> raise PatternMatchingFailure)
| Subterm (b,ic,t) ->
let rec match_next_pattern find_next () =
- let (lmeta,ctxt,find_next') = find_next () in
+ let s = find_next () in
try
- let lmeta = verify_metas_coherence gl lmatch (adjust lmeta) in
- (give_context ctxt ic,lmeta,match_next_pattern find_next')
+ let lmeta = verify_metas_coherence gl lmatch (adjust s.m_sub) in
+ { e_ctx = give_context s.m_ctx ic;
+ e_sub = lmeta;
+ e_nxt = match_next_pattern s.m_nxt }
with
- | Not_coherent_metas -> match_next_pattern find_next' () in
- match_next_pattern (fun () -> match_subterm_gen b t hyp) () in
+ | Not_coherent_metas -> match_next_pattern s.m_nxt ()
+ in
+ match_next_pattern (fun () -> match_subterm_gen b t hyp) ()
+ in
let rec apply_one_mhyp_context_rec = function
| (id,b,hyp as hd)::tl ->
(match patv with
| None ->
let rec match_next_pattern find_next () =
try
- let (ids, lmeta, find_next') = find_next () in
- (get_id_couple id hypname@ids, lmeta, hd,
- match_next_pattern find_next')
+ let s = find_next () in
+ { e_ctx = (get_id_couple id hypname @ s.e_ctx), hd;
+ e_sub = s.e_sub;
+ e_nxt = match_next_pattern s.e_nxt }
with
| PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
match_next_pattern (fun () ->
@@ -1714,19 +1726,20 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
| Some body ->
let rec match_next_pattern_in_body next_in_body () =
try
- let (ids,lmeta,next_in_body') = next_in_body() in
+ let s1 = next_in_body() in
let rec match_next_pattern_in_typ next_in_typ () =
try
- let (ids',lmeta',next_in_typ') = next_in_typ() in
- (get_id_couple id hypname@ids@ids', lmeta', hd,
- match_next_pattern_in_typ next_in_typ')
+ let s2 = next_in_typ() in
+ { e_ctx = (get_id_couple id hypname@s1.e_ctx@s2.e_ctx), hd;
+ e_sub = s2.e_sub;
+ e_nxt = match_next_pattern_in_typ s2.e_nxt }
with
| PatternMatchingFailure ->
- match_next_pattern_in_body next_in_body' () in
+ match_next_pattern_in_body s1.e_nxt () in
match_next_pattern_in_typ
(fun () ->
let hyp = refresh_universes_strict hyp in
- match_pat lmeta hyp pat) ()
+ match_pat s1.e_sub hyp pat) ()
with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
in
match_next_pattern_in_body
@@ -1993,7 +2006,7 @@ and interp_match_goal ist goal lz lr lmr =
let env = pf_env goal in
let apply_goal_sub app ist (id,c) csr mt mhyps hyps =
let rec match_next_pattern find_next () =
- let (lgoal,ctxt,find_next') = find_next () in
+ let { m_sub=lgoal; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
let lctxt = give_context ctxt id in
try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps
with e when is_match_catchable e -> match_next_pattern find_next' () in
@@ -2049,14 +2062,15 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
| Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
in
let rec match_next_pattern find_next =
- let (lids,lm,hyp_match,find_next') = find_next () in
+ let s = find_next () in
+ let lids,hyp_match = s.e_ctx in
db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
try
let id_match = pi1 hyp_match in
let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
- apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
+ apply_hyps_context_rec (lfun@lids) s.e_sub nextlhyps tl
with e when is_match_catchable e ->
- match_next_pattern find_next' in
+ match_next_pattern s.e_nxt in
let init_match_pattern () =
apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
match_next_pattern init_match_pattern
@@ -2186,7 +2200,7 @@ and interp_genarg_var_list1 ist gl x =
and interp_match ist g lz constr lmr =
let apply_match_subterm app ist (id,c) csr mt =
let rec match_next_pattern find_next () =
- let (lmatch,ctxt,find_next') = find_next () in
+ let { m_sub=lmatch; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
let lctxt = give_context ctxt id in
let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in
try eval_with_fail {ist with lfun=lfun} lz g mt
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 06:49:16 +0000