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) ] ];
]
];
using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+ ntactic: [
+ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+ | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
+ GrafiteAst.NChange (loc, what, with_what)
+ | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
+ GrafiteAst.NElim (loc, what, where)
+ | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+ ]
+ ];
tactic: [
[ IDENT "absurd"; t = tactic_term ->
GrafiteAst.Absurd (loc, t)
+ | IDENT "apply"; IDENT "rule"; t = tactic_term ->
+ GrafiteAst.ApplyRule (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
| IDENT "applyP"; t = tactic_term ->
GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
- (num, idents) = intros_spec ->
+ ispecs = intros_spec ->
let pattern = match pattern with
| None -> None, [], Some Ast.UserInput
| Some pattern -> pattern
in
- GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
+ GrafiteAst.Elim (loc, what, using, pattern, ispecs)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, (num, idents))
| IDENT "skip" -> GrafiteAst.Skip loc
]
];
+ ntheorem_flavour: [
+ [ [ IDENT "ntheorem" ] -> `Theorem
+ ]
+ ];
theorem_flavour: [
[ [ IDENT "definition" ] -> `Definition
| [ IDENT "fact" ] -> `Fact
| [ IDENT "theorem" ] -> `Theorem
]
];
+ inline_flavour: [
+ [ attr = theorem_flavour -> attr
+ | [ IDENT "axiom" ] -> `Axiom
+ | [ IDENT "mutual" ] -> `MutualDefinition
+ ]
+ ];
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 ->
+ suri = QSTRING; prefix = OPT QSTRING;
+ flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
let style = match style with
| None -> GrafiteAst.Declarative
| Some depth -> GrafiteAst.Procedural depth
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
- GrafiteAst.Inline (loc,style,suri,prefix)
+ GrafiteAst.Inline (loc,style,suri,prefix, flavour)
| [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
| IDENT "auto"; params = auto_params ->
let alpha = "[a-zA-Z]" in
let num = "[0-9]+" in
let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
- let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+ let decoration = "\\'" in
+ let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
if (try ignore (UriManager.uri_of_string uri); true
GrafiteAst.Obj (loc,
Ast.Theorem
(`Variant,name,typ,Some (Ast.Ident (newname, None))))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
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
let composites = match composites with None -> true | Some _ -> false in
GrafiteAst.Coercion
(loc, t, composites, arity, saturations)
+ | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
+ GrafiteAst.PreferCoercion (loc, t)
+ | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+ GrafiteAst.UnificationHint (loc, t, n)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
| tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
GrafiteAst.Tactic (loc, Some tac, punct)
| punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+ | tac = ntactic; punct = punctuation_tactical ->
+ GrafiteAst.NTactic (loc, tac, punct)
+ | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
+ GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
| tac = non_punctuation_tactical; punct = punctuation_tactical ->
GrafiteAst.NonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
[ ex = executable ->
fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
| com = comment ->
- fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+ fun ?(never_include=false) ~include_paths status ->
+ status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
!out fname;
fun ?(never_include=false) ~include_paths status ->
]
];
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: *)
+
projects / helm.git / blobdiff