module Ast = CicNotationPt
+type 'a localized_option =
+ LSome of 'a
+ | LNone of Token.flocation
+
type statement =
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
- GrafiteAst.statement
+ include_paths:string list ->
+ LexiconEngine.status ->
+ LexiconEngine.status *
+ (CicNotationPt.term, CicNotationPt.term,
+ CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+ GrafiteAst.statement localized_option
let grammar = CicNotationParser.level2_ast_grammar
goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
let goal_path =
match goal_path, hyp_paths with
- None, [] -> Ast.UserInput
- | None, _::_ -> Ast.Implicit
- | Some goal_path, _ -> goal_path
+ None, [] -> Some Ast.UserInput
+ | None, _::_ -> None
+ | Some goal_path, _ -> Some goal_path
in
hyp_paths,goal_path
]
] ->
let wanted,hyp_paths,goal_path =
match wanted_and_sps with
- wanted,None -> wanted, [], Ast.UserInput
+ wanted,None -> wanted, [], Some Ast.UserInput
| wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
in
wanted, hyp_paths, goal_path ] ->
match res with
- None -> None,[],Ast.UserInput
+ None -> None,[],Some Ast.UserInput
| Some ps -> ps]
];
direction: [
GrafiteAst.Intros (loc, Some 1, idents)
| IDENT "intros"; (num, idents) = intros_spec ->
GrafiteAst.Intros (loc, num, idents)
+ | IDENT "inversion"; t = tactic_term ->
+ GrafiteAst.Inversion (loc, t)
| IDENT "lapply";
depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
what = tactic_term;
name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
- name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty)
+ name = IDENT ;
+ coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ;
+ ty = term -> (name,ty,coercion)
] SEP SYMBOL ";"; SYMBOL "}" ->
let params =
List.fold_right
if (try ignore (UriManager.uri_of_string uri); true
with UriManager.IllFormedUri _ -> false)
then
- GrafiteAst.Ident_alias (id, uri)
+ LexiconAst.Ident_alias (id, uri)
else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
let instance =
match instance with Some i -> i | None -> 0
in
- GrafiteAst.Symbol_alias (symbol, instance, dsc)
+ LexiconAst.Symbol_alias (symbol, instance, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- GrafiteAst.Number_alias (instance, dsc)
+ LexiconAst.Number_alias (instance, dsc)
]
];
argument: [
(s, args, t)
]
];
- command: [ [
+
+ include_command: [ [
+ IDENT "include" ; path = QSTRING -> loc,path
+ ]];
+
+ grafite_command: [ [
IDENT "set"; n = QSTRING; v = QSTRING ->
GrafiteAst.Set (loc, n, v)
| IDENT "drop" -> GrafiteAst.Drop loc
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; name = IDENT ->
- GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true)
- | IDENT "coercion" ; name = URI ->
- GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true)
- | IDENT "alias" ; spec = alias_spec ->
- GrafiteAst.Alias (loc, spec)
+ | IDENT "coercion" ; suri = URI ->
+ GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
- | IDENT "include" ; path = QSTRING ->
- GrafiteAst.Include (loc,path)
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
GrafiteAst.Default (loc,what,uris)
+ ]];
+ lexicon_command: [ [
+ IDENT "alias" ; spec = alias_spec ->
+ LexiconAst.Alias (loc, spec)
| IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
- GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
+ LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
- GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
-
- | IDENT "dump" -> GrafiteAst.Dump loc
- | IDENT "render"; u = URI ->
- GrafiteAst.Render (loc, UriManager.uri_of_string u)
+ LexiconAst.Interpretation (loc, id, (symbol, args), l3)
]];
executable: [
- [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
+ [ 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)
]
];
statement: [
- [ ex = executable -> GrafiteAst.Executable (loc,ex)
- | com = comment -> GrafiteAst.Comment (loc, com)
+ [ ex = executable ->
+ fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+ | com = comment ->
+ fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+ | (iloc,fname) = include_command ; SYMBOL "." ->
+ fun ~include_paths status ->
+ let path = DependenciesParser.baseuri_of_script ~include_paths fname in
+ let status =
+ LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+ in
+ status,
+ LSome
+ (GrafiteAst.Executable
+ (loc,GrafiteAst.Command
+ (loc,GrafiteAst.Include (iloc,path))))
+ | scom = lexicon_command ; SYMBOL "." ->
+ fun ~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)))
-
-let parse_dependencies lexbuf =
- let tok_stream,_ =
- CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
- in
- let rec parse acc =
- (parser
- | [< '("URI", u) >] ->
- parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc)
- | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
- parse (GrafiteAst.IncludeDep fname :: acc)
- | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
- parse (GrafiteAst.BaseuriDep baseuri :: acc)
- | [< '("EOI", _) >] -> acc
- | [< 'tok >] -> parse acc
- | [< >] -> acc) tok_stream
- in
- List.rev (parse [])
-
projects / helm.git / blobdiff