Ast: Remove functions which were moved to Eval module.

Updates commit f36210fd16a8e4e4d6ecdd8825bf8b8307943472.

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

diff --git a/src/ast.mli b/src/ast.mli
index e47ddc3..3a528ea 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -87,22 +87,6 @@ val getgoal : env -> loc -> id -> goal
     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 _]. *)
-val to_constant : env -> expr -> constant
-
-(** Take a substitution list and try to turn it into a simple
-    string by evaluating every variable.  If not possible this
-    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 5e271a7..e299769 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -110,7 +110,7 @@ let rec evaluate_goal_arg env = function
      evaluate_goal_arg env expr
 
   | ESubsts (loc, str) ->
-     let str = Ast.substitute env loc str in
+     let str = substitute env loc str in
      Ast.EConstant (loc, Ast.CString str)
 
   | EList (loc, exprs) ->

diff --git a/src/parser.mly b/src/parser.mly
index b84ac15..8b7d8a1 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -40,7 +40,7 @@ let find_on_include_path filename =
   )
 
 let do_include env loc filename optflag file =
-  let filename = Ast.substitute env loc filename in
+  let filename = Eval.substitute env loc filename in
   let filename = find_on_include_path filename in
   if optflag && not (Sys.file_exists filename) then env
   else (

diff --git a/src/run.ml b/src/run.ml
index 0290124..2e36d1b 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -161,7 +161,7 @@ and needs_rebuild env loc deps extra_deps pattern =
       * 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 (Eval.substitute env loc) targs in
      let targs =
        List.map (fun targ ->
            Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in