g_ltac.mlg

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

DECLARE PLUGIN "coq-core.plugins.ltac"

{

open Util
open Pp
open Constrexpr
open Tacexpr
open Genarg
open Genredexpr
open Names
open Attributes

open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pvernac.Vernac_
open Pltac

let fail_default_value = Locus.ArgArg 0

let arg_of_expr = function
    { CAst.v=(TacArg v) } -> v
  | e -> Tacexp (e:raw_tactic_expr)

let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_simple_intropattern) pat
let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac

let reference_to_id qid =
  if Libnames.qualid_is_ident qid then
    CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid
  else
    CErrors.user_err ?loc:qid.CAst.loc
      (str "This expression should be a simple identifier.")

let tactic_mode = Entry.make "tactic_command"

let tacdef_body = Entry.make "tacdef_body"

(* Registers [tactic_mode] as a parser for proof editing *)
let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode

(* Tactics grammar rules *)

let hint = G_proofs.hint

let for_extraargs = ()

let goal_selector = G_vernac.goal_selector
let toplevel_selector = G_vernac.toplevel_selector
let subprf = G_vernac.subprf
let subprf_with_selector = G_vernac.subprf_with_selector

}

GRAMMAR EXTEND Gram
  GLOBAL: tactic tacdef_body ltac_expr tactic_value command hint
          tactic_mode constr_may_eval constr_eval
          term subprf subprf_with_selector;

  tactic_then_last:
    [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
        { Array.map (function None -> CAst.make ~loc (TacId []) | Some t -> t) (Array.of_list lta) }
      | -> { [||] }
    ] ]
  ;
  for_each_goal:
    [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) }
      | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
      | ".."; l = tactic_then_last -> { ([], Some (CAst.make ~loc (TacId []), l)) }
      | ta = ltac_expr -> { ([ta], None) }
      | "|"; tg = for_each_goal -> { let (first,last) = tg in (CAst.make ~loc (TacId []) :: first, last) }
      | -> { ([CAst.make ~loc (TacId [])], None) }
    ] ]
  ;
  tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
                           for [TacExtend] *)
  [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
  ;
  ltac_expr:
    [ "5" RIGHTA
      [ ]
    | "4" LEFTA
      [ ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { CAst.make ~loc (TacThen (ta0,ta1)) }
      | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> {
          let (first,tail) = tg in
          match l , tail with
          | false , Some (t,last) -> CAst.make ~loc (TacThen (ta0,
              CAst.make ~loc (TacExtendTac (Array.of_list first, t, last))))
          | true  , Some (t,last) -> CAst.make ~loc (TacThens3parts (ta0, Array.of_list first, t, last))
          | false , None -> CAst.make ~loc (TacThen (ta0, CAst.make ~loc (TacDispatch first)))
          | true  , None -> CAst.make ~loc (TacThens (ta0,first)) } ]
    | "3" RIGHTA
      [ IDENT "try"; ta = ltac_expr -> { CAst.make ~loc (TacTry ta) }
      | IDENT "do"; n = nat_or_var; ta = ltac_expr -> { CAst.make ~loc (TacDo (n,ta)) }
      | IDENT "timeout"; n = nat_or_var; ta = ltac_expr -> { CAst.make ~loc (TacTimeout (n,ta)) }
      | IDENT "time"; s = OPT string; ta = ltac_expr -> { CAst.make ~loc (TacTime (s,ta)) }
      | IDENT "repeat"; ta = ltac_expr -> { CAst.make ~loc (TacRepeat ta) }
      | IDENT "progress"; ta = ltac_expr -> { CAst.make ~loc (TacProgress ta) }
      | IDENT "once"; ta = ltac_expr -> { CAst.make ~loc (TacOnce  ta) }
      | IDENT "exactly_once"; ta = ltac_expr -> { CAst.make ~loc (TacExactlyOnce ta) }
(*To do: put Abstract in Refiner*)
      | IDENT "abstract"; tc = NEXT -> { CAst.make ~loc (TacAbstract (tc,None)) }
      | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
        { CAst.make ~loc (TacAbstract (tc,Some s)) }
      | IDENT "only"; sel = goal_selector; ":"; ta = ltac_expr -> { CAst.make ~loc (TacSelect (sel, ta)) } ]
(*End of To do*)
    | "2" RIGHTA
      [ ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { CAst.make ~loc (TacOr (ta0,ta1)) }
      | IDENT "tryif" ; ta = ltac_expr ;
              "then" ; tat = ltac_expr ;
              "else" ; tae = ltac_expr -> { CAst.make ~loc (TacIfThenCatch (ta,tat,tae)) }
      | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { CAst.make ~loc (TacOrelse (ta0,ta1)) } ]
    | "1" RIGHTA
      [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
          { CAst.make ~loc (TacFun (it,body)) }
      | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
          llc = LIST1 let_clause SEP "with"; "in";
          body = ltac_expr LEVEL "5" -> { CAst.make ~loc (TacLetIn (isrec,llc,body)) }
      | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
          { CAst.make ~loc (TacMatchGoal (b,false,mrl)) }
      | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
        mrl = match_context_list; "end" ->
          { CAst.make ~loc (TacMatchGoal (b,true,mrl)) }
      |	b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" ->
          { CAst.make ~loc (TacMatch (b,c,mrl)) }
      | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
          { CAst.make ~loc (TacFirst l) }
      | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
          { CAst.make ~loc (TacSolve l) }
      | IDENT "idtac"; l = LIST0 message_token -> { CAst.make ~loc (TacId l) }
      | g=failkw; n = [ n = nat_or_var -> { n } | -> { fail_default_value } ];
          l = LIST0 message_token -> { CAst.make ~loc (TacFail (g,n,l)) }
      | st = simple_tactic -> { st }
      | a = tactic_value -> { CAst.make ~loc (TacArg a) }
      | r = reference; la = LIST0 tactic_arg ->
        { CAst.make ~loc @@ TacArg (TacCall (CAst.make ~loc (r,la))) } ]
    | "0"
      [ "("; a = ltac_expr; ")" -> { a }
      | "["; ">"; tg = for_each_goal; "]" -> {
          let (tf,tail) = tg in
          begin match tail with
          | Some (t,tl) -> CAst.make ~loc (TacExtendTac (Array.of_list tf,t,tl))
          | None -> CAst.make ~loc (TacDispatch tf)
          end }
      | a = tactic_atom -> { CAst.make ~loc (TacArg a) } ] ]
  ;
  failkw:
  [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
  ;
  (* Tactic arguments to the right of an application *)
  tactic_arg:
    [ [ a = tactic_value -> { a }
      | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
      (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
      | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
  ;
  (* Can be used as argument and at toplevel in tactic expressions. *)
  tactic_value:
    [ [ c = constr_eval -> { ConstrMayEval c }
      | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l }
      | IDENT "type_term"; c=uconstr -> { TacPretype c }
      | IDENT "numgoals" -> { TacNumgoals } ] ]
  ;
  (* If a qualid is given, use its short name. TODO: have the shortest
     non ambiguous name where dots are replaced by "_"? Probably too
     verbose most of the time. *)
  fresh_id:
    [ [ s = STRING -> { Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) }
        | qid = qualid -> { Locus.ArgVar (CAst.make ~loc @@ Libnames.qualid_basename qid) } ] ]
  ;
  constr_eval:
    [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
          { ConstrEval (rtc,c) }
      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
          { ConstrContext (id,c) }
      | IDENT "type"; IDENT "of"; c = Constr.constr ->
          { ConstrTypeOf c } ] ]
  ;
  constr_may_eval: (* For extensions *)
    [ [ c = constr_eval -> { c }
      | c = Constr.constr -> { ConstrTerm c } ] ]
  ;
  tactic_atom:
    [ [ n = integer -> { TacGeneric (None, genarg_of_int n) }
      | r = reference -> { TacCall (CAst.make ~loc (r,[])) }
      | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
  ;
  match_key:
    [ [ "match" -> { Once }
      | IDENT "lazymatch" -> { Select }
      | IDENT "multimatch" -> { General } ] ]
  ;
  input_fun:
    [ [ "_" -> { Name.Anonymous }
      | l = ident -> { Name.Name l } ] ]
  ;
  let_clause:
    [ [ idr = identref; ":="; te = ltac_expr ->
         { (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
      | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr ->
         { (na, arg_of_expr te) }
      | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr ->
         { (CAst.map (fun id -> Name id) idr, arg_of_expr (CAst.make ~loc (TacFun (args,te)))) } ] ]
  ;
  match_pattern:
    [ [ IDENT "context";  oid = OPT Constr.ident;
          "["; pc = Constr.cpattern; "]" ->
        { Subterm (oid, pc) }
      | pc = Constr.cpattern -> { Term pc } ] ]
  ;
  match_hyp:
    [ [ na = name; ":"; mp =  match_pattern -> { Hyp (na, mp) }
      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
      | na = name; ":="; mpv = match_pattern ->
        { let t, ty =
            match mpv with
            | Term t -> (match t with
              | { CAst.v = CCast (t, Some DEFAULTcast, ty) } -> Term t, Some (Term ty)
              | _ -> mpv, None)
            | _ -> mpv, None
          in Def (na, t, Option.default (Term (CAst.make @@ CHole (None))) ty) }
    ] ]
  ;
  match_context_rule:
    [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
        "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
      | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
        "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
      | "_"; "=>"; te = ltac_expr -> { All te } ] ]
  ;
  match_context_list:
    [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
      | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
  ;
  match_rule:
    [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) }
      | "_"; "=>"; te = ltac_expr -> { All te } ] ]
  ;
  match_list:
    [ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
      | "|"; mrl = LIST1 match_rule SEP "|" -> { mrl } ] ]
  ;
  message_token:
    [ [ id = identref -> { MsgIdent id }
      | s = STRING -> { MsgString s }
      | n = natural -> { MsgInt n } ] ]
  ;

  ltac_def_kind:
    [ [ ":=" -> { false }
      | "::=" -> { true } ] ]
  ;

  (* Definitions for tactics *)
  tacdef_body:
    [ [ name = Constr.global; it=LIST1 input_fun;
        redef = ltac_def_kind; body = ltac_expr ->
        { if redef then Tacexpr.TacticRedefinition (name, CAst.make ~loc (TacFun (it, body)))
          else
            let id = reference_to_id name in
            Tacexpr.TacticDefinition (id, CAst.make ~loc (TacFun (it, body))) }
      | name = Constr.global; redef = ltac_def_kind;
        body = ltac_expr ->
        { if redef then Tacexpr.TacticRedefinition (name, body)
          else
            let id = reference_to_id name in
            Tacexpr.TacticDefinition (id, body) }
    ] ]
  ;
  tactic:
    [ [ tac = ltac_expr -> { tac } ] ]
  ;
  tactic_mode:
    [ [ p = subprf -> { Vernacexpr.VernacSynPure p }
      | g = OPT toplevel_selector; p = subprf_with_selector -> { Vernacexpr.VernacSynPure (p g) }
      ] ]
  ;
  command: TOP
    [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
        l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
          { Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some (in_tac ta), l)) }
      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
        "with"; ta = Pltac.tactic ->
          { Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some (in_tac ta),Some l)) } ] ]
  ;
  hint: TOP
    [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
        tac = Pltac.tactic ->
        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
  ;
  term: LEVEL "0"
    [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->
        { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
          CAst.make ~loc @@ CGenarg arg } ] ]
  ;
  END

