X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=59f4ca4dc87b4b8f299c14b1e9a2add29b04f4da;hb=109185686ffdc00520eba2b4c3a92f10a111fb60;hp=a0ed8345a9809936f4be5b3c57aa62f022b92004;hpb=976bb1b35d77f3058df3c25c1e2a4767147d606b;p=goals.git diff --git a/src/eval.ml b/src/eval.ml index a0ed834..59f4ca4 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -21,6 +21,8 @@ open Printf open Utils +let pure_cache = Hashtbl.create 13 + let rec to_constant env = function | Ast.EConstant (loc, c) -> c @@ -142,6 +144,56 @@ and expr_to_shell_string env = function 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 @@ -183,16 +235,17 @@ and evaluate_goal_arg env = function (* 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 substituting - * the output into an EList. - * - * XXX In future allow functions to be annotated with a return type. + * 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, code) = +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)" name - (String.concat ", " (List.map (Ast.string_expr ()) args)) in + 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. *) @@ -210,27 +263,44 @@ and call_function env loc name args (params, code) = (List.length params) (List.length args) in List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in - (* 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 lines = ref [] in - (try while true do lines := input_line chan :: !lines done - with End_of_file -> ()); - let lines = List.rev !lines in - 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 - ); - - Ast.EList (Ast.noloc, - (List.map (fun line -> - Ast.EConstant (Ast.noloc, Ast.CString line)) - lines)) + if pure then call_function_pure env loc name returning code + else call_function_really env loc name returning code + +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 + failwithf "function ‘%s’ failed with exit code %d" name r; + Parse.parse_expr (sprintf "function:%s" name) b + + | RetString -> + let r, b = run_code_to_string env loc code in + if r <> 0 then + failwithf "function ‘%s’ failed with exit code %d" name r; + 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 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