git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Implement functions.
[goals.git]
/
src
/
parser.mly
diff --git
a/src/parser.mly
b/src/parser.mly
index
6cb48f7
..
c3148ca
100644
(file)
--- a/
src/parser.mly
+++ b/
src/parser.mly
@@
-40,7
+40,7
@@
let find_on_include_path filename =
)
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 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 filename = find_on_include_path filename in
if optflag && not (Sys.file_exists filename) then env
else (
@@
-61,6
+61,7
@@
let do_include env loc filename optflag file =
%token COMMA
%token EQUALS
%token EOF
%token COMMA
%token EQUALS
%token EOF
+%token FUNCTION
%token GOAL
%token <string> ID
%token INCLUDE
%token GOAL
%token <string> ID
%token INCLUDE
@@
-70,6
+71,7
@@
let do_include env loc filename optflag file =
%token OPTINCLUDE
%token RIGHT_ARRAY
%token RIGHT_PAREN
%token OPTINCLUDE
%token RIGHT_ARRAY
%token RIGHT_PAREN
+%token SEMICOLON
%token <Ast.substs> STRING
%token <string> TACTIC
%token TACTIC_KEYWORD
%token <Ast.substs> STRING
%token <string> TACTIC
%token TACTIC_KEYWORD
@@
-85,11
+87,12
@@
file:
stmts:
| (* none *) { Ast.Env.empty }
stmts:
| (* none *) { Ast.Env.empty }
- | stmts INCLUDE STRING
+ | stmts INCLUDE STRING
option(SEMICOLON)
{ do_include $1 $loc $3 false file }
{ do_include $1 $loc $3 false file }
- | stmts OPTINCLUDE STRING
+ | stmts OPTINCLUDE STRING
option(SEMICOLON)
{ do_include $1 $loc $3 true file }
{ do_include $1 $loc $3 true file }
- | stmts stmt { let name, expr = $2 in Ast.Env.add name expr $1 }
+ | stmts stmt option(SEMICOLON)
+ { let name, expr = $2 in Ast.Env.add name expr $1 }
;
stmt:
;
stmt:
@@
-106,6
+109,10
@@
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))
}
+ | FUNCTION ID params_decl EQUALS CODE
+ {
+ $2, Ast.EFuncDefn ($loc, ($3, $5))
+ }
| 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))
@@
-138,9
+145,9
@@
pattern_param:
;
expr:
;
expr:
- | ID params { Ast.ECall
Goal
($loc, $1, $2) }
+ | ID params { Ast.ECall ($loc, $1, $2) }
| ID { Ast.EVar ($loc, $1) }
| ID { Ast.EVar ($loc, $1) }
- | TACTIC params { Ast.E
CallTactic
($loc, $1, $2) }
+ | TACTIC params { Ast.E
TacticCtor
($loc, $1, $2) }
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;