| 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
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
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
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 (
(* 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 *)
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))
(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) ->
(** 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 *)
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
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 _]. *)
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).
*)
(* 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) =
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
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).
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
)
| '"' { 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)) }
(* 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;
%token RIGHT_PAREN
%token <Ast.substs> STRING
%token <string> TACTIC
+%token TACTIC_KEYWORD
(* Start nonterminals. *)
%start <Ast.env> file
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 }
;
| 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:
;
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) }
;
echo %< "->" %@
touch %@
}
+
+tactic *file (filename) = {
+ test -f %filename || exit 99
+ # XXX older than %<
+}
\ No newline at end of file
git.annexia.org / goals.git / commitdiff