Implement functions.

diff --git a/TODO b/TODO
index 0c67dcd..5db7e8d 100644 (file)
--- a/TODO
+++ b/TODO
@@ -6,7 +6,8 @@ Default parameters, ie:
 You might only allow defaults to be added to the end, or you
 might allow goals to be called with labelled parameters.
 
 You might only allow defaults to be added to the end, or you
 might allow goals to be called with labelled parameters.
 

-Functions, eg. wildcard("*.c").  These should be defined as shell
-scripts with a selection of common functions defined in stdlib.
-

 Fix: You must use 'all ()' on the command line.
 Fix: You must use 'all ()' on the command line.

+
+"Quiet" code.  Generally {CODE} sections in user files should be
+echos, and those in stdlib should run silently (except if debugging).
+Maybe we should have a quiet keyword to indicate this?

diff --git a/src/ast.ml b/src/ast.ml
index b4f86e7..922827c 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -43,8 +43,9 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   | EGoalDefn of loc * goal
   | PTactic of loc * id * substs list
 and expr =
   | EGoalDefn of loc * goal

+  | EFuncDefn of loc * func

   | ETacticDefn of loc * tactic
   | ETacticDefn of loc * tactic

-  | ECallGoal of loc * id * expr list
+  | ECall of loc * id * expr list

   | ETacticCtor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ETacticCtor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list


@@ -53,6 +54,7 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option

+and func = param_decl list * code

 and tactic = param_decl list * code
 and param_decl = id
 and id = string
 and tactic = param_decl list * code
 and param_decl = id
 and id = string


@@ -80,6 +82,19 @@ let getgoal env loc name =
          string_loc loc name in
   goal
 
          string_loc loc name in
   goal
 

+let getfunc env loc name =
+  let expr =
+    try Env.find name env
+    with Not_found ->
+      failwithf "%a: func ‘%s’ not found" string_loc loc name in
+  let func =
+    match expr with
+    | EFuncDefn (loc, func) -> func
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a function"
+         string_loc loc name in
+  func
+

 let gettactic env loc name =
   assert (name.[0] = '*');
   let expr =
 let gettactic env loc name =
   assert (name.[0] = '*');
   let expr =


@@ -134,6 +149,7 @@ and print_env fp env = output_string fp (string_env () env)
 and string_def () (name, expr) =
   match expr with
   | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
 and string_def () (name, expr) =
   match expr with
   | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"

+  | EFuncDefn (loc, func) -> string_func () (Some name, func) ^ "\n"

   | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
   | expr -> sprintf "let %s = %a\n" name string_expr expr;
 
   | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
   | expr -> sprintf "let %s = %a\n" name string_expr expr;
 


@@ -147,6 +163,11 @@ and string_goal () (name, (param_decls, patterns, exprs, code)) =
     (String.concat ", " (List.map (string_expr ()) exprs))
     (match code with None -> "" | Some code -> " = { ... }")
 
     (String.concat ", " (List.map (string_expr ()) exprs))
     (match code with None -> "" | Some code -> " = { ... }")
 

+and string_func () (name, (param_decls, code)) =
+  sprintf "function%s (%s) = { ... }"
+    (match name with None -> "" | Some name -> " " ^ name)
+    (String.concat ", " (List.map (string_param_decl ()) param_decls))
+

 and string_tactic () (name, (param_decls, code)) =
   sprintf "tactic%s (%s) = { ... }"
     (match name with None -> "" | Some name -> " " ^ name)
 and string_tactic () (name, (param_decls, code)) =
   sprintf "tactic%s (%s) = { ... }"
     (match name with None -> "" | Some name -> " " ^ name)


@@ -163,8 +184,9 @@ and print_pattern fp p = output_string fp (string_pattern () p)
 
 and string_expr () = function
   | EGoalDefn (loc, goal) -> string_goal () (None, goal)
 
 and string_expr () = function
   | EGoalDefn (loc, goal) -> string_goal () (None, goal)

