X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Frun.ml;h=0d4fa88a4f703dd9386d22995e4d30d469c463f0;hb=881b2e9b7bad0da8f44418e9e6558710db5ce690;hp=cc9af440c32859d40e6b4cd4ee7516cf4a5f6914;hpb=744ed04530d16567403eccdaf55e479834dbbc0e;p=goals.git diff --git a/src/run.ml b/src/run.ml index cc9af44..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 @@ -69,8 +78,11 @@ and run_target env = function (* Run a goal by name. *) and run_goal env loc name args (params, patterns, deps, code) extra_deps = - Cmdline.debug "%a: running goal %s %a" - Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args)); + (* This is used to print the goal in debug and error messages only. *) + let debug_goal = + sprintf "%s (%s)" name + (String.concat ", " (List.map (Ast.string_expr ()) args)) in + Cmdline.debug "%a: running goal %s" Ast.string_loc loc debug_goal; (* This is the point where we evaluate the goal arguments. We must * do this before creating the new environment, because variables @@ -85,8 +97,9 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps = let params = try List.combine params args with Invalid_argument _ -> - failwithf "%a: calling goal ‘%s’ with wrong number of arguments" - Ast.string_loc loc name in + failwithf "%a: calling goal %s with wrong number of arguments, expecting %d args but got %d args" + Ast.string_loc loc debug_goal + (List.length params) (List.length args) in List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in (* Check all dependencies have been updated. *) @@ -119,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 @@ -138,10 +149,8 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps = match pattern_still_needs_rebuild with | None -> () | Some pattern -> - failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a" - Ast.string_loc loc - name - Ast.string_pattern pattern + failwithf "%a: goal %s ran successfully but it did not rebuild %a" + Ast.string_loc loc debug_goal Ast.string_pattern pattern ) ) @@ -159,7 +168,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 @@ -182,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 ( @@ -196,7 +203,12 @@ and needs_rebuild env loc deps extra_deps pattern = * cargs is a list of parameters (all constants). *) and run_tactic env loc tactic cargs = - Cmdline.debug "%a: running tactic %s" Ast.string_loc loc tactic; + (* This is used to print the tactic in debug and error messages only. *) + let debug_tactic = + Ast.string_expr () + (Ast.ETacticCtor (loc, tactic, + List.map (fun c -> Ast.EConstant (loc, c)) cargs)) in + Cmdline.debug "%a: running tactic %s" Ast.string_loc loc debug_tactic; (* Find all goals in the environment. Returns a list of (name, goal). *) let goals = @@ -231,13 +243,9 @@ and run_tactic env loc tactic cargs = *) let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in let p = Ast.PTactic (loc, tactic, targs) in - if needs_rebuild env loc [] [] p then ( - let t = Ast.ETacticCtor (loc, tactic, - List.map (fun c -> Ast.EConstant (loc, c)) - cargs) in - failwithf "%a: don't know how to build %a" - Ast.string_loc loc Ast.string_expr t - ) + if needs_rebuild env loc [] [] p then + failwithf "%a: don't know how to build %s" + Ast.string_loc loc debug_tactic | [_, name, goal, args] -> (* Single goal matches, run it. *) @@ -275,8 +283,8 @@ and run_tactic env loc tactic cargs = (g, extra_deps) | _ :: _ -> - failwithf "%a: multiple goals with {code} sections match tactic %s" - Ast.string_loc loc tactic in + failwithf "%a: multiple goals found which match tactic %s, but more than one of these goals have {code} sections which is not allowed" + Ast.string_loc loc debug_tactic in run_goal env loc name args goal extra_deps