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
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
*)
(* 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
(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
);
* 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
| 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;
git.annexia.org / goals.git / blobdiff