Make error messages consistently formatted with locations

.gitignore

@@ -15,3 +15,5 @@ version.tex
 bin/
 .depend
 ocamlgraph-1.7
+.merlin
+make_merlin.sh

src/auxl.ml

@@ -31,11 +31,13 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-open Types
+open Types;;
+open Location
 
 (* exceptions ************************************************************ *)
 
 exception ThisCannotHappen
+exception Located_Failure of (loc option)*string
 
 (* debug, warning and error report *************************************** *)
 
@@ -52,17 +54,33 @@ let mode_name m = match m with
   | Lex _ -> "Lex"
   | Menhir _ -> "Menhir"
 
+let colour = ref true
+
+let maybe_pp_loc l = 
+  match l with
+    | None -> ""
+    | Some l -> if !colour then "\027[1m" ^ pp_loc l ^ ":\027[0m\n" else pp_loc l ^ ":\n"
+
+let warning_string () = if !colour then "\027[1m\027[35mWarning: \027[0m" else "Warning: "
+
+let error_string () = if !colour then "\027[1m\027[31mError: \027[0m" else "Error: "
+
 let debug_on = false
 
 let debug s = if debug_on then begin print_string s; flush stdout end
 
-let warning s = print_endline ("warning: " ^ s); flush stdout
+let warning l s = print_endline (maybe_pp_loc l ^ warning_string () ^ s); flush stdout
+
+let report_error l s = print_endline (maybe_pp_loc l ^ error_string () ^ s); flush stdout
+
+
+let error l s = raise (Located_Failure (l, s))
 
-let error s = print_endline ("error: " ^ s); flush stdout; exit 2
+let exit_with l s = print_endline (maybe_pp_loc l ^ error_string () ^ s);  flush stdout; exit 2
 
-let int_error s = print_endline("internal: " ^ s); flush stdout; exit 2
+let int_error s = raise (Located_Failure (None, "internal: " ^ s))
 
-let errorm m s = print_endline ("internal (" ^ mode_name m ^ "): " ^ s); flush stdout; exit 2
+let errorm m s = raise (Located_Failure (None, "internal (" ^ mode_name m ^ "): " ^ s))
 
 
 (* ***************** *)
@@ -301,7 +319,7 @@ let prod_of_prodname ?(warn=true) (xd:syntaxdefn) (pn:prodname) : prod =
       List.find 
 	(fun r -> List.exists (fun p -> p.prod_name=pn) r.rule_ps)
 	xd.xd_rs
-    with Not_found -> if warn then warning ("internal: prod_of_prodname: searching pn = "^pn^"\n"); raise Not_found in
+    with Not_found -> if warn then warning None ("internal: prod_of_prodname: searching pn = "^pn^"\n"); raise Not_found in
   List.find (fun p -> p.prod_name=pn) r.rule_ps
 (*        let prod_of_prod_name : prodname -> prod  *)
 (*            = fun prod_name' ->  *)
@@ -621,6 +639,26 @@ let hom_spec_for_hom_name hn homs =
 let hom_spec_for_pp_mode m homs = 
   hom_spec_for_hom_name (hom_name_for_pp_mode m) homs
 
+let loc_of_symterm st = match st with
+  | St_node (l,_) -> l  
+  | St_nonterm (l,_,_) -> l
+  | St_nontermsub (l,_,_,_) -> l 
+  | St_uninterpreted (l,_) -> l
+
+let loc_of_symterm_element ste = match ste with
+  | Types.Ste_st (loc,_) -> loc
+  | Types.Ste_metavar (loc,_,_) -> loc
+  | Types.Ste_var (loc,_,_) -> loc
+  | Types.Ste_list (loc,_) -> loc
+
+let loc_of_mvr xd mvr = (mvd_of_mvr_nonprimary xd mvr).mvd_loc
+
+let loc_of_ntr (xd:syntaxdefn) (ntr:nontermroot) =
+  (rule_of_ntr xd ntr).rule_loc 
+
+let loc_of_prodname ?(warn=true) (xd:syntaxdefn) (pn:prodname) =
+  (prod_of_prodname xd pn).prod_loc 
+
 let loc_of_raw_element e = 
   match e with
   | Raw_ident (l,_) 
@@ -1040,11 +1078,11 @@ and rename_bound map b = match b with
                           bclu_upper = rename_suffix_item map bclu.bclu_upper }
 
 and rename_bindspec map bs = match bs with
