) 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 *)
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
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
*)