- complete exception reporting in src/core/

- move exception reporting for Ty, Pattern, Term, and Decl
  to Pretty, as it occasionnaly requires some pretty-printing

src/core/decl.ml

@@ -195,7 +195,7 @@ let create_prop_decl k p f = Hsdecl.hashcons (mk_decl (Dprop (k,p,f)))
 
 exception IllegalTypeAlias of tysymbol
 exception ClashIdent of ident
-exception BadLogicDecl of ident
+exception BadLogicDecl of ident * ident
 exception EmptyDecl
 
 let add_id s id =
@@ -233,7 +233,8 @@ let create_ty_decl tdl =
 let create_logic_decl ldl =
   if ldl = [] then raise EmptyDecl;
   let check_decl acc (ls,ld) = match ld with
-    | Some (s,_) when not (ls_equal s ls) -> raise (BadLogicDecl ls.ls_name)
+    | Some (s,_) when not (ls_equal s ls) ->
+        raise (BadLogicDecl (ls.ls_name, s.ls_name))
     | _ -> add_id acc ls.ls_name
   in
   ignore (List.fold_left check_decl Sid.empty ldl);
@@ -534,14 +535,3 @@ let known_add_decl kn d =
   ignore (check_match kn d);
   kn
 
-
-let () = Exn_printer.register
-  (fun fmt exn -> match exn with
-    | UnknownIdent i ->
-      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
-    | UnboundVars vs ->
-      fprintf fmt "anomaly: unknown vars  [%a]" 
-        (Pp.print_iter1 Term.Svs.iter Pp.semi 
-           (fun fmt vs -> pp_print_string fmt vs.vs_name.Ident.id_string)) vs
-        (* TODO other exceptions *)
-    | _ -> raise exn)

src/core/decl.mli

@@ -112,7 +112,7 @@ exception InvalidIndDecl of lsymbol * prsymbol
 exception TooSpecificIndDecl of lsymbol * prsymbol * term
 exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
 
-exception BadLogicDecl of ident
+exception BadLogicDecl of ident * ident
 exception UnboundVars of Svs.t
 exception ClashIdent of ident
 exception EmptyDecl

src/core/env.ml

@@ -66,7 +66,7 @@ let env_tag env = env.env_tag
 
 (** Parsers *)
 
-type read_channel = 
+type read_channel =
   ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
   env -> string -> in_channel -> theory Mnm.t
 
@@ -84,18 +84,18 @@ let register_format name suffixes rc er =
 exception UnknownFormat of string (* parser name *)
 
 let parser_for_file ?name file = match name with
-  | None -> 
-      begin try 
-	let ext = 
+  | None ->
+      begin try
+	let ext =
 	  let s = Filename.chop_extension file in
 	  let n = String.length s in
 	  String.sub file n (String.length file - n)
 	in
 	Hashtbl.find suffixes_table ext
-      with Invalid_argument _ | Not_found -> 
+      with Invalid_argument _ | Not_found ->
 	"why"
       end
-  | Some n -> 
+  | Some n ->
       n
 
 let find_parser table n =
@@ -103,28 +103,33 @@ let find_parser table n =
   with Not_found -> raise (UnknownFormat n)
 
 let read_channel ?name ?debug ?parse_only ?type_only env file ic =
-  let n = parser_for_file ?name file in 
+  let n = parser_for_file ?name file in
   let rc = find_parser read_channel_table n in
   rc ?debug ?parse_only ?type_only env file ic
 
 let report ?name file fmt e =
-  let n = parser_for_file ?name file in 
+  let n = parser_for_file ?name file in
   let er = find_parser error_report_table n in
   er fmt e
 
 let list_formats () =
   let h = Hashtbl.create 17 in
-  let add s p = 
+  let add s p =
     let l = try Hashtbl.find h p with Not_found -> [] in
     Hashtbl.replace h p (s :: l)
   in
   Hashtbl.iter add suffixes_table;
   Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []
 
+(* Exception reporting *)
 
 let () = Exn_printer.register
-  (fun fmt exn -> match exn with
-    | UnknownFormat p -> Format.fprintf fmt "unknown format '%s'" p
-    | _ -> raise exn)
-
+  begin fun fmt exn -> match exn with
+  | TheoryNotFound (sl, s) ->
+      Format.fprintf fmt "Theory not found: %a.%s"
+        (Pp.print_list Pp.dot Format.pp_print_string) sl s
+  | UnknownFormat s ->
+      Format.fprintf fmt "Unknown input format: %s" s
+  | _ -> raise exn
+  end
 

src/core/pretty.ml

@@ -390,3 +390,77 @@ let print_namespace fmt name ns =
   let module P = Print_tree.Make(NsTree) in
   fprintf fmt "@[<hov>%a@]@." P.print (NsTree.Namespace (name, ns))
 
