(* $Id$ *)
-open Printf
+let out = ref ignore
+let set_callback f = out := f
module Ast = CicNotationPt
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
- ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+ new_name: [
+ [ id = IDENT -> Some id
+ | SYMBOL "_" -> None ]
+ ];
+ ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
- | IDENT "auto"; params = auto_params ->
- GrafiteAst.Auto (loc,params)
+ | IDENT "autobatch"; params = auto_params ->
+ GrafiteAst.AutoBatch (loc,params)
| IDENT "cases"; what = tactic_term;
- (num, idents) = intros_spec ->
- GrafiteAst.Cases (loc, what, idents)
+ specs = intros_spec ->
+ GrafiteAst.Cases (loc, what, specs)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Change (loc, what, t)
+ | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
+ specs = intros_spec ->
+ GrafiteAst.Compose (loc, t1, t2, specs)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
- | IDENT "elim"; what = tactic_term; using = using;
+ | IDENT "elim"; what = tactic_term; using = using;
+ pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
- let pattern = Some what, [], Some Ast.UserInput in
- GrafiteAst.Elim (loc, pattern, using, num, idents)
- | IDENT "elim"; pattern = pattern_spec; using = using;
- (num, idents) = intros_spec ->
- GrafiteAst.Elim (loc, pattern, using, num, idents)
+ let pattern = match pattern with
+ | None -> None, [], Some Ast.UserInput
+ | Some pattern -> pattern
+ in
+ GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
- GrafiteAst.ElimType (loc, what, using, num, idents)
+ GrafiteAst.ElimType (loc, what, using, (num, idents))
| IDENT "exact"; t = tactic_term ->
GrafiteAst.Exact (loc, t)
| IDENT "exists" ->
GrafiteAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
GrafiteAst.Fourier loc
- | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+ | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
GrafiteAst.Generalize (loc,p,id)
- | IDENT "goal"; n = int ->
- GrafiteAst.Goal (loc, n)
| IDENT "id" -> GrafiteAst.IdTac loc
| IDENT "intro"; ident = OPT IDENT ->
- let idents = match ident with None -> [] | Some id -> [id] in
- GrafiteAst.Intros (loc, Some 1, idents)
- | IDENT "intros"; (num, idents) = intros_spec ->
- GrafiteAst.Intros (loc, num, idents)
+ let idents = match ident with None -> [] | Some id -> [Some id] in
+ GrafiteAst.Intros (loc, (Some 1, idents))
+ | IDENT "intros"; specs = intros_spec ->
+ GrafiteAst.Intros (loc, specs)
| IDENT "inversion"; t = tactic_term ->
GrafiteAst.Inversion (loc, t)
| IDENT "lapply";
(GrafiteAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
+ [ IDENT "do"; count = int; tac = SELF ->
GrafiteAst.Do (loc, count, tac)
- | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
+ | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
]
| "simple" NONA
[ IDENT "first";
GrafiteAst.Solve (loc, tacs)
| IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
| LPAREN; tac = SELF; RPAREN -> tac
- | tac = tactic -> GrafiteAst.Tactic (loc, tac)
+ | tac = tactic -> tac
]
];
punctuation_tactical:
| SYMBOL "." -> GrafiteAst.Dot loc
]
];
- tactical:
+ non_punctuation_tactical:
[ "simple" NONA
[ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
| IDENT "unfocus" -> GrafiteAst.Unfocus loc
| IDENT "skip" -> GrafiteAst.Skip loc
- | tac = atomic_tactical LEVEL "loops" -> tac
]
];
theorem_flavour: [
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
+ | IDENT "auto"; params = auto_params ->
+ GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WMatch (loc,t)
| [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
LexiconAst.Ident_alias (id, uri)
else
raise
- (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
+ (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
else
raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
- sprintf "Not a valid identifier: %s" id)))
+ Printf.sprintf "Not a valid identifier: %s" id)))
| IDENT "symbol"; symbol = QSTRING;
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
IDENT "for";
p2 =
[ blob = UNPARSED_AST ->
- add_raw_attribute ~text:(sprintf "@{%s}" blob)
+ add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
(CicNotationParser.parse_level2_ast
(Ulexing.from_utf8_string blob))
| blob = UNPARSED_META ->
- add_raw_attribute ~text:(sprintf "${%s}" blob)
+ add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
(CicNotationParser.parse_level2_meta
(Ulexing.from_utf8_string blob))
] ->
]];
executable: [
[ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
- | tac = tactical; punct = punctuation_tactical ->
- GrafiteAst.Tactical (loc, tac, Some punct)
- | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
+ | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
+ GrafiteAst.Tactic (loc, Some tac, punct)
+ | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+ | tac = non_punctuation_tactical; punct = punctuation_tactical ->
+ GrafiteAst.NonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
]
];
fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
fun ~include_paths status ->
- let buri, fullpath =
+ let buri, fullpath =
DependenciesParser.baseuri_of_script ~include_paths fname
in
let status =
LexiconEngine.eval_command status
(LexiconAst.Include (iloc,buri,mode,fullpath))
in
+ !out fname;
status,
LSome
(GrafiteAst.Executable