From: Richard W.M. Jones <rjones@redhat.com>
Date: Thu, 2 Jan 2020 16:11:39 +0000 (+0000)
Subject: eval: Expand goal args before running the goal.
X-Git-Tag: v'0.2'~110
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=8509cad9b10205b7bec23eb59ba63e88c3d0fcb3;p=goals.git

eval: Expand goal args before running the goal.
---

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.
    *)