+(* Exception reporting *)
+
+let () = Exn_printer.register
+  begin fun fmt exn -> match exn with
+  | Ty.TypeMismatch (t1,t2) ->
+      fprintf fmt "Type mismatch between %a and %a"
+        print_ty t1 print_ty t2
+  | Ty.BadTypeArity (ts, ts_arg, app_arg) ->
+      fprintf fmt "Bad type arity: type symbol %a must be applied \
+                   to %i arguments, but is applied to %i"
+        print_ts ts ts_arg app_arg
+  | Ty.DuplicateTypeVar tv ->
+      fprintf fmt "Type variable %a is used twice"
+        print_tv tv
+  | Ty.UnboundTypeVars ts ->
+      fprintf fmt "Unbound type variables: %a"
+        (print_list space print_tv) (Stv.elements ts)
+  | Term.BadArity (ls, ls_arg, app_arg) ->
+      fprintf fmt "Bad arity: symbol %a must be applied \
+                   to %i arguments, but is applied to %i"
+        print_ls ls ls_arg app_arg
+  | Term.DuplicateVar vs ->
+      fprintf fmt "Variable %a is used twice" print_vsty vs
+  | Term.FunctionSymbolExpected ls ->
+      fprintf fmt "Not a function symbol: %a" print_ls ls
+  | Term.PredicateSymbolExpected ls ->
+      fprintf fmt "Not a predicate symbol: %a" print_ls ls
+  | Term.NoMatch ->
+      fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
+  | Pattern.ConstructorExpected ls ->
+      fprintf fmt "The symbol %a is not a constructor"
+        print_ls ls
+  | Pattern.NonExhaustive pl ->
+      fprintf fmt "Non-exhaustive pattern list:@\n@[<hov 2>%a@]"
+        (print_list newline print_pat) pl
+  | Decl.IllegalTypeAlias ts ->
+      fprintf fmt
+        "Type symbol %a is a type alias and cannot be declared as algebraic"
+        print_ts ts
+  | Decl.InvalidIndDecl (_ls, pr) ->
+      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
+        print_pr pr
+  | Decl.TooSpecificIndDecl (_ls, pr, t) ->
+      fprintf fmt "Clause %a in inductive predicate declaration \
+          has too type-specific conclusion %a"
+        print_pr pr print_term t
+  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
+      fprintf fmt "Clause %a in inductive predicate declaration \
+          contains a negative occurrence of dependent symbol %a"
+        print_pr pr print_ls ls1
+  | Decl.BadLogicDecl (id1,id2) ->
+      fprintf fmt "Ill-formed definition: idents %s and %s are different"
+        id1.id_string id2.id_string
+  | Decl.UnboundVars svs ->
+      fprintf fmt "Unbound variables: %a"
+        (print_list comma print_vsty) (Svs.elements svs)
+  | Decl.ClashIdent id ->
+      fprintf fmt "Ident %s is defined twice" id.id_string
+  | Decl.EmptyDecl ->
+      fprintf fmt "Empty declaration"
+  | Decl.KnownIdent id ->
+      fprintf fmt "Ident %s is already declared" id.id_string
+  | Decl.UnknownIdent id ->
+      fprintf fmt "Ident %s is not yet declared" id.id_string
+  | Decl.RedeclaredIdent id ->
+      fprintf fmt "Ident %s is already declared, with a different declaration"
+        id.id_string
+  | Decl.NonExhaustiveExpr (pl, e) ->
+      fprintf fmt
+        "Non-exhaustive pattern list:@\n@[<hov 2>%a@]@\nin expression %a"
+        (print_list newline print_pat) pl print_expr e
+  | _ -> raise exn
+  end
+

src/core/task.ml

@@ -200,3 +200,13 @@ let task_goal = function
   | Some { task_decl = Decl { d_node = Dprop (Pgoal,pr,_) }} -> pr
   | _ -> raise GoalNotFound
 
+(* Exception reporting *)
+
+let () = Exn_printer.register
+  begin fun fmt exn -> match exn with
+  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
+  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
+  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
+  | _ -> raise exn
+  end
+

src/core/term.ml

@@ -171,7 +171,7 @@ let rec pat_freevars s pat = match pat.pat_node with
 
 (* smart constructors for patterns *)
 
-exception BadArity of int * int
+exception BadArity of lsymbol * int * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 
@@ -183,7 +183,7 @@ let pat_app fs pl ty =
   let mtch s ty p = ty_match s ty p.pat_ty in
   ignore (try List.fold_left2 mtch s fs.ls_args pl
     with Invalid_argument _ -> raise (BadArity
-      (List.length fs.ls_args, List.length pl)));
+      (fs, List.length fs.ls_args, List.length pl)));
   pat_app fs pl ty
 
 let pat_as p v =
@@ -518,7 +518,7 @@ let f_app_unsafe = f_app
 
 let fs_tuple n =
   let tyl = ref [] in
-  for i = 1 to n 
+  for i = 1 to n
   do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
   let ty = ty_tuple !tyl in
   create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty
@@ -624,8 +624,8 @@ let t_app_inst fs tl ty =
   in
   let mtch s ty t = ty_match s ty t.t_ty in
   try List.fold_left2 mtch s fs.ls_args tl
