X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=4589a40725b35541c3d0171f425e13d2297d608a;hb=881b2e9b7bad0da8f44418e9e6558710db5ce690;hp=f03e0e4faa568968f75b2e2d2d64bc5eb072d8d9;hpb=0de7a5031184c2f0023c0aea0898a16fd4641dc5;p=goals.git diff --git a/src/eval.ml b/src/eval.ml index f03e0e4..4589a40 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,240 @@ * 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 pure_cache = Hashtbl.create 13 + +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) + + | EList (loc, _) -> + failwithf "%a: list found where constant expression expected" + Ast.string_loc loc + + | 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 + + | ESubsts (loc, str) -> + Filename.quote (substitute env loc str) + + | 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) -and evaluate_target env = function - | Ast.EGoal _ -> assert false + | _ -> + failwithf "%a: cannot call ‘%s’ which is not a function" + Ast.string_loc loc name + ) - (* Call a goal. *) - | Ast.ECall (loc, name, args) -> - let goal = Ast.getgoal env loc name in - run_goal env loc name args goal + (* Tactics expand to the first parameter. *) + | ETacticCtor (loc, _, []) -> Filename.quote "" + | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg - | 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 + | EGoalDefn (loc, _) -> + failwithf "%a: cannot use goal in shell expansion" + Ast.string_loc loc - (* Look up the variable and substitute it. *) + | 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 run_code env loc code = + let code = prepare_code env loc code in + Sys.command code + +and run_code_to_string env loc code = + let code = prepare_code env loc 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 + let i = + match st with + | Unix.WEXITED i -> i + | Unix.WSIGNALED i -> + failwithf "%a: killed by signal %d" Ast.string_loc loc i + | Unix.WSTOPPED i -> + failwithf "%a: stopped by signal %d" Ast.string_loc loc i in + i, Buffer.contents b + +and run_code_to_string_list env loc code = + let code = prepare_code env loc code in + let chan = Unix.open_process_in code in + let lines = ref [] in + (try while true do lines := input_line chan :: !lines done + with End_of_file -> ()); + let st = Unix.close_process_in chan in + let i = + match st with + | Unix.WEXITED i -> i + | Unix.WSIGNALED i -> + failwithf "%a: killed by signal %d" Ast.string_loc loc i + | Unix.WSTOPPED i -> + failwithf "%a: stopped by signal %d" Ast.string_loc loc i in + let lines = List.rev !lines in + i, lines + +and prepare_code env loc (code, quiet) = + let quiet = if Cmdline.debug_flag then false else quiet in + let code = to_shell_script env loc code in + "source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^ + "set -e\n" ^ + (if not quiet then "set -x\n" else "") ^ + "\n" ^ + code + +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) + + | EList (loc, exprs) -> + Ast.EList (loc, List.map (evaluate_goal_arg env) exprs) + + | ETacticCtor (loc, name, exprs) -> + Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs) + + | 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 - (* Lists are inlined when found as a target. *) - | Ast.EList (loc, exprs) -> - evaluate_targets env exprs + | _ -> + failwithf "%a: cannot call ‘%s’ which is not a function" + Ast.string_loc loc name + ) - (* 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] + | EConstant _ + | EGoalDefn _ + | EFuncDefn _ + | ETacticDefn _ as e -> e - | Ast.EConstant (loc, c) -> - run_tactic env loc "file" [c] +(* 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, string or list of strings. + *) +and call_function env loc name args (params, returning, pure, code) = + (* This is used to print the function in debug and error messages only. *) + let debug_func = + sprintf "%s (%s) returning %s" name + (String.concat ", " (List.map (Ast.string_expr ()) args)) + (match returning with RetExpr -> "expression" + | RetString -> "string" + | RetStrings -> "strings") 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,201 +258,53 @@ 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 -> - let code = Ast.substitute 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; + if pure then call_function_pure env loc name returning code + else call_function_really env loc name returning code - (* 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 call_function_really env loc name returning code = + match returning with + | RetExpr -> + let r, b = run_code_to_string env loc code in + if r <> 0 then ( + eprintf "*** function ‘%s’ failed with exit code %d\n" name r; + exit 1 + ); + Parse.parse_expr (sprintf "function:%s" name) b + + | RetString -> + let r, b = run_code_to_string env loc code in + if r <> 0 then ( + eprintf "*** function ‘%s’ failed with exit code %d\n" name r; + exit 1 + ); + Ast.EConstant (loc, Ast.CString b) + + | RetStrings -> + let r, lines = run_code_to_string_list env loc code in + let strs = List.map (fun s -> Ast.EConstant (loc, Ast.CString s)) lines in + EList (loc, strs) + +(* For pure functions, check if the function can be matched to + * a previously memoized result, but don't fail if this goes wrong. *) -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 +and call_function_pure env loc name returning code = + let code_key = + try Some (to_shell_script env loc (fst code)) + with Failure _ -> None in + match code_key with + | None -> call_function_really env loc name returning code + | Some code_key -> + let r = + try Some (Hashtbl.find pure_cache code_key) + with Not_found -> None in + match r with + | Some expr -> expr + | None -> + let expr = call_function_really env loc name returning code in + Hashtbl.add pure_cache code_key expr; + expr