From 7b7cd85810f18286a36215cc164b659bf7db142c Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 31 Dec 2019 09:08:35 +0000 Subject: [PATCH] =?utf8?q?Fix=20=E2=80=98goal=E2=80=99=20when=20it=20appea?= =?utf8?q?rs=20as=20a=20target=20(meaning=20=E2=80=98goal()=E2=80=99).?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- src/eval.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/eval.ml b/src/eval.ml index 66b0164..1688b5f 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -40,10 +40,20 @@ and evaluate_target env = function let args = List.map (Ast.to_constant env) args in run_tactic env loc name args - (* Look up the variable and substitute it. *) + (* If this is a goal then it's the same as calling goal(). If not + * then look up the variable and substitute it. + *) | Ast.EVar (loc, name) -> let expr = Ast.getvar env loc name in - evaluate_target env expr + (match expr with + | EGoal (loc, ([], _, _, _)) -> + evaluate_target env (Ast.ECallGoal (loc, name, [])) + | EGoal _ -> + failwithf "%a: cannot call %s() since this goal has parameters" + Ast.string_loc loc name + | _ -> + evaluate_target env expr + ) (* Lists are inlined when found as a target. *) | Ast.EList (loc, exprs) -> -- 1.8.3.1