add type invariants to WhyML grammar

src/parser/parser.mly

@@ -403,10 +403,11 @@ list1_type_decl:
 
 type_decl:
 | lident labels type_args typedefn
-  { let model, vis, def = $4 in
+  { let model, vis, def, inv = $4 in
     let vis = if model then Abstract else vis in
     { td_loc = floc (); td_ident = add_lab $1 $2;
-      td_params = $3; td_model = model; td_vis = vis; td_def = def } }
+      td_params = $3; td_model = model;
+      td_vis = vis; td_def = def; td_inv = inv } }
 ;
 
 type_args:
@@ -415,14 +416,18 @@ type_args:
 ;
 
 typedefn:
-| /* epsilon */                         { false, Public, TDabstract }
-| equal_model visibility typecases      { $1,    $2,     TDalgebraic $3 }
-| equal_model visibility BAR typecases  { $1,    $2,     TDalgebraic $4 }
-| equal_model visibility record_type    { $1,    $2,     TDrecord $3 }
+| /* epsilon */
+    { false, Public, TDabstract, None }
+| equal_model visibility typecases invariant
+    { $1, $2, TDalgebraic $3, $4 }
+| equal_model visibility BAR typecases invariant
+    { $1, $2, TDalgebraic $4, $5 }
+| equal_model visibility record_type invariant
+    { $1, $2, TDrecord $3, $4 }
 /* abstract/private is not allowed for alias type */
 | equal_model visibility primitive_type
     { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
-      $1, Public, TDalias $3 }
+      $1, Public, TDalias $3, None }
 ;
 
 visibility:
@@ -1122,7 +1127,7 @@ expr:
                      mk_expr (Eif ($2, $5,
                                    mk_expr (Eraise (exit_exn (), None)))))),
            [exit_exn (), None, mk_expr (Etuple [])])) }
-| FOR lident EQUAL expr for_direction expr DO loop_invariant expr DONE
+| FOR lident EQUAL expr for_direction expr DO invariant expr DONE
    { mk_expr (Efor ($2, $4, $5, $6, $8, $9)) }
 | ABSURD
    { mk_expr Eabsurd }
@@ -1238,10 +1243,10 @@ for_direction:
 ;
 
 loop_annotation:
-| loop_invariant opt_variant { { loop_invariant = $1; loop_variant = $2 } }
+| invariant opt_variant { { loop_invariant = $1; loop_variant = $2 } }
 ;
 
-loop_invariant:
+invariant:
 | INVARIANT annotation { Some $2 }
 | /* epsilon */        { None    }
 ;

src/parser/ptree.ml

@@ -127,6 +127,8 @@ type type_def =
 
 type visibility = Public | Private | Abstract
 
