From 2d5b3813df7f7db3abf3bcbfe2c6a657f463c5ee Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 3 Jan 2020 11:35:56 +0000 Subject: [PATCH] Simplify Constructor -> Ctor. --- src/ast.ml | 10 +++++----- src/ast.mli | 2 +- src/eval.ml | 10 +++++----- src/parser.mly | 2 +- src/run.ml | 6 +++--- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index c3e530e..c3b3969 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 - | ETacticConstructor of loc * id * expr list + | ETacticCtor 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 - | ETacticConstructor (loc, name, _) -> + | ETacticCtor (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. *) - | ETacticConstructor (loc, _, []) -> Filename.quote "" - | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg + | ETacticCtor (loc, _, []) -> Filename.quote "" + | ETacticCtor (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)) - | ETacticConstructor (loc, name, params) -> + | ETacticCtor (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 406a829..e47ddc3 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. *) - | ETacticConstructor of loc * id * expr list + | ETacticCtor 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 8657b2c..5e271a7 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -37,7 +37,7 @@ let rec to_constant env = function failwithf "%a: cannot use goal ‘%s’ in constant expression" Ast.string_loc loc name - | ETacticConstructor (loc, name, _) -> + | ETacticCtor (loc, name, _) -> failwithf "%a: cannot use tactic ‘%s’ in constant expression" Ast.string_loc loc name @@ -93,8 +93,8 @@ and expr_to_shell_string env = function Ast.string_loc loc name (* Tactics expand to the first parameter. *) - | ETacticConstructor (loc, _, []) -> Filename.quote "" - | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg + | ETacticCtor (loc, _, []) -> Filename.quote "" + | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg | EGoalDefn (loc, _) -> failwithf "%a: cannot use goal in shell expansion" @@ -116,8 +116,8 @@ let rec evaluate_goal_arg env = function | EList (loc, exprs) -> Ast.EList (loc, List.map (evaluate_goal_arg env) exprs) - | ETacticConstructor (loc, name, exprs) -> - Ast.ETacticConstructor (loc, name, List.map (evaluate_goal_arg env) exprs) + | ETacticCtor (loc, name, exprs) -> + Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs) | ECallGoal (loc, name, _) -> (* Goals don't return anything so they cannot be used in diff --git a/src/parser.mly b/src/parser.mly index 347c072..db70924 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.ETacticConstructor ($loc, $1, $2) } + | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) } | STRING { Ast.ESubsts ($loc, $1) } | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) } ; diff --git a/src/run.ml b/src/run.ml index a0bb592..7d48a7e 100644 --- a/src/run.ml +++ b/src/run.ml @@ -33,7 +33,7 @@ and run_target env = function run_goal env loc name args goal (* Call a tactic. *) - | Ast.ETacticConstructor (loc, name, args) -> + | Ast.ETacticCtor (loc, name, args) -> (* All parameters of tactics must be simple constant expressions * (strings, in future booleans, numbers, etc). *) @@ -108,7 +108,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.ETacticConstructor (loc, tactic, List.map expr_of_substs targs) + Ast.ETacticCtor (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 @@ -227,7 +227,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.ETacticConstructor (loc, tactic, + let t = Ast.ETacticCtor (loc, tactic, List.map (fun c -> Ast.EConstant (loc, c)) cargs) in failwithf "%a: don't know how to build %a" -- 1.8.3.1