let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
-let default_precedence = 50
let default_associativity = Gramext.NonA
let mk_rec_corec ind_kind defs loc =
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
- tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
+ tactic_term: [ [ t = term LEVEL "90" -> t ] ];
new_name: [
[ id = IDENT -> Some id
| SYMBOL "_" -> None ]
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
+ | IDENT "applyP"; t = tactic_term ->
+ GrafiteAst.ApplyP (loc, t)
| IDENT "applyS"; t = tactic_term ; params = auto_params ->
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
| IDENT "autobatch"; params = auto_params ->
GrafiteAst.AutoBatch (loc,params)
| IDENT "cases"; what = tactic_term;
+ pattern = OPT pattern_spec;
specs = intros_spec ->
- GrafiteAst.Cases (loc, what, specs)
+ let pattern = match pattern with
+ | None -> None, [], Some Ast.UserInput
+ | Some pattern -> pattern
+ in
+ GrafiteAst.Cases (loc, what, pattern, specs)
| IDENT "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
| [ 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;
SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
GrafiteAst.Check (loc, t)
| [ IDENT "inline"];
style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
- suri = QSTRING; prefix = OPT QSTRING ->
+ suri = QSTRING; prefix = OPT QSTRING;
+ flavour = OPT [ IDENT "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 ->
];
notation: [
[ dir = OPT direction; s = QSTRING;
- assoc = OPT associativity; prec = OPT precedence;
+ assoc = OPT associativity; prec = precedence;
IDENT "for";
p2 =
[ blob = UNPARSED_AST ->
| None -> default_associativity
| Some assoc -> assoc
in
- let prec =
- match prec with
- | None -> default_precedence
- | Some prec -> prec
- in
let p1 =
add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern
+ (CicNotationParser.parse_level1_pattern prec
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ;
- saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
+ | IDENT "coercion" ;
+ t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
+ arity = OPT int ; saturations = OPT int;
+ composites = OPT (IDENT "nocomposites") ->
let arity = match arity with None -> 0 | Some x -> x in
let saturations = match saturations with None -> 0 | Some x -> x in
let composites = match composites with None -> true | Some _ -> false in
GrafiteAst.Coercion
- (loc, UriManager.uri_of_string suri, composites, arity, saturations)
+ (loc, t, composites, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
| com = comment ->
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 ->
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
else LexiconEngine.eval_command status
(LexiconAst.Include (iloc,buri,mode,fullpath))
in
- !out fname;
status,
LSome
(GrafiteAst.Executable