+type invariant = lexpr option
+
 type type_decl = {
   td_loc    : loc;
   td_ident  : ident;
@@ -134,6 +136,7 @@ type type_decl = {
   td_model  : bool;
   td_vis    : visibility;
   td_def    : type_def;
+  td_inv    : invariant;
 }
 
 type logic_decl = {
@@ -180,7 +183,7 @@ type lazy_op = LazyAnd | LazyOr
 type variant = lexpr * qualid option
 
 type loop_annotation = {
-  loop_invariant : lexpr option;
+  loop_invariant : invariant;
   loop_variant   : variant list;
 }
 
@@ -238,7 +241,7 @@ and expr_desc =
   | Eabsurd
   | Eraise of qualid * expr option
   | Etry of expr * (qualid * ident option * expr) list
-  | Efor of ident * expr * for_direction * expr * lexpr option * expr
+  | Efor of ident * expr * for_direction * expr * invariant * expr
   (* annotations *)
   | Eassert of assertion_kind * lexpr
   | Emark of ident * expr

src/parser/typing.ml

@@ -913,7 +913,9 @@ let prepare_typedef td =
   if td.td_model then
     errorm ~loc:td.td_loc "model types are not allowed in the logic";
   if td.td_vis <> Public then
-    errorm ~loc:td.td_loc "a logic type cannot be abstract or private";
+    errorm ~loc:td.td_loc "logic types cannot be abstract or private";
+  if td.td_inv <> None then
+    errorm ~loc:td.td_loc "logic types cannot have invariants";
   match td.td_def with
   | TDabstract | TDalgebraic _ | TDalias _ ->
       td

src/programs/pgm_typing.ml

@@ -2039,6 +2039,10 @@ let check_type_vars ~loc vars ty =
   check ty
 
 let make_immutable_type td =
+  if td.td_vis = Private then errorm ~loc:td.td_loc
+    "private types are not supported in this version of WhyML";
+  if td.td_inv <> None then errorm ~loc:td.td_loc
+    "type invariants are not supported in this version of WhyML";
   let td = { td with td_model = false; td_vis = Public } in
   let make_immutable_field f = { f with f_mutable = false; f_ghost = false } in
   match td.td_def with

src/whyml/mlw_decl.ml

@@ -30,7 +30,7 @@ open Mlw_expr
 
 type constructor = plsymbol * plsymbol option list
 
-type data_decl = itysymbol * constructor list
+type data_decl = itysymbol * constructor list * post
 
 type pdecl = {
   pd_node : pdecl_node;
@@ -122,6 +122,11 @@ type pre_constructor = preid * (pvsymbol * bool) list
 
 type pre_data_decl = itysymbol * pre_constructor list
 
+let null_invariant { its_pure = ts } =
+  let ty = ty_app ts (List.map ty_var ts.ts_args) in
+  let vs = create_vsymbol (id_fresh "dummy") ty in
+  create_post vs t_true
+
 let create_data_decl tdl =
 (*   let syms = ref Sid.empty in *)
   let news = ref Sid.empty in
@@ -165,11 +170,30 @@ let create_data_decl tdl =
   let build_type (its,cl) =
     Hid.clear projections;
     news := news_id !news its.its_pure.ts_name;
-    its, List.map (build_constructor its) cl
+    its, List.map (build_constructor its) cl, null_invariant its
   in
   let tdl = List.map build_type tdl in
   mk_decl (PDdata tdl) (*!syms*) !news
 
+let add_invariant pd its p =
+  if not its.its_inv then invalid_arg "Mlw_decl.add_invariant";
+  Mvs.iter (fun vs _ -> raise (Decl.UnboundVar vs)) p.t_vars;
+  let rec add = function
+    | (s, cls, inv) :: tdl when its_equal s its ->
+        check_post (t_type inv) p;
+        let v, q = open_post inv in
+        let u, p = open_post p in
+        let q = t_and_simp (t_subst_single v (t_var u) q) p in
+        let inv = create_post u q in
+        (s, cls, inv) :: tdl
+    | td :: tdl ->
+        td :: add tdl
+    | [] -> raise Not_found
+  in
+  match pd.pd_node with
+    | PDdata tdl -> mk_decl (PDdata (add tdl)) (*pd.pd_syms*) pd.pd_news
+    | _ -> invalid_arg "Mlw_decl.add_invariant"
+
 let check_vars vars =
   if not (Stv.is_empty vars.vars_tv) then
     raise (UnboundTypeVar (Stv.choose vars.vars_tv))
@@ -249,10 +273,13 @@ let clone_data_decl sm pd = match pd.pd_node with
         pl in
       let add_cs (cs,pjl) =
         add_pl cs, List.map (Util.option_map add_pl) pjl in
-      let add_td (its,csl) =
+      let add_td (its,csl,inv) =
+        let conv_ts ts = Mts.find_def ts ts sm.sm_pure.Theory.sm_ts in
+        let conv_ls ls = Mls.find_def ls ls sm.sm_pure.Theory.sm_ls in
+        let inv = Term.t_s_map (Ty.ty_s_map conv_ts) conv_ls inv in
         let its = Mits.find its sm.sm_its in
         news := news_id !news its.its_pure.ts_name;
-        its, List.map add_cs csl in
+        its, List.map add_cs csl, inv in
       let tdl = List.map add_td tdl in
       mk_decl (PDdata tdl) (*!syms*) !news
   | _ -> invalid_arg "Mlw_decl.clone_data_decl"
@@ -289,8 +316,19 @@ let known_add_decl _lkn0 kn0 decl =
 
 (* TODO: known_add_decl must check pattern matches for exhaustiveness *)
 
+let rec find_td its1 = function
+  | (its2,csl,inv) :: _ when its_equal its1 its2 -> csl,inv
+  | _ :: tdl -> find_td its1 tdl
+  | [] -> raise Not_found
+
 let find_constructors kn its =
   match (Mid.find its.its_pure.ts_name kn).pd_node with
   | PDtype _ -> []
-  | PDdata dl -> List.assq its dl
+  | PDdata tdl -> fst (find_td its tdl)
+  | PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
+
+let find_invariant kn its =
+  match (Mid.find its.its_pure.ts_name kn).pd_node with
+  | PDtype _ -> null_invariant its
+  | PDdata tdl -> snd (find_td its tdl)
   | PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false

src/whyml/mlw_decl.mli

@@ -30,7 +30,7 @@ open Mlw_expr
 
 type constructor = plsymbol * plsymbol option list
 
-type data_decl = itysymbol * constructor list
+type data_decl = itysymbol * constructor list * post
 
 (** {2 Declaration type} *)
 
@@ -66,6 +66,12 @@ val create_rec_decl : rec_defn -> pdecl
 
 val create_exn_decl : xsymbol -> pdecl
 
+(** {2 Type invariants} *)
+
+val null_invariant : itysymbol -> post
+
+val add_invariant : pdecl -> itysymbol -> post -> pdecl
+
 (** {2 Cloning} *)
 
 val clone_data_decl : Mlw_expr.symbol_map -> pdecl -> pdecl
@@ -79,3 +85,4 @@ val known_add_decl : Decl.known_map -> known_map -> pdecl -> known_map
 val merge_known : known_map -> known_map -> known_map
 
 val find_constructors : known_map -> itysymbol -> constructor list
+val find_invariant : known_map -> itysymbol -> post

src/whyml/mlw_module.ml

@@ -266,7 +266,7 @@ let add_meta uc m al =
 let add_type uc its =
   add_symbol add_ts its.its_pure.ts_name (PT its) uc
 
-let add_data uc (its,csl) =
+let add_data uc (its,csl,_) =
   let add_pl uc pl = add_symbol add_ps pl.pl_ls.ls_name (PL pl) uc in
   let add_pj uc pj = Util.option_fold add_pl uc pj in
   let add_cs uc (cs,pjl) = List.fold_left add_pj (add_pl uc cs) pjl in
@@ -309,7 +309,7 @@ let add_pdecl ~wp uc d =
       let projection = option_map (fun pls -> pls.pl_ls) in
       let constructor (pls,pjl) = pls.pl_ls, List.map projection pjl in
       let defn cl = List.map constructor cl in
-      let dl = List.map (fun (its,cl) -> its.its_pure, defn cl) dl in
+      let dl = List.map (fun (its,cl,_) -> its.its_pure, defn cl) dl in
       add_to_theory Theory.add_data_decl uc dl
   | PDval lv | PDlet { let_sym = lv } ->
       add_let uc lv
@@ -318,6 +318,21 @@ let add_pdecl ~wp uc d =
   | PDexn xs ->
       add_exn uc xs
 
+(* we can safely add a new type invariant as long as
+   the type was introduced in the last program decl,
+   and no let, rec or val could see it *)
+let add_invariant uc its p =
+  let rec add = function
+    | { pd_node = PDtype _ } as d :: dl ->
+        let nd, dl = add dl in nd, d :: dl
+    | d :: dl ->
+        let d = Mlw_decl.add_invariant d its p in d, d :: dl
+    | [] -> invalid_arg "Mlw_module.add_invariant" in
+  let decl, decls = add uc.muc_decls in
+  let kn = Mid.map (const decl) decl.pd_news in
+  let kn = Mid.set_union kn uc.muc_known in
+  { uc with muc_decls = decls; muc_known = kn }
+
 (* create module *)
 
 let th_unit =

src/whyml/mlw_module.mli

@@ -92,6 +92,8 @@ val add_meta : module_uc -> meta -> meta_arg list -> module_uc
 
 val add_pdecl : wp:bool -> module_uc -> pdecl -> module_uc
 
+val add_invariant : module_uc -> itysymbol -> post -> module_uc
+
 (** Builtin symbols *)
 
 val xs_exit : xsymbol (* exception used to break the loops *)

src/whyml/mlw_pretty.ml

@@ -386,9 +386,12 @@ let print_ty_decl fmt ts = match ts.its_def with
 let print_ty_decl fmt ts =
   print_ty_decl fmt ts; forget_tvs_regs ()
 
-let print_data_decl fst fmt (ts,csl) =
-  fprintf fmt "@[<hov 2>%a =@ %a@]"
-    (print_head fst) ts (print_list newline print_constr) csl;
+let print_data_decl fst fmt (ts,csl,inv) =
+  let print_inv fmt inv = if ts.its_inv then
+    fprintf fmt "@ invariant { %a }" print_post inv else () in
+  fprintf fmt "@[<hov 2>%a =@ %a%a@]"
+    (print_head fst) ts (print_list newline print_constr) csl
+    print_inv inv;
   forget_tvs_regs ()
 
 let print_val_decl fmt lv =

src/whyml/mlw_ty.ml

@@ -41,6 +41,7 @@ module rec T : sig
     its_args : tvsymbol list;
     its_regs : region list;
     its_def  : ity option;
+    its_inv  : bool;
     its_abst : bool;
     its_priv : bool;
   }
@@ -75,6 +76,7 @@ end = struct
     its_args : tvsymbol list;
     its_regs : region   list;
     its_def  : ity option;
+    its_inv  : bool;
     its_abst : bool;
     its_priv : bool;
   }
@@ -262,6 +264,10 @@ let ity_subst_unsafe mv mr ity =
 let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
 let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
 
+let rec ity_inv ity = match ity.ity_node with
+  | Ityapp (its,_,_) -> its.its_inv || ity_any ity_inv ity
+  | _ -> ity_any ity_inv ity
+
 let rec reg_fold fn vars acc =
   let on_reg r acc = reg_fold fn r.reg_ity.ity_vars (fn r acc) in
   Sreg.fold on_reg vars.vars_reg acc
@@ -307,12 +313,6 @@ let ity_subst_empty = {
   ity_subst_reg = Mreg.empty;
 }
 
-let ity_subst_union s1 s2 =
-  let check_ity _ ity1 ity2 = ity_equal_check ity1 ity2; Some ity1 in
-  let check_reg _ r1 r2 = reg_equal_check r1 r2; Some r1 in
-  { ity_subst_tv  = Mtv.union  check_ity s1.ity_subst_tv  s2.ity_subst_tv;
-    ity_subst_reg = Mreg.union check_reg s1.ity_subst_reg s2.ity_subst_reg }
-
 let tv_inst s v = Mtv.find_def (ity_var v) v s.ity_subst_tv
 let reg_inst s r = Mreg.find_def r r s.ity_subst_reg
 
@@ -428,12 +428,13 @@ let ity_pur s tl = match s.ts_def with
 
 let create_itysymbol_unsafe, restore_its =
   let ts_to_its = Wts.create 17 in
-  (fun ts ~abst ~priv regs def ->
+  (fun ts ~abst ~priv ~inv regs def ->
     let its = {
       its_pure  = ts;
       its_args  = ts.ts_args;
       its_regs  = regs;
       its_def   = def;
+      its_inv   = inv;
       its_abst  = abst;
       its_priv  = priv;
     } in
@@ -441,7 +442,8 @@ let create_itysymbol_unsafe, restore_its =
     its),
   Wts.find ts_to_its
 
-let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
+let create_itysymbol
+      name ?(abst=false) ?(priv=false) ?(inv=false) args regs def =
   let puredef = option_map ty_of_ity def in
   let purets = create_tysymbol name args puredef in
   (* all regions *)
@@ -458,9 +460,10 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
     raise (UnboundRegion (Sreg.choose (Sreg.diff dregs sregs))) in
   Util.option_iter (fun d -> check d.ity_vars.vars_reg) def;
   (* if a type is an alias then it cannot be abstract or private *)
-  if abst && def <> None then Loc.errorm "A type alias cannot be abstract";
-  if priv && def <> None then Loc.errorm "A type alias cannot be private";
-  create_itysymbol_unsafe purets ~abst ~priv regs def
+  if abst && def <> None then Loc.errorm "Type aliases cannot be abstract";
+  if priv && def <> None then Loc.errorm "Type aliases cannot be private";
+  if inv  && def <> None then Loc.errorm "Type aliases cannot have invariants";
+  create_itysymbol_unsafe purets ~abst ~priv ~inv regs def
 
 let ts_unit = ts_tuple 0
 let ty_unit = ty_tuple []
@@ -483,9 +486,10 @@ let its_clone sm =
     let nits = try restore_its nts with Not_found ->
       let abst = oits.its_abst in
       let priv = oits.its_priv in
+      let inv  = oits.its_inv in
       let regs = List.map conv_reg oits.its_regs in
       let def = Util.option_map conv_ity oits.its_def in
-      create_itysymbol_unsafe nts ~abst ~priv regs def
+      create_itysymbol_unsafe nts ~abst ~priv ~inv regs def
     in
     Hits.replace itsh oits nits;
     nits

src/whyml/mlw_ty.mli

@@ -40,6 +40,7 @@ module rec T : sig
     its_args : tvsymbol list;
     its_regs : region list;
     its_def  : ity option;
+    its_inv  : bool;
     its_abst : bool;
     its_priv : bool;
   }
@@ -95,8 +96,9 @@ exception UnboundRegion of region
 
 val create_region : preid -> ity -> region
 
-val create_itysymbol : preid -> ?abst:bool -> ?priv:bool ->
-  tvsymbol list -> region list -> ity option -> itysymbol
+val create_itysymbol :
+  preid -> ?abst:bool -> ?priv:bool -> ?inv:bool ->
+    tvsymbol list -> region list -> ity option -> itysymbol
 
 val ity_var : tvsymbol -> ity
 val ity_pur : tysymbol -> ity list -> ity
@@ -133,6 +135,7 @@ val ity_v_map : (tvsymbol -> ity) -> (region -> region) -> ity -> ity
 
 val ity_closed : ity -> bool
 val ity_pure : ity -> bool
+val ity_inv : ity -> bool
 
 (* these functions attend the sub-regions *)
 
@@ -168,8 +171,6 @@ val reg_match : ity_subst -> region -> region -> ity_subst
 
 val ity_equal_check : ity -> ity -> unit
 
-val ity_subst_union : ity_subst -> ity_subst -> ity_subst
-
 val ity_full_inst : ity_subst -> ity -> ity
 
 val reg_full_inst : ity_subst -> region -> region
@@ -245,6 +246,7 @@ type variant = term * lsymbol option (* tau * (tau -> tau -> prop) *)
 
 val create_post : vsymbol -> term -> post
 val open_post : post -> vsymbol * term
+val check_post : ty -> post -> unit
 
 type spec = {
   c_pre     : pre;

src/whyml/mlw_typing.ml

@@ -1097,7 +1097,7 @@ let add_types ~wp uc tdl =
         Mstr.add x true seen in
   ignore (Mstr.fold cyc_visit def Mstr.empty);
 
-  (* detect mutable types *)
+  (* detect mutable types and invariants *)
 
   let mutables = Hashtbl.create 5 in
   let rec mut_visit x =
@@ -1107,7 +1107,7 @@ let add_types ~wp uc tdl =
         | Qident { id = x } when Mstr.mem x def -> mut_visit x
         | q ->
             begin match uc_find_ts uc q with
-              | PT its -> its.its_regs <> []
+              | PT its -> its.its_regs <> [] || its.its_inv
               | TS _ -> false
             end
       in
@@ -1116,7 +1116,10 @@ let add_types ~wp uc tdl =
         | PPTtyapp (tyl,q) -> ts_mut q || List.exists check tyl
         | PPTtuple tyl -> List.exists check tyl in
       Hashtbl.replace mutables x false;
-      let mut = match (Mstr.find x def).td_def with
+      let mut =
+        let td = Mstr.find x def in
+        td.td_inv <> None ||
+        match td.td_def with
         | TDabstract -> false
         | TDalias ty -> check ty
         | TDalgebraic csl ->
@@ -1138,8 +1141,10 @@ let add_types ~wp uc tdl =
     try match Hashtbl.find tysymbols x with
       | Some ts -> ts
       | None ->
-          let loc = (Mstr.find x def).td_loc in
-          errorm ~loc "Mutable type in a recursive type definition"
+          let td = Mstr.find x def in let loc = td.td_loc in
+          if td.td_inv <> None
+          then errorm ~loc "Recursive types cannot have invariants"
+          else errorm ~loc "Recursive types cannot have mutable components"
     with Not_found ->
       let d = Mstr.find x def in
       let add_tv acc id =
@@ -1174,19 +1179,20 @@ let add_types ~wp uc tdl =
         | TDalias ty ->
             let def = parse ty in
             let rl = Sreg.elements def.ity_vars.vars_reg in
-            create_itysymbol id ~abst ~priv vl rl (Some def)
+            create_itysymbol id ~abst ~priv ~inv:false vl rl (Some def)
         | TDalgebraic csl when Hashtbl.find mutables x ->
             let projs = Hashtbl.create 5 in
             (* to check projections' types we must fix the tyvars *)
             let add s v = let t = ity_var v in ity_match s t t in
             let sbs = List.fold_left add ity_subst_empty vl in
-            let mk_proj s (id,pty) =
+            let mk_proj (regs,inv) (id,pty) =
               let ity = parse pty in
               let vtv = vty_value ity in
+              let inv = inv || ity_inv ity in
               match id with
                 | None ->
                     let pv = create_pvsymbol (id_fresh "pj") vtv in
-                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
+                    (Sreg.union regs ity.ity_vars.vars_reg, inv), (pv, false)
                 | Some id ->
                     try
                       let pv = Hashtbl.find projs id.id in
@@ -1194,39 +1200,42 @@ let add_types ~wp uc tdl =
                       (* TODO: once we have ghost/mutable fields in algebraics,
                          don't forget to check here that they coincide, too *)
                       ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
-                      s, (pv, true)
+                      (regs, inv), (pv, true)
                     with Not_found ->
                       let pv = create_pvsymbol (Denv.create_user_id id) vtv in
                       Hashtbl.replace projs id.id pv;
-                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
+                      (Sreg.union regs ity.ity_vars.vars_reg, inv), (pv, true)
             in
             let mk_constr s (_loc,cid,pjl) =
               let s,pjl = Util.map_fold_left mk_proj s pjl in
               s, (Denv.create_user_id cid, pjl)
             in
-            let s,def = Util.map_fold_left mk_constr Sreg.empty csl in
+            let init = (Sreg.empty, d.td_inv <> None) in
+            let (regs,inv),def = Util.map_fold_left mk_constr init csl in
             Hashtbl.replace predefs x def;
-            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
+            create_itysymbol id ~abst ~priv ~inv vl (Sreg.elements regs) None
         | TDrecord fl when Hashtbl.find mutables x ->
-            let mk_field s f =
+            let mk_field (regs,inv) f =
               let ghost = f.f_ghost in
               let ity = parse f.f_pty in
+              let inv = inv || ity_inv ity in
               let fid = Denv.create_user_id f.f_ident in
-              let s,mut = if f.f_mutable then
+              let regs,mut = if f.f_mutable then
                 let r = create_region fid ity in
-                Sreg.add r s, Some r
+                Sreg.add r regs, Some r
               else
-                Sreg.union s ity.ity_vars.vars_reg, None
+                Sreg.union regs ity.ity_vars.vars_reg, None
               in
               let vtv = vty_value ?mut ~ghost ity in
-              s, (create_pvsymbol fid vtv, true)
+              (regs, inv), (create_pvsymbol fid vtv, true)
             in
-            let s,pjl = Util.map_fold_left mk_field Sreg.empty fl in
+            let init = (Sreg.empty, d.td_inv <> None) in
+            let (regs,inv),pjl = Util.map_fold_left mk_field init fl in
             let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
             Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
-            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
+            create_itysymbol id ~abst ~priv ~inv vl (Sreg.elements regs) None
         | TDalgebraic _ | TDrecord _ | TDabstract ->
-            create_itysymbol id ~abst ~priv vl [] None
+            create_itysymbol id ~abst ~priv ~inv:false vl [] None
       in
       Hashtbl.add tysymbols x (Some ts);
       ts
@@ -1307,7 +1316,7 @@ let add_types ~wp uc tdl =
   let check its = Mid.mem its.its_pure.ts_name kn in
   let check ity = ity_s_any check Util.ffalse ity in
   let is_impure_type ts =
-    ts.its_abst || ts.its_priv || ts.its_regs <> [] ||
+    ts.its_abst || ts.its_priv || ts.its_inv || ts.its_regs <> [] ||
     option_apply false check ts.its_def
   in
   let check (pv,_) =
@@ -1342,6 +1351,31 @@ let add_types ~wp uc tdl =
     else
       add_decl_with_tuples uc (Decl.create_ty_decl ts.its_pure)
   in
+  let add_invariant uc d = match d.td_inv with
+    | None -> uc
+    | Some f ->
+        let ts = Util.of_option (Hashtbl.find tysymbols d.td_ident.id) in
+        let ty = ty_app ts.its_pure (List.map ty_var ts.its_pure.ts_args) in
+        let x = "result" in
+        let f = match d.td_def with
+          | TDrecord fl ->
+              let loc = f.pp_loc in
+              let field { f_loc = loc; f_ident = id } =
+                Qident id, { pat_loc = loc; pat_desc = PPpvar id } in
+              let pat = PPprec (List.map field fl) in
+              let pat = { pat_loc = loc; pat_desc = pat } in
+              let id = { id = x; id_lab = []; id_loc = loc } in
+              let id = { pp_loc = loc; pp_desc = Ptree.PPvar (Qident id) } in
+              { pp_loc = loc; pp_desc = Ptree.PPmatch (id, [pat, f]) }
+          | TDabstract | TDalias _ | TDalgebraic _ -> f
+        in
+        let res = create_vsymbol (id_fresh x) ty in
+        let log_vars = Mstr.singleton x res in
+        let log_denv = Typing.add_var x (dty_of_ty ty) Typing.denv_empty in
+        let f = Typing.type_fmla (get_theory uc) log_denv log_vars f in
+        let uc = (count_term_tuples f; flush_tuples uc) in
+        Mlw_module.add_invariant uc ts (Mlw_ty.create_post res f)
+  in
   try
     let uc = List.fold_left add_type_decl uc abstr in
     let uc = if algeb = [] then uc else
@@ -1352,6 +1386,7 @@ let add_types ~wp uc tdl =
         add_decl_with_tuples uc (Decl.create_data_decl d)
     in
     let uc = List.fold_left add_type_decl uc alias in
+    let uc = List.fold_left add_invariant uc tdl in
     uc
   with
     | ClashSymbol s ->