X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=f00ce29c0a63aae7ca5b849fcea05d7ff81dbe40;hb=87e6a2f2a8d79dd10b17f3647dffb3774f0d582f;hp=af5721348dcb8ec40bb3cbacc4739bfa8c26efb1;hpb=7f776dee39a35732964a30091e55aa795169bca5;p=goals.git diff --git a/src/eval.ml b/src/eval.ml index af57213..f00ce29 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -25,24 +25,35 @@ let rec evaluate_targets env exprs = List.iter (evaluate_target env) exprs and evaluate_target env = function - | Ast.EGoal _ -> assert false + | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false (* Call a goal. *) - | Ast.ECall (loc, name, args) -> + | Ast.ECallGoal (loc, name, args) -> let goal = Ast.getgoal env loc name in run_goal env loc name args goal - | Ast.ETactic (loc, name, args) -> + (* Call a tactic. *) + | Ast.ETacticConstructor (loc, name, args) -> (* All parameters of tactics must be simple constant expressions * (strings, in future booleans, numbers, etc). *) let args = List.map (Ast.to_constant env) args in run_tactic env loc name args - (* Look up the variable and substitute it. *) + (* If this is a goal then it's the same as calling goal(). If not + * then look up the variable and substitute it. + *) | Ast.EVar (loc, name) -> let expr = Ast.getvar env loc name in - evaluate_target env expr + (match expr with + | EGoalDefn (loc, ([], _, _, _)) -> + evaluate_target env (Ast.ECallGoal (loc, name, [])) + | EGoalDefn _ -> + failwithf "%a: cannot call %s() since this goal has parameters" + Ast.string_loc loc name + | _ -> + evaluate_target env expr + ) (* Lists are inlined when found as a target. *) | Ast.EList (loc, exprs) -> @@ -51,13 +62,16 @@ and evaluate_target env = function (* A string (with or without substitutions) implies *file(filename). *) | Ast.ESubsts (loc, str) -> let str = Ast.substitute env loc str in - run_tactic env loc "file" [Ast.CString str] + run_tactic env loc "*file" [Ast.CString str] | Ast.EConstant (loc, c) -> - run_tactic env loc "file" [c] + run_tactic env loc "*file" [c] (* Run a goal by name. *) 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)); + (* Create a new environment which maps the parameter names to * the args. *) @@ -84,7 +98,7 @@ and run_goal env loc name args (params, patterns, deps, code) = let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in let expr_of_pattern = function | Ast.PTactic (loc, tactic, targs) -> - Ast.ETactic (loc, tactic, List.map expr_of_substs targs) + Ast.ETacticConstructor (loc, tactic, List.map expr_of_substs targs) in let pexprs = List.map expr_of_pattern patterns in let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in @@ -117,29 +131,62 @@ and run_goal env loc name args (params, patterns, deps, code) = (* Return whether the target (pattern) needs to be rebuilt. *) and needs_rebuild env loc deps pattern = + Cmdline.debug "%a: testing if %a needs rebuild" + Ast.string_loc loc Ast.string_pattern pattern; + match pattern with | Ast.PTactic (loc, tactic, targs) -> - (* Resolve the targs down to constants. *) - let targs = List.map ((* XXX Ast.to_shell_script *) - Ast.substitute env loc) targs in - (* XXX Look up the tactic. - * We would do that, but for now hard code the *file tactic. XXX + (* Look up the tactic. *) + let params, code = Ast.gettactic env loc tactic in + + (* Resolve the targs down to constants. Since needs_rebuild + * should be called with env containing the goal params, this + * should substitute any parameters in the tactic arguments. *) - assert (tactic = "file"); - assert (List.length targs = 1); - let targ = List.hd targs in - not (Sys.file_exists targ) + let targs = List.map (Ast.substitute env loc) targs in + let targs = + List.map (fun targ -> + Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in + + (* Create a new environment binding parameter names + * to tactic args. + *) + let env = + let params = + try List.combine params targs + with Invalid_argument _ -> + failwithf "%a: calling tactic ‘%s’ with wrong number of arguments" + Ast.string_loc loc tactic in + List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in + + (* Add some standard variables to the environment. *) + let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in + let env = + match deps with + | [] -> env + | d :: _ -> Ast.Env.add "^" d env in + let code = Ast.to_shell_script env loc code in + let code = "set -e\nset -x\n\n" ^ code in + let r = Sys.command code in + if r = 99 (* means "needs rebuild" *) then true + else if r = 0 (* means "doesn't need rebuild" *) then false + else ( + eprintf "*** tactic ‘%s’ failed with exit code %d\n" tactic r; + exit 1 + ) (* Find the goal which matches the given tactic and run it. * 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; + (* Find all goals in the environment. Returns a list of (name, goal). *) let goals = let env = Ast.Env.bindings env in filter_map (function - | name, Ast.EGoal (loc, goal) -> Some (name, goal) + | name, Ast.EGoalDefn (loc, goal) -> Some (name, goal) | _ -> None) env in (* Find all patterns. Returns a list of (pattern, name, goal). *) @@ -171,9 +218,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.ETactic (loc, tactic, - List.map (fun c -> Ast.EConstant (loc, c)) - cargs) in + let t = Ast.ETacticConstructor (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 )