Implement functions.

[goals.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 0290124..d8cabb9 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -25,12 +25,21 @@ let rec run_targets env exprs =
   List.iter (run_target env) exprs
 
 and run_target env = function
-  | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false
+  | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false
 
-  (* Call a goal. *)
-  | Ast.ECallGoal (loc, name, args) ->
-     let goal = Ast.getgoal env loc name in
-     run_goal env loc name args goal []
+  (* Call a goal or function. *)
+  | Ast.ECall (loc, name, args) ->
+     let expr = Ast.getvar env loc name in
+     (match expr with
+      | Ast.EGoalDefn (_, goal) ->
+         run_goal env loc name args goal []
+      | Ast.EFuncDefn (_, func) ->
+         let expr = Eval.call_function env loc name args func in
+         run_target env expr
+      | _ ->
+         failwithf "%a: tried to call ‘%s’ which is not a goal or a function"
+           Ast.string_loc loc name
+     )
 
   (* Call a tactic. *)
   | Ast.ETacticCtor (loc, name, args) ->
@@ -46,8 +55,8 @@ and run_target env = function
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      (match expr with
-      | EGoalDefn (loc, ([], _, _, _)) ->
-         run_target env (Ast.ECallGoal (loc, name, []))
+      | Ast.EGoalDefn (loc, ([], _, _, _)) ->
+         run_target env (Ast.ECall (loc, name, []))
       | EGoalDefn _ ->
          failwithf "%a: cannot call %s() since this goal has parameters"
            Ast.string_loc loc name
@@ -161,7 +170,7 @@ and needs_rebuild env loc deps extra_deps pattern =
       * should be called with env containing the goal params, this
       * should substitute any parameters in the tactic arguments.
       *)
-     let targs = List.map (Ast.substitute env loc) targs in
+     let targs = List.map (Eval.substitute env loc) targs in
      let targs =
        List.map (fun targ ->
            Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in