add Mlw_pretty, fix some bugs, improve error reporting

Makefile.in

@@ -372,7 +372,8 @@ install_local: bin/why3
 # Whyml (new API)
 ########
 
-MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_typing mlw_main
+MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_pretty \
+	    mlw_typing mlw_main
 
 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 

src/core/decl.ml

@@ -404,8 +404,8 @@ exception BadLogicDecl of lsymbol * lsymbol
 exception BadConstructor of lsymbol
 
 exception BadRecordField of lsymbol
-exception RecordFieldMissing of lsymbol
-exception DuplicateRecordField of lsymbol
+exception RecordFieldMissing of lsymbol * lsymbol
+exception DuplicateRecordField of lsymbol * lsymbol
 
 exception EmptyDecl
 exception EmptyAlgDecl of tysymbol
@@ -425,21 +425,21 @@ let create_ty_decl tdl =
   if tdl = [] then raise EmptyDecl;
   let add s (ts,_) = Sts.add ts s in
   let tss = List.fold_left add Sts.empty tdl in
-  let check_proj tyv s tya ls = match ls with
+  let check_proj cs tyv s tya ls = match ls with
     | None -> s
     | Some ({ ls_args = [ptyv]; ls_value = Some ptya } as ls) ->
         ty_equal_check tyv ptyv;
         ty_equal_check tya ptya;
-        Sls.add_new (DuplicateRecordField ls) ls s
+        Sls.add_new (DuplicateRecordField (cs,ls)) ls s
     | Some ls -> raise (BadRecordField ls)
   in
   let check_constr tys ty pjs (syms,news) (fs,pl) =
     ty_equal_check ty (exn_option (BadConstructor fs) fs.ls_value);
     let fs_pjs =
-      try List.fold_left2 (check_proj ty) Sls.empty fs.ls_args pl
+      try List.fold_left2 (check_proj fs ty) Sls.empty fs.ls_args pl
       with Invalid_argument _ -> raise (BadConstructor fs) in
     if not (Sls.equal pjs fs_pjs) then
-      raise (RecordFieldMissing (Sls.choose (Sls.diff pjs fs_pjs)));
+      raise (RecordFieldMissing (fs, Sls.choose (Sls.diff pjs fs_pjs)));
     let vs = ty_freevars Stv.empty ty in
     let rec check seen ty = match ty.ty_node with
       | Tyvar v when Stv.mem v vs -> ()
@@ -801,12 +801,12 @@ let parse_record kn fll =
   let pjs = List.fold_left (fun s pj -> Sls.add pj s) Sls.empty pjl in
   let flm = List.fold_left (fun m (pj,v) ->
     if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
-    Mls.add_new (DuplicateRecordField pj) pj v m) Mls.empty fll in
+    Mls.add_new (DuplicateRecordField (cs,pj)) pj v m) Mls.empty fll in
   cs,pjl,flm
 
 let make_record kn fll ty =
   let cs,pjl,flm = parse_record kn fll in
-  let get_arg pj = Mls.find_exn (RecordFieldMissing pj) pj flm in
+  let get_arg pj = Mls.find_exn (RecordFieldMissing (cs,pj)) pj flm in
   fs_app cs (List.map get_arg pjl) ty
 
 let make_record_update kn t fll ty =

src/core/decl.mli

@@ -140,8 +140,8 @@ exception EmptyIndDecl of lsymbol
 
 exception BadConstructor of lsymbol
 exception BadRecordField of lsymbol
-exception RecordFieldMissing of lsymbol
-exception DuplicateRecordField of lsymbol
+exception RecordFieldMissing of lsymbol * lsymbol
+exception DuplicateRecordField of lsymbol * lsymbol
 
 (** {2 Utilities} *)
 

src/core/pretty.ml

@@ -540,10 +540,10 @@ let () = Exn_printer.register
       fprintf fmt "Bad constructor symbol: %a" print_ls ls
   | Decl.BadRecordField ls ->
       fprintf fmt "Not a record field: %a" print_ls ls
