From: Richard W.M. Jones <rjones@redhat.com>
Date: Sat, 28 Dec 2019 16:28:41 +0000 (+0000)
Subject: Implement tactics.
X-Git-Tag: v'0.2'~123
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=214f84c3b07227767fef90934895a167b15113a1;p=goals.git

Implement tactics.
---

diff --git a/src/ast.ml b/src/ast.ml
index 9e5784b..9f3326a 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -38,8 +38,9 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   | EGoal of loc * goal
-  | ECall of loc * id * expr list
-  | ETactic of loc * id * expr list
+  | ETactic of loc * tactic
+  | ECallGoal of loc * id * expr list
+  | ECallTactic of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -47,6 +48,7 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
+and tactic = param_decl list * code
 and param_decl = id
 and id = string
 and code = substs
@@ -73,6 +75,20 @@ let getgoal env loc name =
          string_loc loc name in
   goal
 
+let gettactic env loc name =
+  assert (name.[0] = '*');
+  let expr =
+    try Env.find name env
+    with Not_found ->
+      failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
+  let tactic =
+    match expr with
+    | ETactic (loc, tactic) -> tactic
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a tactic"
+         string_loc loc name in
+  tactic
+
 let rec to_constant env = function
   | EConstant (loc, c) -> c
 
@@ -87,18 +103,22 @@ let rec to_constant env = function
      failwithf "%a: list found where constant expression expected"
        string_loc loc
 
-  | ECall (loc, name, _) ->
+  | ECallGoal (loc, name, _) ->
      failwithf "%a: cannot use goal ‘%s’ in constant expression"
        string_loc loc name
 
-  | ETactic (loc, name, _) ->
-     failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
+  | ECallTactic (loc, name, _) ->
+     failwithf "%a: cannot use tactic ‘%s’ in constant expression"
        string_loc loc name
 
   | EGoal (loc, _) ->
      failwithf "%a: cannot use goal in constant expression"
        string_loc loc
 
