X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Feval.ml;h=daa13b66bde938c75545cb7fec9cc7c7f8f87a4b;hb=a925b902c8f87f9dfc7e39f6c31426e7527cefee;hp=b8dbe54661be8491f2ae975701aae4d7b92b36ea;hpb=c46c3a5c7793753f2f15c1655517f3f9b8fee644;p=goals.git diff --git a/src/eval.ml b/src/eval.ml index b8dbe54..daa13b6 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -27,31 +27,19 @@ and evaluate_target env = function (* Call a goal. *) | Ast.ECall (loc, name, args) -> - let expr = - try Ast.Env.find name env - with Not_found -> - failwithf "%a: goal ‘%s’ not found" Ast.string_loc loc name in - let goal = - match expr with - | Ast.EGoal (loc, goal) -> goal - | _ -> - failwithf "%a: tried to call ‘%s’ which is not a goal" - Ast.string_loc loc name in - run_goal loc env name args goal + let goal = Ast.getgoal env loc name in + run_goal env loc name args goal | Ast.ETactic (loc, name, args) -> - (* All parameters of tactics must be simple expressions (strings, - * in future booleans, numbers, etc). + (* All parameters of tactics must be simple constant expressions + * (strings, in future booleans, numbers, etc). *) - let args = List.map (simplify env) args in - run_goal_for_tactic loc env name args + let args = List.map (Ast.to_constant env) args in + run_tactic env loc name args (* Look up the variable and substitute it. *) | Ast.EVar (loc, name) -> - let expr = - try Ast.Env.find name env - with Not_found -> - failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in + let expr = Ast.getvar env loc name in evaluate_target env expr (* Lists are inlined when found as a target. *) @@ -60,146 +48,237 @@ and evaluate_target env = function (* A string (with or without substitutions) implies *file(filename). *) | Ast.ESubsts (loc, str) -> - let str = substitute loc env str in - run_goal_for_tactic loc env "file" [Ast.CString str] + let str = Ast.substitute env loc str in + run_tactic env loc "file" [Ast.CString str] | Ast.EConstant (loc, c) -> - run_goal_for_tactic loc env "file" [c] + run_tactic env loc "file" [c] -(* Find the goal which matches the given tactic and run it. - * Params is a list of constants. - *) -and run_goal_for_tactic loc env tactic const_args = - (* Search across all goals for a matching tactic. *) - let goals = - let env = Ast.Env.bindings env in - filter_map - (function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None) - env in - let name, goal = - (* If there are multiple goals matching, this must choose - * the most recently defined (XXX). - *) - try - List.find - (fun (_, (_, patterns, _, _)) -> - List.exists (matching_pattern loc env tactic const_args) patterns) - goals - with - Not_found -> - failwithf "%a: don't know how to build %s %s" - Ast.string_loc loc - tactic - (String.concat ", " - (List.map (function Ast.CString s -> s) const_args)) in - - let args = [] (* XXX calculate free variables *) in - run_goal loc env name args goal - -(* XXX This only does exact matches at the moment. *) -and matching_pattern loc env tactic const_args = function - | Ast.PTactic (loc, constructor, params) - when tactic = constructor && - List.length const_args = List.length params -> - (* Try to simplify the parameters of this pattern down - * to constants, but don't fail here if we can't do this. - *) - (try - let params = List.map (substitute loc env) params in - let params = List.map (fun s -> Ast.CString s) params in - const_args = params - with Failure _ -> false - ) - - | Ast.PTactic _ -> false - - | Ast.PVar (loc, name) -> assert false -(* - NOT IMPLEMENTED - we need variables to contain constructors! - (try - let expr = Ast.StringMap.find name env in - let expr = simplify env expr in - with Not_found -> false - ) -*) - -(* Run a named goal. *) -and run_goal loc env name args (params, patterns, deps, code) = - (* Substitute the args for the parameters in the environment. *) - 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 +(* Run a goal by name. *) +and run_goal env loc name args (params, patterns, deps, code) = + (* Create a new environment which maps the parameter names to + * the args. + *) let env = - List.fold_left (fun env (k, v) -> Ast.Env.add k v env) - env params in + 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 + List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in - (* Evaluate the dependencies first. *) + (* Check all dependencies have been updated. *) evaluate_targets env deps; - (* Check if any target needs to be updated. *) - (* XXX *) + (* Check if any target (ie. pattern) needs to be rebuilt. *) + let rebuild = List.exists (needs_rebuild env loc deps) patterns in - (* Run the code (if any). *) - (match code with - | None -> () - | Some code -> - let code = substitute loc env code in - Printf.printf "running : %s\n" code - ); + if rebuild then ( + (* Run the code (if any). *) + (match code with + | None -> () + | Some code -> + (* Add some standard variables to the environment. *) + 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.PVar (loc, name) -> + Ast.EVar (loc, name) + in + let pexprs = List.map expr_of_pattern patterns in + let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in + 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 + Printf.printf "running : %s\n" code + ); - (* Check all targets were updated (else it's an error). *) - (* XXX *) + (* Check all targets were updated (else it's an error). *) + let pattern_still_needs_rebuild = + try Some (List.find (needs_rebuild env loc deps) patterns) + with Not_found -> None in + 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 + ) + +(* Return whether the target (pattern) needs to be rebuilt. *) +and needs_rebuild env loc deps 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 + *) + assert (tactic = "file"); + assert (List.length targs = 1); + let targ = List.hd targs in + not (Sys.file_exists targ) + | Ast.PVar _ -> assert false (* XXX not implemented *) -(* Take any expression and simplify it down to a constant. - * If the expression cannot be simplified then this throws - * an error. +(* Find the goal which matches the given tactic and run it. + * cargs is a list of parameters (all constants). *) -and simplify env = function - | Ast.EConstant (loc, c) -> c +and run_tactic env loc tactic cargs = + (* 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) + | _ -> None) env in - | Ast.EVar (loc, name) -> - let expr = - try Ast.Env.find name env - with Not_found -> - failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in - simplify env expr + (* Find all patterns. Returns a list of (pattern, name, goal). *) + let patterns : (Ast.pattern * Ast.id * Ast.goal) list = + List.flatten + (List.map (fun (name, ((_, patterns, _, _) as goal)) -> + List.map (fun pattern -> (pattern, name, goal)) patterns) goals) in - | Ast.ESubsts (loc, str) -> - Ast.CString (substitute loc env str) + (* Find any patterns (ie. tactics) which match the one we + * are searching for. This returns a binding for the goal args, + * so we end up with a list of (pattern, name, goal, args). + *) + let patterns : (Ast.pattern * Ast.id * Ast.goal * Ast.expr list) list = + filter_map ( + fun (pattern, name, ((params, _, _, _) as goal)) -> + match matching_pattern env loc tactic cargs pattern params with + | None -> None + | Some args -> Some (pattern, name, goal, args) + ) patterns in + + match patterns with + | [_, name, goal, args] -> + run_goal env loc name args goal + + | [] -> + (* There's no matching goal, but we don't need one if + * the tactic doesn't need to be rebuilt. + *) + 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 + failwithf "%a: don't know how to build %a" + Ast.string_loc loc Ast.string_expr t + ) - | Ast.EList (loc, _) -> - failwithf "%a: list found where constant expression expected" - Ast.string_loc loc + | _ -> + (* If there are multiple matching goals, then assuming the goals + * are different we must pick the one which was defined last in + * the file. However we don't do that right now. XXX + *) + assert false (* TODO! *) - | Ast.ECall (loc, name, _) -> - failwithf "%a: cannot use goal ‘%s’ in constant expression" - Ast.string_loc loc name +(* Test if pattern matches *tactic(cargs). If it does + * then we return Some args where args is the arguments that must + * be passed to the matching goal. The params parameter is + * the names of the parameters of that goal. + *) +and matching_pattern env loc tactic cargs pattern params = + match pattern with + | Ast.PVar (loc, name) -> assert false (* TODO! *) + | Ast.PTactic (loc, ttactic, targs) + when tactic <> ttactic || + List.length cargs <> List.length targs -> + None (* Can't possibly match if tactic name or #args is different. *) + | Ast.PTactic (loc, ttactic, targs) -> + (* Do the args match with a possible params binding? *) + try Some (matching_params env loc params targs cargs) + with Not_found -> None - | Ast.ETactic (loc, name, _) -> - failwithf "%a: cannot use tactic ‘*%s’ in constant expression" - Ast.string_loc loc name +(* Return a possible binding. For example the goal is: + * goal compile (name) = "%name.o": "%name.c" {} + * which means that params = ["name"] and targs = ["%name.o"]. + * + * If we are called with cargs = ["file1.o"], we would + * return ["file1"]. + * + * On non-matching this raises Not_found. + *) +and matching_params env loc params targs cargs = + (* This is going to record the resulting binding. *) + let res = ref Ast.Env.empty in + List.iter2 (matching_param env loc params res) targs cargs; - | Ast.EGoal (loc, _) -> - failwithf "%a: cannot use goal in constant expression" - Ast.string_loc loc + (* Rearrange the result into goal parameter order. Also this + * checks that every parameter got a binding. + *) + let res = !res in + List.map ( + (* Allow the Not_found exception to escape if no binding for this param. *) + fun param -> Ast.Env.find param res + ) params -(* Take a substitution list and try to turn it into a simple - * string by evaluating every variable. If not possible this - * throws an error. Returns a string. +(* If targ = "%name.o" and carg = "file.o" then this would set + * name => "file" in !res. If they don't match, raises Not_found. *) -and substitute loc env substs = - let b = Buffer.create 13 in - List.iter ( - function - | Ast.SString s -> Buffer.add_string b s - | Ast.SVar name -> - let expr = - try Ast.Env.find name env - with Not_found -> - failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in - match simplify env expr with - | Ast.CString s -> Buffer.add_string b s - ) substs; - Buffer.contents b +and matching_param env loc params res targ carg = + match carg with + | Ast.CString carg -> + (* Substitute any non parameters in targ from the environment. *) + let targ = + List.map ( + function + | Ast.SString _ as s -> s + | Ast.SVar name -> + if not (List.mem name params) then ( + try + let expr = Ast.getvar env loc name in + match Ast.to_constant env expr with + | Ast.CString s -> Ast.SString s + with Failure _ -> raise Not_found + ) + else + Ast.SVar name + ) targ in + + (* Do the actual pattern matching. Any remaining SVar elements + * must refer to goal parameters. + *) + let carg = ref carg in + let rec loop = function + | [] -> + (* End of targ, we must have matched all of carg. *) + if !carg <> "" then raise Not_found + | Ast.SString s :: rest -> + (* Does this match the first part of !carg? *) + let clen = String.length !carg in + let slen = String.length s in + if slen > clen || s <> String.sub !carg 0 slen then + raise Not_found; + (* Yes, so continue after the matching prefix. *) + carg := String.sub !carg slen (clen-slen); + loop rest + | Ast.SVar name :: Ast.SString s :: rest -> + (* This is a goal parameter. Find s later in !carg. *) + let i = string_find !carg s in + if i = -1 then raise Not_found; + (* Set the binding in !res. *) + let r = Ast.EConstant (Ast.noloc, + Ast.CString (String.sub !carg 0 i)) in + res := Ast.Env.add name r !res; + (* Continue after the match. *) + let skip = i + String.length s in + carg := String.sub !carg skip (String.length !carg - skip); + loop rest + | Ast.SVar name :: [] -> + (* Matches the whole remainder of the string. *) + let r = Ast.EConstant (Ast.noloc, Ast.CString !carg) in + res := Ast.Env.add name r !res + | Ast.SVar x :: Ast.SVar y :: _ -> + (* TODO! We cannot match a target like "%x%y". *) + assert false + in + loop targ