X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=c2d655103bf14648c1f8fe723c45c3f4732371f7;hb=2ac1b84cb49ad04e27b4543436b0227153fbfb15;hp=74873e5c233d5fd50da4674ac74e287568b2955e;hpb=8d9aa27f1bf7a0a99a66924ba10fd24a0d691163;p=goals.git diff --git a/src/eval.ml b/src/eval.ml index 74873e5..c2d6551 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -1,4 +1,4 @@ -(* Goalfile evaluation +(* Goalfile Abstract Syntax Tree * Copyright (C) 2019 Richard W.M. Jones * Copyright (C) 2019 Red Hat Inc. * @@ -17,45 +17,185 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) +open Printf + open Utils -let rec evaluate_targets env exprs = - List.iter (evaluate_target env) exprs +let rec to_constant env = function + | Ast.EConstant (loc, c) -> c + + | EVar (loc, name) -> + let expr = Ast.getvar env loc name in + to_constant env expr + + | ESubsts (loc, str) -> + CString (substitute env loc str) -and evaluate_target env = function - | Ast.EGoal _ -> assert false + | EList (loc, _) -> + failwithf "%a: list found where constant expression expected" + Ast.string_loc loc - (* Call a goal. *) - | Ast.ECall (loc, name, args) -> - let goal = Ast.getgoal env loc name in - run_goal env loc name args goal + | ECall (loc, name, args) -> + let expr = Ast.getvar env loc name in + (match expr with + | EGoalDefn _ -> + (* Goals don't return anything so they cannot be used in + * constant expressions. Use a function instead. + *) + failwithf "%a: cannot use goal call ‘%s’ in shell expansion" + Ast.string_loc loc name + + | EFuncDefn (loc, func) -> + to_constant env (call_function env loc name args func) + + | _ -> + failwithf "%a: cannot use ‘%s’ in constant expression" + Ast.string_loc loc name + ) + + | ETacticCtor (loc, name, _) -> + failwithf "%a: cannot use tactic ‘%s’ in constant expression" + Ast.string_loc loc name + + | EGoalDefn (loc, _) -> + failwithf "%a: cannot use goal in constant expression" + Ast.string_loc loc + + | EFuncDefn (loc, _) -> + failwithf "%a: cannot use function in constant expression" + Ast.string_loc loc + + | ETacticDefn (loc, _) -> + failwithf "%a: cannot use tactic in constant expression" + Ast.string_loc loc + +and substitute env loc substs = + let b = Buffer.create 13 in + List.iter ( + function + | Ast.SString s -> Buffer.add_string b s + | SVar name -> + let expr = Ast.getvar env loc name in + match to_constant env expr with + | Ast.CString s -> Buffer.add_string b s + ) substs; + Buffer.contents b + +and to_shell_script env loc substs = + let b = Buffer.create 13 in + List.iter ( + function + | Ast.SString s -> Buffer.add_string b s + | SVar name -> + let expr = Ast.getvar env loc name in + let s = expr_to_shell_string env expr in + Buffer.add_string b s + ) substs; + Buffer.contents b + +and expr_to_shell_string env = function + | Ast.EConstant (loc, CString s) -> Filename.quote s + + | EVar (loc, name) -> + let expr = Ast.getvar env loc name in + expr_to_shell_string env expr - | Ast.ETactic (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 + | ESubsts (loc, str) -> + Filename.quote (substitute env loc str) - (* Look up the variable and substitute it. *) + | EList (loc, exprs) -> + let strs = List.map (expr_to_shell_string env) exprs in + (* These are shell quoted so we can just concat them with space. *) + String.concat " " strs + + | ECall (loc, name, args) -> + let expr = Ast.getvar env loc name in + (match expr with + | EGoalDefn _ -> + (* Goals don't return anything so they cannot be used in + * shell script expansions. Use a function instead. + *) + failwithf "%a: cannot use goal call ‘%s’ in shell expansion" + Ast.string_loc loc name + + | EFuncDefn (loc, func) -> + expr_to_shell_string env (call_function env loc name args func) + + | _ -> + failwithf "%a: cannot call ‘%s’ which is not a function" + Ast.string_loc loc name + ) + + (* Tactics expand to the first parameter. *) + | ETacticCtor (loc, _, []) -> Filename.quote "" + | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg + + | EGoalDefn (loc, _) -> + failwithf "%a: cannot use goal in shell expansion" + Ast.string_loc loc + + | EFuncDefn (loc, _) -> + failwithf "%a: cannot use function in shell expansion" + Ast.string_loc loc + + | ETacticDefn (loc, _) -> + failwithf "%a: cannot use tactic in shell expansion" + Ast.string_loc loc + +and evaluate_goal_arg env = function | Ast.EVar (loc, name) -> let expr = Ast.getvar env loc name in - evaluate_target env expr + evaluate_goal_arg env expr + + | ESubsts (loc, str) -> + let str = substitute env loc str in + Ast.EConstant (loc, Ast.CString str) - (* Lists are inlined when found as a target. *) - | Ast.EList (loc, exprs) -> - evaluate_targets env exprs + | EList (loc, exprs) -> + Ast.EList (loc, List.map (evaluate_goal_arg env) exprs) - (* 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] + | ETacticCtor (loc, name, exprs) -> + Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs) - | Ast.EConstant (loc, c) -> - run_tactic env loc "file" [c] + | ECall (loc, name, args) -> + let expr = Ast.getvar env loc name in + (match expr with + | EGoalDefn _ -> + (* Goals don't return anything so they cannot be used in + * goal args. Use a function instead. + *) + failwithf "%a: cannot use goal call ‘%s’ in goal argument" + Ast.string_loc loc name + + | EFuncDefn (loc, func) -> + call_function env loc name args func + + | _ -> + failwithf "%a: cannot call ‘%s’ which is not a function" + Ast.string_loc loc name + ) + + | EConstant _ + | EGoalDefn _ + | EFuncDefn _ + | ETacticDefn _ as e -> e + +(* Functions are only called from goal args or when substituting + * into a shell script or constant expression (this may change if we + * implement ‘:=’ assignment for variables). This evaluates a + * function by running the associated shell script and parsing + * the output as an expression. + *) +and call_function env loc name args (params, code) = + (* This is used to print the function in debug and error messages only. *) + let debug_func = + sprintf "%s (%s)" name + (String.concat ", " (List.map (Ast.string_expr ()) args)) in + Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func; + + (* Evaluate function args. Must be done before updating the environment. *) + let args = List.map (evaluate_goal_arg env) args 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. *) @@ -63,216 +203,32 @@ and run_goal env loc name args (params, patterns, deps, code) = 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 function %s with wrong number of arguments, expecting %d args but got %d args" + Ast.string_loc loc debug_func + (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. *) - evaluate_targets env deps; - - (* Check if any target (ie. pattern) needs to be rebuilt. *) - let rebuild = - List.exists (needs_rebuild env loc name deps) patterns in - - 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). *) - let pattern_still_needs_rebuild = - try Some (List.find (needs_rebuild env loc name 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 name 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 *) - -(* 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 = - (* 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 - - (* 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 - - (* 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 - - let _, name, goal, args = - match patterns with - | [p] -> p - | [] -> - 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 - | _ -> - (* 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! *) in - - run_goal env loc name args goal - -(* 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 - -(* 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; - - (* 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 - -(* 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 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 + (* Run the code. *) + let code = to_shell_script env loc code in + let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in + + let chan = Unix.open_process_in code in + let b = Buffer.create 1024 in + (try + while true do + Buffer.add_string b (input_line chan); + Buffer.add_char b '\n' + done + with End_of_file -> ()); + let st = Unix.close_process_in chan in + (match st with + | Unix.WEXITED 0 -> () + | Unix.WEXITED i -> + eprintf "*** function ‘%s’ failed with exit code %d\n" name i + | Unix.WSIGNALED i -> + eprintf "*** function ‘%s’ killed by signal %d\n" name i + | Unix.WSTOPPED i -> + eprintf "*** function ‘%s’ stopped by signal %d\n" name i + ); + + Parse.parse_expr (sprintf "function:%s" name) (Buffer.contents b)