From 318cea9f1c7669d23d27fc362bf06b9aca1b61a1 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 23 Dec 2019 18:00:51 +0000 Subject: [PATCH] Attach parser location information to AST nodes. --- src/ast.ml | 42 +++++++++++++++---------- src/ast.mli | 22 ++++++++----- src/eval.ml | 99 ++++++++++++++++++++++++++++++++-------------------------- src/main.ml | 2 +- src/parser.mly | 21 ++++++------- 5 files changed, 106 insertions(+), 80 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index 5b31c0d..6a7823c 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -17,21 +17,31 @@ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. *) +open Lexing open Printf module StringMap = Map.Make (String) +type loc = position * position +let noloc = dummy_pos, dummy_pos + +let string_loc () loc = + let pos = fst loc in + sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol) +let print_loc fp loc = + fprintf fp "%s" (string_loc () loc) + type env = expr StringMap.t and pattern = - | PTactic of id * substs list - | PVar of id + | PTactic of loc * id * substs list + | PVar of loc * id and expr = - | EGoal of goal - | ECall of id * expr list - | EVar of id - | EList of expr list - | ESubsts of substs - | EConstant of constant + | EGoal of loc * goal + | ECall of loc * id * expr list + | EVar of loc * id + | EList of loc * expr list + | ESubsts of loc * substs + | EConstant of loc * constant and constant = | CString of string and goal = id list * pattern list * expr list * code option @@ -78,7 +88,7 @@ let rec print_env fp env = and print_def fp name expr = match expr with - | EGoal (params, patterns, exprs, code) -> + | EGoal (loc, (params, patterns, exprs, code)) -> fprintf fp "goal %s (%s) =\n" name (String.concat ", " params); fprintf fp " "; iter_with_commas fp print_pattern patterns; @@ -98,25 +108,25 @@ and print_def fp name expr = fprintf fp "\n" and print_pattern fp = function - | PTactic (name, params) -> + | PTactic (loc, name, params) -> fprintf fp "%s (" name; iter_with_commas fp print_substs params; fprintf fp ")" - | PVar id -> print_id fp id + | PVar (loc, id) -> print_id fp id and print_expr fp = function | EGoal _ -> assert false (* printed above *) - | ECall (name, params) -> + | ECall (loc, name, params) -> fprintf fp "%s (" name; iter_with_commas fp print_expr params; fprintf fp ")" - | EVar var -> print_id fp var - | EList xs -> + | EVar (loc, var) -> print_id fp var + | EList (loc, xs) -> fprintf fp "["; iter_with_commas fp print_expr xs; fprintf fp "]" - | ESubsts s -> print_substs fp s - | EConstant c -> print_constant fp c + | ESubsts (loc, s) -> print_substs fp s + | EConstant (loc, c) -> print_constant fp c and print_constant fp = function | CString s -> fprintf fp "%S" s diff --git a/src/ast.mli b/src/ast.mli index 57c2a71..4162eb3 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -28,27 +28,33 @@ module StringMap : sig val bindings: 'a t -> (key * 'a) list end +(** Location where we parsed from $loc = $startpos, $endpos *) +type loc = Lexing.position * Lexing.position +val noloc : loc +val print_loc : out_channel -> loc -> unit +val string_loc : unit -> loc -> string + (** 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 + | PTactic of loc * id * substs list (** match named variable, which must be a string or list *) - | PVar of id + | PVar of loc * id and expr = (** goal (params) = patterns : exprs = code *) - | EGoal of goal + | EGoal of loc * goal (** goalname (params), tactic (params) etc. *) - | ECall of id * expr list + | ECall of loc * id * expr list (** variable *) - | EVar of id + | EVar of loc * id (** list *) - | EList of expr list + | EList of loc * expr list (** string with %-substitutions *) - | ESubsts of substs + | ESubsts of loc * substs (** constant expression, such as a plain string, int, boolean, etc. *) - | EConstant of constant + | EConstant of loc * constant and constant = | CString of string and goal = id list * pattern list * expr list * code option diff --git a/src/eval.ml b/src/eval.ml index 6b56b8f..779cb5d 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -23,61 +23,65 @@ let rec evaluate_targets env exprs = List.iter (evaluate_target env) exprs and evaluate_target env = function - | Ast.EGoal goal -> assert false + | Ast.EGoal _ -> assert false (* This could be an instruction to call a goal, or it * could be a tactic. *) - | Ast.ECall ("file", [filename]) (* XXX define tactics! *) -> + | Ast.ECall (loc, "file", [filename]) (* XXX define tactics! *) -> (* All parameters of tactics must be simple expressions (strings, * in future booleans, numbers, etc). *) let args = [filename] in let args = List.map (simplify env) args in - run_goal_for_tactic env "file" args + run_goal_for_tactic loc env "file" args - | Ast.ECall ("file", _) -> - failwith "file tactic called with wrong number of parameters" + | Ast.ECall (loc, "file", _) -> + failwithf "%a: file tactic called with wrong number of parameters" + Ast.string_loc loc - | Ast.ECall (name, args) -> + | Ast.ECall (loc, name, args) -> let expr = try Ast.StringMap.find name env - with Not_found -> failwithf "%s: goal not found" name in + with Not_found -> + failwithf "%a: goal ‘%s’ not found" Ast.string_loc loc name in let goal = match expr with - | Ast.EGoal goal -> goal + | Ast.EGoal (loc, goal) -> goal | _ -> - failwithf "%s: tried to call something which is not a goal" name in - run_goal env name args goal + failwithf "%a: tried to call ‘%s’ which is not a goal" + Ast.string_loc loc name in + run_goal loc env name args goal (* Look up the variable and substitute it. *) - | Ast.EVar name -> + | Ast.EVar (loc, name) -> let expr = try Ast.StringMap.find name env - with Not_found -> failwithf "%s: variable not found" name in + with Not_found -> + failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in evaluate_target env expr (* Lists are inlined when found as a target. *) - | Ast.EList exprs -> + | Ast.EList (loc, exprs) -> evaluate_targets env exprs (* A string (with or without substitutions) implies file (filename). *) - | Ast.ESubsts str -> - let str = substitute env str in - run_goal_for_tactic env "file" [Ast.CString str] + | Ast.ESubsts (loc, str) -> + let str = substitute loc env str in + run_goal_for_tactic loc env "file" [Ast.CString str] - | Ast.EConstant c -> - run_goal_for_tactic env "file" [c] + | Ast.EConstant (loc, c) -> + run_goal_for_tactic loc env "file" [c] (* Find the goal which matches the given tactic and run it. * Params is a list of constants. *) -and run_goal_for_tactic env tactic const_args = +and run_goal_for_tactic loc env tactic const_args = (* Search across all goals for a matching tactic. *) let goals = let env = Ast.StringMap.bindings env in filter_map - (function (name, Ast.EGoal goal) -> Some (name, goal) | _ -> None) + (function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None) env in let name, goal = (* If there are multiple goals matching, this must choose @@ -86,36 +90,37 @@ and run_goal_for_tactic env tactic const_args = try List.find (fun (_, (_, patterns, _, _)) -> - List.exists (matching_pattern env tactic const_args) patterns) + List.exists (matching_pattern loc env tactic const_args) patterns) goals with Not_found -> - failwithf "don't know how to build %s %s" + failwithf "%a: don't know how to build %s %s" + Ast.string_loc loc tactic (String.concat ", " (List.map (function Ast.CString s -> s) const_args)) in let args = [] (* XXX calculate free variables *) in - run_goal env name args goal + run_goal loc env name args goal (* XXX This only does exact matches at the moment. *) -and matching_pattern env tactic const_args = function - | PTactic (constructor, params) +and matching_pattern loc env tactic const_args = function + | Ast.PTactic (loc, constructor, params) when tactic = constructor && List.length const_args = List.length params -> (* Try to simplify the parameters of this pattern down * to constants, but don't fail here if we can't do this. *) (try - let params = List.map (substitute env) params in + let params = List.map (substitute loc env) params in let params = List.map (fun s -> Ast.CString s) params in const_args = params with Failure _ -> false ) - | PTactic _ -> false + | Ast.PTactic _ -> false - | PVar name -> assert false + | Ast.PVar (loc, name) -> assert false (* NOT IMPLEMENTED - we need variables to contain constructors! (try @@ -126,12 +131,13 @@ and matching_pattern env tactic const_args = function *) (* Run a named goal. *) -and run_goal env name args (params, patterns, deps, code) = +and run_goal loc env name args (params, patterns, deps, code) = (* Substitute the args for the parameters in the environment. *) let params = try List.combine params args with Invalid_argument _ -> - failwithf "%s: calling goal with wrong number of arguments" name in + failwithf "%a: calling goal ‘%s’ with wrong number of arguments" + Ast.string_loc loc name in let env = List.fold_left (fun env (k, v) -> Ast.StringMap.add k v env) env params in @@ -146,7 +152,7 @@ and run_goal env name args (params, patterns, deps, code) = (match code with | None -> () | Some code -> - let code = substitute env code in + let code = substitute loc env code in Printf.printf "running : %s\n" code ); @@ -158,31 +164,35 @@ and run_goal env name args (params, patterns, deps, code) = * an error. *) and simplify env = function - | Ast.EConstant c -> c + | Ast.EConstant (loc, c) -> c - | Ast.EVar name -> + | Ast.EVar (loc, name) -> let expr = try Ast.StringMap.find name env - with Not_found -> failwithf "%s: variable not found" name in + with Not_found -> + failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in simplify env expr - | Ast.ESubsts str -> - Ast.CString (substitute env str) + | Ast.ESubsts (loc, str) -> + Ast.CString (substitute loc env str) - | Ast.EList _ -> - failwith "list found where constant expression expected" + | Ast.EList (loc, _) -> + failwithf "%a: list found where constant expression expected" + Ast.string_loc loc - | Ast.ECall (name, _) -> - failwithf "%s: cannot use goal or tactic in constant expression" name + | Ast.ECall (loc, name, _) -> + failwithf "%a: cannot use goal or tactic ‘%s’ in constant expression" + Ast.string_loc loc name - | Ast.EGoal _ -> - failwith "cannot use in constant expression" + | Ast.EGoal (loc, _) -> + failwithf "%a: cannot use goal in constant expression" + Ast.string_loc loc (* Take a substitution list and try to turn it into a simple * string by evaluating every variable. If not possible this * throws an error. Returns a string. *) -and substitute env substs = +and substitute loc env substs = let b = Buffer.create 13 in List.iter ( function @@ -190,7 +200,8 @@ and substitute env substs = | Ast.SVar name -> let expr = try Ast.StringMap.find name env - with Not_found -> failwithf "%s: variable not found" name in + with Not_found -> + failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in match simplify env expr with | Ast.CString s -> Buffer.add_string b s ) substs; diff --git a/src/main.ml b/src/main.ml index c19f1ac..b95d1f5 100644 --- a/src/main.ml +++ b/src/main.ml @@ -90,7 +90,7 @@ let main () = (* If no target was set on the command line, use "all ()". *) let targets = if targets <> [] then targets - else [Ast.ECall ("all", [])] in + else [Ast.ECall (Ast.noloc, "all", [])] in Ast.print_env stdout env; diff --git a/src/parser.mly b/src/parser.mly index afc9d18..69cb063 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -57,15 +57,14 @@ stmt: { let name, params = match $1 with | None -> - let pos = $startpos in - sprintf "_goal@%d" pos.pos_lnum, [] + sprintf "_goal@%d" $startpos.pos_lnum, [] | Some x -> x in - name, Ast.EGoal (params, $2, $4, $5) + name, Ast.EGoal ($loc, (params, $2, $4, $5)) } | goal_stmt CODE { let name, params = $1 in - name, Ast.EGoal (params, [], [], Some $2) + name, Ast.EGoal ($loc, (params, [], [], Some $2)) } | LET ID EQUALS expr { $2, $4 } ; @@ -82,9 +81,9 @@ patterns: | separated_list(COMMA, pattern) { $1 } ; pattern: - | STRING { Ast.PTactic ("file", [$1]) } - | ID pattern_params { Ast.PTactic ($1, $2) } - | ID { Ast.PVar $1 } + | STRING { Ast.PTactic ($loc, "file", [$1]) } + | ID pattern_params { Ast.PTactic ($loc, $1, $2) } + | ID { Ast.PVar ($loc, $1) } ; pattern_params: | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 } @@ -94,10 +93,10 @@ pattern_param: ; expr: - | ID params { Ast.ECall ($1, $2) } - | ID { Ast.EVar $1 (* This might be replaced with ECall later. *) } - | STRING { Ast.ESubsts $1 } - | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList $2 } + | ID params { Ast.ECall ($loc, $1, $2) } + | ID { Ast.EVar ($loc, $1) } + | STRING { Ast.ESubsts ($loc, $1) } + | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) } ; barelist: | separated_list(COMMA, expr) { $1 } -- 1.8.3.1