Define *file() syntax for tactic constructors.

Alternative syntaxes considered where ~file and &file.

diff --git a/src/ast.ml b/src/ast.ml
index 6a7823c..885eefe 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -38,6 +38,7 @@ and pattern =
 and expr =
   | EGoal of loc * goal
   | ECall of loc * id * expr list
+  | ETactic of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -109,7 +110,7 @@ and print_def fp name expr =
 
 and print_pattern fp = function
   | PTactic (loc, name, params) ->
-     fprintf fp "%s (" name;
+     fprintf fp "*%s (" name;
      iter_with_commas fp print_substs params;
      fprintf fp ")"
   | PVar (loc, id) -> print_id fp id
@@ -120,6 +121,10 @@ and print_expr fp = function
      fprintf fp "%s (" name;
      iter_with_commas fp print_expr params;
      fprintf fp ")"
+  | ETactic (loc, name, params) ->
+     fprintf fp "*%s (" name;
+     iter_with_commas fp print_expr params;
+     fprintf fp ")"
   | EVar (loc, var) -> print_id fp var
   | EList (loc, xs) ->
      fprintf fp "[";

diff --git a/src/ast.mli b/src/ast.mli
index 4162eb3..c7e3be4 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -45,9 +45,11 @@ and pattern =
 and expr =
   (** goal (params) = patterns : exprs = code *)
   | EGoal of loc * goal
-  (** goalname (params), tactic (params) etc. *)
+  (** goalname (params) etc. *)
   | ECall of loc * id * expr list
-  (** variable *)
+  (** *tactic (params) etc. *)
+  | ETactic of loc * id * expr list
+  (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)
   | EList of loc * expr list

diff --git a/src/eval.ml b/src/eval.ml
index 779cb5d..e928564 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -25,21 +25,7 @@ let rec evaluate_targets env exprs =
 and evaluate_target env = function
   | Ast.EGoal _ -> assert false
 
-  (* This could be an instruction to call a goal, or it
-   * could be a tactic.
-   *)
-  | Ast.ECall (loc, "file", [filename]) (* XXX define tactics! *) ->
-     (* All parameters of tactics must be simple expressions (strings,
-      * in future booleans, numbers, etc).
-      *)
-     let args = [filename] in
-     let args = List.map (simplify env) args in
-     run_goal_for_tactic loc env "file" args
-
-  | Ast.ECall (loc, "file", _) ->
-     failwithf "%a: file tactic called with wrong number of parameters"
-       Ast.string_loc loc
-
+  (* Call a goal. *)
   | Ast.ECall (loc, name, args) ->
      let expr =
        try Ast.StringMap.find name env
@@ -53,6 +39,13 @@ and evaluate_target env = function
             Ast.string_loc loc name in
      run_goal loc env name args goal
 
+  | Ast.ETactic (loc, name, args) ->
+     (* All parameters of tactics must be simple expressions (strings,
+      * in future booleans, numbers, etc).
+      *)
+     let args = List.map (simplify env) args in
+     run_goal_for_tactic loc env name args
+
   (* Look up the variable and substitute it. *)
   | Ast.EVar (loc, name) ->
      let expr =
@@ -65,7 +58,7 @@ and evaluate_target env = function
   | Ast.EList (loc, exprs) ->
      evaluate_targets env exprs
 
-  (* A string (with or without substitutions) implies file (filename). *)
+  (* A string (with or without substitutions) implies *file(filename). *)
   | Ast.ESubsts (loc, str) ->
      let str = substitute loc env str in
      run_goal_for_tactic loc env "file" [Ast.CString str]
@@ -181,7 +174,11 @@ and simplify env = function
        Ast.string_loc loc
 
   | Ast.ECall (loc, name, _) ->
-     failwithf "%a: cannot use goal or tactic ‘%s’ in constant expression"
+     failwithf "%a: cannot use goal ‘%s’ in constant expression"
+       Ast.string_loc loc name
+
+  | Ast.ETactic (loc, name, _) ->
+     failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
        Ast.string_loc loc name
 
   | Ast.EGoal (loc, _) ->

diff --git a/src/lexer.mll b/src/lexer.mll
index d0f4a1d..a9b11d1 100644 (file)
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -52,6 +52,9 @@ rule read =
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
     | "let"   { LET }
+    | "*" id  { let id = Lexing.lexeme lexbuf in
+                let len = String.length id in
+                TACTIC (String.sub id 1 (len-1)) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | _       { raise (SyntaxError ("unexpected character: " ^
                                     Lexing.lexeme lexbuf)) }

diff --git a/src/parser.mly b/src/parser.mly
index 69cb063..3531b08 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -25,16 +25,17 @@ open Printf
 %token <Ast.substs> CODE
 %token COLON
 %token COMMA
-%token <string> ID
 %token EQUALS
 %token EOF
 %token GOAL
+%token <string> ID
 %token LEFT_ARRAY
 %token LEFT_PAREN
 %token LET
 %token RIGHT_ARRAY
 %token RIGHT_PAREN
 %token <Ast.substs> STRING
+%token <string> TACTIC
 
 (* Start nonterminals. *)
 %start <Ast.env> file
@@ -95,6 +96,7 @@ pattern_param:
 expr:
     | ID params  { Ast.ECall ($loc, $1, $2) }
     | ID         { Ast.EVar ($loc, $1) }
+    | TACTIC params { Ast.ETactic ($loc, $1, $2) }
     | STRING     { Ast.ESubsts ($loc, $1) }
     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
     ;

diff --git a/tests/test1.gl b/tests/test1.gl
index fc059d0..afdcc34 100644 (file)
--- a/tests/test1.gl
+++ b/tests/test1.gl
@@ -1,6 +1,6 @@
 # Test.
 
-goal all = : ["file1.o", "file2.o"]
+goal all = : "file1.o", *file("file2.o")
 
 "file1.o" : "file1.c" {
   echo file1.c "->" file1.o