git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
stdlib: Implement last() and nth() functions.
[goals.git]
/
src
/
parser.mly
diff --git
a/src/parser.mly
b/src/parser.mly
index
b84ac15
..
57a0c5c
100644
(file)
--- a/
src/parser.mly
+++ b/
src/parser.mly
@@
-21,11
+21,13
@@
open Utils
open Printf
open Utils
open Printf
-(* This is initialized with Lexer.read once the program
- * starts. Doing this avoids a circular dependency caused
- * by include files.
+(* There are several circular dependencies between the lexer
+ * (caused by includes) and eval. These references break
+ * the circular dependencies. They are initialized when
+ * the program starts, hence are never really None.
*)
let lexer_read = ref None
*)
let lexer_read = ref None
+let eval_substitute = ref None
let find_on_include_path filename =
if not (Filename.is_implicit filename) then filename
let find_on_include_path filename =
if not (Filename.is_implicit filename) then filename
@@
-36,31
+38,35
@@
let find_on_include_path filename =
let path = inc // filename in
if Sys.file_exists path then path else loop incs
in
let path = inc // filename in
if Sys.file_exists path then path else loop incs
in
- loop
Cmdline.includes
+ loop
(Cmdline.includes ())
)
let do_include env loc filename optflag file =
)
let do_include env loc filename optflag file =
- let filename = Ast.substitute env loc filename in
+ let eval_substitute =
+ match !eval_substitute with None -> assert false | Some f -> f in
+ let filename = eval_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 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
=
+ let
lexer_read
=
match !lexer_read with None -> assert false | Some r -> r in
match !lexer_read with None -> assert false | Some r -> r in
- let env' = file
reader
lexbuf in
+ let env' = file
lexer_read
lexbuf in
close_in fp;
Ast.Env.merge env env'
)
%}
(* Tokens. *)
close_in fp;
Ast.Env.merge env env'
)
%}
(* Tokens. *)
-%token <Ast.
substs
> CODE
+%token <Ast.
code
> CODE
%token COLON
%token COMMA
%token EQUALS
%token EOF
%token COLON
%token COMMA
%token EQUALS
%token EOF
+%token EXPRESSION
+%token FUNCTION
%token GOAL
%token <string> ID
%token INCLUDE
%token GOAL
%token <string> ID
%token INCLUDE
@@
-68,16
+74,20
@@
let do_include env loc filename optflag file =
%token LEFT_PAREN
%token LET
%token OPTINCLUDE
%token LEFT_PAREN
%token LET
%token OPTINCLUDE
+%token PURE
+%token RETURNING
%token RIGHT_ARRAY
%token RIGHT_PAREN
%token SEMICOLON
%token <Ast.substs> STRING
%token RIGHT_ARRAY
%token RIGHT_PAREN
%token SEMICOLON
%token <Ast.substs> STRING
+%token STRING_KEYWORD
+%token STRINGS
%token <string> TACTIC
%token TACTIC_KEYWORD
(* Start nonterminals. *)
%start <Ast.expr Ast.Env.t> file
%token <string> TACTIC
%token TACTIC_KEYWORD
(* Start nonterminals. *)
%start <Ast.expr Ast.Env.t> file
-%start <Ast.expr> expr
+%start <Ast.expr> expr
_only
%%
file:
%%
file:
@@
-108,6
+118,14
@@
stmt:
let name, params = $1 in
name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
}
let name, params = $1 in
name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
}
+ | GOAL ID
+ {
+ $2, Ast.EGoalDefn ($loc, ([], [], [], None))
+ }
+ | option(PURE) FUNCTION ID params_decl return_decl EQUALS CODE
+ {
+ $3, Ast.EFuncDefn ($loc, ($4, $5, $1 <> None, $7))
+ }
| TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
{
$2, Ast.ETacticDefn ($loc, ($3, $5))
| TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
{
$2, Ast.ETacticDefn ($loc, ($3, $5))
@@
-124,13
+142,18
@@
params_decl:
;
param_decl:
| ID { $1 }
;
param_decl:
| ID { $1 }
+return_decl:
+ | { RetExpr }
+ | RETURNING EXPRESSION { RetExpr }
+ | RETURNING STRINGS { RetStrings }
+ | RETURNING STRING_KEYWORD { RetString }
patterns:
| separated_list(COMMA, pattern) { $1 }
;
pattern:
| STRING { Ast.PTactic ($loc, "*file", [$1]) }
patterns:
| separated_list(COMMA, pattern) { $1 }
;
pattern:
| STRING { Ast.PTactic ($loc, "*file", [$1]) }
- |
ID
pattern_params { Ast.PTactic ($loc, $1, $2) }
+ |
TACTIC
pattern_params { Ast.PTactic ($loc, $1, $2) }
;
pattern_params:
| LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
;
pattern_params:
| LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
@@
-140,15
+163,28
@@
pattern_param:
;
expr:
;
expr:
- | ID params { Ast.ECall
Goal
($loc, $1, $2) }
+ | ID params { Ast.ECall ($loc, $1, $2) }
| ID { Ast.EVar ($loc, $1) }
| TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;
barelist:
| ID { Ast.EVar ($loc, $1) }
| TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;
barelist:
- |
separated
_list(COMMA, expr) { $1 }
+ |
right_flexible
_list(COMMA, expr) { $1 }
;
params:
| LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
;
;
params:
| LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
;
+
+(* This is used by Parse.parse_expr where we have to parse
+ * a standalone string (eg. from the command line).
+ *)
+expr_only:
+ | expr EOF { $1 }
+ ;
+
+(* http://gallium.inria.fr/blog/lr-lists/ *)
+right_flexible_list(delim, X):
+ | (* nothing *) { [] }
+ | x = X { [x] }
+ | x = X delim xs = right_flexible_list(delim, X) { x :: xs }