{

open Stdarg
open Tacarg
open Vernacextend
open Libnames

let pr_ltac_selector s = Pp.(Goal_select.pr_goal_selector s ++ str ":")

}

VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector }
| [ toplevel_selector(s) ] -> { s }
END

{

let pr_ltac_info n = str "Info" ++ spc () ++ int n

}

VERNAC ARGUMENT EXTEND ltac_info PRINTED BY { pr_ltac_info }
| [ "Info" natural(n) ] -> { n }
END

{

let pr_ltac_use_default b =
  if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()

}

VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default }
| [ "." ] -> { false }
| [ "..." ] -> { true }
END

{

let rm_abstract tac =
  let (loc, tac2) = CAst.(tac.loc, tac.v) in
  match tac2 with
  | TacAbstract (t,_) -> t, true
  | TacSolve [ {CAst.loc; v=TacAbstract(t,_)} ] -> CAst.make ?loc (TacSolve [t]), true
  | _ -> tac, false

let is_explicit_terminator = function
  | {CAst.v=(TacSolve _)} -> true
  | _ -> false

}

VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
    { classify_as_proofstep } -> {
    let g = Option.default (Goal_select.get_default_goal_selector ()) g in
    let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
    let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in
    ComTactic.solve g ~info t ~with_end_tac
  }
