From 87e6a2f2a8d79dd10b17f3647dffb3774f0d582f Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 2 Jan 2020 15:59:48 +0000 Subject: [PATCH] Ast: Rename ECallTactic to ETacticConstructor. This is a constructor, it's not 'calling' anything. --- src/ast.ml | 10 +++++----- src/ast.mli | 2 +- src/eval.ml | 6 +++--- src/parser.mly | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index 1f67413..c3e530e 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -45,7 +45,7 @@ and expr = | EGoalDefn of loc * goal | ETacticDefn of loc * tactic | ECallGoal of loc * id * expr list - | ECallTactic of loc * id * expr list + | ETacticConstructor of loc * id * expr list | EVar of loc * id | EList of loc * expr list | ESubsts of loc * substs @@ -112,7 +112,7 @@ let rec to_constant env = function failwithf "%a: cannot use goal ‘%s’ in constant expression" string_loc loc name - | ECallTactic (loc, name, _) -> + | ETacticConstructor (loc, name, _) -> failwithf "%a: cannot use tactic ‘%s’ in constant expression" string_loc loc name @@ -168,8 +168,8 @@ and expr_to_shell_string env = function string_loc loc name (* Tactics expand to the first parameter. *) - | ECallTactic (loc, _, []) -> Filename.quote "" - | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg + | ETacticConstructor (loc, _, []) -> Filename.quote "" + | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg | EGoalDefn (loc, _) -> failwithf "%a: cannot use goal in shell expansion" @@ -252,7 +252,7 @@ and string_expr () = function | ECallGoal (loc, name, params) -> sprintf "%s (%s)" name (String.concat ", " (List.map (string_expr ()) params)) - | ECallTactic (loc, name, params) -> + | ETacticConstructor (loc, name, params) -> sprintf "%s (%s)" name (String.concat ", " (List.map (string_expr ()) params)) | EVar (loc, var) -> var diff --git a/src/ast.mli b/src/ast.mli index 1fee78e..b42294c 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -51,7 +51,7 @@ and expr = (** call goalname (params) etc. *) | ECallGoal of loc * id * expr list (** call *tactic (params) etc. *) - | ECallTactic of loc * id * expr list + | ETacticConstructor of loc * id * expr list (** variable, or goal call with no parameters *) | EVar of loc * id (** list *) diff --git a/src/eval.ml b/src/eval.ml index 770acf1..f00ce29 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -33,7 +33,7 @@ and evaluate_target env = function run_goal env loc name args goal (* Call a tactic. *) - | Ast.ECallTactic (loc, name, args) -> + | Ast.ETacticConstructor (loc, name, args) -> (* All parameters of tactics must be simple constant expressions * (strings, in future booleans, numbers, etc). *) @@ -98,7 +98,7 @@ and run_goal env loc name args (params, patterns, deps, code) = let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in let expr_of_pattern = function | Ast.PTactic (loc, tactic, targs) -> - Ast.ECallTactic (loc, tactic, List.map expr_of_substs targs) + Ast.ETacticConstructor (loc, tactic, List.map expr_of_substs targs) in let pexprs = List.map expr_of_pattern patterns in let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in @@ -218,7 +218,7 @@ and run_tactic env loc tactic cargs = let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in let p = Ast.PTactic (loc, tactic, targs) in if needs_rebuild env loc [] p then ( - let t = Ast.ECallTactic (loc, tactic, + let t = Ast.ETacticConstructor (loc, tactic, List.map (fun c -> Ast.EConstant (loc, c)) cargs) in failwithf "%a: don't know how to build %a" diff --git a/src/parser.mly b/src/parser.mly index 6cb48f7..347c072 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -140,7 +140,7 @@ pattern_param: expr: | ID params { Ast.ECallGoal ($loc, $1, $2) } | ID { Ast.EVar ($loc, $1) } - | TACTIC params { Ast.ECallTactic ($loc, $1, $2) } + | TACTIC params { Ast.ETacticConstructor ($loc, $1, $2) } | STRING { Ast.ESubsts ($loc, $1) } | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) } ; -- 1.8.3.1