From de8cee391af67aafc966c7cde8c3f0c4fff53da3 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 10:08:38 +0000 Subject: Adapt pieces of code needing -rectypes * in Matching and Tacinterp : ad-hoc types for encoding matching result and "next" continuation * in Class_tactics, occurrences of types such as "type t = (foo * (unit->t) option" have been specialized to something like type t = TNone | TSome of foo * (unit -> t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/matching.ml | 12 ++++++---- pretyping/matching.mli | 14 +++++++----- tactics/class_tactics.ml4 | 38 +++++++++++++++++++++----------- tactics/tacinterp.ml | 56 +++++++++++++++++++++++++++++------------------ 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 -- cgit v1.2.3