-  | Decl.RecordFieldMissing ls ->
-      fprintf fmt "Record field missing: %a" print_ls ls
-  | Decl.DuplicateRecordField ls ->
-      fprintf fmt "Duplicate record field: %a" print_ls ls
+  | Decl.RecordFieldMissing (_cs,ls) ->
+      fprintf fmt "Field %a is missing" print_ls ls
+  | Decl.DuplicateRecordField (_cs,ls) ->
+      fprintf fmt "Field %a is used twice in the same constructor" print_ls ls
   | Decl.IllegalTypeAlias ts ->
       fprintf fmt
         "Type symbol %a is a type alias and cannot be declared as algebraic"

src/core/pretty.mli

@@ -36,6 +36,7 @@ val print_ts : formatter -> tysymbol -> unit      (* type symbol *)
 val print_ls : formatter -> lsymbol -> unit       (* logic symbol *)
 val print_cs : formatter -> lsymbol -> unit       (* constructor symbol *)
 val print_pr : formatter -> prsymbol -> unit      (* proposition name *)
+val print_th : formatter -> theory -> unit        (* theory name *)
 
 val print_ty : formatter -> ty -> unit            (* type *)
 val print_vsty : formatter -> vsymbol -> unit     (* variable : type *)

src/parser/typing.ml

@@ -575,7 +575,7 @@ and dterm_node ~localize loc uc env = function
             let e = dterm ~localize uc env e in
             unify_raise ~loc e.dt_ty ty;
             e
-        | None -> error ~loc (RecordFieldMissing pj)
+        | None -> error ~loc (RecordFieldMissing (cs,pj))
       in
       let al = List.map2 get_val pjl tyl in
       Tapp (cs,al), Util.of_option ty
@@ -861,13 +861,17 @@ let add_types dl th =
           let projection (id,_) fty = match id with
             | None -> None
             | Some id ->
-                begin try Hashtbl.find ht id.id
+                try
+                  let pj = Hashtbl.find ht id.id in
+                  let ty = of_option pj.ls_value in
+                  ignore (Loc.try2 id.id_loc ty_equal_check ty fty);
+                  Some pj
                 with Not_found ->
                   let fn = create_user_id id in
-                  let pj = Some (create_fsymbol fn [ty] fty) in
+                  let pj = create_fsymbol fn [ty] fty in
+                  Hashtbl.replace csymbols id.id id.id_loc;
                   Hashtbl.replace ht id.id pj;
-                  pj
-                end
+                  Some pj
           in
           let constructor (loc, id, pl) =
             let tyl = List.map param pl in
@@ -881,10 +885,14 @@ let add_types dl th =
     in
     ts, d
   in
-  let th = try add_ty_decl th (List.map decl dl)
-    with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (ClashSymbol s)
-  in
-  th
+  try add_ty_decl th (List.map decl dl)
+  with
+    | ClashSymbol s ->
+        error ~loc:(Hashtbl.find csymbols s) (ClashSymbol s)
+    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
+        error ~loc:(Hashtbl.find csymbols s) (RecordFieldMissing (cs,ls))
+    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
+        error ~loc:(Hashtbl.find csymbols s) (DuplicateRecordField (cs,ls))
 
 let prepare_typedef td =
   if td.td_model then

src/whyml/mlw_decl.ml

@@ -69,9 +69,6 @@ let syms_ity s ity = ity_s_fold syms_its syms_ts s ity
 
 (** {2 Declaration constructors} *)
 
-exception BadConstructor of psymbol
-exception BadRecordField of psymbol
-
 type pre_pconstructor = preid * (pvsymbol * bool) list
 
 type pre_ity_defn =
@@ -115,7 +112,8 @@ let create_ity_decl tdl =
     let ps_ls = { ps = ps; ls = ls } in
     news := Sid.add ps.p_name !news;
     (* build the projections, if any *)
-    let build_proj pv id =
+    let build_proj pv =
+      let id = id_clone pv.pv_vs.vs_name in
       let ls = create_fsymbol id [result.pv_vs.vs_ty] pv.pv_vs.vs_ty in
       let t = fs_app ls [t_var result.pv_vs] pv.pv_vs.vs_ty in
       let post = t_equ (t_var pv.pv_vs) t in
