From: Richard W.M. Jones Date: Fri, 3 Jan 2020 21:10:16 +0000 (+0000) Subject: Ast: Remove functions which were moved to Eval module. X-Git-Tag: v'0.2'~87 X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=84972c63d0dbc5a0da05ae08a5b99a9ad81baadc;p=goals.git 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 --- 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 --- 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 --- 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 --- 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 --- 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