-let rec to_constant env = function
- | EConstant (loc, c) -> c
-
- | EVar (loc, name) ->
- let expr = getvar env loc name in
- to_constant env expr
-
- | ESubsts (loc, str) ->
- CString (substitute env loc str)
-
- | EList (loc, _) ->
- failwithf "%a: list found where constant expression expected"
- string_loc loc
-
- | ECallGoal (loc, name, _) ->
- failwithf "%a: cannot use goal ‘%s’ in constant expression"
- string_loc loc name
-
- | ETacticCtor (loc, name, _) ->
- failwithf "%a: cannot use tactic ‘%s’ in constant expression"
- string_loc loc name
-
- | EGoalDefn (loc, _) ->
- failwithf "%a: cannot use goal in constant expression"
- string_loc loc
-
- | ETacticDefn (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 (
- function
- | SString s -> Buffer.add_string b s
- | SVar name ->
- let expr = getvar env loc name in
- match to_constant env expr with
- | CString s -> Buffer.add_string b s
- ) 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
-
- | ECallGoal (loc, name, _) ->
- failwithf "%a: cannot use goal ‘%s’ in shell expansion"
- string_loc loc name
-
- (* Tactics expand to the first parameter. *)
- | ETacticCtor (loc, _, []) -> Filename.quote ""
- | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
-
- | EGoalDefn (loc, _) ->
- failwithf "%a: cannot use goal in shell expansion"
- string_loc loc
-
- | ETacticDefn (loc, _) ->
- failwithf "%a: cannot use tactic in shell expansion"
- string_loc loc
-