+  | ETactic (loc, _) ->
+     failwithf "%a: cannot use tactic in constant expression"
+       string_loc loc
+
 and substitute env loc substs =
   let b = Buffer.create 13 in
   List.iter (
@@ -138,18 +158,22 @@ and expr_to_shell_string env = function
      (* These are shell quoted so we can just concat them with space. *)
      String.concat " " strs
 
-  | ECall (loc, name, _) ->
+  | ECallGoal (loc, name, _) ->
      failwithf "%a: cannot use goal ‘%s’ in shell expansion"
        string_loc loc name
 
   (* Tactics expand to the first parameter. *)
-  | ETactic (loc, _, []) -> Filename.quote ""
-  | ETactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+  | ECallTactic (loc, _, []) -> Filename.quote ""
+  | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 
   | EGoal (loc, _) ->
      failwithf "%a: cannot use goal in shell expansion"
        string_loc loc
 
+  | ETactic (loc, _) ->
+     failwithf "%a: cannot use tactic in shell expansion"
+       string_loc loc
+
 module Substs = struct
   type t = {
       mutable elems : subst list; (* built in reverse order *)
@@ -190,6 +214,7 @@ and print_env fp env = output_string fp (string_env () env)
 and string_def () (name, expr) =
   match expr with
   | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+  | ETactic (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
   | expr -> sprintf "let %s = %a\n" name string_expr expr;
 
 and print_def fp name expr = output_string fp (string_def () (name, expr))
@@ -202,22 +227,28 @@ and string_goal () (name, (param_decls, patterns, exprs, code)) =
     (String.concat ", " (List.map (string_expr ()) exprs))
     (match code with None -> "" | Some code -> " = { ... }")
 
+and string_tactic () (name, (param_decls, code)) =
+  sprintf "tactic%s (%s) = { ... }"
+    (match name with None -> "" | Some name -> " " ^ name)
+    (String.concat ", " (List.map (string_param_decl ()) param_decls))
+
 and string_param_decl () name = name
 
 and string_pattern () = function
   | PTactic (loc, name, params) ->
-     sprintf "*%s (%s)" name (String.concat ", "
+     sprintf "%s (%s)" name (String.concat ", "
                                 (List.map (string_substs ()) params))
 
 and print_pattern fp p = output_string fp (string_pattern () p)
 
 and string_expr () = function
   | EGoal (loc, goal) -> string_goal () (None, goal)
-  | ECall (loc, name, params) ->
+  | ETactic (loc, goal) -> string_tactic () (None, goal)
+  | ECallGoal (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
-  | ETactic (loc, name, params) ->
-     sprintf "*%s (%s)"
+  | ECallTactic (loc, name, params) ->
+     sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | EVar (loc, var) -> var
   | EList (loc, xs) ->
diff --git a/src/ast.mli b/src/ast.mli
index 7a8e43f..56bfa7b 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -41,12 +41,14 @@ and pattern =
   (** match tactic such as *file ("filename") *)
   | PTactic of loc * id * substs list
 and expr =
-  (** goal (params) = patterns : exprs = code *)
+  (** goal (params) = patterns : exprs code *)
   | EGoal of loc * goal
-  (** goalname (params) etc. *)
-  | ECall of loc * id * expr list
-  (** *tactic (params) etc. *)
-  | ETactic of loc * id * expr list
+  (** tactic (params) = code *)
+  | ETactic of loc * tactic
+  (** call goalname (params) etc. *)
+  | ECallGoal of loc * id * expr list
+  (** call *tactic (params) etc. *)
+  | ECallTactic of loc * id * expr list
   (** variable, or goal call with no parameters *)
   | EVar of loc * id
   (** list *)
@@ -58,7 +60,8 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
-  (** Goal parameter is the parameter name and an optional default value. *)
+and tactic = param_decl list * code
+  (** Goal/tactic parameter. *)
 and param_decl = id
 and id = string
 and code = substs
@@ -77,6 +80,10 @@ val getvar : env -> loc -> id -> expr
     found or if the named variable is not a goal. *)
 val getgoal : env -> loc -> id -> goal
 
+(** Look up a tactic in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a tactic. *)
+val gettactic : env -> loc -> id -> tactic
+
 (** Take any expression and simplify it down to a constant.
     If the expression cannot be simplified then this raises
     [Failure _]. *)
diff --git a/src/eval.ml b/src/eval.ml
index af57213..27aa971 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -25,14 +25,15 @@ let rec evaluate_targets env exprs =
   List.iter (evaluate_target env) exprs
 
 and evaluate_target env = function
-  | Ast.EGoal _ -> assert false
+  | Ast.EGoal _ | Ast.ETactic _ -> assert false
 
   (* Call a goal. *)
-  | Ast.ECall (loc, name, args) ->
+  | Ast.ECallGoal (loc, name, args) ->
      let goal = Ast.getgoal env loc name in
      run_goal env loc name args goal
 
-  | Ast.ETactic (loc, name, args) ->
+  (* Call a tactic. *)
+  | Ast.ECallTactic (loc, name, args) ->
      (* All parameters of tactics must be simple constant expressions
       * (strings, in future booleans, numbers, etc).
       *)
@@ -51,10 +52,10 @@ and evaluate_target env = function
   (* A string (with or without substitutions) implies *file(filename). *)
   | Ast.ESubsts (loc, str) ->
      let str = Ast.substitute env loc str in
-     run_tactic env loc "file" [Ast.CString str]
+     run_tactic env loc "*file" [Ast.CString str]
 
   | Ast.EConstant (loc, c) ->
-     run_tactic env loc "file" [c]
+     run_tactic env loc "*file" [c]
 
 (* Run a goal by name. *)
 and run_goal env loc name args (params, patterns, deps, code) =
@@ -84,7 +85,7 @@ and run_goal env loc name args (params, patterns, deps, code) =
         let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
         let expr_of_pattern = function
           | Ast.PTactic (loc, tactic, targs) ->
-             Ast.ETactic (loc, tactic, List.map expr_of_substs targs)
+             Ast.ECallTactic (loc, tactic, List.map expr_of_substs targs)
         in
         let pexprs = List.map expr_of_pattern patterns in
         let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
@@ -119,16 +120,44 @@ and run_goal env loc name args (params, patterns, deps, code) =
 and needs_rebuild env loc deps pattern =
   match pattern with
   | Ast.PTactic (loc, tactic, targs) ->
-     (* Resolve the targs down to constants. *)
-     let targs = List.map ((* XXX Ast.to_shell_script *)
-                            Ast.substitute env loc) targs in
-     (* XXX Look up the tactic.
-      * We would do that, but for now hard code the *file tactic. XXX
+     (* Look up the tactic. *)
+     let params, code = Ast.gettactic env loc tactic in
+
+     (* Resolve the targs down to constants.  Since needs_rebuild
+      * should be called with env containing the goal params, this
+      * should substitute any parameters in the tactic arguments.
+      *)
+     let targs = List.map (Ast.substitute env loc) targs in
+     let targs =
+       List.map (fun targ ->
+           Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
+
+     (* Create a new environment binding parameter names
+      * to tactic args.
       *)
-     assert (tactic = "file");
-     assert (List.length targs = 1);
-     let targ = List.hd targs in
-     not (Sys.file_exists targ)
+     let env =
+       let params =
+         try List.combine params targs
+         with Invalid_argument _ ->
+           failwithf "%a: calling tactic ‘%s’ with wrong number of arguments"
+             Ast.string_loc loc tactic in
+       List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
+
+     (* Add some standard variables to the environment. *)
+     let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
+     let env =
+       match deps with
+       | [] -> env
+       | d :: _ -> Ast.Env.add "^" d env in
+     let code = Ast.to_shell_script env loc code in
+     let code = "set -e\nset -x\n\n" ^ code in
+     let r = Sys.command code in
+     if r = 99 (* means "needs rebuild" *) then true
+     else if r = 0 (* means "doesn't need rebuild" *) then false
+     else (
+       eprintf "*** tactic ‘%s’ failed with exit code %d\n" tactic r;
+       exit 1
+     )
 
 (* Find the goal which matches the given tactic and run it.
  * cargs is a list of parameters (all constants).
@@ -171,9 +200,9 @@ and run_tactic env loc tactic cargs =
      let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
      let p = Ast.PTactic (loc, tactic, targs) in
      if needs_rebuild env loc [] p then (
-       let t = Ast.ETactic (loc, tactic,
-                            List.map (fun c -> Ast.EConstant (loc, c))
-                              cargs) in
+       let t = Ast.ECallTactic (loc, tactic,
+                                List.map (fun c -> Ast.EConstant (loc, c))
+                                  cargs) in
        failwithf "%a: don't know how to build %a"
          Ast.string_loc loc Ast.string_expr t
      )
diff --git a/src/lexer.mll b/src/lexer.mll
index a9b11d1..273b09d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -51,10 +51,10 @@ rule read =
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
+    | "tactic" { TACTIC_KEYWORD }
     | "let"   { LET }
-    | "*" id  { let id = Lexing.lexeme lexbuf in
-                let len = String.length id in
-                TACTIC (String.sub id 1 (len-1)) }
+    | "*" id  { (* NB: The initial '*' is part of the name. *)
+                TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | _       { raise (SyntaxError ("unexpected character: " ^
                                     Lexing.lexeme lexbuf)) }
diff --git a/src/main.ml b/src/main.ml
index 33d91b6..7565b10 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -90,7 +90,7 @@ let main () =
   (* If no target was set on the command line, use "all ()". *)
   let targets =
     if targets <> [] then targets
-    else [Ast.ECall (Ast.noloc, "all", [])] in
+    else [Ast.ECallGoal (Ast.noloc, "all", [])] in
 
   Ast.print_env stderr env;
 
diff --git a/src/parser.mly b/src/parser.mly
index f058044..3a17124 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -36,6 +36,7 @@ open Printf
 %token RIGHT_PAREN
 %token <Ast.substs> STRING
 %token <string> TACTIC
+%token TACTIC_KEYWORD
 
 (* Start nonterminals. *)
 %start <Ast.env> file
@@ -67,6 +68,10 @@ stmt:
       let name, params = $1 in
       name, Ast.EGoal ($loc, (params, [], [], Some $2))
     }
+    | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
+    {
+      $2, Ast.ETactic ($loc, ($3, $5))
+    }
     | LET ID EQUALS expr { $2, $4 }
     ;
 
@@ -84,7 +89,7 @@ patterns:
     | separated_list(COMMA, pattern) { $1 }
     ;
 pattern:
-    | STRING     { Ast.PTactic ($loc, "file", [$1]) }
+    | STRING     { Ast.PTactic ($loc, "*file", [$1]) }
     | ID pattern_params { Ast.PTactic ($loc, $1, $2) }
     ;
 pattern_params:
@@ -95,9 +100,9 @@ pattern_param:
     ;
 
 expr:
-    | ID params  { Ast.ECall ($loc, $1, $2) }
+    | ID params  { Ast.ECallGoal ($loc, $1, $2) }
     | ID         { Ast.EVar ($loc, $1) }
-    | TACTIC params { Ast.ETactic ($loc, $1, $2) }
+    | TACTIC params { Ast.ECallTactic ($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 ec4011f..d944b94 100644
--- a/tests/test1.gl
+++ b/tests/test1.gl
@@ -7,3 +7,8 @@ goal compile (name) =
   echo %< "->" %@
   touch %@
 }
+
+tactic *file (filename) = {
+    test -f %filename || exit 99
+    # XXX older than %<
+}
\ No newline at end of file