LexiconEngine.status ->
LexiconEngine.status * ast_statement localized_option
-let grammar = CicNotationParser.level2_ast_grammar
+type parser_status = {
+ grammar : Grammar.g;
+ term : CicNotationPt.term Grammar.Entry.e;
+ statement : statement Grammar.Entry.e;
+}
-let term = CicNotationParser.term
-let statement = Grammar.Entry.create grammar "statement"
+let initial_parser () =
+ let grammar = CicNotationParser.level2_ast_grammar () in
+ let term = CicNotationParser.term () in
+ let statement = Grammar.Entry.create grammar "statement" in
+ { grammar = grammar; term = term; statement = statement }
+;;
+
+let grafite_parser = ref (initial_parser ())
let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
| BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
| BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+let initialize_parser () =
+ (* {{{ parser initialization *)
+ let term = !grafite_parser.term in
+ let statement = !grafite_parser.statement in
+ let let_defs = CicNotationParser.let_defs () in
+ let protected_binder_vars = CicNotationParser.protected_binder_vars () in
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
]
];
inductive_spec: [ [
- fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
+ fst_name = IDENT;
+ params = LIST0 protected_binder_vars;
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
fst_constructors = LIST0 constructor SEP SYMBOL "|";
tl = OPT [ "with";
] ];
record_spec: [ [
- name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
+ name = IDENT;
+ params = LIST0 protected_binder_vars;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
name = IDENT ;
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
+ | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
+ GrafiteAst.Eval (loc, kind, t)
| [ IDENT "inline"];
style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
suri = QSTRING; prefix = OPT QSTRING;
Ast.Theorem (flavour, name, Ast.Implicit, Some body))
| IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
- | LETCOREC ; defs = CicNotationParser.let_defs ->
+ | LETCOREC ; defs = let_defs ->
mk_rec_corec `CoInductive defs loc
- | LETREC ; defs = CicNotationParser.let_defs ->
+ | LETREC ; defs = let_defs ->
mk_rec_corec `Inductive defs loc
| IDENT "inductive"; spec = inductive_spec ->
let (params, ind_types) = spec in
]
];
END
+(* }}} *)
+;;
+
+let _ = initialize_parser () ;;
let exc_located_wrapper f =
try
let parse_statement lexbuf =
exc_located_wrapper
- (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+ (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
+
+let statement () = !grafite_parser.statement
+
+let history = ref [] ;;
+
+let push () =
+ LexiconSync.push ();
+ history := !grafite_parser :: !history;
+ grafite_parser := initial_parser ();
+ initialize_parser ()
+;;
+
+let pop () =
+ LexiconSync.pop ();
+ match !history with
+ | [] -> assert false
+ | gp :: tail ->
+ grafite_parser := gp;
+ history := tail
+;;
+
+(* vim:set foldmethod=marker: *)
+