(************************************************************************)
(*         *   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)         *)
(************************************************************************)

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

{

open Names
module CoqConstr = Constr
open CoqConstr
open Constrexpr
open Constrexpr_ops
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pvernac.Vernac_
open Ltac_plugin
open Glob_term
open Stdarg
open Pp
open Ppconstr
open Printer
open Util
open Ssrprinters
open Ssrcommon

}

DECLARE PLUGIN "coq-core.plugins.ssreflect"

{

(* Defining grammar rules with "xx" in it automatically declares keywords too,
 * we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;

(* global syntactic changes and vernacular commands *)

(** Alternative notations for "match" and anonymous arguments. *)(* ************)

(* Syntax:                                                        *)
(*  if <term> is <pattern> then ... else ...                      *)
(*  if <term> is <pattern> [in ..] return ... then ... else ...   *)
(*  let: <pattern> := <term> in ...                               *)
(*  let: <pattern> [in ...] := <term> return ... in ...           *)
(* The scope of a top-level 'as' in the pattern extends over the  *)
(* 'return' type (dependent if/let).                              *)
(* Note that the optional "in ..." appears next to the <pattern>  *)
(* rather than the <term> in then "let:" syntax. The alternative  *)
(* would lead to ambiguities in, e.g.,                            *)
(* let: p1 := (*v---INNER LET:---v *)                             *)
(*   let: p2 := let: p3 := e3 in k return t in k2 in k1 return t' *)
(* in b       (*^--ALTERNATIVE INNER LET--------^ *)              *)

(* Caveat : There is no pretty-printing support, since this would *)
(* require a modification to the Coq kernel (adding a new match   *)
(* display style -- why aren't these strings?); also, the v8.1    *)
(* pretty-printer only allows extension hooks for printing        *)
(* integer or string literals.                                    *)
(*   Also note that in the v8 grammar "is" needs to be a keyword; *)
(* as this can't be done from an ML extension file, the new       *)
(* syntax will only work when ssreflect.v is imported.            *)

let no_ct = None, None and no_rt = None
let aliasvar = function
  | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na
  | _ -> None
let mk_cnotype mp = aliasvar mp, None
let mk_ctype mp t = aliasvar mp, Some t
let mk_rtype t = Some t
let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt
let mk_let ?loc rt ct mp c1 =
  CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)])
let mk_pat c (na, t) = (c, na, t)

}

GRAMMAR EXTEND Gram
  GLOBAL: binder_constr;
  ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]];
  ssr_mpat: [[ p = pattern -> { [[p]] } ]];
  ssr_dpat: [
    [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt }
    | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt }
    | mp = ssr_mpat -> { mp, no_ct, no_rt }
  ] ];
  ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]];
  ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]];
  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]];
  binder_constr: TOP [
    [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
      { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
    | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
      { let b1, ct, rt = db1 in
      let b1, b2 = let open CAst in
        let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
      in
      CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) }
    | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
      { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 }
    | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr;
      rt = ssr_rtype; "in"; c1 = lconstr ->
      { mk_let ~loc rt [mk_pat c (mk_cnotype mp)] mp c1 }
    | "let"; ":"; mp = ssr_mpat; "in"; t = pattern; ":="; c = lconstr;
      rt = ssr_rtype; "in"; c1 = lconstr ->
      { mk_let ~loc rt [mk_pat c (mk_ctype mp t)] mp c1 }
  ] ];
END

GRAMMAR EXTEND Gram
  GLOBAL: closed_binder;
  closed_binder: TOP [
    [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
      { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] }
  ] ];
END

(** Vernacular commands: Prenex Implicits *)

(* This should really be implemented as an extension to the implicit   *)
(* arguments feature, but unfortuately that API is sealed. The current *)
(* workaround uses a combination of notations that works reasonably,   *)
(* with the following caveats:                                         *)
(*  - The pretty-printing always elides prenex implicits, even when    *)
(*    they are obviously needed.                                       *)
(*  - Prenex Implicits are NEVER exported from a module, because this  *)
(*    would lead to faulty pretty-printing and scoping errors.         *)
(*  - The command "Import Prenex Implicits" can be used to reassert    *)
(*    Prenex Implicits for all the visible constants that had been     *)
(*    declared as Prenex Implicits.                                    *)

{

let declare_one_prenex_implicit locality f =
  let fref =
    try Smartlocate.global_with_alias f
    with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
  let rec loop = function
  | a :: args' when Impargs.is_status_implicit a ->
    MaxImplicit :: loop args'
  | args' when List.exists Impargs.is_status_implicit args' ->
      errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
  | _ -> [] in
  let impls =
    match Impargs.implicits_of_global fref  with
    | [cond,impls] -> impls
    | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f)
    | _ -> errorstrm (str "Multiple implicits not supported") in
  match loop impls  with
  | [] ->
    errorstrm (str "Expected some implicits for " ++ pr_qualid f)
  | impls ->
    Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls]

}

VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
  | #[ locality = Attributes.locality; ] [ "Prenex" "Implicits" ne_global_list(fl) ]
  -> {
         let locality = Locality.make_section_locality locality in
         List.iter (declare_one_prenex_implicit locality) fl;
     }
END

(* Vernac grammar visibility patch *)

GRAMMAR EXTEND Gram
  GLOBAL: gallina_ext;
  gallina_ext: TOP
   [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" ->
      { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) }
   ] ]
  ;
