(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

{

open Names
open Libnames

open Pcoq.Prim

let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"]
let _ = List.iter CLexer.add_keyword prim_kw


let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id

let check_int loc = function
  | { NumTok.int = i; frac = ""; exp = "" } -> i
  | _ -> CErrors.user_err ~loc (Pp.str "This number is not an integer.")

let my_int_of_string loc s =
  try
    int_of_string s
  with Failure _ ->
    CErrors.user_err ~loc (Pp.str "This number is too large.")

let rec contiguous tok n m =
    n == m
  ||
    let (_, ep) = Loc.unloc (tok n) in
    let (bp, _) = Loc.unloc (tok (n + 1)) in
    Int.equal ep bp && contiguous tok (succ n) m

let rec lookahead_kwds strm n = function
  | [] -> ()
  | x :: xs ->
      let toks = Stream.npeek (n+1) strm in
      match List.nth toks n with
      | Tok.KEYWORD y ->
          if String.equal x y then lookahead_kwds strm (succ n) xs
          else raise Stream.Failure
      | _ -> raise Stream.Failure
      | exception (Failure _) -> raise Stream.Failure

(* [test_nospace m] fails if the next m tokens are not contiguous keywords *)
let test_nospace m = assert(m <> []); Pcoq.Entry.of_parser "test_nospace"
   (fun tok strm ->
      let n = Stream.count strm in
      lookahead_kwds strm 0 m;
      if contiguous tok n (n + List.length m - 1) then ()
      else raise Stream.Failure)

let test_nospace_pipe_closedcurly =
  test_nospace ["|"; "}"]


}

GRAMMAR EXTEND Gram
  GLOBAL:
    bigint natural integer identref name ident var preident
    fullyqualid qualid reference dirpath ne_lstring
    ne_string string lstring pattern_ident pattern_identref by_notation
    smart_global bar_cbrace;
  preident:
    [ [ s = IDENT -> { s } ] ]
  ;
  ident:
    [ [ s = IDENT -> { Id.of_string s } ] ]
  ;
  pattern_ident:
    [ [ LEFTQMARK; id = ident -> { id } ] ]
  ;
  pattern_identref:
    [ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
  ;
  var: (* as identref, but interpret as a term identifier in ltac *)
    [ [ id = ident -> { CAst.make ~loc id } ] ]
  ;
  identref:
    [ [ id = ident -> { CAst.make ~loc id } ] ]
  ;
  field:
    [ [ s = FIELD -> { Id.of_string s } ] ]
  ;
  fields:
    [ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') }
      | id = field -> { ([],id) }
      ] ]
  ;
  fullyqualid:
    [ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) }
      | id = ident -> { CAst.make ~loc [id] }
      ] ]
  ;
  basequalid:
    [ [ id = ident; f=fields -> { let (l,id') = f in  local_make_qualid loc (l@[id]) id' }
      | id = ident -> { qualid_of_ident ~loc id }
      ] ]
  ;
  name:
    [ [ IDENT "_"  -> { CAst.make ~loc Anonymous }
      | id = ident -> { CAst.make ~loc @@ Name id } ] ]
  ;
  reference:
    [ [ id = ident; f = fields -> {
        let (l,id') = f in
        local_make_qualid loc (l@[id]) id' }
      | id = ident -> { local_make_qualid loc [] id }
      ] ]
  ;
  by_notation:
    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ]
  ;
  smart_global:
    [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c }
      | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ]
  ;
  qualid:
    [ [ qid = basequalid -> { qid } ] ]
  ;
  ne_string:
    [ [ s = STRING ->
        { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s }
    ] ]
  ;
  ne_lstring:
    [ [ s = ne_string -> { CAst.make ~loc s } ] ]
  ;
  dirpath:
    [ [ id = ident; l = LIST0 field ->
        { DirPath.make (List.rev (id::l)) } ] ]
  ;
  string:
    [ [ s = STRING -> { s } ] ]
  ;
  lstring:
    [ [ s = string -> { CAst.make ~loc s } ] ]
  ;
  integer:
    [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
      | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
  ;
  natural:
    [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
  ;
  bigint: (* Negative numbers are dealt with elsewhere *)
    [ [ i = NUMERAL -> { check_int loc i } ] ]
  ;
  bar_cbrace:
    [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ]
  ;
END