Implement pure functions.

diff --git a/src/ast.ml b/src/ast.ml
index 76b0ff3..8e56fb5 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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