X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=779cb5d60ee8aae623f161aab99254aca3f5ec76;hb=318cea9f1c7669d23d27fc362bf06b9aca1b61a1;hp=6b56b8f90b3b34f7668f97945ebebd45db160a9a;hpb=98a2cfdd3bdf5641e268e7db7c7ea2d23656b296;p=goals.git

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;