@@ -129,7 +127,7 @@ let create_ity_decl tdl =
       ps_ls
     in
     let build_proj pv =
-      try Hvs.find projections pv.pv_vs with Not_found -> build_proj pv id in
+      try Hvs.find projections pv.pv_vs with Not_found -> build_proj pv in
     let build_proj (pv, pj) =
       syms := ity_s_fold syms_its syms_ts !syms pv.pv_ity;
       if pj then Some (build_proj pv) else None in

src/whyml/mlw_expr.ml

@@ -24,19 +24,19 @@ open Mlw_ty
 
 (* program symbols *)
 type psymbol = {
-  p_name: ident;
-  p_tvs:   Stv.t;
-  p_reg:   Sreg.t;
-  p_vty:   vty;
-  (* pv_ghost: bool; *)
+  p_name : ident;
+  p_tvs  : Stv.t;
+  p_reg  : Sreg.t;
+  p_vty  : vty;
 }
 
-let create_psymbol id tvars regs vty =
+let create_psymbol id tvars regs vty = {
   (* TODO? check that tvars/regs are in vty *)
-  { p_name = id_register id;
-    p_tvs   = tvars;
-    p_reg   = regs;
-    p_vty   = vty; }
+  p_name = id_register id;
+  p_tvs  = tvars;
+  p_reg  = regs;
+  p_vty  = vty;
+}
 
 let ps_equal : psymbol -> psymbol -> bool = (==)
 

src/whyml/mlw_expr.mli

@@ -24,16 +24,15 @@ open Mlw_ty
 
 (* program symbols *)
 type psymbol = private {
-  p_name: ident;
-  p_tvs:   Stv.t;  (* type variables that cannot be instantiated *)
-  p_reg:   Sreg.t; (* regions that cannot be instantiated *)
-  p_vty:   vty;
-  (* pv_ghost: bool; *)
+  p_name : ident;
+  p_tvs  : Stv.t;  (* type variables that cannot be instantiated *)
+  p_reg  : Sreg.t; (* regions that cannot be instantiated *)
+  p_vty  : vty;
 }
 
-val create_psymbol: preid -> Stv.t -> Sreg.t -> vty -> psymbol
+val create_psymbol : preid -> Stv.t -> Sreg.t -> vty -> psymbol
 
-val ps_equal: psymbol -> psymbol -> bool
+val ps_equal : psymbol -> psymbol -> bool
 
 (* program expressions *)
 

src/whyml/mlw_main.ml

@@ -28,6 +28,12 @@ let read_channel env path file c =
   if Debug.test_flag Typing.debug_parse_only then
     Mstr.empty, Mstr.empty
   else
-    List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
+    let mm, tm =
+      List.fold_left (add_theory_module env path) (Mstr.empty, Mstr.empty) ml
+    in
+    Mstr.iter (fun _ m ->
+      Mlw_pretty.print_module Format.err_formatter m;
+      Format.pp_print_newline Format.err_formatter ()) mm;
+    mm, tm
 
 let library_of_env = Env.register_format "whyml-exp" ["mlx"] read_channel

src/whyml/mlw_module.ml

@@ -50,8 +50,6 @@ let empty_ns = {
   ns_ns = Mstr.empty;
 }
 
-exception ClashSymbol of string
-
 let ns_replace eq chk x vo vn =
   if not chk then vn else
   if eq vo vn then vo else

