do not generate itysymbols for pure types

+ rename Mlw_ty.ity_pure to ity_immutable

src/whyml/mlw_decl.ml

@@ -105,6 +105,8 @@ let syms_expr s _e = s (* TODO *)
 let create_ty_decl its =
 (*   let syms = Opt.fold syms_ity Sid.empty its.its_def in *)
   let news = Sid.singleton its.its_ts.ts_name in
+  (* an abstract type must be declared using Theory.create_ty_decl *)
+  if its.its_def = None then invalid_arg "Mlw_decl.create_ty_decl";
   mk_decl (PDtype its) Sid.empty news
 
 type pre_constructor = preid * (pvsymbol * bool) list

src/whyml/mlw_dty.ml

@@ -92,22 +92,21 @@ let its_app s tl =
   let add m v t = Mtv.add v t m in
   let mv = try List.fold_left2 add Mtv.empty s.its_ts.ts_args tl
     with Invalid_argument _ ->
-      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl))
-  in
+      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
   match s.its_def with
   | Some ity ->
       snd (ity_inst_fresh mv Mreg.empty ity)
   | None ->
-      let _, rl =
-        Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
+      let _,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
       its_app_real s tl rl
 
-let ts_app ts dl = match ts.ts_def with
+let ts_app ts dl =
+  let add m v t = Mtv.add v t m in
+  let mv = try List.fold_left2 add Mtv.empty ts.ts_args dl
+    with Invalid_argument _ ->
+      raise (BadTypeArity (ts, List.length ts.ts_args, List.length dl)) in
+  match ts.ts_def with
   | Some ty ->
-      let add m v t = Mtv.add v t m in
-      let mv = try List.fold_left2 add Mtv.empty ts.ts_args dl
-        with Invalid_argument _ ->
-          raise (BadTypeArity (ts, List.length ts.ts_args, List.length dl)) in
       snd (ity_inst_fresh mv Mreg.empty (ity_of_ty ty))
   | None ->
       ts_app_real ts dl

src/whyml/mlw_ty.ml

@@ -46,8 +46,8 @@ module rec T : sig
     | Ityapp of itysymbol * ity list * region list
 
   and region = {
-    reg_name  : ident;
-    reg_ity   : ity;
+    reg_name : ident;
+    reg_ity  : ity;
   }
 
 end = struct
@@ -80,8 +80,8 @@ end = struct
     | Ityapp of itysymbol * ity list * region list
 
   and region = {
-    reg_name  : ident;
-    reg_ity   : ity;
+    reg_name : ident;
+    reg_ity  : ity;
   }
 
 end
@@ -251,7 +251,7 @@ let ity_subst_unsafe mv mr ity =
   ity_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r 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 ity_immutable ity = Sreg.is_empty ity.ity_vars.vars_reg
 
 let rec ity_has_inv ity = match ity.ity_node with
   | Ityapp (its,_,_) -> its.its_inv || ity_any ity_has_inv ity
@@ -305,7 +305,7 @@ let reg_equal_check r1 r2 =
 let reg_full_inst s r = Mreg.find r s.ity_subst_reg
 
 let ity_full_inst s ity =
-  if ity_closed ity && ity_pure ity then ity
+  if ity_closed ity && ity_immutable ity then ity
   else ity_subst_unsafe s.ity_subst_tv s.ity_subst_reg ity
 
 let rec ity_match s ity1 ity2 =
@@ -381,9 +381,10 @@ let ity_app_fresh s tl =
       raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
   (* refresh regions *)
   let mr,rl = Lists.map_fold_left (reg_refresh mv) Mreg.empty s.its_regs in
+  let sub = { ity_subst_tv = mv; ity_subst_reg = mr } in
   (* every top region in def is guaranteed to be in mr *)
   match s.its_def with
-  | Some ity -> ity_subst_unsafe mv mr ity
+  | Some ity -> ity_full_inst sub ity
   | None -> ity_app_unsafe s tl rl
 
 let ity_app s tl rl =
@@ -402,15 +403,19 @@ let ity_app s tl rl =
   | Some ity -> ity_full_inst sub ity
   | None -> ity_app_unsafe s tl rl
 
