Commits

Thomas Tuerk committed ab99359

cleanup of the type Typed_ast.env_tag

env_tag stored the type of constant as well as for which targets a constant was defined.
By moving the targets into an explicit new field "const_targets" of the record "const_descr",
a lot of code could be simplified. As part of this change, the exception "Ident.No_type",
which was used to report general type errors, was removed from
the identier module and replaced by one in "Reporting_basic".

Comments (0)

Files changed (15)

               const_type = dict_type;
               env_tag = K_let;
               spec_l = l;
+              const_targets = Target.all_targets;
               relation_info = None;
               target_rep = Targetmap.empty;
             }
 open Format
 open Pp
 
-exception No_type of Ast.l * string
-
-let raise_error l msg pp n =
-  let pp ppf = Format.fprintf ppf "%s: %a" msg pp n in
-    raise (No_type(l, Pp.pp_to_string pp))
-
-let raise_error_string l msg =
-    raise (No_type(l, msg))
-
 (* None of the Name.lskips_t can actually have any lskips, but the last one
  * might have parentheses, so Name.t isn't suitable *)
 type t = Ast.lex_skips * Name.t list * Name.t
   let prelim_id = (None, m, (n,None)) in
     List.iter (fun (_, sk) ->
                  if sk <> None && sk <> Some([]) then
-                   raise_error l "illegal whitespace in identifier"
-                     error_pp prelim_id)
+                   raise (Reporting_basic.err_type_pp l "illegal whitespace in identifier"
+                     error_pp prelim_id))
       m;
     match ms with
       | [] ->
           List.iter 
             (fun n ->
                if Name.get_lskip n <> None && Name.get_lskip n <> Some([]) then
-                 raise_error l "illegal whitespace in identifier"
-                   error_pp prelim_id 
+                 raise (Reporting_basic.err_type_pp l "illegal whitespace in identifier"
+                   error_pp prelim_id)
                else
                  ())
             (ms' @ [n]);
     spacing), e.g. [(*Foo*) M . x] *)
 type t
 
-exception No_type of Ast.l * string
-val raise_error_string : Ast.l -> string -> 'a
-val raise_error : Ast.l -> string -> (Format.formatter -> 'a -> unit) -> 'a -> 'b
-
 (** Pretty print *)
 val pp : Format.formatter -> t -> unit
 

src/initial_env.ml

   let defs' = {defs with m_env = m_env'} in
   let c_env'' = Nfmap.fold (fun c_env k c ->
         let c_d = c_env_lookup (Ast.Trans ("add_target_to_def", None)) c_env c in
-        let c_d' = match c_d.env_tag with
-                    | K_val -> { c_d with env_tag = K_target(false,Targetset.singleton target) }
-                    | (K_constr | K_field) -> c_d
-                    | _ -> assert false
-        in 
+        let c_d' = { c_d with const_targets = Targetset.singleton target } in
         c_env_update c_env c c_d')
         c_env' defs.v_env
   in
   with
       | Trans.Trans_error(l,msg) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans (l, msg)))
-      | Ident.No_type(l,msg) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, msg)))
 
 let main () =
   let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in

src/process_file.ml

       (env : Typed_ast.env)
       (ast, end_lex_skips)
       : Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
-  try
     let (env,tast) = Typecheck.check_defs ts mod_path env ast in
       (env,(tast,end_lex_skips))
-  with
-    | Ident.No_type(l,m) ->
-        raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
 
 let check_ast_as_module (ts : Target.Targetset.t) (mod_path : Name.t list)
       (e : Typed_ast.env) 

src/reporting_basic.ml

   | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
   | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
   | Err_lex (p, c) -> ("Lexical error", false, Pos p, "unknown character "^(String.make 1 c))
-  | Err_type (l, m) -> ("Type error", false, Loc l, m)
   | Err_trans_header (l, m) -> ("Header translation error", false,  Loc l, m)
   | Err_internal (l, m) -> ("LEM internal error", false, Loc l, m)
   | Err_rename (l, m) -> ("Renaming error", false, Loc l, m)
+  | Err_type (l, m) -> ("Type error", false, Loc l, m)
 
 exception Fatal_error of error
 
 let err_unreachable b l m = Fatal_error (Err_unreachable (b, l, m))
 let err_general b l m = Fatal_error (Err_general (b, l, m))
 
+let err_type l m = Fatal_error (Err_type (l, m))
+
+let err_type_pp l msg pp n =
+  let pp ppf = Format.fprintf ppf "%s: %a" msg pp n in
+  err_type l (Pp.pp_to_string pp)
 
 let report_error e = 
   let (m1, verb_pos, pos_l, m2) = dest_err e in

src/reporting_basic.mli

   | Err_syntax_locn of Ast.l * string
   | Err_lex of Lexing.position * char
   | Err_type of Ast.l * string
+    (** A typechecking error *)
   | Err_internal of Ast.l * string
   | Err_rename of Ast.l * string
   
 (** [err_unreachable b l m] is an abreviatiation for [Fatal_error (Err_unreachable (b, l, m))] *)
 val err_unreachable : bool -> Ast.l -> string -> exn
 
