From 0de7a5031184c2f0023c0aea0898a16fd4641dc5 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 27 Dec 2019 19:56:19 +0000 Subject: [PATCH] Add Ast.to_shell_script. Previously we were confusing Ast.substitute with the place where we need to shell quote. --- src/ast.ml | 39 +++++++++++++++++++++++++++++++++++++++ src/ast.mli | 6 ++++++ src/eval.ml | 3 ++- 3 files changed, 47 insertions(+), 1 deletion(-) diff --git a/src/ast.ml b/src/ast.ml index 62af833..c828bb0 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -112,6 +112,45 @@ and substitute env loc substs = ) substs; Buffer.contents b +let rec to_shell_script env loc substs = + let b = Buffer.create 13 in + List.iter ( + function + | SString s -> Buffer.add_string b s + | SVar name -> + let expr = getvar env loc name in + let s = expr_to_shell_string env expr in + Buffer.add_string b s + ) substs; + Buffer.contents b + +and expr_to_shell_string env = function + | EConstant (loc, CString s) -> Filename.quote s + + | EVar (loc, name) -> + let expr = getvar env loc name in + expr_to_shell_string env expr + + | ESubsts (loc, str) -> + Filename.quote (substitute env loc str) + + | EList (loc, exprs) -> + let strs = List.map (expr_to_shell_string env) exprs in + (* These are shell quoted so we can just concat them with space. *) + String.concat " " strs + + | ECall (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 + + | EGoal (loc, _) -> + failwithf "%a: cannot use goal in shell expansion" + string_loc loc + module Substs = struct type t = { mutable elems : subst list; (* built in reverse order *) diff --git a/src/ast.mli b/src/ast.mli index 978099e..9bb2c9a 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -90,6 +90,12 @@ val to_constant : env -> expr -> constant raises [Failure _]. *) val substitute : env -> loc -> substs -> string +(** Similar to {!substitute} except this is used where we will + pass the result immediately to the shell to execute. Variables + are substituted with shell quoted strings. Raises [Failure _] + on error. *) +val to_shell_script : env -> loc -> substs -> string + (** This is used for incrementally building Ast.substs in the parser. *) module Substs : sig type t diff --git a/src/eval.ml b/src/eval.ml index c6cbda1..f03e0e4 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -101,7 +101,8 @@ and needs_rebuild env loc name deps pattern = match pattern with | Ast.PTactic (loc, tactic, targs) -> (* Resolve the targs down to constants. *) - let targs = List.map (Ast.substitute env loc) targs in + 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 *) -- 1.8.3.1