From 976bb1b35d77f3058df3c25c1e2a4767147d606b Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 3 Jan 2020 21:33:48 +0000 Subject: [PATCH] Implement functions. --- TODO | 7 +-- src/ast.ml | 26 ++++++++++- src/ast.mli | 13 ++++-- src/eval.ml | 133 +++++++++++++++++++++++++++++++++++++++++++++++++++------ src/eval.mli | 4 ++ src/lexer.mll | 11 +++-- src/main.ml | 2 +- src/parser.mly | 7 ++- src/run.ml | 23 +++++++--- 9 files changed, 192 insertions(+), 34 deletions(-) diff --git a/TODO b/TODO index 0c67dcd..5db7e8d 100644 --- 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. -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. + +"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 --- 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 + | EFuncDefn of loc * func | 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 @@ -53,6 +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 * code 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 +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 = @@ -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" + | 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; @@ -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 -> " = { ... }") +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) @@ -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) + | EFuncDefn (loc, func) -> string_func () (None, func) | 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) -> diff --git a/src/ast.mli b/src/ast.mli index 3a528ea..f8b88f0 100644 --- 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 + (** function (params) = code *) + | EFuncDefn of loc * func (** 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 *) @@ -63,8 +65,9 @@ and expr = 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 - (** Goal/tactic parameter. *) + (** Goal/func/tactic parameter. *) 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 +(** 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 diff --git a/src/eval.ml b/src/eval.ml index e299769..a0ed834 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -17,6 +17,8 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) +open Printf + 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 - | 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" @@ -45,6 +61,10 @@ let rec to_constant env = function 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 @@ -61,7 +81,7 @@ and substitute env loc substs = ) 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 @@ -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 - | 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 "" @@ -100,11 +134,15 @@ and expr_to_shell_string env = function 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 -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 @@ -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) - | 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 _ + | EFuncDefn _ | 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 --- 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 + +(* 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 --- 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 } - | "tactic" { TACTIC_KEYWORD } + | "tactic" + { TACTIC_KEYWORD } + | "function" + { FUNCTION } | "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) } diff --git a/src/main.ml b/src/main.ml index 88cd084..2e7ac44 100644 --- 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 - else [Ast.ECallGoal (Ast.noloc, "all", [])] in + else [Ast.ECall (Ast.noloc, "all", [])] in if Cmdline.debug_flag then Ast.print_env stderr env; diff --git a/src/parser.mly b/src/parser.mly index 8b7d8a1..c3148ca 100644 --- 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 FUNCTION %token GOAL %token ID %token INCLUDE @@ -108,6 +109,10 @@ stmt: 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)) @@ -140,7 +145,7 @@ pattern_param: ; 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) } diff --git a/src/run.ml b/src/run.ml index 2e36d1b..d8cabb9 100644 --- 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 - | 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) -> @@ -46,8 +55,8 @@ and run_target env = function | 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 -- 1.8.3.1