From 214f84c3b07227767fef90934895a167b15113a1 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sat, 28 Dec 2019 16:28:41 +0000 Subject: [PATCH] Implement tactics. --- src/ast.ml | 55 ++++++++++++++++++++++++++++++++++++++----------- src/ast.mli | 19 +++++++++++------ src/eval.ml | 65 ++++++++++++++++++++++++++++++++++++++++++---------------- src/lexer.mll | 6 +++--- src/main.ml | 2 +- src/parser.mly | 11 +++++++--- tests/test1.gl | 5 +++++ 7 files changed, 120 insertions(+), 43 deletions(-) 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 STRING %token TACTIC +%token TACTIC_KEYWORD (* Start nonterminals. *) %start 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 -- 1.8.3.1