-  with Invalid_argument _ -> 
-    raise (BadArity (List.length fs.ls_args, List.length tl))
+  with Invalid_argument _ -> raise (BadArity
+    (fs, List.length fs.ls_args, List.length tl))
 
 let t_app fs tl ty = ignore (t_app_inst fs tl ty); t_app fs tl ty
 
@@ -634,7 +634,7 @@ let t_app_infer fs tl =
   let s =
     try List.fold_left2 mtch Mtv.empty fs.ls_args tl
     with Invalid_argument _ -> raise (BadArity
-      (List.length fs.ls_args, List.length tl))
+      (fs, List.length fs.ls_args, List.length tl))
   in
   let ty = match fs.ls_value with
     | Some ty -> ty_inst s ty
@@ -649,8 +649,8 @@ let f_app_inst ps tl =
   in
   let mtch s ty t = ty_match s ty t.t_ty in
   try List.fold_left2 mtch s ps.ls_args tl
-  with Invalid_argument _ -> 
-    raise (BadArity (List.length ps.ls_args, List.length tl))
+  with Invalid_argument _ -> raise (BadArity
+    (ps, List.length ps.ls_args, List.length tl))
 
 let f_app ps tl = ignore (f_app_inst ps tl); f_app ps tl
 
@@ -1444,11 +1444,11 @@ let rec t_subst_term t1 t2 lvl t = if t_equal t t1 then t2 else
 and f_subst_term t1 t2 lvl f =
   f_map_unsafe (t_subst_term t1 t2) (f_subst_term t1 t2) lvl f
 
-let t_subst_term t1 t2 t = 
+let t_subst_term t1 t2 t =
   check_ty_equal t1.t_ty t2.t_ty;
   t_subst_term t1 t2 0 t
 
-let f_subst_term t1 t2 f = 
+let f_subst_term t1 t2 f =
   check_ty_equal t1.t_ty t2.t_ty;
   f_subst_term t1 t2 0 f
 
@@ -1471,7 +1471,7 @@ let rec t_subst_term_alpha t1 t2 lvl t = if t_equal t t1 then t2 else
 and f_subst_term_alpha t1 t2 lvl f =
   f_map_unsafe (t_subst_term_alpha t1 t2) (f_subst_term_alpha t1 t2) lvl f
 
-let t_subst_term_alpha t1 t2 t = 
+let t_subst_term_alpha t1 t2 t =
   check_ty_equal t1.t_ty t2.t_ty;
   t_subst_term_alpha t1 t2 0 t
 

src/core/term.mli

@@ -57,8 +57,8 @@ val create_psymbol : preid -> ty list -> lsymbol
 
 (** {2 Exceptions} *)
 
-exception BadArity of int * int
 exception DuplicateVar of vsymbol
+exception BadArity of lsymbol * int * int
 exception FunctionSymbolExpected of lsymbol
 exception PredicateSymbolExpected of lsymbol
 

src/core/theory.ml

@@ -570,3 +570,23 @@ let tuple_theory n =
 
 let tuple_theory = Util.memo tuple_theory
 
+(* Exception reporting *)
+
+let () = Exn_printer.register
+  begin fun fmt exn -> match exn with
+  | NonLocal id ->
+      Format.fprintf fmt "Non-local ident: %s" id.id_string
+  | CannotInstantiate id ->
+      Format.fprintf fmt "Cannot instantiate a defined ident %s" id.id_string
+  | BadInstance (id1, id2) ->
+      Format.fprintf fmt "Cannot instantiate ident %s with %s"
+        id1.id_string id2.id_string
+  | CloseTheory ->
+      Format.fprintf fmt "Cannot close theory: some namespaces are still open"
+  | NoOpenedNamespace ->
+      Format.fprintf fmt "No opened namespaces"
+  | ClashSymbol s ->
+      Format.fprintf fmt "Symbol %s is already defined in the current scope" s
+  | _ -> raise exn
+  end
+

src/core/ty.ml

@@ -226,27 +226,3 @@ let ty_tuple tyl =
 
 let is_ts_tuple ts = ts == ts_tuple (List.length ts.ts_args)
 
-
-open Format
-let print_tv fmt tv = pp_print_string fmt tv.tv_name.id_string
-let print_ts fmt ts = pp_print_string fmt ts.ts_name.id_string
-
-let rec print_ty fmt ty = match ty.ty_node with
-  | Tyvar v -> print_tv fmt v
-  | Tyapp (ts, []) -> print_ts fmt ts
-  | Tyapp (ts, [t]) -> fprintf fmt "%a@ %a" print_ty t print_ts ts
-  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
-      (Pp.print_list Pp.comma print_ty) l print_ts ts
-
-
-let () = Exn_printer.register
-  (fun fmt exn -> match exn with
-    | TypeMismatch (t1,t2) ->
-        Format.fprintf fmt "Type mismatch between %a and %a" 
-          print_ty t1 print_ty t2
-    | BadTypeArity(ts, ts_arg, app_arg) ->
-      Format.fprintf fmt 
-        "Bad type arity type symbol %a is applied \
-         with %i arguments instead of %i"
-        print_ts ts ts_arg app_arg
-    | _ -> raise exn)