END

(** View hint database and View application. *)(* ******************************)

(* There are three databases of lemmas used to mediate the application  *)
(* of reflection lemmas: one for forward chaining, one for backward     *)
(* chaining, and one for secondary backward chaining.                   *)

(* View hints *)

{

let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
  | { v = CAppExpl ((r,x), args) } when isCHoles args ->
    prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
  | { v = CApp ({ v = CRef _ }, _) } as c -> prc env sigma c
  | { v = CApp (c, args) } when isCxHoles args ->
    prc env sigma c ++ str "|" ++ int (List.length args)
  | c -> prc env sigma c

let pr_rawhintref env sigma c =
  match DAst.get c with
  | GApp (f, args) when isRHoles args ->
    pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args)
  | _ -> pr_glob_constr_env env sigma c

let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c

let pr_ssrhintref env sigma prc _ _ = prc env sigma

let mkhintref ?loc c n = match c.CAst.v with
  | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((r, x), mkCHoles ?loc n)
  | _ -> mkAppC (c, mkCHoles ?loc n)

}

ARGUMENT EXTEND ssrhintref
  TYPED AS constr
  PRINTED BY { pr_ssrhintref env sigma }
  RAW_PRINTED BY { pr_raw_ssrhintref env sigma }
  GLOB_PRINTED BY { pr_glob_ssrhintref env sigma }
  | [ constr(c) ] -> {  c  }
  | [ constr(c) "|" natural(n) ] -> {  mkhintref ~loc c n  }
END

{

(* View purpose *)

let pr_viewpos = function
  | Some Ssrview.AdaptorDb.Forward -> str " for move/"
  | Some Ssrview.AdaptorDb.Backward -> str " for apply/"
  | Some Ssrview.AdaptorDb.Equivalence -> str " for apply//"
  | None -> mt ()

let pr_ssrviewpos _ _ _ = pr_viewpos

}

ARGUMENT EXTEND ssrviewpos PRINTED BY { pr_ssrviewpos }
  | [ "for" "move" "/" ] -> {  Some Ssrview.AdaptorDb.Forward  }
  | [ "for" "apply" "/" ] -> {  Some Ssrview.AdaptorDb.Backward  }
  | [ "for" "apply" "/" "/" ] -> {  Some Ssrview.AdaptorDb.Equivalence  }
  | [ "for" "apply" "//" ] -> {  Some Ssrview.AdaptorDb.Equivalence  }
  | [ ] -> {  None  }
END

{

let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc ()

}

ARGUMENT EXTEND ssrviewposspc TYPED AS ssrviewpos PRINTED BY { pr_ssrviewposspc }
  | [ ssrviewpos(i) ] -> {  i  }
END

{

let print_view_hints env sigma kind l =
  let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
  let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
  Feedback.msg_notice  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())

}

VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
  {
    let env = Global.env () in
    let sigma = Evd.from_env env in
    (match i with
    | Some k ->
      print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
    | None ->
        List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
          [ Ssrview.AdaptorDb.Forward;
            Ssrview.AdaptorDb.Backward;
            Ssrview.AdaptorDb.Equivalence ])
  }
END

{

let glob_view_hints lvh =
  List.map (Constrintern.intern_constr (Global.env ()) (Evd.from_env (Global.env ()))) lvh

}

VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
  |  [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] ->
     { let hints = glob_view_hints lvh in
       match n with
       | None ->
          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Forward hints;
          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Backward hints
       | Some k ->
          Ssrview.AdaptorDb.declare k hints }
END

(** Search compatibility *)

{

open G_vernac
}

GRAMMAR EXTEND Gram
  GLOBAL: query_command;

  query_command: TOP
    [ [ IDENT "Search"; s = search_query; l = search_queries; "." ->
          { let (sl,m) = l in
            fun g ->
              Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) }
      ] ]
;
END

(** Keyword compatibility fixes. *)

(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)
(* identifiers used as keywords. This is incompatible with ssreflect.v *)
(* which makes "by" and "of" true keywords, because of technicalities  *)
(* in the internal lexer-parser API of Coq. We patch this here by      *)
(* adding new parsing rules that recognize the new keywords.           *)
(*   To make matters worse, the Coq grammar for tactics fails to       *)
(* export the non-terminals we need to patch. Fortunately, the CamlP5  *)
(* API provides a backdoor access (with loads of Obj.magic trickery).  *)

(* Coq v8.3 defines "by" as a keyword, some hacks are not needed any   *)
(* longer and thus comment out. Such comments are marked with v8.3     *)

{

open Pltac

}

GRAMMAR EXTEND Gram
  GLOBAL: hypident;
  hypident: TOP [
  [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypTypeOnly }
  | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypValueOnly }
  ] ];
END

GRAMMAR EXTEND Gram
  GLOBAL: constr_eval;
  constr_eval: TOP [
    [ IDENT "type"; "of"; c = Constr.constr -> { Genredexpr.ConstrTypeOf c }]
  ];
END

(* We wipe out all the keywords generated by the grammar rules we defined. *)
(* The user is supposed to Require Import ssreflect or Require ssreflect   *)
(* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
(* consequence the extended ssreflect grammar.                             *)
{

let () = CLexer.set_keyword_state frozen_lexer ;;

}

(* vim: set filetype=ocaml foldmethod=marker: *)