+  | EFuncDefn (loc, func) -> string_func () (None, func)

   | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
   | ETacticDefn (loc, goal) -> string_tactic () (None, goal)

-  | ECallGoal (loc, name, params) ->
+  | ECall (loc, name, params) ->

      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | ETacticCtor (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | ETacticCtor (loc, name, params) ->

diff --git a/src/ast.mli b/src/ast.mli
index 3a528ea..f8b88f0 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -46,10 +46,12 @@ and pattern =
 and expr =
   (** goal (params) = patterns : exprs code *)
   | EGoalDefn of loc * goal
 and expr =
   (** goal (params) = patterns : exprs code *)
   | EGoalDefn of loc * goal

+  (** function (params) = code *)
+  | EFuncDefn of loc * func

   (** tactic (params) = code *)
   | ETacticDefn of loc * tactic
   (** tactic (params) = code *)
   | ETacticDefn of loc * tactic

-  (** call goalname (params) etc. *)
-  | ECallGoal of loc * id * expr list
+  (** call goal (params) or function (params) *)
+  | ECall of loc * id * expr list

   (** call *tactic (params) etc. *)
   | ETacticCtor of loc * id * expr list
   (** variable, or goal call with no parameters *)
   (** call *tactic (params) etc. *)
   | ETacticCtor of loc * id * expr list
   (** variable, or goal call with no parameters *)


@@ -63,8 +65,9 @@ and expr =
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option
 and constant =
   | CString of string
 and goal = param_decl list * pattern list * expr list * code option

+and func = param_decl list * code

 and tactic = param_decl list * code
 and tactic = param_decl list * code

-  (** Goal/tactic parameter. *)
+  (** Goal/func/tactic parameter. *)

 and param_decl = id
 and id = string
 and code = substs
 and param_decl = id
 and id = string
 and code = substs


@@ -83,6 +86,10 @@ val getvar : env -> loc -> id -> expr
     found or if the named variable is not a goal. *)
 val getgoal : env -> loc -> id -> goal
 
     found or if the named variable is not a goal. *)
 val getgoal : env -> loc -> id -> goal
 

+(** Look up a function in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a function. *)
+val getfunc : env -> loc -> id -> func
+

 (** Look up a tactic in the environment.  Raise [Failure _] if not
     found or if the named variable is not a tactic. *)
 val gettactic : env -> loc -> id -> tactic
 (** Look up a tactic in the environment.  Raise [Failure _] if not
     found or if the named variable is not a tactic. *)
 val gettactic : env -> loc -> id -> tactic

diff --git a/src/eval.ml b/src/eval.ml
index e299769..a0ed834 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -17,6 +17,8 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 

+open Printf
+

 open Utils
 
 let rec to_constant env = function
 open Utils
 
 let rec to_constant env = function


@@ -33,9 +35,23 @@ let rec to_constant env = function
      failwithf "%a: list found where constant expression expected"
        Ast.string_loc loc
 
      failwithf "%a: list found where constant expression expected"
        Ast.string_loc loc
 

-  | ECallGoal (loc, name, _) ->
-     failwithf "%a: cannot use goal ‘%s’ in constant expression"
-       Ast.string_loc loc name
+  | 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"
 
   | ETacticCtor (loc, name, _) ->
      failwithf "%a: cannot use tactic ‘%s’ in constant expression"


@@ -45,6 +61,10 @@ let rec to_constant env = function
      failwithf "%a: cannot use goal in constant expression"
        Ast.string_loc 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
   | ETacticDefn (loc, _) ->
      failwithf "%a: cannot use tactic in constant expression"
        Ast.string_loc loc


@@ -61,7 +81,7 @@ and substitute env loc substs =
   ) substs;
   Buffer.contents b
 
   ) substs;
   Buffer.contents b
 

