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