*)
%{
+open Utils
open Printf
+
+(* This is initialized with Lexer.read once the program
+ * starts. Doing this avoids a circular dependency caused
+ * 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 EOF
%token GOAL
%token <string> ID
+%token INCLUDE
%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
(* Start nonterminals. *)
-%start <Ast.env> file
+%start <Ast.expr Ast.Env.t> file
%start <Ast.expr> expr
%%
;
stmts:
- | list(stmt)
- { List.fold_left (
- fun env (name, expr) -> Ast.Env.add name expr env
- ) Ast.Env.empty $1
- }
+ | (* none *) { Ast.Env.empty }
+ | 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:
| option(goal_stmt) patterns COLON barelist option(CODE)
{ let name, params =
| 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) }
;