+(** [err_type l msg] is an abreviatiation for [Fatal_error (Err_type (l, m)], i.e. for a general type-checking error
+    at location [l] with error message [msg]. *)
+val err_type : Ast.l -> string -> exn
+
+(** [err_type l msg pp n] is similar to [err_type]. However it uses the formatter [pp] to format [n], resulting
+    in a string [label]. The error message then has the form [label : msg]. *)
+val err_type_pp : Ast.l -> string -> (Format.formatter -> 'a -> unit) -> 'a -> exn
+
 (** Report error should only be used by main to print the error in the end. Everywhere else,
     raising a [Fatal_error] exception is recommended. *)
 val report_error : error -> 'a
 
+
         begin
           let c_descr = c_env_lookup l_unk env.c_env c.descr in
           match c_descr.env_tag with
-            | K_let | K_target _ ->
+            | K_let ->
                 if c_descr.const_class = [] then
                   None
                 else
           let c_descr = c_env_lookup l_unk env.c_env c.descr in
           match c_descr.env_tag with
             | K_method -> None 
-            | K_let | K_target _ ->
+            | K_let ->
                 if c_descr.const_tparams = [] then None
                 else    
                   let (nvars,tvars) = Types.tnvar_split c_descr.const_tparams in
 open Target
 (* open Typecheck_ctxt *)
 
-let raise_error = Ident.raise_error
-let raise_error_string = Ident.raise_error_string
-
 let r = Ulib.Text.of_latin1
 
 module Refl = struct
     | None -> 
       let mp_rev = List.rev mp_names in
       let p = Path.mk_path (List.rev (List.tl mp_rev)) (List.hd mp_rev) in
-      raise_error l "unknown module" Path.pp p
+      raise (Reporting_basic.err_type_pp l "unknown module" Path.pp p)
 
 (* Assume that the names in mp must refer to modules. Corresponds to judgment
  * look_m_id 'E1(id) gives E2' *)
   let n = Name.strip_lskip (Name.from_x xl) in 
   match lookup_mod_descr_opt e mp' n with
       | None -> 
-          raise_error (Ast.xl_to_l xl) "unknown module"
-            Name.pp (Name.strip_lskip (Name.from_x xl))
+          raise (Reporting_basic.err_type_pp (Ast.xl_to_l xl) "unknown module"
+            Name.pp (Name.strip_lskip (Name.from_x xl)))
       | Some(e) -> e
 
 (* Assume that the names in mp must refer to modules. Corresponds to judgment
   let e = path_lookup l e (List.map (fun (xl,_) -> xl_to_nl xl) mp) in
     match Nfmap.apply e.p_env (Name.strip_lskip (Name.from_x xl)) with
       | None ->
-          raise_error l (Printf.sprintf "unbound type %s" msg)
-            Ident.pp (Ident.from_id i)
+          raise (Reporting_basic.err_type_pp l (Printf.sprintf "unbound type %s" msg)
+            Ident.pp (Ident.from_id i))
       | Some(p, _) -> p
 
 (* Assume that the names in mp must refer to modules. Looks up a name, not
   let e = {e with local_env = e_l} in
     match env_apply e (Name.strip_lskip (Name.from_x xl)) with
       | None ->
-          raise_error l (Printf.sprintf "unbound name")
-            Ident.pp (Ident.from_id i)
+          raise (Reporting_basic.err_type_pp l (Printf.sprintf "unbound name")
+            Ident.pp (Ident.from_id i))
       | Some(nk, p, _) -> (nk, p)
 
 
   match tnv, t.typ with
    | Nv _ , {t = Tne _} -> ()
    | Ty _ , {t = Tne _} -> 
-     raise_error l (Printf.sprintf "type constructor expected type argument, given a length")
-         Ident.pp (Ident.from_id i)
+     raise (Reporting_basic.err_type_pp l (Printf.sprintf "type constructor expected type argument, given a length")
+         Ident.pp (Ident.from_id i))
      (* TODO KG: Improve this type error location and add variable name *)
    | Nv _ , _ -> 
-     raise_error l (Printf.sprintf "type constructor expected length argument, given a type")
-         Ident.pp (Ident.from_id i)
+     raise (Reporting_basic.err_type_pp l (Printf.sprintf "type constructor expected length argument, given a type")
+         Ident.pp (Ident.from_id i))
    | Ty _ , _ -> ()
 
 let rec typ_to_src_t (wild_f : Ast.l -> lskips -> src_t) 
                         typ = { t = Tapp(List.map annot_to_typ sts,p) };
                         rest = (); }
                   else
-                    raise_error l (Printf.sprintf "type constructor expected %d type arguments, given %d" 
+                    raise (Reporting_basic.err_type_pp l (Printf.sprintf "type constructor expected %d type arguments, given %d" 
                                    (List.length td.type_tparams)
                                    (List.length typs))
-                      Ident.pp (Ident.from_id i)
+                      Ident.pp (Ident.from_id i))
               | Some(Tc_class _) ->
-                  raise_error l "type class used as type constructor" 
-                    Ident.pp (Ident.from_id i)
+                  raise (Reporting_basic.err_type_pp l "type class used as type constructor" 
+                    Ident.pp (Ident.from_id i))
           end
     | Ast.Typ_paren(sk1,typ,sk2) ->
         let st = typ_to_src_t wild_f do_tvar do_nvar d e typ in
           typ = { t = Tfn(st1.typ, st2.typ) };
           rest = (); }
       | Tfn(_,{t=Tfn(_,_)}), _ ->
-        raise (Ident.No_type(l,"Too few arguments in indrel function specification (expecting an arrow here)"))
+        raise (Reporting_basic.err_type l "Too few arguments in indrel function specification (expecting an arrow here)")
       | Tfn(t1, _t2), _ -> compare_io t1 typ' (* _t2 is assumed to be bool *)
       | _ -> compare_end typt typ'
   and compare_io _ (Ast.Typ_l(typ,l)) = 
                locn = l;
                typ = { t = Tapp([], p) };
                rest = (); }
-        else raise (Ident.No_type(l,"Only input or output may be used here")) 
-      | _ -> raise (Ident.No_type(l,"Only input or output may be used here"))
+        else raise (Reporting_basic.err_type l "Only input or output may be used here") 
+      | _ -> raise (Reporting_basic.err_type l "Only input or output may be used here")
   and compare_wu (Ast.Typ_l(typ,l)) =
       match typ with
       | Ast.Typ_app(i, []) -> 
         begin match wit with
           | _ when Path.compare p Path.unitpath = 0 -> ()
           | Some(wit_p) when Path.compare p wit_p = 0 -> ()
-          | _ -> raise_error l "Expected unit or the witness" Path.pp p
+          | _ -> raise (Reporting_basic.err_type_pp l "Expected unit or the witness" Path.pp p)
         end;
         { term = Typ_app({id with descr = p},[]);
           locn = l;
           typ = { t = Tapp([],p) };
           rest = (); }
-      | _ -> raise (Ident.No_type(l, "Expected unit or the witness"))
+      | _ -> raise (Reporting_basic.err_type l "Expected unit or the witness")
   and compare_end _ (Ast.Typ_l(typ,l) as typ') = 
    (* The other type should be bool, we don't check that *) 
    try compare_wu typ' 
                 typ = { t = Tapp(List.map (fun x -> x.typ) sub, 
                                  Path.mk_path [] (Name.from_string n)) }; 
                 rest = (); }
-            | _ -> raise (Ident.No_type(l, "Expected list, unique, pure, option, unit or witness"))
+            | _ -> raise (Reporting_basic.err_type l "Expected list, unique, pure, option, unit or witness")
           end
-        | _ -> raise (Ident.No_type(l, "Expected list, unique, pure, option, unit or witness"))
+        | _ -> raise (Reporting_basic.err_type l "Expected list, unique, pure, option, unit or witness")
   in
   compare_spine typt typ
 
     | DupRefs.Has_dups(f, l) ->
         let fd = c_env_lookup l c_env f in
         let n = Path.get_name fd.const_binding in
-        raise_error l "duplicate field name" 
+        raise (Reporting_basic.err_type_pp l "duplicate field name" 
           (fun fmt x -> Format.fprintf fmt "%a" Name.pp x)
-          n
+          n)
     | _ -> ()
 
   (* Ensures that a monad operator is bound to a value constant that has no
     let error_path = mid.descr.mod_binding in    
       match Nfmap.apply v_env (Name.from_rope (r name)) with
         | None ->
-            raise_error mid.id_locn (Printf.sprintf "monad module missing %s" name)
-              Path.pp error_path
+            raise (Reporting_basic.err_type_pp mid.id_locn (Printf.sprintf "monad module missing %s" name)
+              Path.pp error_path)
         | Some(c) ->
             let c_d = c_env_lookup mid.id_locn c_env c in
             if c_d.const_class <> [] then
-              raise_error mid.id_locn (Printf.sprintf "monad operator %s has class constraints" name) 
-                Path.pp error_path
+              raise (Reporting_basic.err_type_pp mid.id_locn (Printf.sprintf "monad operator %s has class constraints" name) 
+                Path.pp error_path)
             else if c_d.const_ranges <> [] then
-              raise_error mid.id_locn (Printf.sprintf "monad operator %s has length constraints" name) 
-                Path.pp error_path
+              raise (Reporting_basic.err_type_pp mid.id_locn (Printf.sprintf "monad operator %s has length constraints" name) 
+                Path.pp error_path)
             else
               (List.map
                  (function 
                    | Nv _ -> 
-                       raise_error mid.id_locn (Printf.sprintf "monad operator %s has length variable type parameters" name) 
-                         Path.pp error_path
+                       raise (Reporting_basic.err_type_pp mid.id_locn (Printf.sprintf "monad operator %s has length variable type parameters" name) 
+                         Path.pp error_path)
                    | Ty(v) -> v)
                  c_d.const_tparams,
                c_d.const_type)
       | None -> assert false
       | Some(Tc_class(tv,methods)) -> (p, tv,methods)
       | Some(Tc_type _) ->
-          raise_error (match id with Ast.Id(_,_,l) -> l)
-            "type constructor used as type class" Ident.pp (Ident.from_id id)
+          raise (Reporting_basic.err_type_pp (match id with Ast.Id(_,_,l) -> l)
+            "type constructor used as type class" Ident.pp (Ident.from_id id))
 
 let tnvar_to_flat (tnvar : Ast.tnvar) : Typed_ast.tnvar =
   match tnvar with
         let (tv',l) = 
           List.find (fun (tv',_) -> TNvar.compare tv tv' = 0) tvs
         in
-          raise_error l "duplicate type variable" TNvar.pp tv'
+          raise (Reporting_basic.err_type_pp l "duplicate type variable" TNvar.pp tv')
     | DupTvs.No_dups(tvs_set) ->
         tvs_set
 
 let anon_error l = 
-  raise (Ident.No_type(l, "anonymous types not permitted here: _"))
+  raise (Reporting_basic.err_type l "anonymous types not permitted here: _")
 
 let rec check_free_tvs (tvs : TNset.t) (Ast.Typ_l(t,l)) : unit =
   match t with
        if TNset.mem (Ty (Tyvar.from_rope x)) tvs then
         ()
        else
-        raise_error l "unbound type variable" 
-          Tyvar.pp (Tyvar.from_rope x)
+        raise (Reporting_basic.err_type_pp l "unbound type variable" 
+          Tyvar.pp (Tyvar.from_rope x))
     | Ast.Typ_fn(t1,_,t2) -> 
         check_free_tvs tvs t1; check_free_tvs tvs t2
     | Ast.Typ_tup(ts) -> 
        if TNset.mem (Nv (Nvar.from_rope x)) nvs then
         ()
        else
-        raise_error l "unbound length variable" Nvar.pp (Nvar.from_rope x)
+        raise (Reporting_basic.err_type_pp l "unbound length variable" Nvar.pp (Nvar.from_rope x))
    | Ast.Nexp_constant _ -> ()
    | Ast.Nexp_sum(n1,_,n2) | Ast.Nexp_times(n1,_,n2) -> check_free_ns nvs n1 ; check_free_ns nvs n2
    | Ast.Nexp_paren(_,n,_) -> check_free_ns nvs n
       if TNset.mem tnv'' env then
          ()
       else
-         raise_error l "unbound type variable" pp_tnvar tnv''
+         raise (Reporting_basic.err_type_pp l "unbound type variable" pp_tnvar tnv'')
     end;
       (((Ident.from_id id, tnv'), sk),
        (p, tnv'')))
       : defn_ctxt = 
   let k = Name.strip_lskip k in
     if Nfmap.in_dom k ctxt.new_defs.m_env then
-      raise_error l "duplicate module definition" Name.pp k
+      raise (Reporting_basic.err_type_pp l "duplicate module definition" Name.pp k)
     else
       ctxt_add 
         (fun x -> x.m_env) 
           (fun ppf -> 
              (Pp.lst "@\nand@\n" pp_class_constraint) ppf cs)
       in
-        raise (Ident.No_type(l, "unsatisfied type class constraints:\n" ^ t1))
+        raise (Reporting_basic.err_type l ("unsatisfied type class constraints:\n" ^ t1))
 
 module Make_checker(T : sig 
                       (* The backend targets that each identifier use must be
             begin
               match Nfmap.apply env.v_env (Name.strip_lskip (Name.from_x xl)) with
                 | None ->
-                    raise_error l "unbound field name" 
-                      Ident.pp (Ident.from_id i)
+                    raise (Reporting_basic.err_type_pp l "unbound field name" 
+                      Ident.pp (Ident.from_id i))
                 | Some(c) ->
                     let c_d = c_env_lookup l T.e.c_env c in
                     if c_d.env_tag = K_method then
-                      raise_error l "method name used as a field name"
-                        Ident.pp (Ident.from_id i)
+                      raise (Reporting_basic.err_type_pp l "method name used as a field name"
+                        Ident.pp (Ident.from_id i))
                     else if c_d.env_tag = K_constr then
-                      raise_error l "constructor name used as a field name"
-                      Ident.pp (Ident.from_id i) 
+                      raise (Reporting_basic.err_type_pp l "constructor name used as a field name"
+                      Ident.pp (Ident.from_id i))
                     else
-                      raise_error l "top level variable binding used as a field name"
-                        Ident.pp (Ident.from_id i)
+                      raise (Reporting_basic.err_type_pp l "top level variable binding used as a field name"
+                        Ident.pp (Ident.from_id i))
             end
         | Some(f) ->
           begin
   let add_binding (pat_e : pat_env) ((v : Name.lskips_t), (l : Ast.l)) (t : t) 
         : pat_env =
     if Nfmap.in_dom (Name.strip_lskip v) pat_e then
-      raise_error l "duplicate binding" Name.pp (Name.strip_lskip v)
+      raise (Reporting_basic.err_type_pp l "duplicate binding" Name.pp (Name.strip_lskip v))
     else
       Nfmap.insert pat_e (Name.strip_lskip v,(t,l))
 
                       let (pats,pat_e) = check_pats l_e acc ps in
                         if (List.length pats <> List.length arg_ts) || (not is_constr) then (
                           if (List.length pats == 0) then (*handle as var*) None else
-                          raise_error l' 
+                          raise (Reporting_basic.err_type_pp l' 
                              (if is_constr then
                                (Printf.sprintf "constructor pattern expected %d arguments, given %d"
                                  (List.length arg_ts) (List.length pats)) 
                               else "non-constructor pattern given arguments")
-                            Ident.pp (Ident.from_id i)
+                            Ident.pp (Ident.from_id i))
                         ) else (
                           let (id,t) = inst_const (id_to_identl i) T.e c in
                           C.equate_types l'' "constructor pattern" t 
                       match mp with
                         | [] ->
                             if ps <> [] then
-                              raise_error l' "non-constructor pattern given arguments" 
-                                Ident.pp (Ident.from_id i)
+                              raise (Reporting_basic.err_type_pp l' "non-constructor pattern given arguments" 
+                                Ident.pp (Ident.from_id i))
                             else
                               let ax = C.new_type () in
                               let n = Name.from_x xl in
                                 (A.mk_pvar l n ret_type, 
                                  add_binding acc (n,l') ax)
                         | _ ->
-                            raise_error l' "non-constructor pattern has a module path" 
-                              Ident.pp (Ident.from_id i)
+                            raise (Reporting_basic.err_type_pp l' "non-constructor pattern has a module path" 
+                              Ident.pp (Ident.from_id i))
                       end
               end
         | Ast.P_record(sk1,ips,sk2,term_semi,sk3) ->
           in
           let id = Ast.Id(List.rev prefix_acc,xl,l_add) in
             if unbound then
-              raise_error (Ast.xl_to_l xl) 
+              raise (Reporting_basic.err_type_pp (Ast.xl_to_l xl) 
                 (if for_field then "unbound field name" else "unbound variable")
-                Ident.pp (Ident.from_id id)
+                Ident.pp (Ident.from_id id))
             else
               (id, None)
       | (xl',sk)::mp' ->
               begin
                 match Nfmap.apply env.m_env n with
                   | None ->
-                      raise_error (Ast.xl_to_l xl') 
+                      raise (Reporting_basic.err_type_pp (Ast.xl_to_l xl') 
                         ("unbound module name or " ^
                          if for_field then "field name" else "variable")
-                        Ident.pp (Ident.from_id id)
+                        Ident.pp (Ident.from_id id))
                   | Some(md) ->
                       get_id_mod_prefix for_field None md.mod_env
                         (Ast.Id(mp',xl,l_add)) 
   (* Corresponds to inst_val 'D,E |- val id : t gives S' and the 
   * var and val cases of check_exp_aux *)
   let check_val (l_e : lex_env) (mp : (Ast.x_l * Ast.lex_skips) list) 
-        (n : Name.lskips_t) (l : Ast.l) : exp =
+        (n : Name.lskips_t) (l : Ast.l) : exp =    
     match lookup_l l_e mp n with
-      | Some(t,l,n) ->
+      | Some(t,l,n) -> 
+          (* The name is bound to a local variable, so return a variable *)
           A.mk_var l n t
       | None -> 
+          (* check whether the name is bound to a constant (excluding fields) *)
           let mp' = List.map (fun (xl,_) -> xl_to_nl xl) mp in
-          let mp'' = List.map (fun (xl,skips) -> (Name.from_x xl, skips)) mp in
           let e = path_lookup l T.e.local_env mp' in
             match Nfmap.apply e.v_env (Name.strip_lskip n) with
-              | None ->
-                  if Ulib.Text.to_string (Name.to_rope (Name.strip_lskip n)) = "Coq.TYPE_EQ" then
-                    prerr_endline "Coq.TYPE_EQ HERE!";
-                  raise_error l "unbound variable" Name.pp (Name.strip_lskip n)
+              | None    -> 
+                  (* not bound to a constant either, so it's unbound *)
+                  raise (Reporting_basic.err_type_pp l "unbound variable" Name.pp (Name.strip_lskip n))
               | Some(c) ->
+                  (* its bound, but is it bound for the necessary targets? *)
                   let cd = c_env_lookup l T.e.c_env c in
-                  begin
-                    match cd.env_tag with
-                      | K_method -> ()
-                      | K_instance -> ()
-                      | K_constr -> ()
-                      | K_field -> ()
-                      | K_val ->
-                          if not (Targetset.is_empty T.targets) then
-                            raise_error l "unbound variable (has a val specification, but no definition)"
-                              Name.pp (Name.strip_lskip n)
-                          else
-                            ()
-                      | (K_let | (* TODO: think about it *) K_relation) -> ()
-                      | K_target(letdef,defined_targets) ->
-                          let undefined_targets = 
-                            Targetset.diff T.targets defined_targets
-                          in
-                            if not letdef && 
-                               not (Targetset.is_empty undefined_targets) then
-                              raise_error l 
-                                (Pp.pp_to_string
-                                   (fun ppf -> 
-                                      Format.fprintf ppf
-                                        "unbound variable for targets {%a}"
-                                        (Pp.lst ";" (fun ppf t -> Pp.pp_str ppf (non_ident_target_to_string t)))
-                                        (Targetset.elements undefined_targets)))
-                                Name.pp (Name.strip_lskip n)
-                            else
-                              ()
-                  end;
+                  let undefined_targets = Targetset.diff T.targets cd.const_targets in
+                  if not (Targetset.is_empty undefined_targets) then
+                     raise (Reporting_basic.err_type_pp l (Pp.pp_to_string (fun ppf -> 
+                        Format.fprintf ppf
+                           "unbound variable for targets {%a}"
+                           (Pp.lst ";" (fun ppf t -> Pp.pp_str ppf (non_ident_target_to_string t)))
+                           (Targetset.elements undefined_targets)
+                        )) Name.pp (Name.strip_lskip n))                     
+                  else ();
+
+                  (* its bound for all the necessary targets, so lets return the constant *)
+                  let mp'' = List.map (fun (xl,skips) -> (Name.from_x xl, skips)) mp in
                   let (id,t) = inst_const (Ident.mk_ident_ast mp'' n l, l) T.e c in
                     C.equate_types l "top-level binding use" t (C.new_type());
                     A.mk_const l id (Some(t))
               A.mk_infix l arg1 id arg2 rt
         | Ast.Record(sk1,r,sk2) ->
             let (res,t,given_fields) = check_fexps l_e r in
-            let one_field = match given_fields with [] -> raise_error_string l "empty records, no fields given" | f::_ -> f in
+            let one_field = match given_fields with [] -> raise (Reporting_basic.err_type l "empty records, no fields given") | f::_ -> f in
             let all_fields = get_field_all_fields l T.e one_field in
             let missing_fields = Util.list_diff all_fields given_fields in
             if (Util.list_longer 0 missing_fields) then
                   let names = List.map field_get_name missing_fields in
                   let names_string = Pp.pp_to_string (fun ppf -> (Pp.lst "@, @" Name.pp) ppf names) in
                   let message = Printf.sprintf "missing %s: %s" (if Util.list_longer 1 missing_fields then "fields" else "field") names_string in
-                  raise_error_string l message
+                  raise (Reporting_basic.err_type l message)
               end;
               C.equate_types l "record expression" t ret_type;
               A.mk_record l sk1 res sk2 rt
             let monad_type_ctor = 
               match Nfmap.apply mod_env.p_env (Name.from_rope (r "t")) with
                 | None ->
-                    raise_error mod_id.id_locn "monad module missing type t"
-                      Ident.pp (Ident.from_id mn)
+                    raise (Reporting_basic.err_type_pp mod_id.id_locn "monad module missing type t"
+                      Ident.pp (Ident.from_id mn))
                 | Some((p,l)) -> p
             in
             let () =
               match Pfmap.apply T.d monad_type_ctor with
                 | None -> assert false
                 | Some(Tc_class _) ->
-                    raise_error mod_id.id_locn "type class used as monad" 
-                      Path.pp monad_type_ctor
+                    raise (Reporting_basic.err_type_pp mod_id.id_locn "type class used as monad" 
+                      Path.pp monad_type_ctor)
                 | Some(Tc_type(td)) -> begin
                     match td.type_tparams with
                      | [Nv _] ->
-                         raise_error mod_id.id_locn "monad type constructor with a number parameter" 
-                          Path.pp monad_type_ctor
+                         raise (Reporting_basic.err_type_pp mod_id.id_locn "monad type constructor with a number parameter" 
+                          Path.pp monad_type_ctor)
                      | [Ty _] -> ()
                      | tnvars ->
-                          raise_error mod_id.id_locn 
+                          raise (Reporting_basic.err_type_pp mod_id.id_locn 
                             (Printf.sprintf "monad type constructor with %d parameters" 
                               (List.length tnvars))
-                            Path.pp monad_type_ctor
+                            Path.pp monad_type_ctor)
                   end
             in
             let (return_tvs, return_type) = 
                       T.d return_type 
                       { t = Tfn({t = Tvar(tv)}, build_monad_type tv) }
                 | tvs ->
-                    raise_error mod_id.id_locn (Printf.sprintf "monad return function with %d type parameters" (List.length tvs))
-                      Path.pp mod_id.descr.mod_binding
+                    raise (Reporting_basic.err_type_pp mod_id.id_locn (Printf.sprintf "monad return function with %d type parameters" (List.length tvs))
+                      Path.pp mod_id.descr.mod_binding)
             in
             let (bind_tvs, bind_type) = 
               check_const_for_do mod_id T.e.c_env mod_env.v_env "bind" in
                         (build_bind_type tv1 tv2);
                       1
                     with
-                      Ident.No_type _ ->
+                      Reporting_basic.Fatal_error (Reporting_basic.Err_type _) ->
                         assert_equal mod_id.id_locn "do/>>="
                           T.d bind_type
                           (build_bind_type tv2 tv1);
                       2)
                 | tvs ->
-                    raise_error mod_id.id_locn (Printf.sprintf "monad >>= function with %d type parameters" (List.length tvs))
-                      Path.pp mod_id.descr.mod_binding
+                    raise (Reporting_basic.err_type_pp mod_id.id_locn (Printf.sprintf "monad >>= function with %d type parameters" (List.length tvs))
+                      Path.pp mod_id.descr.mod_binding)
             in
             let (lns_env,lns) = check_lns l_e monad_type_ctor lns in
             let lns = List.rev lns in
          function
            | Ast.Qb_var(xl) ->
                if is_list then
-                 raise_error (Ast.xl_to_l xl) "unrestricted quantifier in list comprehension"
-                   Name.pp (Name.strip_lskip (Name.from_x xl));
+                 raise (Reporting_basic.err_type_pp (Ast.xl_to_l xl) "unrestricted quantifier in list comprehension"
+                   Name.pp (Name.strip_lskip (Name.from_x xl)));
                let a = C.new_type () in
                let n = Name.from_x xl in
                  (add_binding env (n, Ast.xl_to_l xl) a,
                   Qb_restr(true,s1, pt, s2, et, s3)::lst)
            | Ast.Qb_restr(s1,(Ast.Pat_l(_,l) as p),s2,e,s3) ->
                if is_list then
-                 raise_error l "set-restricted quantifier in list comprehension"
+                 raise (Reporting_basic.err_type_pp l "set-restricted quantifier in list comprehension"
                    (* TODO: Add a pretty printer *)
-                   (fun _ _ -> ()) p;
+                   (fun _ _ -> ()) p);
                let et = check_exp (Nfmap.union l_e env) e in
                let (pt,p_env) = check_pat (Nfmap.union l_e env) p env in
                let a = C.new_type () in
          let const_data = Nfmap.apply T.new_module_env.v_env n in
            match const_data with
              | None ->
+                 (* The constant is not defined yet. Check whether the definition is target
+                    specific and raise an exception in this case. *)
                  begin
                    match def_targets with
                      | Some _ -> 
-                         raise_error l
+                         raise (Reporting_basic.err_type_pp l
                            "target-specific definition without preceding 'val' specification"
-                           Name.pp n
+                           Name.pp n)
                      | None -> ()
                  end
              | Some(c) ->
+                 (* The constant is defined. Check, whether we are alowed to add another, target specific
+                    definition. *)
                  let cd = c_env_lookup l T.e.c_env c in
                  begin
-                   match (cd.env_tag,def_targets) with
-                     | ((K_method|K_instance),_) ->
-                         raise_error l "defined variable is already defined as a class method" 
-                           Name.pp n
-                     | (K_val,_) ->
-                         ()
-                     | (K_let,None) | (K_target(true,_),None)->
-                         raise_error l
-                           "defined variable is already defined"
-                           Name.pp n
-                     | (K_let,Some _) ->
-                         raise_error l
-                           "target-specific definition without preceding 'val' specification"
-                           Name.pp n
-                     | (K_constr, _) ->
-                         raise_error l "defined variable is already defined as a constructor"
-                           Name.pp n
-                     | (K_relation, _) ->
-                         raise_error l "defined variable is already defined as a relation"
-                           Name.pp n
-                     | (K_field, _) ->
-                         raise_error l "defined variable is already defined as a field"
-                           Name.pp n
-                     | (K_target(false,_), None) -> 
-                         ()
-                     | (K_target(_,prior_targets),Some(def_targets)) ->
-                         let duplicate_targets = 
-                           Targetset.inter prior_targets def_targets
-                         in
-                         let relevant_duplicate_targets =
-                           Targetset.inter duplicate_targets T.targets
-                         in
-                           if not (Targetset.is_empty relevant_duplicate_targets) then
-                             raise_error l
+                   match cd.env_tag with
+                     | K_let ->
+                         (* only let's (and vals) can aquire more targets,
+                            check whether only new targets are added *)
+                         let duplicate_targets = (match def_targets with
+                            | None -> cd.const_targets
+                            | Some dt -> Targetset.inter cd.const_targets dt) in
+                         let relevant_duplicate_targets = Targetset.inter duplicate_targets T.targets in
+                         let _ = if not (Targetset.is_empty relevant_duplicate_targets) then
+                             raise (Reporting_basic.err_type_pp l
                                (Printf.sprintf "defined variable already has a %s-specific definition" 
                                   (non_ident_target_to_string 
                                      (Targetset.choose relevant_duplicate_targets)))
-                               Name.pp n 
-                 end;
-                 let a = C.new_type () in
-                   C.equate_types cd.spec_l "applying val specification" a cd.const_type;
-                   C.equate_types l "applying val specification" a t
+                               Name.pp n) in
+                         
+                         (* enforce that the already defined constant and the new one have the same type. *)
+                         let a = C.new_type () in begin
+                           C.equate_types cd.spec_l "applying val specification" a cd.const_type;
+                           C.equate_types l "applying val specification" a t
+                         end
+                     | _ -> 
+                         (* everything else can't be extended, so raise an exception *)
+                         raise (Reporting_basic.err_type_pp l ("defined variable is already defined as a " ^ 
+                              (env_tag_to_string cd.env_tag))
+                           Name.pp n)
+                 end
       ) def_env;
     let Tconstraints(tnvars, constraints,l_constraints) = C.inst_leftover_uvars l in
       Nfmap.iter
     Nfmap.iter
       (fun n (t,l) ->
          if not (def_targets = None) then
-           raise_error l "instance method must not be target specific"
-             Name.pp n;
+           raise (Reporting_basic.err_type_pp l "instance method must not be target specific"
+             Name.pp n);
          let const_ref = Nfmap.apply T.e.local_env.v_env n in
          let const_data = Util.option_map (fun c -> c_env_lookup l T.e.c_env c) const_ref in
          match const_data with
                    C.equate_types cd.spec_l "applying val specification" a spec_typ;
                    C.equate_types l "applying val specification" a t
              | _ -> 
-                 raise_error l "instance method not bound to class method"
-                   Name.pp n)
+                 raise (Reporting_basic.err_type_pp l "instance method not bound to class method"
+                   Name.pp n))
       def_env;
     let Tconstraints(tnvars, constraints,l_constraints) = C.inst_leftover_uvars l in
       unsat_constraint_err l constraints;
         let (tv',l) = 
           List.find (fun (tv',_) -> TNvar.compare tv tv' = 0) tvs
         in
-          raise_error l "duplicate type variable" TNvar.pp tv'
+          raise (Reporting_basic.err_type_pp l "duplicate type variable" TNvar.pp tv')
     | DupTvs.No_dups(tvs_set) ->
         tvs_set
 
 let anon_error l = 
-  raise (Ident.No_type(l, "anonymous types not permitted here: _"))
+  raise (Reporting_basic.err_type l "anonymous types not permitted here: _")
 
 let rec check_free_tvs (tvs : TNset.t) (Ast.Typ_l(t,l)) : unit =
   match t with
        if TNset.mem (Ty (Tyvar.from_rope x)) tvs then
         ()
        else
-        raise_error l "unbound type variable" 
-          Tyvar.pp (Tyvar.from_rope x)
+        raise (Reporting_basic.err_type_pp l "unbound type variable" 
+          Tyvar.pp (Tyvar.from_rope x))
     | Ast.Typ_fn(t1,_,t2) -> 
         check_free_tvs tvs t1; check_free_tvs tvs t2
     | Ast.Typ_tup(ts) -> 
        if TNset.mem (Nv (Nvar.from_rope x)) nvs then
         ()
        else
-        raise_error l "unbound length variable" Nvar.pp (Nvar.from_rope x)
+        raise (Reporting_basic.err_type_pp l "unbound length variable" Nvar.pp (Nvar.from_rope x))
    | Ast.Nexp_constant _ -> ()
    | Ast.Nexp_sum(n1,_,n2) | Ast.Nexp_times(n1,_,n2) -> check_free_ns nvs n1 ; check_free_ns nvs n2
    | Ast.Nexp_paren(_,n,_) -> check_free_ns nvs n
       (constraints : (Path.t * Types.tnvar) list)
       (* The length constraints that the definition's length variables must satisfy *) 
       (lconstraints : Types.range list)
-      (* The status for just this definition, must be either K_let or
-       * K_target(false, ts), and if it is K_target, there must be a preceding
-       * K_val *)
       (env_tag : env_tag) 
+      (new_targs_opt : Targetset.t option) 
       (l_env : lex_env) 
       : defn_ctxt =
+  let new_targs = Util.option_default all_targets new_targs_opt in
   let (c_env, new_env) =
     Nfmap.fold
       (fun (c_env, new_env) n (t,l) ->
         match Nfmap.apply ctxt.new_defs.v_env n with
           | None ->
+              (* not present yet, so insert a new one *)
               let c_d = 
                     { const_binding = Path.mk_path mod_path n;
                       const_tparams = tnvars;
                       const_type = t;
                       spec_l = l;
                       env_tag = env_tag;
+                      const_targets = new_targs;
 		      relation_info = None;
                       target_rep = Targetmap.empty } in
               let (c_env', c) = c_env_save c_env None c_d in
           | Some(c) -> 
               (* The definition is already in the context.  Here we just assume
                * it is compatible with the existing definition, having
-               * previously checked it. *) 
+               * previously checked it. So, we only need to update the set of targets. *) 
               let c_d = c_env_lookup l c_env c in
-              let tag =
-                match (c_d.env_tag, env_tag) with
-                  | (K_val, K_val) | (K_let,K_let) | ((K_method|K_instance|K_field|K_constr),_) 
-                  | (_,(K_method|K_instance|K_field|K_constr)) | (K_let, K_val) | (K_target _, K_val) -> 
-                      assert false
-                  | (K_val, K_let) -> K_target(true, Targetset.empty)
-                  | (K_val, K_target(letdef,targets)) -> 
-                      K_target(letdef,targets)
-                  | (K_let, K_target(_,targets)) -> K_target(true,targets)
-                  | (K_target(_,targets),K_let) -> K_target(true,targets)
-                  | (K_target(letdef1,targets1), K_target(letdef2,targets2)) ->
-                      K_target(letdef1||letdef2, 
-                               Targetset.union targets1 targets2) in
-              let (c_env', c) = c_env_save c_env (Some c) { c_d with env_tag = tag } in
+              let targs = Targetset.union c_d.const_targets new_targs in
+              let (c_env', c) = c_env_save c_env (Some c) { c_d with const_targets = targs } in
               (c_env', Nfmap.insert new_env (n, c)))
       (ctxt.ctxt_c_env, Nfmap.empty) l_env
   in
             match Pfmap.apply context.all_tdefs p with
               | None -> assert false
               | Some(Tc_type _) ->
-                  raise_error l "duplicate type constructor definition"
-                    Name.pp tn
+                  raise (Reporting_basic.err_type_pp l "duplicate type constructor definition"
+                    Name.pp tn)
               | Some(Tc_class _) ->
-                  raise_error l "type constructor already defined as a type class" 
-                    Name.pp tn
+                  raise (Reporting_basic.err_type_pp l "type constructor already defined as a type class" 
+                    Name.pp tn)
           end
   in
   let regex = match regex with | Some(Name_restrict(_,_,_,_,r,_)) -> Some r | _ -> None in
               if (regex = None)
                 then add_d_to_ctxt new_ctxt type_path 
                         (mk_tc_type_abbrev (List.map fst tvs) src_t.typ)
-                else raise_error l "Type abbreviations may not restrict identifier names" Name.pp tn
+                else raise (Reporting_basic.err_type_pp l "Type abbreviations may not restrict identifier names" Name.pp tn)
         | None ->
             add_d_to_ctxt new_ctxt type_path 
               (mk_tc_type (List.map fst tvs) regex)
       let (n,l) = xl_to_nl name in
       if ((Name.to_string (Name.strip_lskip n)) = "name")
          then Some(Name_restrict(sk1,(n,l),sk2,sk3,regex,sk4))
-      else raise_error l "Type name restrictions must begin with 'name'" Name.pp (Name.strip_lskip n)
+      else 
+         raise (Reporting_basic.err_type_pp l "Type name restrictions must begin with 'name'" Name.pp (Name.strip_lskip n))
 
 (* Check a type definition and add it to the context.  mod_path is the path to
  * the enclosing module.  Ignores any constructors or fields, just handles the
            match Nfmap.apply ctxt.new_defs.f_env fn' with
              | None -> ()
              | Some _ ->
-                 raise_error l' "duplicate field name definition"
-                   Name.pp fn'
+                 raise (Reporting_basic.err_type_pp l' "duplicate field name definition"
+                   Name.pp fn')
          in
          let (c_env', f) = c_env_save ctxt.ctxt_c_env None field_descr in
          let ctxt = {ctxt with ctxt_c_env = c_env'} in
         let ctn = Name.from_x ctor_name in
         let ctn' = Name.strip_lskip ctn in
         let constr_descr : const_descr = build_descr ctn' l' src_ts in        
-        let () = 
+        let () = (* check, whether the constructor name is already used *)
           match Nfmap.apply ctxt.new_defs.v_env ctn' with
-            | None -> ()
+            | None -> (* not used, so everything OK*) ()
             | Some(c) ->
-                begin
+                begin (* already used, produce the right error message *)
                   let c_d = c_env_lookup l' ctxt.ctxt_c_env c in
-                  match c_d.env_tag with
-                    | K_method|K_instance ->
-                        raise_error l' "constructor already defined as a class method name"
-                          Name.pp ctn'
-                    | K_field ->
-                        raise_error l' "constructor already defined as a field"
-                          Name.pp ctn'
-                    | K_constr -> raise_error l' "duplicate constructor definition" Name.pp ctn'
-                    | K_val | K_let | K_target _ ->
-                       raise_error l' "constructor already defined as a top-level variable binding" 
-                         Name.pp ctn'
+                  let err_msg = begin
+                    match c_d.env_tag with
+                      | K_constr -> "duplicate constructor definition"
+                      | _ -> "constructor already defined as a " ^ (env_tag_to_string c_d.env_tag)
+                  end in
+                  raise (Reporting_basic.err_type_pp l' err_msg Name.pp ctn')
                 end
         in
         let (c_env', c) = c_env_save ctxt.ctxt_c_env None constr_descr in
                    spec_l = l;
                    env_tag = K_field;
                    relation_info = None;
+                   const_targets = all_targets;
                    target_rep = Targetmap.empty })
               context
               (Seplist.map (fun (x,y,src_t) -> (x,y,src_t)) recs)
                    spec_l = l;
                    env_tag = K_constr;
                    relation_info = None;
+                   const_targets = all_targets;
                    target_rep = Targetmap.empty})
               tvs_set
               context
   let (src_cp, tyvars, tnvarset, (sem_cp,sem_rp)) = check_constraint_prefix ctxt cp in 
   let () = check_free_tvs tnvarset typ in
   let src_t = typ_to_src_t anon_error ignore ignore ctxt.all_tdefs ctxt.cur_env typ in
-  let () = 
+  let () = (* check that the name is really fresh *)
     match Nfmap.apply ctxt.new_defs.v_env n' with
       | None -> ()
-      | Some(c) ->
+      | Some(c) -> (* not fresh, so raise an exception *)
           begin 
             let c_d = c_env_lookup l' ctxt.ctxt_c_env c in
-            match c_d.env_tag with
-              | K_method | K_instance->
-                  raise_error l' "specified variable already defined as a class method name"
-                    Name.pp n'
-              | K_field ->
-                  raise_error l' "specified variable already defined as a field"
-                    Name.pp n'
-              | K_constr ->
-                  raise_error l' "specified variable already defined as a constructor"
-                    Name.pp n'
-              | K_val | K_target _ -> 
-                  raise_error l' "specified variable already specified"
-                    Name.pp n'
-              | K_let -> 
-                  raise_error l' "specified variable already defined"
-                    Name.pp n'
+            let err_message = "specified variable already defined as a " ^ (env_tag_to_string c_d.env_tag) in
+            raise (Reporting_basic.err_type_pp l' err_message Name.pp n')
           end
   in
   let v_d =
       const_ranges = sem_rp;
       const_type = src_t.typ;
       spec_l = l;
-      env_tag = K_val;
+      env_tag = K_let;
+      const_targets = Targetset.empty;
       relation_info = None;
       target_rep = Targetmap.empty }
   in
       | Some(c) ->
           begin
             let c_d = c_env_lookup l' ctxt.ctxt_c_env c in
-            match c_d.env_tag with
-              | K_method | K_instance ->
-                  raise_error l' "duplicate class method definition"
-                    Name.pp n'
-              | K_constr ->
-                  raise_error l' "class method already defined as a constructor"
-                    Name.pp n'
-              | K_field ->
-                  raise_error l' "class method already defined as a field"
-                    Name.pp n'
-              | K_val | K_let | K_target _ ->
-                  raise_error l' "class method already defined as a top-level variable"
-                    Name.pp n'
+            let err_message = 
+              match c_d.env_tag with
+                | (K_method | K_instance) -> "duplicate class method definition"
+                | _ -> "class method already defined as a " ^ (env_tag_to_string c_d.env_tag)
+            in
+            raise (Reporting_basic.err_type_pp l' err_message Name.pp n')
           end
   in
   let v_d =
       const_type = src_t.typ;
       spec_l = l;
       env_tag = K_method;
+      const_targets = all_targets;
       relation_info = None;
       target_rep = Targetmap.empty }
   in
              targs
              all_targets)
 
-let target_opt_to_env_tag : Targetset.t option -> env_tag = function
-  | None -> K_let
-  | Some(ts) -> K_target(false,ts)
-
 let check_target_opt : Ast.targets option -> Typed_ast.targets_opt = function
   | None -> None
   | Some(Ast.Targets_concrete(s1,targs,s2)) -> 
   let (nls, pL, ty_opt, sk, e) = begin match lb_aux with
     | Let_val (p, ty_opt, sk, e) -> begin
          let nls = match Pattern_syntax.pat_to_ext_name p with 
-                  | None -> raise_error_string l "unsupported pattern in top-level let definition"
+                  | None -> raise (Reporting_basic.err_type l "unsupported pattern in top-level let definition")
                   | Some nls -> nls in
          (nls, [], ty_opt, sk, e)
       end
   in
   let target_set_opt = target_opt_to_set_opt target_opt_ast in
   let target_opt = check_target_opt target_opt_ast in
-  let env_tag = target_opt_to_env_tag target_set_opt in
 
   let module Checker = Make_checker(T) in
   match vd with
       | Ast.Let_def(sk,_,lb) ->
           let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set_opt l lb in 
           let _ = unsat_constraint_err l constraints in
-          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
+          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints K_let target_set_opt e_v in
           let (vd : val_def) = letbind_to_funcl_aux sk target_opt ctxt' lb in
           (ctxt', e_v, vd, Tconstraints(tnvs,constraints,lconstraints))
       | Ast.Let_rec(sk1,sk2,_,funcls) ->
           let funcls = Seplist.from_list funcls in
           let (lbs,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_funs for_method target_set_opt l funcls in 
           let _ = unsat_constraint_err l constraints in
-          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
+          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints K_let target_set_opt e_v in
           let fauxs = letbinds_to_funcl_aux_rec l ctxt' lbs in
             (ctxt', e_v, (Fun_def(sk1,Some sk2,target_opt,fauxs)), Tconstraints(tnvs,constraints,lconstraints))
       | Ast.Let_inline (sk1,sk2,_,lb) -> 
           let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set_opt l lb in 
           let _ = unsat_constraint_err l constraints in
-          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
+          let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints K_let target_set_opt e_v in
           let (nls, n_ref, _, pL, ty_opt, sk3, et) = letbind_to_funcl_aux_dest ctxt' lb in
           let args = match Util.map_all Pattern_syntax.pat_to_ext_name pL with
-                       | None -> raise_error_string l "non-variable pattern in inline"
+                       | None -> raise (Reporting_basic.err_type l "non-variable pattern in inline")
                        | Some a -> a in         
           let new_tr = CR_inline (l, args, et) in
           let d = c_env_lookup l ctxt'.ctxt_c_env n_ref in
           let (n, l) = xl_to_nl name in
           let n_s = Name.strip_lskip n in
           let _ = if (NameSet.mem n_s ctxt.lemmata_labels) then 
-                      raise_error l
+                      raise (Reporting_basic.err_type_pp l
                         "lemmata-label already used"
-                         Name.pp n_s
+                         Name.pp n_s)
                    else () in
           (add_lemma_to_ctxt ctxt n_s,  sk0, lty', target_opt, Some ((n,l), sk1), sk2, exp, sk3)
 
       : TNset.t * Ulib.Text.t =
   let l = src_t.locn in 
   let err () = 
-    raise_error l "class instance type must be a type constructor applied to type variables"
-      pp_type src_t.typ
+    raise (Reporting_basic.err_type_pp l "class instance type must be a type constructor applied to type variables"
+      pp_type src_t.typ)
   in
   let to_tnvar src_t = 
     match src_t.term with
         begin
           match Pfmap.apply ctxt.all_tdefs p.descr with
             | Some(Tc_type {type_abbrev = Some _}) ->
-                raise_error p.id_locn "type abbreviation in class instance type"
-                  Ident.pp (match p.id_path with | Id_some id -> id | Id_none _ -> assert false)
+                raise (Reporting_basic.err_type_pp p.id_locn "type abbreviation in class instance type"
+                  Ident.pp (match p.id_path with | Id_some id -> id | Id_none _ -> assert false))
             | _ -> 
                 (tvs_to_set (List.map to_tnvar ts),
                  Name.to_rope (Path.to_name p.descr))
                 let cd' = List.fold_left (fun cd t -> 
                    match constant_descr_rename t (Name.strip_lskip n') l cd with
                      | Some (cd', _) -> cd'
-                     | None -> raise_error_string l "internal error: count not rename constant. This is a bug and should not happen.")
+                     | None -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, "could not rename constant. This is a bug and should not happen."))))
                    cd (targets_opt_to_list targs) in
                 let c_env' = c_env_update ctxt.ctxt_c_env c cd' in
                 {ctxt with ctxt_c_env = c_env'}
           let module C = Exps_in_context(struct let env_opt = None let avoid = None end) in
           let newctxt = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs)
             constraints lconstraints
-            (target_opt_to_env_tag target_set_opt) e_v in
+            K_relation target_set_opt e_v in
 
           let add_const_ns (RName(sk1, rel_name, _, sk2, rel_type, witness_opt, check_opt, indfns_opt, sk3)) = begin
               let n = Name.strip_lskip rel_name in
                     match Pfmap.apply ctxt.all_tdefs p with
                       | None -> assert false
                       | Some(Tc_class _) ->
-                          raise_error l' "duplicate type class definition" 
-                            Name.pp cn'
+                          raise (Reporting_basic.err_type_pp l' "duplicate type class definition" 
+                            Name.pp cn')
                       | Some(Tc_type _) ->
-                          raise_error l' "type class already defined as a type constructor" 
-                            Name.pp cn'
+                          raise (Reporting_basic.err_type_pp l' "type class already defined as a type constructor" 
+                            Name.pp cn')
                   end
           in
           let ctxt =
                    const_type = { t = Tfn ({ t = Tapp (tparams_t, type_path) }, t) };
                    spec_l = l;
                    env_tag = K_field;
+                   const_targets = all_targets;
                    relation_info = None;
                    target_rep = Targetmap.empty })
               ctxt''
           let unused_tvs = TNset.diff tnvarset used_tvs in
           let _ = 
             if not (TNset.is_empty unused_tvs) then
-              raise_error l "instance type does not use all type variables"
-                TNset.pp unused_tvs
+              raise (Reporting_basic.err_type_pp l "instance type does not use all type variables"
+                TNset.pp unused_tvs)
           in
           let (p, tv, methods) = lookup_class_p ctxt id in
           let instance_name = 
                               | Some(_,l) -> l
                               | _ -> assert false
                           in
-                            raise_error l "duplicate definition in an instance" 
-                              Name.pp v
+                            raise (Reporting_basic.err_type_pp l "duplicate definition in an instance" 
+                              Name.pp v)
                       | None ->
                           Nfmap.union e_v' e_v
                  in
               (fun (n,t) ->
                  match Nfmap.apply e_v n with
                    | None ->
-                       raise_error l "missing class method" Name.pp n
+                       raise (Reporting_basic.err_type_pp l "missing class method" Name.pp n)
                    | Some(t) ->
                        ())
               methods
                             (* TODO: check the following *)
                             env_tag = K_instance;
                             spec_l = l;
+                            const_targets = all_targets;
                             relation_info = None;
                             target_rep = Targetmap.empty; } in
                  let (c_env', c) = c_env_save c_env None c_d in
                     | Some(Tc_type { type_varname_regexp = Some(restrict) }) -> 
                        if (Str.string_match (Str.regexp restrict) id 0) 
                          then None
-                         else  raise_error (exp_to_locn e) 
+                         else  raise (Reporting_basic.err_type_pp (exp_to_locn e) 
                                ("variables with type " ^ t_to_string (exp_to_typ e) ^ " are restricted to names matching the regular expression " ^ restrict)
-                               Name.pp (Name.strip_lskip n))
+                               Name.pp (Name.strip_lskip n)))
                  | _ -> None
               end
   | _ -> None
                     | Some(Tc_type { type_varname_regexp = Some(restrict) }) -> 
                        if (Str.string_match (Str.regexp restrict) id 0) 
                          then None
-                         else  raise_error p.locn 
+                         else  raise (Reporting_basic.err_type_pp p.locn 
                                ("variables with type " ^t_to_string p.typ ^ " are restricted to names matching the regular expression " ^ restrict)
-                               Name.pp (Name.strip_lskip n) )
+                               Name.pp (Name.strip_lskip n) ))
                  | _ -> None
               end
   | _ -> None
 type 'a lskips_seplist = ('a, lskips) Seplist.t
 
 type env_tag = 
-  | K_method
-  | K_instance
+  | K_let
   | K_field
   | K_constr
-  | K_val
-  | K_let
   | K_relation
-  | K_target of bool * Targetset.t
+  | K_method
+  | K_instance
 
 type ('a,'b) annot = { term : 'a; locn : Ast.l; typ : t; rest : 'b }
 
                     const_type : t; 
 		    relation_info: rel_info option;
                     env_tag : env_tag;
+                    const_targets : Targetset.t;
                     spec_l : Ast.l;
                     target_rep : const_target_rep Targetmap.t }
 
          match Cdmap.apply c_env_map c with
            | None -> 
              let m = Format.sprintf "constant-id %d not present in environment" c in
-             raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
+             raise (Reporting_basic.err_type l m)
            | Some(cd) -> cd
 
 let c_env_update (c_env_count, c_env_map) c_id c_d =
     | K_field -> Format.fprintf ppf "field"
     | K_constr -> Format.fprintf ppf "constr"
     | K_instance -> Format.fprintf ppf "instance"
-    | K_val -> Format.fprintf ppf "val"
     | K_let -> Format.fprintf ppf "let"
     | K_relation -> Format.fprintf ppf "relation"
-    | K_target(exists_general, targets) -> 
-        Format.fprintf ppf "target(%b,%s)"
-        exists_general "???"
 
 let pp_const_descr ppf c =
   fprintf ppf "@[<2>forall@ (@[%a@]).@ @[%a@]@ @[%a@]@ =>@ %a@]@ (%a)@ %a"
                 | (_,None) -> v1
                 | (Some(v),Some(v')) ->
                     if for_pat then
-                      raise (Ident.No_type(l, "Duplicate variable in a pattern: " ^
+                      raise (Reporting_basic.err_type l ("Duplicate variable in a pattern: " ^
                                         Pp.pp_to_string (fun ppf -> Name.pp ppf k)))
                     else
                       begin
                         try
                           type_eq l "merge_free_env" v v'
                         with
-                          | Ident.No_type(l,s) ->
-                              raise (Ident.No_type(l,s ^ "\n in merging: " ^ Pp.pp_to_string (fun ppf -> Name.pp ppf k)))
+                          | Reporting_basic.Fatal_error (Reporting_basic.Err_type (l,s)) ->
+                              raise (Reporting_basic.err_type l (s ^ "\n in merging: " ^ Pp.pp_to_string (fun ppf -> Name.pp ppf k)))
                       end;
                     v1)
            e_res
                  try
                    type_eq l "bind_free_env" v v'
                  with
-                   | Ident.No_type(l,s) ->
-                       raise (Ident.No_type(l,s ^ "\nin binding " ^ Pp.pp_to_string (fun ppf -> Name.pp ppf k)))
+                   | Reporting_basic.Fatal_error (Reporting_basic.Err_type (l,s)) ->
+                       raise (Reporting_basic.err_type l (s ^ "\nin binding " ^ Pp.pp_to_string (fun ppf -> Name.pp ppf k)))
                end;
                Nfmap.remove e_res k)
       exp_env
                  type_eq l "mk_app" t1 e2.typ;
                  Some t2
              | _ -> 
-                 raise (Ident.No_type(l, "non-function in application")))
+                 raise (Reporting_basic.err_type l "non-function in application"))
     in
       { term = App(e1,e2);
         locn = l;
                          type_eq l "mk_infix" t3 e3.typ;
                          t4
                      | _ -> 
-                         raise (Ident.No_type(l, "non-function in infix application"))
+                         raise (Reporting_basic.err_type l "non-function in infix application")
                  end
              | _ ->
-                 raise (Ident.No_type(l, "non-function in infix application"))))
+                 raise (Reporting_basic.err_type l "non-function in infix application")))
     in
       match exp_to_term e2 with
         | Var _ | Constant _ -> 
                         if allow_duplicates then
                           Some(v')
                         else
-                          raise (Ident.No_type(l, "Duplicate variable in a pattern: " ^
+                          raise (Reporting_basic.err_type l ("Duplicate variable in a pattern: " ^
                                                    Pp.pp_to_string (fun ppf -> Name.pp ppf k))))
                bindings
                p.rest.pvars

src/typed_ast.mli

 (** Get only the comments (and a trailing space) *)
 val lskips_only_comments : lskips list -> lskips
 
-(** What kind of top-level definition a particular constant is *)
+(** [env_tag] is used by [const_descr] to describe the type of constant. Constants can be defined in multiple ways:
+    the most common way is via a [let]-statement. Record-type definitions introduce fields-accessor 
+    functions and variant types introduce constructors. There are methods, instances and relations as well.
+    A [let] definition can be made via a [val] definition and multiple, target specific lets. *)
 type env_tag = 
+  | K_let      (** A let definition, the most common case. Convers val as well, details see above. *)
+  | K_field    (** A field *)
+  | K_constr   (** A type constructor *)
+  | K_relation (** A relation *)
   | K_method   (** A class method *)
-  | K_instance  (** A method instance *)
-  | K_field   (** A field *)
-  | K_constr (** A type constructor *)
-  | K_val  (** A val specification that has no definitions *)
-  | K_let   (** A let definition with no target specific definitions or val spec *)
-  | K_relation (** A definition coming from a relation *)
-  | K_target of bool * Target.Targetset.t
-      (** A definition that also has a val specification. There is a target-specific
-          definition for each target in the set, and the bool is true if there is a
-          target non-specific definition *)
+  | K_instance (** A method instance *)
 
 
 type ('a,'b) annot = { term : 'a; locn : Ast.l; typ : Types.t; rest : 'b }
     env_tag : env_tag;
     (** What kind of definition it is. *)
 
+    const_targets : Target.Targetset.t;
+    (** If the constant is defined for all targets [None], otherwise the set of targets, it is defined for. *)
+
     spec_l : Ast.l;
     (** The location for the first occurrence of a definition/specification of
-        this constant *)
-
+        this constant. *)
+    
     target_rep : const_target_rep Target.Targetmap.t; 
     (** Target-specific representation of for this constant *)
   }

src/typed_ast_syntax.ml

 let space_init_ws ws = (space, ws)
 
 
+let env_tag_to_string = function
+    | K_field    -> "field"
+    | K_constr   -> "constructor"
+    | K_instance -> "instance of a class method"
+    | K_method   -> "class method"
+    | K_let      -> "top-level variable binding"
+    | K_relation -> "relation"
+
+
+
 (* -------------------------------------------------------------------------- *)
 (* navigating environments                                                    *)
 (* -------------------------------------------------------------------------- *)
 let mk_app_exp d e1 e2 =
   let l = Ast.Trans ("mk_app_exp", None) in
   let b_ty = match Types.dest_fn_type (Some d) (exp_to_typ e1) with
-               | None -> raise (Ident.No_type(l, "non-function in application"))
+               | None -> raise (Reporting_basic.err_type l "non-function in application")
                | Some (_, b_ty) -> b_ty
   in
   C.mk_app l e1 e2 (Some b_ty)

src/typed_ast_syntax.mli

 (** [val_def_get_name d] tries to extract the name of the defined function. *)
 val val_def_get_name : def_aux -> Name.t option 
 
-
-
+(** [env_tag_to_string tag] formats [tag] as a string. This functions should only be used
+    for human-readable output in e.g. error-messages. *)
+val env_tag_to_string : env_tag -> string
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+open Reporting_basic
+
 type tnvar = 
   | Ty of Tyvar.t
   | Nv of Nvar.t
 let type_mismatch l m t1 t2 = 
   let t1 = t_to_string t1 in
   let t2 = t_to_string t2 in
-    raise (Ident.No_type(l, "type mismatch: " ^ m ^ "\n" ^ t1 ^ "\nand\n" ^ t2))
+    raise (err_type l ("type mismatch: " ^ m ^ "\n" ^ t1 ^ "\nand\n" ^ t2))
 
 let nexp_mismatch l n1 n2 =
   let n1 = nexp_to_string n1 in
   let n2 = nexp_to_string n2 in
-    raise (Ident.No_type(l, "numeric expression mismatch:\n" ^ n1 ^ "\nand\n" ^ n2))
+    raise (err_type l ("numeric expression mismatch:\n" ^ n1 ^ "\nand\n" ^ n2))
 
 let inconsistent_constraints r l =
-  raise (Ident.No_type(l, "Constraints, including " ^ range_to_string r ^ " are inconsistent\n"))
+  raise (err_type l ("Constraints, including " ^ range_to_string r ^ " are inconsistent\n"))
 
 (* Converts to linear normal form, summation of (optionally constant-multiplied) variables, with the "smallest" variable on the left *)
 let normalize nexp =
   let rec occurs_check (t_box : t) (t : t) : unit =
     let t = resolve_subst t in
       if t_box == t then
-        raise (Ident.No_type(Ast.Unknown, "Failed occurs check"))
+        raise (err_type Ast.Unknown "Failed occurs check")
       else
         match t.t with
           | Tfn(t1,t2) ->
   let rec occurs_nexp_check (n_box : nexp) (n : nexp) : unit =
      let n = resolve_nexp_subst n in 
        if n_box == n then
-          raise (Ident.No_type(Ast.Unknown, "Nexpressions failed occurs check"))
+          raise (err_type Ast.Unknown "Nexpressions failed occurs check")
        else
           match n.nexp with
             | Nadd(n1,n2) | Nmult(n1,n2) -> 
     if (try ignore(solve_numeric_constraints [] (negate_c::constraints));
             false
         with 
-          | Ident.No_type _ -> true
+          | (Fatal_error (Err_type _)) -> true
           | e -> raise e)
        then ()
-       else raise (Ident.No_type(l, ("Constraint " ^ range_to_string c ^ " is required by let definition but not implied by val specification\n")))
+       else raise (err_type l ("Constraint " ^ range_to_string c ^ " is required by let definition but not implied by val specification\n"))
 
   let rec solve_constraints instances (unsolvable : PTset.t)= function
     | [] -> unsolvable 
       | Tne(n) -> (match n.nexp with
                    | Nvar(nv) -> (p, Nv nv)
                    | _ -> let t1 = Pp.pp_to_string (fun ppf -> pp_instance_constraint ppf (p, t)) in
-                      raise (Ident.No_type(l, "unsatisfied type class constraint:\n" ^t1)))
+                      raise (err_type l ("unsatisfied type class constraint:\n" ^t1)))
       | _ -> 
           let t1 = 
             Pp.pp_to_string (fun ppf -> pp_instance_constraint ppf (p, t))
           in 
-            raise (Ident.No_type(l, "unsatisfied type class constraint:\n" ^ t1))
+            raise (err_type l ("unsatisfied type class constraint:\n" ^ t1))
 
   let inst_leftover_uvars l =  
     let used_tvs = ref TNset.empty in