-let ity_pur s tl = match s.ts_def with
-  | Some ty ->
-      let add m v t = Mtv.add v t m in
-      let m = try List.fold_left2 add Mtv.empty s.ts_args tl
-        with Invalid_argument _ ->
-          raise (Ty.BadTypeArity (s, List.length s.ts_args, List.length tl)) in
-      ity_subst_unsafe m Mreg.empty (ity_of_ty ty)
-  | None ->
-      ity_pur_unsafe s tl
+let ity_pur s tl =
+  (* type variable map *)
+  let add m v t = Mtv.add v t m in
+  let mv = try List.fold_left2 add Mtv.empty s.ts_args tl
+    with Invalid_argument _ ->
+      raise (Ty.BadTypeArity (s, List.length s.ts_args, List.length tl)) in
+  let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
+  (* every top region in def is guaranteed to be in mr *)
+  match s.ts_def with
+  | Some ty -> ity_full_inst sub (ity_of_ty ty)
+  | None -> ity_pur_unsafe s tl
+
+(* itysymbol creation *)
 
 let create_itysymbol_unsafe, restore_its =
   let ts_to_its = Wts.create 17 in
@@ -445,9 +450,11 @@ let create_itysymbol
     raise (UnboundRegion (Sreg.choose (Sreg.diff dregs sregs))) in
   Opt.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 "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";
+  if def <> None then begin
+    if abst then Loc.errorm "Type aliases cannot be abstract";
+    if priv then Loc.errorm "Type aliases cannot be private";
+    if inv  then Loc.errorm "Type aliases cannot have invariants"
+  end;
   create_itysymbol_unsafe purets ~abst ~priv ~inv regs def
 
 let ts_unit = ts_tuple 0
@@ -473,7 +480,7 @@ let its_clone sm =
       let priv = oits.its_priv in
       let inv  = oits.its_inv in
       let regs = List.map conv_reg oits.its_regs in
-      let def = Opt.map conv_ity oits.its_def in
+      let def  = Opt.map conv_ity oits.its_def in
       create_itysymbol_unsafe nts ~abst ~priv ~inv regs def
     in
     Hits.replace itsh oits nits;
@@ -524,7 +531,7 @@ let xs_equal : xsymbol -> xsymbol -> bool = (==)
 let create_xsymbol id ity =
   let id = id_register id in
   if not (ity_closed ity) then raise (PolymorphicException (id, ity));
