diff options
Diffstat (limited to 'rewrite.ml4')
-rw-r--r-- | rewrite.ml4 | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/rewrite.ml4 b/rewrite.ml4 index 6229262..383d706 100644 --- a/rewrite.ml4 +++ b/rewrite.ml4 @@ -32,6 +32,10 @@ let push_anomaly msg = function | Util.Anomaly _ as e -> raise e | _ -> Coq.anomaly msg + + + + module M = Matcher open Term @@ -435,6 +439,41 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ) goal +(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against + the pattern, and introduces an hypothesis H of type p = t. (Note + that we have performed the substitution in p). +*) + +let aac_match ~eq pattern term h = fun gl -> + let env = Tacmach.pf_env gl in + let evar_map = Tacmach.project gl in + let carrier = Typing.type_of env evar_map term in + let rel = Coq.Relation.make carrier eq in + let equiv,gl = Coq.Equivalence.from_relation gl rel in + (* first, we decompose the pattern as an arity. *) + let x_args, pat = Term.decompose_lam pattern in + (* then, we reify the pattern and the term, using the provided equality *) + let envs = Theory.Trans.empty_envs () in + let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in + let gl,ir = Theory.Trans.ir_of_envs gl rel envs in + let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in + (* then, we pick the first solution to the matching problem *) + let sigma = match Search_monad.choose solutions with + | None -> Coq.user_error "no solution to the matching problem" + | Some sigma -> sigma + in + let p_sigma = Matcher.Subst.instantiate sigma left in + let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in + (* Then, we have to assert the fact that p_sigma is equal to term *) + let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in + let evar_map = Tacmach.project gl in + Tacticals.tclTHENLIST + [ + Refiner.tclEVARS evar_map; + Tactics.assert_by h equation (by_aac_reflexivity term equiv ir p_sigma right); + ] gl + + open Coq.Rewrite open Tacmach open Tacticals @@ -522,3 +561,11 @@ TACTIC EXTEND _aacu_instances_ | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] -> [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ] END + +TACTIC EXTEND _aac_match_ +| [ "aac_match" constr(p) constr(t) ident(h)] -> + [ fun gl -> + let ty = Tacmach.pf_type_of gl t in + let eq = Coq.Leibniz.eq ty in + aac_match ~eq p t (Names.Name h) gl] +END |