From 94430834302e922af6c27a1c88e13f862a57dd0f Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 23 Dec 2019 08:05:24 +0000 Subject: [PATCH] Add environment to store variables and goals. --- TODO | 1 + src/ast.ml | 33 +++++++++++++++++++-------------- src/ast.mli | 27 ++++++++++++++++++--------- src/eval.ml | 2 +- src/eval.mli | 2 +- src/main.ml | 51 ++++++++++++++++----------------------------------- src/parse.ml | 4 ++-- src/parse.mli | 2 +- src/parser.mly | 18 ++++++++++-------- 9 files changed, 69 insertions(+), 71 deletions(-) create mode 100644 TODO diff --git a/TODO b/TODO new file mode 100644 index 0000000..8eb190d --- /dev/null +++ b/TODO @@ -0,0 +1 @@ +'let :=' for immediate evaluation in assignment. diff --git a/src/ast.ml b/src/ast.ml index 63b8285..ef73459 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -19,18 +19,20 @@ open Printf -type file = stmt list -and stmt = - | Let of id * expr - | Goal of id * id list * pattern list * expr list * code option +module StringMap = Map.Make (String) + +type env = expr StringMap.t and pattern = | PTactic of id * substs list | PVarSubst of id and expr = + | EGoal of goal | ECall of id * expr list | EVar of id - | EString of substs | EList of expr list + | ESubsts of substs + | EString of string +and goal = id list * pattern list * expr list * code option and id = string and code = substs and substs = subst list @@ -69,15 +71,12 @@ let iter_with_commas f fp x ) xs -let rec print_file fp file = - List.iter (print_stmt fp) file +let rec print_env fp env = + StringMap.iter (print_def fp) env -and print_stmt fp = function - | Let (name, expr) -> - fprintf fp "let %s = " name; - print_expr fp expr; - fprintf fp "\n" - | Goal (name, params, patterns, exprs, code) -> +and print_def fp name expr = + match expr with + | EGoal (params, patterns, exprs, code) -> fprintf fp "goal %s (%s) =\n" name (String.concat ", " params); fprintf fp " "; iter_with_commas fp print_pattern patterns; @@ -91,6 +90,10 @@ and print_stmt fp = function fprintf fp "\n }" ); fprintf fp "\n" + | expr -> + fprintf fp "let %s = " name; + print_expr fp expr; + fprintf fp "\n" and print_pattern fp = function | PTactic (name, params) -> @@ -100,16 +103,18 @@ and print_pattern fp = function | PVarSubst id -> print_id fp id and print_expr fp = function + | EGoal _ -> assert false (* printed above *) | ECall (name, params) -> fprintf fp "%s (" name; iter_with_commas fp print_expr params; fprintf fp ")" | EVar var -> print_id fp var - | EString s -> print_substs fp s; | EList xs -> fprintf fp "["; iter_with_commas fp print_expr xs; fprintf fp "]" + | ESubsts s -> print_substs fp s + | EString s -> fprintf fp "%S" s and print_id = output_string diff --git a/src/ast.mli b/src/ast.mli index e2189cf..fd9f088 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -17,26 +17,35 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) -type file = stmt list -and stmt = - (** let id = expr *) - | Let of id * expr - (** goal id (params) = patterns : exprs = code *) - | Goal of id * id list * pattern list * expr list * code option +module StringMap : sig + type key = string + type 'a t + val empty: 'a t + val add: key -> 'a -> 'a t -> 'a t +end + +(** An environment is a set of variable and goal definitions, mapping + variable or goal name -> expression. *) +type env = expr StringMap.t and pattern = (** match tactic such as file ("filename") *) | PTactic of id * substs list (** match named variable, which must be a string or list *) | PVarSubst of id and expr = + (** goal (params) = patterns : exprs = code *) + | EGoal of goal (** goalname (params), tactic (params) etc. *) | ECall of id * expr list (** variable *) | EVar of id - (** string with %-substitutions *) - | EString of substs (** list *) | EList of expr list + (** string with %-substitutions *) + | ESubsts of substs + (** string with no substitutions *) + | EString of string +and goal = id list * pattern list * expr list * code option and id = string and code = substs and substs = subst list @@ -56,4 +65,4 @@ module Substs : sig val add_var : t -> string -> unit end -val print_file : out_channel -> file -> unit +val print_env : out_channel -> env -> unit diff --git a/src/eval.ml b/src/eval.ml index 1df1a17..0d4d91f 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -17,5 +17,5 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) -let evaluate file vars exprs = +let evaluate env exprs = () diff --git a/src/eval.mli b/src/eval.mli index 2e55981..167b41e 100644 --- a/src/eval.mli +++ b/src/eval.mli @@ -17,6 +17,6 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) -val evaluate : Ast.file -> (string, Ast.expr) Hashtbl.t -> Ast.expr list -> unit +val evaluate : Ast.env -> Ast.expr list -> unit (** This drives evaluation of the list of expressions (in parallel) until they are complete or we reach an error. *) diff --git a/src/main.ml b/src/main.ml index 2685160..2111eaf 100644 --- a/src/main.ml +++ b/src/main.ml @@ -22,7 +22,8 @@ open Printf open Utils (* See also "let id" in [lexer.mll]. *) -let var_regexp = Str.regexp "\\([a-zA-Z_][a-zA-Z0-9_]*\\)=\\(.*\\)" +let var_regexp = + Str.regexp "\\([a-zA-Z_][a-zA-Z0-9_]*\\)[ \t]*=[ \t]*\\(.*\\)" let usage = "\ @@ -53,58 +54,38 @@ let main () = let filename = !filename in (* Parse the input file. *) - let file = Parse.parse_goalfile filename in + let env = Parse.parse_goalfile filename in (* Parse the command line anon args. Each parameter has the * form "name=" to assign a value to a variable, or * "" to indicate a target to build. *) - let assignments = ref [] in let targets = ref [] in + let env = ref env in List.iter ( fun arg -> - if Str.string_match var_regexp arg 0 then ( (* assignment *) + if Str.string_match var_regexp arg 0 then ( + (* assignment *) let name = Str.matched_group 1 arg in let expr = Parse.parse_cli_expr (Str.matched_group 2 arg) in - assignments := Ast.Let (name, expr) :: !assignments + env := Ast.StringMap.add name expr !env ) - else ( (* target *) + else ( + (* target *) let expr = Parse.parse_cli_expr arg in targets := expr :: !targets ) ) !args; + let targets = List.rev !targets and env = !env in - (* If no target was set on the command line, find - * the first goal in the file. - *) - if !targets = [] then ( - try - let first_goal = - List.find (function Ast.Goal _ -> true | _ -> false) file in - match first_goal with - | Ast.Goal (name, [], _, _, _) -> - targets := [Ast.ECall (name, [])] - | Ast.Goal (name, _, _, _, _) -> - failwithf "%s: first target ‘%s’ has parameters and so cannot be used as the default target" - filename name - | _ -> assert false - with - (* Actually this is fine. If there are no goals we'll do nothing. *) - Not_found -> () - ); - - let targets = List.rev !targets in - - (* Assignments are simply treated as statements added to the end of - * the file (so they override earlier assignments to the same variable, - * if any). - *) - let file = file @ List.rev !assignments in + (* If no target was set on the command line, use "all ()". *) + let targets = + if targets <> [] then targets + else [Ast.ECall ("all", [])] in - (* We start with an empty symbol table. *) - let vars = Hashtbl.create 13 in + (*Ast.print_env stdout env;*) (* Evaluate the target expressions in turn. *) - Eval.evaluate file vars targets + Eval.evaluate env targets let () = main () diff --git a/src/parse.ml b/src/parse.ml index 9363143..07647c2 100644 --- a/src/parse.ml +++ b/src/parse.ml @@ -52,9 +52,9 @@ let parse_goalfile filename = let fp = open_in filename in let lexbuf = Lexing.from_channel fp in lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename }; - let file : Ast.file = parse_file lexbuf in + let env : Ast.env = parse_file lexbuf in close_in fp; - file + env (* This is used to parse dependency expressions on the command line. *) let parse_cli_expr str = diff --git a/src/parse.mli b/src/parse.mli index 7535de2..39893a1 100644 --- a/src/parse.mli +++ b/src/parse.mli @@ -17,5 +17,5 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) -val parse_goalfile : string -> Ast.file +val parse_goalfile : string -> Ast.env val parse_cli_expr : string -> Ast.expr diff --git a/src/parser.mly b/src/parser.mly index add72bb..9ce3996 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -36,10 +36,8 @@ open Printf %token RIGHT_PAREN %token STRING -%type stmt - (* Start nonterminals. *) -%start file +%start file %start expr %% @@ -48,7 +46,11 @@ file: ; stmts: - | list(stmt) { $1 } + | list(stmt) + { List.fold_left ( + fun env (name, expr) -> Ast.StringMap.add name expr env + ) Ast.StringMap.empty $1 + } ; stmt: | option(goal_stmt) patterns COLON barelist option(CODE) @@ -58,14 +60,14 @@ stmt: let pos = $startpos in sprintf "_goal@%d" pos.pos_lnum, [] | Some x -> x in - Ast.Goal (name, params, $2, $4, $5) + name, Ast.EGoal (params, $2, $4, $5) } | goal_stmt CODE { let name, params = $1 in - Ast.Goal (name, params, [], [], Some $2) + name, Ast.EGoal (params, [], [], Some $2) } - | LET ID EQUALS expr { Ast.Let ($2, $4) } + | LET ID EQUALS expr { $2, $4 } ; goal_stmt: @@ -94,7 +96,7 @@ pattern_param: expr: | ID params { Ast.ECall ($1, $2) } | ID { Ast.EVar $1 (* This might be replaced with ECall later. *) } - | STRING { Ast.EString $1 } + | STRING { Ast.ESubsts $1 } | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList $2 } ; barelist: -- 1.8.3.1