END

VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
    {
      let solving_tac = is_explicit_terminator t in
      let pbr = if solving_tac then Some "par" else None in
      VtProofStep{ proof_block_detection = pbr }
    } -> {
      let t, abstract = rm_abstract t in
      let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in
      ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
    }
END

{

let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")"

}

VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY { pr_ltac_tactic_level }
| [ "(" "at" "level" natural(n) ")" ] -> { n }
END

VERNAC ARGUMENT EXTEND ltac_production_sep
| [ "," string(sep) ] -> { sep }
END

{

let pr_ltac_production_item = function
| Tacentries.TacTerm s -> quote (str s)
| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg
| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false
| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) ->
  let sep = match sep with
  | None -> mt ()
  | Some sep -> str "," ++ spc () ++ quote (str sep)
  in
  str arg ++ str "(" ++ Id.print id ++ sep ++ str ")"

let check_non_empty_string ?loc s =
  if String.is_empty s then CErrors.user_err ?loc (str "Invalid empty string.")

}

VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item }
| [ string(s) ] -> { check_non_empty_string ~loc s; Tacentries.TacTerm s }
| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
  { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) }
| [ ident(nt) ] ->
  { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) }
END

VERNAC COMMAND EXTEND VernacTacticNotation
| #[ deprecation; locality; ]
  [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
  { VtSideff ([], VtNow) } SYNTERP AS tacobj {
    let n = Option.default 0 n in
    let local = Locality.make_module_locality locality in
    Tacentries.add_tactic_notation_syntax local n ?deprecation r
  } ->
  {
    Tacentries.add_tactic_notation ?deprecation tacobj e
  }
END

VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
  { Feedback.msg_notice (Tacentries.print_ltac r) }
END

VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
| [ "Locate" "Ltac" reference(r) ] ->
  { Tacentries.print_located_tactic r }
END

{

let pr_ltac_ref = Libnames.pr_qualid

let pr_tacdef_body env sigma tacdef_body =
  let id, redef, body =
    match tacdef_body with
    | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body
    | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
  in
  let idl, body =
    match body with
      | {CAst.v=(Tacexpr.TacFun (idl,b))} -> idl,b
      | _ -> [], body in
  id ++
    prlist (function Name.Anonymous -> str " _"
      | Name.Name id -> spc () ++ Id.print id) idl
  ++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
  ++ Pptactic.pr_raw_tactic env sigma body

}

VERNAC ARGUMENT EXTEND ltac_tacdef_body
PRINTED BY { pr_tacdef_body env sigma }
| [ tacdef_body(t) ] -> { t }
END

VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
    VtSideff (List.map (function
      | TacticDefinition ({CAst.v=r},_) -> r
      | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater)
  } -> {
         Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
  }
END

VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY
| [ "Print" "Ltac" "Signatures" ] -> { Tacentries.print_ltacs () }
END