-let rec to_shell_script env loc substs =
+and to_shell_script env loc substs =

   let b = Buffer.create 13 in
   List.iter (
     function
   let b = Buffer.create 13 in
   List.iter (
     function


@@ -88,9 +108,23 @@ and expr_to_shell_string env = function
      (* These are shell quoted so we can just concat them with space. *)
      String.concat " " strs
 
      (* These are shell quoted so we can just concat them with space. *)
      String.concat " " strs
 

-  | ECallGoal (loc, name, _) ->
-     failwithf "%a: cannot use goal ‘%s’ in shell expansion"
-       Ast.string_loc loc name
+  | 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 ""
 
   (* Tactics expand to the first parameter. *)
   | ETacticCtor (loc, _, []) -> Filename.quote ""


@@ -100,11 +134,15 @@ and expr_to_shell_string env = function
      failwithf "%a: cannot use goal in shell expansion"
        Ast.string_loc 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
 
   | ETacticDefn (loc, _) ->
      failwithf "%a: cannot use tactic in shell expansion"
        Ast.string_loc loc
 

-let rec evaluate_goal_arg env = function
+and evaluate_goal_arg env = function

   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      evaluate_goal_arg env expr
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      evaluate_goal_arg env expr


@@ -119,13 +157,80 @@ let rec evaluate_goal_arg env = function
   | ETacticCtor (loc, name, exprs) ->
      Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 
   | ETacticCtor (loc, name, exprs) ->
      Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 

-  | ECallGoal (loc, name, _) ->
-     (* Goals don't return anything so they cannot be used in
-      * goal args.  Use a function instead.
-      *)
-     failwithf "%a: cannot use goal ‘%s’ in goal argument"
-       Ast.string_loc loc name
+  | 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 _
 
   | EConstant _
   | EGoalDefn _

+  | EFuncDefn _

   | ETacticDefn _ as e -> e
   | 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 substituting
+ * the output into an EList.
+ *
+ * XXX In future allow functions to be annotated with a return type.
+ *)
+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
+
+  (* Create a new environment which maps the parameter names to
+   * the args.
+   *)
+  let env =
+    let params =
+      try List.combine params args
+      with Invalid_argument _ ->
+        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
+
+  (* 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))

diff --git a/src/eval.mli b/src/eval.mli
index e1d73f0..40a4de8 100644 (file)
--- a/src/eval.mli
+++ b/src/eval.mli
@@ -36,3 +36,7 @@ val to_shell_script : Ast.env -> Ast.loc -> Ast.substs -> string
 (** Evaluate a goal argument.  This substitutes any variables found,
     and recursively calls functions. *)
 val evaluate_goal_arg : Ast.env -> Ast.expr -> Ast.expr
 (** Evaluate a goal argument.  This substitutes any variables found,
     and recursively calls functions. *)
 val evaluate_goal_arg : Ast.env -> Ast.expr -> Ast.expr

+
+(* Call a function. *)
+val call_function : Ast.env -> Ast.loc -> Ast.id -> Ast.expr list -> Ast.func ->
+                    Ast.expr

diff --git a/src/lexer.mll b/src/lexer.mll
index f2d0830..66c6b9f 100644 (file)
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -52,10 +52,15 @@ rule read =
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }
     | '"'     { read_string (Ast.Substs.create ()) lexbuf }
     | "{"     { read_code (Ast.Substs.create ()) (ref 1) lexbuf }
     | "goal"  { GOAL }

-    | "tactic" { TACTIC_KEYWORD }
+    | "tactic"
+              { TACTIC_KEYWORD }
+    | "function"
+              { FUNCTION }

     | "let"   { LET }
     | "let"   { LET }

-    | "include" { INCLUDE }
-    | "-include" { OPTINCLUDE }
+    | "include"
+              { INCLUDE }
+    | "-include"
+              { OPTINCLUDE }

     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }
     | "*" id  { (* NB: The initial '*' is part of the name. *)
                 TACTIC (Lexing.lexeme lexbuf) }
     | id      { ID (Lexing.lexeme lexbuf) }