-| Bind(mse,nt)->Bind(rename_mse map mse,rename_nonterm map nt)
-| AuxFnDef(auxfn,mse)->AuxFnDef(auxfn, rename_mse map mse)
-| NamesEqual(mse,mse')->NamesEqual(rename_mse map mse,rename_mse map mse')
-| NamesDistinct(mse,mse')->NamesDistinct(rename_mse map mse,rename_mse map mse')
-| AllNamesDistinct(mse)->AllNamesDistinct(rename_mse map mse)
+| Bind(loc,mse,nt)->Bind(loc,rename_mse map mse,rename_nonterm map nt)
+| AuxFnDef(loc,auxfn,mse)->AuxFnDef(loc,auxfn, rename_mse map mse)
+| NamesEqual(loc,mse,mse')->NamesEqual(loc,rename_mse map mse,rename_mse map mse')
+| NamesDistinct(loc,mse,mse')->NamesDistinct(loc,rename_mse map mse,rename_mse map mse')
+| AllNamesDistinct(loc,mse)->AllNamesDistinct(loc,rename_mse map mse)
 
 and rename_mse map mse = match mse with
 | MetaVarExp(mv)->MetaVarExp(rename_metavar map mv)
@@ -1119,8 +1157,8 @@ and rename_freevar map fv =
     fv_that = rename_nt_or_mv_root map fv.fv_that; }
 
 and rename_parsing_annotations map pas =
-  { pa_data = List.map (fun (ntr1,pa_type,ntr2)-> 
-      (rename_nontermroot map ntr1,pa_type,rename_nontermroot map ntr2)) pas.pa_data }
+  { pa_data = List.map (fun (ntr1,pa_type,ntr2,l)-> 
+      (rename_nontermroot map ntr1,pa_type,rename_nontermroot map ntr2,l)) pas.pa_data }
 
 and rename_dependencies map xddep =
   { xd_dep_ts = List.map (List.map (rename_nt_or_mv_root map)) xddep.xd_dep_ts;
@@ -1265,7 +1303,7 @@ let avoid xd mvs0 nts0 =
         match mvd.mvd_indexvar with
         | true ->
             if mvr=mvd.mvd_name then 
-              warning ("warning: indexvar \""^mvr^"\" is primary so may give a name-clash\n") ;
+              warning None ("warning: indexvar \""^mvr^"\" is primary so may give a name-clash\n") ;
             None
         | false ->
             if mvr=mvd.mvd_name then Some mv else None
@@ -1350,7 +1388,7 @@ let secondaryify xd mvs0 nts0 =
         match mvd.mvd_indexvar with
         | true ->
             if mvr=mvd.mvd_name then 
-              warning ("indexvar \""^mvr^"\" is primary so may give a name-clash\n") ;
+              warning None ("indexvar \""^mvr^"\" is primary so may give a name-clash\n") ;
             Some mv
         | false ->
             Some mv
@@ -1479,49 +1517,51 @@ uppercase *)
 
 let rec detect_conflicts l =
   match l with
-  | [] -> (false,"")
-  | (_,x)::tl -> 
-      if List.mem x (List.map (fun x -> snd x) tl)
-      then (true,x)
+  | [] -> (false,"",dummy_loc)
+  | (loc,_,x)::tl -> 
+      if List.mem x (List.map (fun (_,_,x) -> x) tl)
+      then (true,x,loc)
       else detect_conflicts tl
 
+let remove_fst (_,x,y) = (x,y)
+
+
 let capitalize_prodnames sd =
   let rule_list = sd.syntax.xd_rs in
   let prod_list = List.flatten (List.map (fun r -> r.rule_ps) rule_list) in
-  let prod_name_list = List.map (fun p -> p.prod_name) prod_list in
-  let map_prod_names = List.map (fun pn -> (pn,String.capitalize pn)) prod_name_list in
-  let (conflict,err_msg) = detect_conflicts map_prod_names in
+  (* let prod_name_list = List.map (fun p -> p.prod_name) prod_list in *)
+  let map_prod_names = List.map (fun p -> (p.prod_loc, p.prod_name, String.capitalize p.prod_name)) prod_list in
+  let (conflict,err_msg,loc) = detect_conflicts map_prod_names in
   if conflict
