* by include files.
*)
let lexer_read = ref None
+
+let find_on_include_path filename =
+ if not (Filename.is_implicit filename) then filename
+ else (
+ let rec loop = function
+ | [] -> filename
+ | inc :: incs ->
+ let path = inc // filename in
+ if Sys.file_exists path then path else loop incs
+ in
+ loop Cmdline.includes
+ )
+
+let do_include env loc filename optflag file =
+ let filename = Ast.substitute env loc filename in
+ let filename = find_on_include_path filename in
+ if optflag && not (Sys.file_exists filename) then env
+ else (
+ let fp = open_in filename in
+ let lexbuf = Lexing.from_channel fp in
+ lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
+ let reader =
+ match !lexer_read with None -> assert false | Some r -> r in
+ let env' = file reader lexbuf in
+ close_in fp;
+ Ast.Env.merge env env'
+ )
%}
(* Tokens. *)
%token LEFT_ARRAY
%token LEFT_PAREN
%token LET
+%token OPTINCLUDE
%token RIGHT_ARRAY
%token RIGHT_PAREN
+%token SEMICOLON
%token <Ast.substs> STRING
%token <string> TACTIC
%token TACTIC_KEYWORD
stmts:
| (* none *) { Ast.Env.empty }
- | stmts INCLUDE STRING
- {
- let env = $1 in
- let filename = Ast.substitute env $loc $3 in
- let rec find_on_include_path =
- function
- | [] -> filename
- | inc :: incs ->
- let path = inc // filename in
- if Sys.file_exists path then path
- else find_on_include_path incs
- in
- let filename =
- if Filename.is_implicit filename then
- find_on_include_path Cmdline.includes
- else filename in
- let fp = open_in filename in
- let lexbuf = Lexing.from_channel fp in
- lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
- let reader =
- match !lexer_read with None -> assert false | Some r -> r in
- let env' = file reader lexbuf in
- close_in fp;
- Ast.Env.merge env env'
- }
- | stmts stmt { let name, expr = $2 in Ast.Env.add name expr $1 }
+ | stmts INCLUDE STRING option(SEMICOLON)
+ { do_include $1 $loc $3 false file }
+ | stmts OPTINCLUDE STRING option(SEMICOLON)
+ { do_include $1 $loc $3 true file }
+ | stmts stmt option(SEMICOLON)
+ { let name, expr = $2 in Ast.Env.add name expr $1 }
;
stmt:
| None ->
sprintf "_goal@%d" $startpos.pos_lnum, []
| Some x -> x in
- name, Ast.EGoal ($loc, (params, $2, $4, $5))
+ name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
}
| goal_stmt CODE
{
let name, params = $1 in
- name, Ast.EGoal ($loc, (params, [], [], Some $2))
+ name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
}
| TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
{
- $2, Ast.ETactic ($loc, ($3, $5))
+ $2, Ast.ETacticDefn ($loc, ($3, $5))
}
| LET ID EQUALS expr { $2, $4 }
;
expr:
| ID params { Ast.ECallGoal ($loc, $1, $2) }
| ID { Ast.EVar ($loc, $1) }
- | TACTIC params { Ast.ECallTactic ($loc, $1, $2) }
+ | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;