X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Frun.ml;h=0d4fa88a4f703dd9386d22995e4d30d469c463f0;hb=d513d8b6aa8c70191deb3e1a8392819c9181a8f9;hp=2e36d1b7a4120a48fb884494efeb77df6cc2f220;hpb=84972c63d0dbc5a0da05ae08a5b99a9ad81baadc;p=goals.git

diff --git a/src/run.ml b/src/run.ml
index 2e36d1b..0d4fa88 100644
--- 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
@@ -123,9 +132,7 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps =
           match deps with
           | [] -> env
           | d :: _ -> Ast.Env.add "^" d env in
-        let code = Eval.to_shell_script env loc code in
-        let code = "set -e\nset -x\n\n" ^ code in
-        let r = Sys.command code in
+        let r = Eval.run_code env loc code in
         if r <> 0 then (
           eprintf "*** goal ‘%s’ failed with exit code %d\n" name r;
           exit 1
@@ -184,9 +191,7 @@ and needs_rebuild env loc deps extra_deps pattern =
        match deps with
        | [] -> env
        | d :: _ -> Ast.Env.add "^" d env in
-     let code = Eval.to_shell_script env loc code in
-     let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in
-     let r = Sys.command code in
+     let r = Eval.run_code env loc code in
      if r = 99 (* means "needs rebuild" *) then true
      else if r = 0 (* means "doesn't need rebuild" *) then false
      else (