-  then error ("Renaming of production name \""^err_msg^"\" generates a conflict\n")
-  else map_prod_names
+  then error (Some loc) ("Renaming of production name \""^err_msg^"\" generates a conflict\n")
+  else List.map remove_fst map_prod_names
 
 let uncapitalize_prodnames sd =
   let rule_list = sd.syntax.xd_rs in
   let prod_list = List.flatten (List.map (fun r -> r.rule_ps) rule_list) in
-  let prod_name_list = List.map (fun p -> p.prod_name) prod_list in
-  let map_prod_names = List.map (fun pn -> (pn,String.uncapitalize pn)) prod_name_list in
-  let (conflict,err_msg) = detect_conflicts map_prod_names in
+  let map_prod_names = List.map (fun p -> (p.prod_loc, p.prod_name, String.uncapitalize p.prod_name)) prod_list in
+  let (conflict,err_msg,loc) = detect_conflicts map_prod_names in
   if conflict
-  then error ("Renaming of production name \""^err_msg^"\" generates a conflict\n")
-  else map_prod_names
+  then error (Some loc) ("Renaming of production name \""^err_msg^"\" generates a conflict\n")
+  else List.map remove_fst map_prod_names
 
 let uncapitalize_primary_nontermroots sd = 
   let rule_list = sd.syntax.xd_rs in
-  let nontermroots_list = List.map (fun r -> r.rule_ntr_name) rule_list in
-  let map_nontermroots = List.map (fun ntr -> (ntr,String.uncapitalize ntr)) nontermroots_list in
-  let (conflict,err_msg) = detect_conflicts map_nontermroots in
+  let nontermroots_list = List.map (fun r -> (r.rule_loc, r.rule_ntr_name)) rule_list in
+  let map_nontermroots = List.map (fun (loc,ntr) -> (loc,ntr,String.uncapitalize ntr)) nontermroots_list in
+  let (conflict,err_msg,loc) = detect_conflicts map_nontermroots in
   if conflict
-  then error ("Renaming of primary nontermroot \""^err_msg^"\" generates a conflict\n")
-  else map_nontermroots
+  then error (Some loc) ("Renaming of primary nontermroot \""^err_msg^"\" generates a conflict\n")
+  else List.map remove_fst map_nontermroots
 
 let uncapitalize_primary_metavarroots sd =
   let metavardefn_list = sd.syntax.xd_mds in
-  let metavarroots_list = List.map (fun mvd -> mvd.mvd_name) metavardefn_list in
-  let map_metavarroots = List.map (fun mvr -> (mvr,String.uncapitalize mvr)) metavarroots_list in
-  let (conflict,err_msg) = detect_conflicts map_metavarroots in
+  let metavarroots_list = List.map (fun mvd -> (mvd.mvd_loc, mvd.mvd_name)) metavardefn_list in
+  let map_metavarroots = List.map (fun (loc,mvr) -> (loc,mvr,String.uncapitalize mvr)) metavarroots_list in
+  let (conflict,err_msg,loc) = detect_conflicts map_metavarroots in
   if conflict
-  then error ("Renaming of primary metavar \""^err_msg^"\" generates a conflict\n")
-  else map_metavarroots 
+  then error (Some loc) ("Renaming of primary metavar \""^err_msg^"\" generates a conflict\n")
+  else List.map remove_fst map_metavarroots 
 
 let caml_rename sd =
   let map_prod_names = capitalize_prodnames sd in
@@ -1741,7 +1781,7 @@ let rec pp_tex_escape_alltt s =
 
 let isa_filename_check s =
   match string_remove_suffix s ".thy" with
-  | None -> error ("Isabelle filenames must end with .thy\n")
+  | None -> error None ("Isabelle filenames must end with .thy\n")
   | Some s1 -> s1
 
 let hol_filename_check s =
@@ -1781,7 +1821,7 @@ let prod_require_nominal m xd p =
   List.exists
     ( fun bs -> 
       match bs with
-      | Bind (MetaVarExp (mvr,_), nt) -> 
+      | Bind (_, MetaVarExp (mvr,_), nt) -> 
 	  is_nominal_atom m xd (mvd_of_mvr xd (primary_mvr_of_mvr xd mvr) )
       | _ -> false )
     p.prod_bs

src/bounds.ml