diff --git a/src/main.ml b/src/main.ml
index 88cd084..2e7ac44 100644 (file)
--- a/src/main.ml
+++ b/src/main.ml
@@ -47,7 +47,7 @@ let main () =
   (* If no target was set on the command line, use "all ()". *)
   let targets =
     if targets <> [] then targets
   (* If no target was set on the command line, use "all ()". *)
   let targets =
     if targets <> [] then targets

-    else [Ast.ECallGoal (Ast.noloc, "all", [])] in
+    else [Ast.ECall (Ast.noloc, "all", [])] in

 
   if Cmdline.debug_flag then
     Ast.print_env stderr env;
 
   if Cmdline.debug_flag then
     Ast.print_env stderr env;

diff --git a/src/parser.mly b/src/parser.mly
index 8b7d8a1..c3148ca 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -61,6 +61,7 @@ let do_include env loc filename optflag file =
 %token COMMA
 %token EQUALS
 %token EOF
 %token COMMA
 %token EQUALS
 %token EOF

+%token FUNCTION

 %token GOAL
 %token <string> ID
 %token INCLUDE
 %token GOAL
 %token <string> ID
 %token INCLUDE


@@ -108,6 +109,10 @@ stmt:
       let name, params = $1 in
       name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
     }
       let name, params = $1 in
       name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
     }

+    | FUNCTION ID params_decl EQUALS CODE
+    {
+      $2, Ast.EFuncDefn ($loc, ($3, $5))
+    }

     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
     {
       $2, Ast.ETacticDefn ($loc, ($3, $5))
     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
     {
       $2, Ast.ETacticDefn ($loc, ($3, $5))


@@ -140,7 +145,7 @@ pattern_param:
     ;
 
 expr:
     ;
 
 expr:

-    | ID params  { Ast.ECallGoal ($loc, $1, $2) }
+    | ID params  { Ast.ECall ($loc, $1, $2) }

     | ID         { Ast.EVar ($loc, $1) }
     | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
     | STRING     { Ast.ESubsts ($loc, $1) }
     | ID         { Ast.EVar ($loc, $1) }
     | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
     | STRING     { Ast.ESubsts ($loc, $1) }

diff --git a/src/run.ml b/src/run.ml
index 2e36d1b..d8cabb9 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -25,12 +25,21 @@ let rec run_targets env exprs =
   List.iter (run_target env) exprs
 
 and run_target env = function
   List.iter (run_target env) exprs
 
 and run_target env = function

-  | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false
+  | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false

 
 

-  (* Call a goal. *)
-  | Ast.ECallGoal (loc, name, args) ->
-     let goal = Ast.getgoal env loc name in
-     run_goal env loc name args goal []
+  (* Call a goal or function. *)
+  | Ast.ECall (loc, name, args) ->
+     let expr = Ast.getvar env loc name in
+     (match expr with
+      | Ast.EGoalDefn (_, goal) ->
+         run_goal env loc name args goal []
+      | Ast.EFuncDefn (_, func) ->
+         let expr = Eval.call_function env loc name args func in
+         run_target env expr
+      | _ ->
+         failwithf "%a: tried to call ‘%s’ which is not a goal or a function"
+           Ast.string_loc loc name
+     )

 
   (* Call a tactic. *)
   | Ast.ETacticCtor (loc, name, args) ->
 
   (* Call a tactic. *)
   | Ast.ETacticCtor (loc, name, args) ->


@@ -46,8 +55,8 @@ and run_target env = function
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      (match expr with
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      (match expr with

-      | EGoalDefn (loc, ([], _, _, _)) ->
-         run_target env (Ast.ECallGoal (loc, name, []))
+      | Ast.EGoalDefn (loc, ([], _, _, _)) ->
+         run_target env (Ast.ECall (loc, name, []))

       | EGoalDefn _ ->
          failwithf "%a: cannot call %s() since this goal has parameters"
            Ast.string_loc loc name
       | EGoalDefn _ ->
          failwithf "%a: cannot call %s() since this goal has parameters"
            Ast.string_loc loc name