module Ast = CicNotationPt
+exception NoInclusionPerformed of string (* full path *)
+
type 'a localized_option =
LSome of 'a
| LNone of GrafiteAst.loc
GrafiteAst.statement
type statement =
+ ?never_include:bool ->
include_paths:string list ->
LexiconEngine.status ->
LexiconEngine.status * ast_statement localized_option
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 "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+ GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
- | IDENT "subst" ->
- GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
+ | IDENT "coercion" ; suri = URI ; 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, true, arity, saturations)
+ (loc, UriManager.uri_of_string suri, 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 ->
];
statement: [
[ ex = executable ->
- fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+ fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
| com = comment ->
- fun ~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 "." ->
- fun ~include_paths status ->
- let buri, fullpath =
- DependenciesParser.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
in
let status =
- LexiconEngine.eval_command status
- (LexiconAst.Include (iloc,buri,mode,fullpath))
+ if never_include then raise (NoInclusionPerformed fullpath)
+ else LexiconEngine.eval_command status
+ (LexiconAst.Include (iloc,buri,mode,fullpath))
in
!out fname;
status,
(loc,GrafiteAst.Command
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
- fun ~include_paths status ->
+ fun ?(never_include=false) ~include_paths status ->
let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
let parse_statement lexbuf =
exc_located_wrapper
(fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+