1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)

open Printer
open Pretyping
open Globnames
open Glob_term
open Tacmach

open Ssrmatching_plugin
open Ssrmatching

open Ssrast
open Ssrprinters
open Ssrcommon

let char_to_kind = function
  | '(' -> xInParens
  | '@' -> xWithAt
  | ' ' -> xNoFlag
  | 'x' -> xCpattern
  | _ -> assert false

(** Backward chaining tactics: apply, exact, congr. *)

(** The "apply" tactic *)

let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
(* ppdebug(lazy(str"sigma@interp_agen=" ++ pr_evar_map None (project gl))); *)
  let k = char_to_kind k in
  let rc = pf_intern_term ist gl c in
  let rcs' = rc :: rcs in
  match goclr with
  | None -> clr, rcs'
  | Some ghyps ->
    let clr' = snd (interp_hyps ist gl ghyps) @ clr in
    if k <> xNoFlag then clr', rcs' else
    let loc = rc.CAst.loc in
    match DAst.get rc with
    | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
    | GRef (VarRef id, _) when not_section_id id ->
        SsrHyp (Loc.tag ?loc id) :: clr', rcs'
    | _ -> clr', rcs'

let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)

let interp_agens ist gl gagens =
  match List.fold_right (interp_agen ist gl) gagens ([], []) with
  | clr, rlemma :: args ->
    let n = interp_nbargs ist gl rlemma - List.length args in
    let rec loop i =
      if i > n then
         errorstrm Pp.(str "Cannot apply lemma " ++ pf_pr_glob_constr gl rlemma)
      else
        try interp_refine ist gl (mkRApp rlemma (mkRHoles i @ args))
        with _ -> loop (i + 1) in
    clr, loop 0
  | _ -> assert false

let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)

let apply_rconstr ?ist t gl =
(* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
  let n = match ist, DAst.get t with
    | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
    | Some ist, _ -> interp_nbargs ist gl t
    | _ -> anomaly "apply_rconstr without ist and not RVar" in
  let mkRlemma i = mkRApp t (mkRHoles i) in
  let cl = pf_concl gl in
  let rec loop i =
    if i > n then
      errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t)
    else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in
  refine_with (loop 0) gl

let mkRAppView ist gl rv gv =
  let nb_view_imps = interp_view_nbimps ist gl rv in
  mkRApp rv (mkRHoles (abs nb_view_imps))

let prof_apply_interp_with = mk_profiler "ssrapplytac.interp_with";;

let refine_interp_apply_view i ist gl gv =
  let pair i = List.map (fun x -> i, x) in
  let rv = pf_intern_term ist gl gv in
  let v = mkRAppView ist gl rv gv in
  let interp_with (i, hint) =
    interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
  let interp_with x = prof_apply_interp_with.profile interp_with x in
  let rec loop = function
  | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
  | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
  loop (pair i Ssrview.viewtab.(i) @
        if i = 2 then pair 1 Ssrview.viewtab.(1) else [])

let apply_top_tac gl =
  Tacticals.tclTHENLIST [introid top_id; apply_rconstr (mkRVar top_id); Proofview.V82.of_tactic (Tactics.clear [top_id])] gl

let inner_ssrapplytac gviews ggenl gclr ist gl =
 let _, clr = interp_hyps ist gl gclr in
 let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
 let ggenl, tclGENTAC =
   if gviews <> [] && ggenl <> [] then
     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g) (List.hd ggenl) in
     [], Tacticals.tclTHEN (genstac (ggenl,[]) ist)
   else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
 tclGENTAC (fun gl ->
  match gviews, ggenl with
  | v :: tl, [] ->
    let dbl = if List.length tl = 1 then 2 else 1 in
    Tacticals.tclTHEN
      (List.fold_left (fun acc v -> Tacticals.tclTHENLAST acc (vtac v dbl)) (vtac v 1) tl)
      (cleartac clr) gl
  | [], [agens] ->
    let clr', (sigma, lemma) = interp_agens ist gl agens in
    let gl = pf_merge_uc_of sigma gl in
    Tacticals.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr'] gl
  | _, _ -> Tacticals.tclTHEN apply_top_tac (cleartac clr) gl) gl