From a27fa75b6854fa3f75e34817cb0bf63646d644e4 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 7 Jan 2020 08:57:58 +0000 Subject: [PATCH] Implement pure functions. --- src/ast.ml | 7 ++++--- src/ast.mli | 2 +- src/eval.ml | 28 +++++++++++++++++++++++++++- src/lexer.mll | 1 + src/parser.mly | 5 +++-- stdlib/prelude.gl | 7 ++++++- 6 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index 76b0ff3..8e56fb5 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -54,7 +54,7 @@ and expr = and constant = | CString of string and goal = param_decl list * pattern list * expr list * code option -and func = param_decl list * returning * code +and func = param_decl list * returning * bool * code and tactic = param_decl list * code and param_decl = id and id = string @@ -166,8 +166,9 @@ and string_goal () (name, (param_decls, patterns, exprs, code)) = | Some (code, false) -> " = { ... }" | Some (code, true) -> " = @{ ... }") -and string_func () (name, (param_decls, returning, (code, quiet))) = - sprintf "function%s returning %s (%s) = %s{ ... }" +and string_func () (name, (param_decls, returning, pure, (code, quiet))) = + sprintf "%sfunction%s returning %s (%s) = %s{ ... }" + (if pure then "pure " else "") (match name with None -> "" | Some name -> " " ^ name) (match returning with RetExpr -> "expression" | RetString -> "string" diff --git a/src/ast.mli b/src/ast.mli index 371c209..cf776eb 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -65,7 +65,7 @@ and expr = and constant = | CString of string and goal = param_decl list * pattern list * expr list * code option -and func = param_decl list * returning * code +and func = param_decl list * returning * bool * code and tactic = param_decl list * code and param_decl = id (** goal/func/tactic parameter. *) and id = string diff --git a/src/eval.ml b/src/eval.ml index 0d945af..6115321 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 @@ -213,7 +215,7 @@ and evaluate_goal_arg env = function * 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, 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) returning %s" name @@ -238,6 +240,10 @@ and call_function env loc name args (params, returning, code) = (List.length params) (List.length args) in List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in + 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 = let r, b = run_code env loc code in if r <> 0 then ( eprintf "*** function ‘%s’ failed with exit code %d\n" name r; @@ -259,3 +265,23 @@ and call_function env loc name args (params, returning, code) = let strs = List.rev strs in let strs = List.map (fun s -> Ast.EConstant (loc, Ast.CString s)) strs 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 diff --git a/src/lexer.mll b/src/lexer.mll index 6afa40c..2b6c4e8 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -57,6 +57,7 @@ rule read = { TACTIC_KEYWORD } | "function" { FUNCTION } + | "pure" { PURE } | "let" { LET } | "include" { INCLUDE } diff --git a/src/parser.mly b/src/parser.mly index 7f606ef..7146a99 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -74,6 +74,7 @@ let do_include env loc filename optflag file = %token LEFT_PAREN %token LET %token OPTINCLUDE +%token PURE %token RETURNING %token RIGHT_ARRAY %token RIGHT_PAREN @@ -117,9 +118,9 @@ stmt: let name, params = $1 in name, Ast.EGoalDefn ($loc, (params, [], [], Some $2)) } - | FUNCTION ID params_decl return_decl EQUALS CODE + | option(PURE) FUNCTION ID params_decl return_decl EQUALS CODE { - $2, Ast.EFuncDefn ($loc, ($3, $4, $6)) + $3, Ast.EFuncDefn ($loc, ($4, $5, $1 <> None, $7)) } | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE { diff --git a/stdlib/prelude.gl b/stdlib/prelude.gl index 240d40d..f4ab20e 100644 --- a/stdlib/prelude.gl +++ b/stdlib/prelude.gl @@ -41,7 +41,7 @@ tactic *exists (filename) = @{ # Text functions. # Sort + uniq a list. -function sort (xs) returning strings = @{ +pure function sort (xs) returning strings = @{ for f in %xs; do echo "$f"; done | sort -u } @@ -49,6 +49,11 @@ function sort (xs) returning strings = @{ # File functions. # Expand a wildcard into a list of filenames. +# +# This function is probably not "pure" since it depends on the +# current working directory and also files may be created in +# the directory while goals is running which would affect the +# result. function wildcard (wc) returning strings = @{ shopt -s nullglob # Note that the substitution is quoted by goals, so to expand -- 1.8.3.1