GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
| IDENT "applyS"; t = tactic_term ; params = auto_params ->
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
| 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;
| IDENT "autobatch"; params = auto_params ->
GrafiteAst.AutoBatch (loc,params)
| IDENT "cases"; what = tactic_term;
- 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 "clear"; ids = LIST1 IDENT ->
GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
- | 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
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 ->
| 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 "." ->
| com = comment ->
fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths 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
else LexiconEngine.eval_command status
(LexiconAst.Include (iloc,buri,mode,fullpath))
in
| Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
| Stdpp.Exc_located (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
| Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
| Stdpp.Exc_located (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
| Stdpp.Exc_located (floc, exn) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
| Stdpp.Exc_located (floc, exn) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))