@@ -31,12 +31,12 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-exception NotImplementedYet;;
+exception NotImplementedYet;; 
 
 open Types;;
 open Location;;
 
-exception Bounds of string
+exception Bounds of loc * string
 
 
 (** ******************************** *)
@@ -55,7 +55,7 @@ let sie_null = [Si_punct ""]
 
 (* given a bounds environment be and a suffix suff, return at most one bound *)
 (* referenced in the suffix. fail if the suffix references >1 bound*)
-let findbounds (be : bound list) (suff : suffix) : bound option
+let findbounds (be : bound list) (suff : suffix) loc : bound option
     = let rec indices suff = 
       match suff with
       | [] -> []
@@ -66,7 +66,7 @@ let findbounds (be : bound list) (suff : suffix) : bound option
     | [] -> None
     | [i] -> (*print_string ("<<<< "^string_of_int i^" >>>>");flush stdout;*)
         Some(List.nth be i)
-    | _ -> raise (Bounds "findbounds: multiple suffix indices in a suffix")
+    | _ -> raise (Bounds (loc, "findbounds: multiple suffix indices in a suffix"))
 
 (* collect all the nonterms/metavars in a symterm *)
 (* (and their nontermsub-lower-and-top data if they have it), *)
@@ -75,13 +75,13 @@ let rec nt_or_mv_of_symterm (be : bound list) st
 : ((nt_or_mv * subntr_data) * bound option ) list = 
   match st with
   | St_node (_,stnb) -> nt_or_mv_of_symterm_node_body be stnb
-  | St_nonterm (_,_,(ntr,sf)) -> [ (((Ntr ntr),sf),None),findbounds be sf ]  
-  | St_nontermsub (_,ntrl,ntrt,(ntr,sf)) -> [(((Ntr ntr),sf),Some(ntrl,ntrt(*ntru*))),findbounds be sf ]
+  | St_nonterm (_,_,(ntr,sf)) -> [ (((Ntr ntr),sf),None),findbounds be sf (Auxl.loc_of_symterm st) ]  
+  | St_nontermsub (_,ntrl,ntrt,(ntr,sf)) -> [(((Ntr ntr),sf),Some(ntrl,ntrt(*ntru*))),findbounds be sf (Auxl.loc_of_symterm st) ]
   | St_uninterpreted (_,_)-> []
 and nt_or_mv_of_symterm_element be ste =
   match ste with
   | Ste_st (_,st) -> nt_or_mv_of_symterm be st
-  | Ste_metavar (_,_,(mvr,sf)) -> [ (((Mvr mvr),sf),None),findbounds be sf ]
+  | Ste_metavar (_,_,(mvr,sf)) -> [ (((Mvr mvr),sf),None),findbounds be sf (Auxl.loc_of_symterm_element ste) ]
   | Ste_var _ -> []
   | Ste_list (_,stlis)  -> 
       List.concat (List.map (nt_or_mv_of_symterm_list_item be) stlis)
@@ -102,7 +102,7 @@ let nt_or_mv_of_symterms sts =
 
 
 (* check for each Bound_dotform bound that it occurs with only one length constraint. Return the bounds without duplicates *)
-let check_length_consistency : 
+let check_length_consistency loc : 
     ((nt_or_mv* subntr_data) * bound option ) list ->  bound list 
         = 
       function xys ->
@@ -115,7 +115,7 @@ let check_length_consistency :
                 (try  (
                   let i=List.assoc (bd.bd_lower,bd.bd_upper) acc in
                   if i=bd.bd_length then f acc bounds' 
-                  else raise (Bounds ("bound "^Grammar_pp.pp_plain_bound b^" has inconsistent length constraints, \""^Grammar_pp.pp_plain_dots i ^"\" and \""^ Grammar_pp.pp_plain_dots bd.bd_length ^ "\"")))
+                  else raise (Bounds (loc, "bound "^Grammar_pp.pp_plain_bound b^" has inconsistent length constraints, \""^Grammar_pp.pp_plain_dots i ^"\" and \""^ Grammar_pp.pp_plain_dots bd.bd_length ^ "\"")))
                 with
                   Not_found -> f (((bd.bd_lower,bd.bd_upper),bd.bd_length)::acc) bounds' )
             | b::bounds' -> f acc bounds' in
