From 8509cad9b10205b7bec23eb59ba63e88c3d0fcb3 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 2 Jan 2020 16:11:39 +0000 Subject: [PATCH] eval: Expand goal args before running the goal. --- src/eval.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/eval.ml b/src/eval.ml index f00ce29..1b622b4 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -72,6 +72,23 @@ and run_goal env loc name args (params, patterns, deps, code) = Cmdline.debug "%a: running goal %s %a" Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args)); + (* Expand any variables in the args first. *) + let rec expand = function + | Ast.EVar (loc, name) -> + let expr = Ast.getvar env loc name in + expand expr + | Ast.ETacticConstructor (loc, name, exprs) -> + Ast.ETacticConstructor (loc, name, List.map expand exprs) + | Ast.EList (loc, exprs) -> + Ast.EList (loc, List.map expand exprs) + | Ast.EGoalDefn _ + | Ast.ETacticDefn _ + | Ast.ECallGoal _ + | Ast.ESubsts _ + | Ast.EConstant _ as e -> e + in + let args = List.map expand args in + (* Create a new environment which maps the parameter names to * the args. *) -- 1.8.3.1