]
];
using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+ ntactic: [
+ [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+ | IDENT "nchange"; what = tactic_term; with_what = tactic_term ->
+ GrafiteAst.NChange (loc, what, with_what)
+ ]
+ ];
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
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))
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)
| 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 ->