@@ -142,7 +142,7 @@ let check_length_consistency :
 
 (* check for each nt_or_mv (and subntr data) that it doesn't appear with *)
 (* multiple different bounds, and return a list without duplicates *)
-let check_bounds_consistency : 
+let check_bounds_consistency loc : 
     ((nt_or_mv*subntr_data) * bound option) list -> 
       ((nt_or_mv*subntr_data) * bound option) list 
         = function xbos ->
@@ -154,8 +154,9 @@ let check_bounds_consistency :
                 | None -> f ((x,bo)::acc) xbos'
                 | Some bo' -> 
                     (if bo=bo' then f acc xbos'
-                    else 
-                      raise (Bounds ("inconsistent bounds for "^Grammar_pp.pp_plain_nt_or_mv (fst x)^": "^Grammar_pp.pp_plain_bound_option bo ^" and "^Grammar_pp.pp_plain_bound_option bo'  )))) in
+                    else
+                    (* TODO *)
+                      raise (Bounds (loc, "inconsistent bounds for "^Grammar_pp.pp_plain_nt_or_mv (fst x)^": "^Grammar_pp.pp_plain_bound_option bo ^" and "^Grammar_pp.pp_plain_bound_option bo'  )))) in
           f [] xbos
 
 (* split into those without a bound and those with one *)
@@ -328,10 +329,10 @@ let dotenv23 ntmvsn_without_bounds ntmvsn_with_bounds  =
 let bound_extraction m xd loc sts : dotenv * dotenv3 * string = 
   try  
     let x = nt_or_mv_of_symterms sts in
-    let bounds = check_length_consistency x in
+    let bounds = check_length_consistency loc x in
     let pp_bounds = String.concat "  " 
         (List.map Grammar_pp.pp_plain_bound bounds) in
-    let ntmvsn_with_boundopts = check_bounds_consistency x in
+    let ntmvsn_with_boundopts = check_bounds_consistency loc x in
     let ntmvsn_without_bounds,ntmvsn_with_bounds = split_bounded ntmvsn_with_boundopts in
     let bound_with_ntmvsnss = nt_or_mv_per_bound ntmvsn_with_bounds in
     let de1 = dotenv1 m xd bound_with_ntmvsnss in
@@ -347,7 +348,7 @@ let bound_extraction m xd loc sts : dotenv * dotenv3 * string =
         ^ Grammar_pp.pp_plain_dotenv de in
     de, de3, s
   with 
-    Bounds s' -> raise (Bounds (s'^" at "^Location.pp_loc loc))
+    Bounds (_, s') -> raise (Bounds (loc, s'))
 (*  with e ->  *)
  (*   "exception in bound_extraction" *)
 

src/bounds.mli

@@ -31,7 +31,9 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-exception Bounds of string
+open Types;;
+
+exception Bounds of loc * string 
 val nt_or_mv_of_symterms : 
     Types.symterm list ->	 
     ((Types.nt_or_mv * Types.subntr_data) * Types.bound option) list

src/context_pp.ml

@@ -84,7 +84,7 @@ let context_app_rhs m xd lookup (hole:nonterm) (target:nontermroot) (r:rule) (p:
 	( match m with
 	| Caml _ -> Auxl.capitalize_prodnames_in_symterm (List.hd sts)
 	| _ -> List.hd sts )
-      | _ -> Auxl.warning ("internal: multiple parses context fake rhs: "^fake_rhs^"\n"); List.hd sts in
+      | _ -> Auxl.warning None ("internal: multiple parses context fake rhs: "^fake_rhs^"\n"); List.hd sts in
     let sie = [] in
     let ((de1,de2) as de,de3,pptbe) = Bounds.bound_extraction m xd dummy_loc [sts_e]  in
     (true, Some (Grammar_pp.pp_symterm m xd sie de sts_e))

src/coq_induct.ml

@@ -50,7 +50,7 @@ let need_induction m xd r =
 	      | _ -> false)
 	    elb.elb_es
       | Lang_option _ | Lang_sugaroption _ -> 
-	  Auxl.error "interal: option types not implemented in pp_induction\n"
+	  Auxl.error (Some r.rule_loc) "interal: option types not implemented in pp_induction\n"
       | Lang_nonterm (_,_) | Lang_metavar (_,_) | Lang_terminal _ -> false
     in List.exists element_uses_list_nt p.prod_es in
   (not r.rule_meta) && (List.exists uses_list_nt r.rule_ps)