-  if not (ity_pure ity) then raise (MutableException (id, ity));
+  if not (ity_immutable ity) then raise (MutableException (id, ity));
   { xs_name = id; xs_ity = ity; }
 
 module Exn = MakeMSH (struct

src/whyml/mlw_ty.mli

@@ -46,8 +46,8 @@ module rec T : sig
     | Ityapp of itysymbol * ity list * region list
 
   and region = private {
-    reg_name  : ident;
-    reg_ity   : ity;
+    reg_name : ident;
+    reg_ity  : ity;
   }
 
 end
@@ -118,9 +118,9 @@ val ity_s_any : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool
 
 val its_clone : Theory.symbol_map -> itysymbol Mits.t * region Mreg.t
 
-val ity_closed  : ity -> bool
-val ity_pure    : ity -> bool
-val ity_has_inv : ity -> bool
+val ity_closed    : ity -> bool
+val ity_immutable : ity -> bool
+val ity_has_inv   : ity -> bool
 
 (* these functions attend the sub-regions *)
 
@@ -175,7 +175,7 @@ val create_varset : Stv.t -> Sreg.t -> varset
 (* exception symbols *)
 type xsymbol = private {
   xs_name : ident;
-  xs_ity  : ity; (* closed and pure *)
+  xs_ity  : ity; (* closed and immutable *)
 }
 
 val xs_equal : xsymbol -> xsymbol -> bool

src/whyml/mlw_typing.ml

@@ -1334,6 +1334,41 @@ let add_types ~wp uc tdl =
         Mstr.add x true seen in
   ignore (Mstr.fold cyc_visit def Mstr.empty);
 
+  (* detect impure types *)
+
+  let impures = Hstr.create 5 in
+  let rec imp_visit x =
+    try Hstr.find impures x
+    with Not_found ->
+      let ts_imp = function
+        | Qident { id = x } when Mstr.mem x def -> imp_visit x
+        | q ->
+            begin match uc_find_ts uc q with
+              | PT _ -> true | TS _ -> false
+            end
+      in
+      let rec check = function
+        | PPTtyvar _ -> false
+        | PPTtyapp (tyl,q) -> ts_imp q || List.exists check tyl
+        | PPTtuple tyl -> List.exists check tyl in
+      Hstr.replace impures x false;
+      let imp =
+        let td = Mstr.find x def in
+        match td.td_def with
+        | TDabstract -> false
+        | TDalias ty -> check ty
+        | TDalgebraic csl ->
+            let cons (_,_,l) = List.exists (fun (_,ty) -> check ty) l in
+            td.td_inv <> [] || td.td_vis <> Public || List.exists cons csl
+        | TDrecord fl ->
+            let field f = f.f_ghost || f.f_mutable || check f.f_pty in
+            td.td_inv <> [] || td.td_vis <> Public || List.exists field fl
+      in
+      Hstr.replace impures x imp;
+      imp
+  in
+  Mstr.iter (fun x _ -> ignore (imp_visit x)) def;
+
   (* detect mutable types and invariants *)
 
   let mutables = Hstr.create 5 in
@@ -1355,16 +1390,16 @@ let add_types ~wp uc tdl =
       Hstr.replace mutables x false;
       let mut =
         let td = Mstr.find x def in
-        td.td_inv <> [] ||
         match td.td_def with
         | TDabstract -> false
         | TDalias ty -> check ty
         | TDalgebraic csl ->
-            let proj (_,pty) = check pty in
-            List.exists (fun (_,_,l) -> List.exists proj l) csl
+            let cons (_,_,l) = List.exists (fun (_,ty) -> check ty) l in
+            td.td_inv <> [] || List.exists cons csl
         | TDrecord fl ->
             let field f = f.f_mutable || check f.f_pty in
-            List.exists field fl in
+            td.td_inv <> [] || List.exists field fl
+      in
       Hstr.replace mutables x mut;
       mut
   in
@@ -1395,7 +1430,7 @@ let add_types ~wp uc tdl =
       let priv = d.td_vis = Private in
       Hstr.add tysymbols x None;
       let get_ts = function
-        | Qident { id = x } when Mstr.mem x def -> PT (its_visit x)
+        | Qident { id = x } when Mstr.mem x def -> its_visit x
         | q -> uc_find_ts uc q
       in
       let rec parse = function
@@ -1413,10 +1448,13 @@ let add_types ~wp uc tdl =
             ity_pur ts (List.map parse tyl)
       in
       let ts = match d.td_def with
-        | TDalias ty ->
+        | TDalias ty when Hstr.find impures x ->
             let def = parse ty in
             let rl = Sreg.elements def.ity_vars.vars_reg in
-            create_itysymbol id ~abst ~priv ~inv:false vl rl (Some def)
+            PT (create_itysymbol id ~abst ~priv ~inv:false vl rl (Some def))
+        | TDalias ty ->
+            let def = ty_of_ity (parse ty) in
+            TS (create_tysymbol id vl (Some def))
         | TDalgebraic csl when Hstr.find mutables x ->
             let projs = Hstr.create 5 in
             (* to check projections' types we must fix the tyvars *)
@@ -1449,8 +1487,9 @@ let add_types ~wp uc tdl =
             in
             let init = (Sreg.empty, d.td_inv <> []) in
             let (regs,inv),def = Lists.map_fold_left mk_constr init csl in
+            let rl = Sreg.elements regs in
             Hstr.replace predefs x def;
-            create_itysymbol id ~abst ~priv ~inv vl (Sreg.elements regs) None
+            PT (create_itysymbol id ~abst ~priv ~inv vl rl None)
         | TDrecord fl when Hstr.find mutables x ->
             let mk_field (regs,inv) f =
               let ghost = f.f_ghost in
@@ -1468,11 +1507,14 @@ let add_types ~wp uc tdl =
             in
             let init = (Sreg.empty, d.td_inv <> []) in
             let (regs,inv),pjl = Lists.map_fold_left mk_field init fl in
+            let rl = Sreg.elements regs in
             let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
             Hstr.replace predefs x [Denv.create_user_id cid, pjl];
-            create_itysymbol id ~abst ~priv ~inv vl (Sreg.elements regs) None
+            PT (create_itysymbol id ~abst ~priv ~inv vl rl None)
+        | TDalgebraic _ | TDrecord _ when Hstr.find impures x ->
+            PT (create_itysymbol id ~abst ~priv ~inv:false vl [] None)
         | TDalgebraic _ | TDrecord _ | TDabstract ->
-            create_itysymbol id ~abst ~priv ~inv:false vl [] None
+            TS (create_tysymbol id vl None)
       in
       Hstr.add tysymbols x (Some ts);
       ts
@@ -1484,12 +1526,13 @@ let add_types ~wp uc tdl =
   let def_visit d (abstr,algeb,alias) =
     let x = d.td_ident.id in
     let ts = Opt.get (Hstr.find tysymbols x) in
+    let vl = match ts with
+      | PT s -> s.its_ts.ts_args | TS s -> s.ts_args in
     let add_tv s x v = Mstr.add x.id v s in
-    let vars =
-      List.fold_left2 add_tv Mstr.empty d.td_params ts.its_ts.ts_args in
+    let vars = List.fold_left2 add_tv Mstr.empty d.td_params vl in
     let get_ts = function
       | Qident { id = x } when Mstr.mem x def ->
-          PT (Opt.get (Hstr.find tysymbols x))
+          Opt.get (Hstr.find tysymbols x)
       | q -> uc_find_ts uc q
     in
     let rec parse = function
@@ -1548,25 +1591,11 @@ let add_types ~wp uc tdl =
   in
   let abstr,algeb,alias = List.fold_right def_visit tdl ([],[],[]) in
 
-  (* detect pure type declarations *)
+  (* create pure type declarations *)
 
-  let kn = get_known uc in
-  let check its = Mid.mem its.its_ts.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_inv || ts.its_regs <> [] ||
-    Opt.fold (fun _ -> check) false ts.its_def
-  in
-  let check (pv,_) =
-    let vtv = pv.pv_vtv in
-    vtv.vtv_ghost || vtv.vtv_mut <> None || check vtv.vtv_ity in
-  let is_impure_data (ts,csl) =
-    is_impure_type ts ||
-    List.exists (fun (_,l) -> List.exists check l) csl
-  in
-  let mk_pure_decl (ts,csl) =
+  let mk_pure_decl ts csl =
     let pjt = Hvs.create 3 in
-    let ty = ty_app ts.its_ts (List.map ty_var ts.its_ts.ts_args) in
+    let ty = ty_app ts (List.map ty_var ts.ts_args) in
     let mk_proj (pv,f) =
       let vs = pv.pv_vs in
       if f then try vs.vs_ty, Some (Hvs.find pjt vs) with Not_found ->
@@ -1581,26 +1610,28 @@ let add_types ~wp uc tdl =
       let cs = create_fsymbol id (List.map fst pjl) ty in
       cs, List.map snd pjl
     in
-    ts.its_ts, List.map mk_constr csl
+    List.map mk_constr csl
   in
-  let add_type_decl uc ts =
-    if is_impure_type ts then
-      add_pdecl_with_tuples ~wp uc (create_ty_decl ts)
-    else
-      add_decl_with_tuples uc (Decl.create_ty_decl ts.its_ts)
+  let mk_data_decl (s,csl) (alg_pur,alg_imp) = match s with
+    | PT its -> alg_pur, (its, csl) :: alg_imp
+    | TS ts  -> (ts, mk_pure_decl ts csl) :: alg_pur, alg_imp
   in
-  let add_invariant uc d = if d.td_inv = [] then uc else
-    add_type_invariant d.td_loc uc d.td_ident d.td_params d.td_inv
+  let alg_pur,alg_imp = List.fold_right mk_data_decl algeb ([],[]) in
+
+  (* add type declarations *)
+
+  let add_type_decl uc = function
+    | PT ts -> add_pdecl_with_tuples ~wp uc (create_ty_decl ts)
+    | TS ts -> add_decl_with_tuples uc (Decl.create_ty_decl ts)
   in
+  let add_invariant uc d = if d.td_inv = [] then uc else
+    add_type_invariant d.td_loc uc d.td_ident d.td_params d.td_inv in
   try
     let uc = List.fold_left add_type_decl uc abstr in
-    let uc = if algeb = [] then uc else
-      if List.exists is_impure_data algeb then
-        add_pdecl_with_tuples ~wp uc (create_data_decl algeb)
-      else
-        let d = List.map mk_pure_decl algeb in
-        add_decl_with_tuples uc (Decl.create_data_decl d)
-    in
+    let uc = if alg_imp = [] then uc else
+      add_pdecl_with_tuples ~wp uc (create_data_decl alg_imp) in
+    let uc = if alg_pur = [] then uc else
+      add_decl_with_tuples uc (Decl.create_data_decl alg_pur) in
     let uc = List.fold_left add_type_decl uc alias in
     let uc = List.fold_left add_invariant uc tdl in
     uc

src/whyml/mlw_wp.ml

@@ -277,7 +277,7 @@ let update_var env mreg vs =
     let vs = Opt.fold (fun _ -> get_vs) vs mut in
     (* should we update our value further? *)
     let check_reg r _ = reg_occurs r ity.ity_vars in
-    if ity_pure ity || not (Mreg.exists check_reg mreg) then t_var vs
+    if ity_immutable ity || not (Mreg.exists check_reg mreg) then t_var vs
     else analyze_var update fs_app env.pure_known env.prog_known vs ity
   in
   update vs (vtv_of_vs vs)