Ast: Remove functions which were moved to Eval module.

[goals.git] / src / ast.ml

diff --git a/src/ast.ml b/src/ast.ml
index c3b3969..b4f86e7 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -94,91 +94,6 @@ let gettactic env loc name =
          string_loc loc name in
   tactic
 
-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
-
 module Substs = struct
   type t = {
       mutable elems : subst list; (* built in reverse order *)