src/whyml/mlw_pretty.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+open Why3
+open Pp
+open Util
+open Ident
+open Ty
+open Term
+open Theory
+open Pretty
+open Mlw_ty
+open Mlw_expr
+open Mlw_decl
+open Mlw_module
+
+let debug_print_labels = Debug.register_flag "print_labels"
+let debug_print_locs = Debug.register_flag "print_locs"
+let debug_print_reg_types = Debug.register_flag "print_reg_types"
+
+let rprinter =
+  let isanitize = sanitizer char_to_alpha char_to_alnumus in
+  create_ident_printer [] ~sanitizer:isanitize
+
+let forget_regs () = Ident.forget_all rprinter
+let forget_tvs_regs () = Ident.forget_all rprinter; forget_tvs ()
+let forget_all () = Ident.forget_all rprinter; forget_all ()
+
+(* ghost regions are prefixed with "?" *)
+let print_reg fmt reg =
+  fprintf fmt "%s%s" (if reg.reg_ghost then "?" else "")
+    (id_unique rprinter reg.reg_name)
+
+let print_pv fmt pv =
+  fprintf fmt "%s%a" (if pv.pv_ghost then "?" else "")
+    print_vs pv.pv_vs
+
+let forget_pv pv = forget_var pv.pv_vs
+
+(* theory names always start with an upper case letter *)
+let print_mod fmt m = print_th fmt m.mod_theory
+
+let print_its fmt ts = print_ts fmt ts.its_pure
+
+(** Types *)
+
+let protect_on x s = if x then "(" ^^ s ^^ ")" else s
+
+let rec print_ity_node inn fmt ity = match ity.ity_node with
+  | Ityvar v -> print_tv fmt v
+  | Itypur (ts,tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
+      (print_list comma (print_ity_node false)) tl
+  | Itypur (ts,[]) -> print_ts fmt ts
+  | Itypur (ts,tl) -> fprintf fmt (protect_on inn "%a@ %a")
+      print_ts ts (print_list space (print_ity_node true)) tl
+  | Ityapp (ts,[],rl) -> fprintf fmt (protect_on inn "%a@ <%a>")
+      print_its ts (print_list comma print_regty) rl
+  | Ityapp (ts,tl,rl) -> fprintf fmt (protect_on inn "%a@ <%a>@ %a")
+      print_its ts (print_list comma print_regty) rl
+      (print_list space (print_ity_node true)) tl
+
+and print_regty fmt reg =
+  if Debug.test_flag debug_print_reg_types then print_reg fmt reg else
+  fprintf fmt "%a:@,%a" print_reg reg (print_ity_node false) reg.reg_ity
+
+let print_ity = print_ity_node false
+
+let print_reg_opt fmt = function
+  | Some r -> fprintf fmt "<%a>" print_regty r
+  | None -> ()
+
+let print_pvty fmt pv = fprintf fmt "%a%a:@,%a"
+  print_pv pv print_reg_opt pv.pv_mutable print_ity pv.pv_ity
+
+(* Labels and locs - copied from Pretty *)
+
+let print_labels = print_iter1 Slab.iter space print_label
+
+let print_ident_labels fmt id =
+  if Debug.test_flag debug_print_labels &&
+      not (Slab.is_empty id.id_label) then
+    fprintf fmt "@ %a" print_labels id.id_label;
+  if Debug.test_flag debug_print_locs then
+    Util.option_iter (fprintf fmt "@ %a" print_loc) id.id_loc
+
+(** Type declarations *)
+
+let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
+let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ity_node true) ty
+
+let print_constr fmt (cs,pjl) =
+  let rec cs_args vty pjl = match vty, pjl with
+    | VTvalue _, [] -> []
+    | VTarrow (pv,cty), pj::pjl ->
+        (pv,pj) :: cs_args cty.c_vty pjl
+    | _, _ -> assert false
+  in
+  let pjl = cs_args cs.ps.p_vty pjl in
+  let print_pj fmt (pv,pj) = match pj with
+    | Some { ls = ls } ->
+        fprintf fmt "@ (%s%s%a%a:@,%a)"
+          (if pv.pv_ghost then "ghost " else "")
+          (if pv.pv_mutable <> None then "mutable " else "")
+          print_ls ls print_reg_opt pv.pv_mutable print_ity pv.pv_ity
+    | None when pv.pv_ghost || pv.pv_mutable <> None ->
+        fprintf fmt "@ (%s%a@ %a)"
+          (if pv.pv_ghost then "ghost" else "")
+          print_reg_opt pv.pv_mutable
+          print_ity pv.pv_ity
+    | None ->
+        print_ty_arg fmt pv.pv_ity
+  in
+  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs.ls
+    print_ident_labels cs.ls.ls_name
+    (print_list nothing print_pj) pjl
+
+let print_type_decl fst fmt (ts,def) =
+  let print_head fmt ts =
+    fprintf fmt "%s %s%s%a%a <%a>%a"
+      (if fst then "type" else "with")
+      (if ts.its_abst then "abstract " else "")
+      (if ts.its_priv then "private " else "")
+      print_its ts
+      print_ident_labels ts.its_pure.ts_name
+      (print_list comma print_regty) ts.its_regs
+      (print_list nothing print_tv_arg) ts.its_args
+  in
+  match def with
+  | ITabstract -> begin match ts.its_def with
+      | None ->
+          fprintf fmt "@[<hov 2>%a@]" print_head ts
+      | Some ty ->
+          fprintf fmt "@[<hov 2>%a =@ %a@]" print_head ts print_ity ty
+      end
+  | ITalgebraic csl ->
+      fprintf fmt "@[<hov 2>%a =@\n@[<hov>%a@]@]"
+        print_head ts (print_list newline print_constr) csl
+
+let print_type_decl first fmt d =
+  print_type_decl first fmt d; forget_tvs_regs ()
+
+(* Declarations *)
+
+let print_list_next sep print fmt = function
+  | [] -> ()
+  | [x] -> print true fmt x
+  | x :: r -> print true fmt x; sep fmt ();
+      print_list sep (print false) fmt r
+
+let print_pdecl fmt d = match d.pd_node with
+  | PDtype tl -> print_list_next newline print_type_decl fmt tl
+
+let print_next_type_decl  = print_type_decl false
+let print_type_decl       = print_type_decl true
+
+let print_module fmt m =
+  fprintf fmt "@[<hov 2>module %a%a@\n%a@]@\nend@."
+    print_mod m print_ident_labels m.mod_theory.th_name
+    (print_list newline2 print_pdecl) m.mod_decls
+
+(* Print exceptions *)
+
+let () = Exn_printer.register
+  begin fun fmt exn -> match exn with
+  | BadItyArity (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_its ts ts_arg app_arg
+  | BadRegArity (ts, ts_arg, app_arg) ->
+      fprintf fmt "Bad region arity: type symbol %a must be applied \
+                   to %i regions, but is applied to %i"
+        print_its ts ts_arg app_arg
+  | DuplicateRegion r ->
+      fprintf fmt "Region %a is used twice" print_reg r
+  | UnboundRegion r ->
+      fprintf fmt "Unbound region %a" print_reg r
+  | RegionMismatch (r1,r2) ->
+      fprintf fmt "Region mismatch between %a and %a"
+        print_regty r1 print_regty r2
+  | Mlw_ty.TypeMismatch (t1,t2) ->
+      fprintf fmt "Type mismatch between %a and %a"
+        print_ity t1 print_ity t2
+  | _ -> raise exn
+  end

src/whyml/mlw_pretty.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+open Why3
+open Mlw_ty
+open Mlw_expr
+open Mlw_decl
+open Mlw_module
+
+val forget_all      : unit -> unit     (* flush id_unique *)
+val forget_regs     : unit -> unit     (* flush id_unique for regions *)
+val forget_tvs_regs : unit -> unit     (* flush for type vars and regions *)
+val forget_pv       : pvsymbol -> unit (* flush for a program variable *)
+
+val print_reg : formatter -> region -> unit       (* region *)
+val print_pv  : formatter -> pvsymbol -> unit     (* program variable *)
+
+val print_its : formatter -> itysymbol -> unit    (* type symbol *)
+val print_mod : formatter -> modul -> unit        (* module name *)
+
+val print_ity : formatter -> ity -> unit          (* individual type *)
+val print_pvty : formatter -> pvsymbol -> unit    (* variable : type *)
+
+val print_type_decl : formatter -> ity_decl -> unit
+val print_next_type_decl : formatter -> ity_decl -> unit
+
+val print_pdecl : formatter -> pdecl -> unit
+
+val print_module : formatter -> modul -> unit
+

src/whyml/mlw_ty.ml

@@ -160,7 +160,7 @@ let ity_s_all pr pts ity =
   try ity_s_fold (all_fn pr) (all_fn pts) true ity with FoldSkip -> false
 
 let ity_s_any pr pts ity =
-  try ity_s_fold (any_fn pr) (all_fn pts) false ity with FoldSkip -> true
+  try ity_s_fold (any_fn pr) (any_fn pts) false ity with FoldSkip -> true
 
 (* traversal functions on type variables and regions *)
 
@@ -202,7 +202,6 @@ exception BadRegArity of itysymbol * int * int
 
 exception DuplicateRegion of region
 exception UnboundRegion of region
-exception InvalidRegion of region
 
 exception RegionMismatch of region * region
 exception TypeMismatch of ity * ity

src/whyml/mlw_ty.mli

@@ -78,7 +78,6 @@ exception BadItyArity of itysymbol * int * int
 exception BadRegArity of itysymbol * int * int
 exception DuplicateRegion of region
 exception UnboundRegion of region
-exception InvalidRegion of region
 
 val create_region : preid -> ?ghost:bool -> ity -> region
 

src/whyml/mlw_typing.ml

@@ -33,7 +33,7 @@ open Mlw_module
 
 (** errors *)
 
-exception DuplicateVar of string
+exception DuplicateProgVar of string
 exception DuplicateTypeVar of string
 (*
 exception PredicateExpected
@@ -56,9 +56,9 @@ let rec print_qualid fmt = function
 
 let () = Exn_printer.register (fun fmt e -> match e with
   | DuplicateTypeVar s ->
-      Format.fprintf fmt "Duplicate type parameter %s" s
-  | DuplicateVar s ->
-      Format.fprintf fmt "Duplicate variable %s" s
+      Format.fprintf fmt "Type parameter %s is used twice" s
+  | DuplicateProgVar s ->
+      Format.fprintf fmt "Parameter %s is used twice" s
 (*
   | PredicateExpected ->
       Format.fprintf fmt "syntax error: predicate expected"
@@ -100,7 +100,9 @@ let find_tysymbol q uc =
 let look_for_loc tdl s =
   let look_id loc id = if id.id = s then Some id.id_loc else loc in
   let look_pj loc (id,_) = option_fold look_id loc id in
-  let look_cs loc (_,id,pjl) = List.fold_left look_pj (look_id loc id) pjl in
+  let look_cs loc (csloc,id,pjl) =
+    let loc = if id.id = s then Some csloc else loc in
+    List.fold_left look_pj loc pjl in
   let look_fl loc f = look_id loc f.f_ident in
   let look loc d =
     let loc = look_id loc d.td_ident in
@@ -313,6 +315,8 @@ let add_types uc tdl =
               | Some id ->
                   try
                     let pv = Hashtbl.find projs id.id in
+                    (* once we have ghost/mutable fields in algebraics,
+                       don't forget to check here that they coincide, too *)
                     Loc.try2 id.id_loc ity_equal_check pv.pv_ity ity;
                     pv, true
                   with Not_found ->
@@ -376,7 +380,15 @@ let add_types uc tdl =
       let d = create_ty_decl def in
       add_decl_with_tuples uc d
   with
-    | ClashSymbol s -> error ?loc:(look_for_loc tdl s) (ClashSymbol s)
+    | ClashSymbol s ->
+        error ?loc:(look_for_loc tdl s) (ClashSymbol s)
+    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
+        error ?loc:(look_for_loc tdl s) (RecordFieldMissing (cs,ls))
+    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
+        error ?loc:(look_for_loc tdl s) (DuplicateRecordField (cs,ls))
+    | DuplicateVar { vs_name = { id_string = s }} ->
+        errorm ?loc:(look_for_loc tdl s)
+          "Field %s is used twice in the same constructor" s
 
 (** Use/Clone of theories and modules *)