|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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 GLOBAL PLUGIN
{
open Names
open Libnames
open Procq.Prim
let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
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 my_to_nat_string ?loc s =
match NumTok.Unsigned.to_nat s with
| Some n -> n
| None ->
CErrors.user_err ?loc Pp.(str "This number is not an integer.")
let test_pipe_closedcurly =
let open Procq.Lookahead in
to_entry "test_pipe_closedcurly" begin
lk_kw "|" >> lk_kw "}" >> check_no_space
end
let test_minus_nat =
let open Procq.Lookahead in
to_entry "test_minus_nat" begin
lk_kw "-" >> lk_nat >> check_no_space
end
}
GRAMMAR EXTEND Gram
GLOBAL:
bignat bigint natural integer identref name ident hyp preident
fullyqualid qualid reference dirpath ne_lstring
ne_string string lstring pattern_ident by_notation
smart_global bar_cbrace strategy_level fields;
preident:
[ [ s = IDENT -> { s } ] ]
;
ident:
[ [ s = IDENT -> { Id.of_string s } ] ]
;
pattern_ident:
[ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ]
;
identref:
[ [ id = ident -> { CAst.make ~loc id } ] ]
;
hyp: (* as identref, but interpreted as an hypothesis in tactic notations *)
[ [ id = identref -> { 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] }
] ]
;
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 -> { qualid_of_ident ~loc id }
] ]
;
qualid: (* Synonymous to reference *)
[ [ qid = reference -> { qid } ] ]
;
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 } ] ]
;
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 = bigint -> { my_int_of_string ~loc i } ] ]
;
natural:
[ [ i = bignat -> { my_int_of_string ~loc i } ] ]
;
bigint:
[ [ i = bignat -> { i }
| test_minus_nat; "-"; i = bignat -> { "-" ^ i } ] ]
;
bignat:
[ [ i = NUMBER -> { my_to_nat_string ~loc i } ] ]
;
bar_cbrace:
[ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
;
strategy_level:
[ [ IDENT "expand" -> { Conv_oracle.Expand }
| IDENT "opaque" -> { Conv_oracle.Opaque }
| n=integer -> { Conv_oracle.Level n }
| IDENT "transparent" -> { Conv_oracle.transparent } ] ]
;
END
[ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
]
|
