whyml: remove redundant its_args and rename its_pure to its_ts

src/whyml/mlw_decl.ml

@@ -54,7 +54,7 @@ let syms_ps s ps = Sid.add ps.ps_name s
 let syms_xs s xs = Sid.add xs.xs_name s
 let syms_pl s pl = Sid.add pl.pl_ls.ls_name s
 
-let syms_its s its = Sid.add its.its_pure.ts_name s
+let syms_its s its = Sid.add its.its_ts.ts_name s
 
 let syms_ty s ty = ty_s_fold syms_ts s ty
 let syms_term s t = t_s_fold syms_ty syms_ls s t
@@ -104,14 +104,14 @@ 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_pure.ts_name in
+  let news = Sid.singleton its.its_ts.ts_name in
   mk_decl (PDtype its) Sid.empty news
 
 type pre_constructor = preid * (pvsymbol * bool) list
 
 type pre_data_decl = itysymbol * pre_constructor list
 
-let null_invariant { its_pure = ts } =
+let null_invariant { its_ts = 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
@@ -123,7 +123,7 @@ let create_data_decl tdl =
   let build_constructor its (id,al) =
     (* check well-formedness *)
     let vtvs = List.map (fun (pv,_) -> pv.pv_vtv) al in
-    let tvs = List.fold_right Stv.add its.its_args Stv.empty in
+    let tvs = List.fold_right Stv.add its.its_ts.ts_args Stv.empty in
     let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
     let check_vars { vars_tv = atvs; vars_reg = aregs } =
       if not (Stv.subset atvs tvs) then
@@ -137,7 +137,7 @@ let create_data_decl tdl =
     (* build the constructor ps *)
     let hidden = its.its_abst in
     let rdonly = its.its_priv in
-    let tvl = List.map ity_var its.its_args in
+    let tvl = List.map ity_var its.its_ts.ts_args in
     let res = vty_value (ity_app its tvl its.its_regs) in
     let pls = create_plsymbol ~hidden ~rdonly id vtvs res in
     news := news_id !news pls.pl_ls.ls_name;
@@ -158,7 +158,7 @@ let create_data_decl tdl =
   in
   let build_type (its,cl) =
     Hid.clear projections;
-    news := news_id !news its.its_pure.ts_name;
+    news := news_id !news its.its_ts.ts_name;
     its, List.map (build_constructor its) cl, null_invariant its
   in
   let tdl = List.map build_type tdl in
@@ -269,7 +269,7 @@ let clone_data_decl sm pd = match pd.pd_node with
         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;
+        news := news_id !news its.its_ts.ts_name;
         its, List.map add_cs csl, inv in
       let tdl = List.map add_td tdl in
       mk_decl (PDdata tdl) Sid.empty !news
@@ -307,13 +307,13 @@ let rec find_td its1 = function
   | [] -> raise Not_found
 
 let find_constructors kn its =
-  match (Mid.find its.its_pure.ts_name kn).pd_node with
+  match (Mid.find its.its_ts.ts_name kn).pd_node with
   | PDtype _ -> []
   | 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
+  match (Mid.find its.its_ts.ts_name kn).pd_node with
   | PDtype _ -> null_invariant its
   | PDdata tdl -> snd (find_td its tdl)
   | PDval _ | PDlet _ | PDrec _ | PDexn _ -> assert false
@@ -351,10 +351,11 @@ let inst_constructors lkn kn ity = match ity.ity_node with
       List.map (fun (cs,_) -> cs, List.map subst cs.ls_args) csl
   | Ityapp (its,_,_) ->
       let csl = find_constructors kn its in
-      let d = Mid.find its.its_pure.ts_name lkn in
-      let is_rec = Mid.mem its.its_pure.ts_name d.Decl.d_syms in
+      let d = Mid.find its.its_ts.ts_name lkn in
+      let is_rec = Mid.mem its.its_ts.ts_name d.Decl.d_syms in
       if csl = [] || is_rec then raise (NonupdatableType ity);
-      let base = ity_app its (List.map ity_var its.its_args) its.its_regs in
+      let args = List.map ity_var its.its_ts.ts_args in
+      let base = ity_app its args its.its_regs in
       let sbs = ity_match ity_subst_empty base ity in
       let subst vtv =
         let ghost = vtv.vtv_ghost in

src/whyml/mlw_dty.ml

@@ -90,9 +90,9 @@ and reg_refresh mv mr r = match Mreg.find_opt r mr with
 
 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_args tl
+  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_args, List.length tl))
+      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl))
   in
   match s.its_def with
   | Some ity ->

src/whyml/mlw_module.ml

@@ -280,13 +280,13 @@ let add_meta uc m al =
 (** Program decls *)
 
 let add_type uc its =
-  add_symbol add_ts its.its_pure.ts_name (PT its) uc
+  add_symbol add_ts its.its_ts.ts_name (PT its) uc
 
 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 = Opt.fold add_pl uc pj in
   let add_cs uc (cs,pjl) = List.fold_left add_pj (add_pl uc cs) pjl in
-  let uc = add_symbol add_ts its.its_pure.ts_name (PT its) uc in
+  let uc = add_symbol add_ts its.its_ts.ts_name (PT its) uc in
   if its.its_abst then uc else List.fold_left add_cs uc csl
 
 let add_let uc = function
@@ -324,13 +324,13 @@ let add_pdecl ~wp uc d =
   match d.pd_node with
   | PDtype its ->
       let uc = add_type uc its in
-      add_to_theory Theory.add_ty_decl uc its.its_pure
+      add_to_theory Theory.add_ty_decl uc its.its_ts
   | PDdata dl ->
       let uc = List.fold_left add_data uc dl in
       let projection = Opt.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_ts, defn cl) dl in
       add_to_theory Theory.add_data_decl uc dl
   | PDval lv | PDlet { let_sym = lv } ->
       add_let uc lv
@@ -347,7 +347,7 @@ exception TooLateInvariant
 
 let add_invariant uc its p =
   let rec add = function
-    | d :: dl when Mid.mem its.its_pure.ts_name d.pd_news ->
+    | d :: dl when Mid.mem its.its_ts.ts_name d.pd_news ->
         let d = Mlw_decl.add_invariant d its p in d, d :: dl
     | { pd_node = PDtype _ } as d :: dl ->
         let nd, dl = add dl in nd, d :: dl
@@ -539,7 +539,7 @@ let clone_export uc m inst =
         with Not_found -> TS ts end
     | PT pt ->
         begin try let pt = Mits.find pt psm.sm_its in
-          store_path uc p pt.its_pure.ts_name; PT pt
+          store_path uc p pt.its_ts.ts_name; PT pt
         with Not_found -> PT pt end in
   let find_prs p def id =
     try let s = Hid.find psh id in match s with

src/whyml/mlw_ocaml.ml

@@ -599,7 +599,7 @@ open Mlw_expr
 open Mlw_decl
 open Mlw_module
 
-let print_its info fmt ts = print_ts info fmt ts.its_pure
+let print_its info fmt ts = print_ts info fmt ts.its_ts
 let print_pv info fmt pv =
   if pv.pv_vtv.vtv_ghost then
     fprintf fmt "((* ghost %a *))" (print_lident info) pv.pv_vs.vs_name
@@ -642,7 +642,7 @@ let rec print_ity_node inn info fmt ity = match ity.ity_node with
         end
       end
   | Ityapp (ts, tl, _) ->
-      begin match query_syntax info.info_syn ts.its_pure.ts_name with
+      begin match query_syntax info.info_syn ts.its_ts.ts_name with
         | Some s -> syntax_arguments s (print_ity_node true info) fmt tl
         | None -> begin match tl with
             | [] -> print_its info fmt ts
@@ -859,15 +859,16 @@ let print_type_decl info fmt its = match its.its_def with
   | None ->
       fprintf fmt
         "@[<hov 2>type %a%a (* to be defined (uninterpreted type) *)@]@\n@\n"
-        print_tv_args its.its_args (print_its info) its
+        print_tv_args its.its_ts.ts_args (print_its info) its
   | Some ty ->
       fprintf fmt "@[<hov 2>type %a%a =@ %a@]@\n@\n"
-        print_tv_args its.its_args (print_its info) its (print_ity info) ty
+        print_tv_args its.its_ts.ts_args
+        (print_its info) its (print_ity info) ty
 
 let print_type_decl info fmt its =
-  if has_syntax info its.its_pure.ts_name then
+  if has_syntax info its.its_ts.ts_name then
     fprintf fmt "(* type %a is overridden by driver *)"
-      (print_lident info) its.its_pure.ts_name
+      (print_lident info) its.its_ts.ts_name
   else begin print_type_decl info fmt its; forget_tvs () end
 
 let print_exn_decl info fmt xs =
@@ -910,12 +911,12 @@ let print_pdata_decl info fst fmt (its, csl, _) =
   in
   fprintf fmt "@[<hov 2>%s %a%a =@\n@[<hov>%a@]@]"
     (if fst then "type" else "and")
-    print_tv_args its.its_args (print_its info) its print_defn csl
+    print_tv_args its.its_ts.ts_args (print_its info) its print_defn csl
 
 let print_pdata_decl info first fmt (its, _, _ as d) =
-  if has_syntax info its.its_pure.ts_name then
+  if has_syntax info its.its_ts.ts_name then
     fprintf fmt "(* type %a is overridden by driver *)"
-      (print_lident info) its.its_pure.ts_name
+      (print_lident info) its.its_ts.ts_name
   else begin print_pdata_decl info first fmt d; forget_tvs () end
 
 let is_record = function
@@ -940,7 +941,7 @@ let print_pprojections info fmt (_, csl, _) =
   List.iter print pjl
 
 let print_pprojections info fmt (ts, _, _ as d) =
-  if not (has_syntax info ts.its_pure.ts_name) && not (is_record d) then begin
+  if not (has_syntax info ts.its_ts.ts_name) && not (is_record d) then begin
     print_pprojections info fmt d; forget_tvs ()
   end
 

src/whyml/mlw_pretty.ml

@@ -73,7 +73,7 @@ let print_ps fmt ps =
 
 let forget_ps ps = forget_id iprinter ps.ps_name
 
-let print_its fmt ts = print_ts fmt ts.its_pure
+let print_its fmt ts = print_ts fmt ts.its_ts
 
 (** Types *)
 
@@ -368,9 +368,9 @@ let print_head fst fmt ts =
     (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_ident_labels ts.its_ts.ts_name
     (print_list comma print_regty) ts.its_regs
-    (print_list nothing print_tv_arg) ts.its_args
+    (print_list nothing print_tv_arg) ts.its_ts.ts_args
 
 let print_ty_decl fmt ts = match ts.its_def with
   | None ->

src/whyml/mlw_ty.ml

@@ -26,8 +26,7 @@ module rec T : sig
   type varmap = varset Mid.t
 
   type itysymbol = {
-    its_pure : tysymbol;
-    its_args : tvsymbol list;
+    its_ts   : tysymbol;
     its_regs : region list;
     its_def  : ity option;
     its_inv  : bool;
@@ -61,9 +60,8 @@ end = struct
   type varmap = varset Mid.t
 
   type itysymbol = {
-    its_pure : tysymbol;
-    its_args : tvsymbol list;
-    its_regs : region   list;
+    its_ts   : tysymbol;
+    its_regs : region list;
     its_def  : ity option;
     its_inv  : bool;
     its_abst : bool;
@@ -132,7 +130,7 @@ let create_varset tvs regs = {
 
 module Itsym = MakeMSHW (struct
   type t = itysymbol
-  let tag its = its.its_pure.ts_name.id_tag
+  let tag its = its.its_ts.ts_name.id_tag
 end)
 
 module Sits = Itsym.S
@@ -143,7 +141,7 @@ module Wits = Itsym.W
 let its_equal : itysymbol -> itysymbol -> bool = (==)
 let ity_equal : ity       -> ity       -> bool = (==)
 
-let its_hash its = id_hash its.its_pure.ts_name
+let its_hash its = id_hash its.its_ts.ts_name
 let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
 
 module Hsity = Hashcons.Make (struct
@@ -349,7 +347,7 @@ let reg_match s r1 r2 =
 let rec ty_of_ity ity = match ity.ity_node with
   | Ityvar v -> ty_var v
   | Itypur (s,tl) -> ty_app s (List.map ty_of_ity tl)
-  | Ityapp (s,tl,_) -> ty_app s.its_pure (List.map ty_of_ity tl)
+  | Ityapp (s,tl,_) -> ty_app s.its_ts (List.map ty_of_ity tl)
 
 let rec ity_of_ty ty = match ty.ty_node with
   | Tyvar v -> ity_var v
@@ -378,9 +376,9 @@ and reg_refresh mv mr r = match Mreg.find_opt r mr with
 let ity_app_fresh 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.its_args tl
+  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_args, List.length tl)) in
+      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
   (* every top region in def is guaranteed to be in mr *)
@@ -391,15 +389,15 @@ let ity_app_fresh s tl =
 let ity_app s tl rl =
   (* type variable map *)
   let add m v t = Mtv.add v t m in
-  let mv = try List.fold_left2 add Mtv.empty s.its_args tl
+  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_args, List.length tl)) in
+      raise (BadItyArity (s, List.length s.its_ts.ts_args, List.length tl)) in
   (* region map *)
   let sub = { ity_subst_tv = mv; ity_subst_reg = Mreg.empty } in
   let sub = try List.fold_left2 reg_match sub s.its_regs rl
     with Invalid_argument _ ->
       raise (BadRegArity (s, List.length s.its_regs, List.length rl)) in
-  (* every type var and top region in def are in its_args and its_regs *)
+  (* every type var and top region in def are in its_ts.ts_args and its_regs *)
   match s.its_def with
   | Some ity -> ity_full_inst sub ity
   | None -> ity_app_unsafe s tl rl
@@ -418,8 +416,7 @@ let create_itysymbol_unsafe, restore_its =
   let ts_to_its = Wts.create 17 in
   (fun ts ~abst ~priv ~inv regs def ->
     let its = {
-      its_pure  = ts;
-      its_args  = ts.ts_args;
+      its_ts    = ts;
       its_regs  = regs;
       its_def   = def;
       its_inv   = inv;
@@ -498,7 +495,7 @@ let its_clone sm =
     | Ityvar _ -> ity
   and conv_its its =
     try Hits.find itsh its with Not_found ->
-      try add_ts its (Mts.find its.its_pure sm.Theory.sm_ts)
+      try add_ts its (Mts.find its.its_ts sm.Theory.sm_ts)
       with Not_found -> its
   and conv_ts ts =
     Mts.find_def ts ts sm.Theory.sm_ts

src/whyml/mlw_ty.mli

@@ -26,8 +26,7 @@ module rec T : sig
   type varmap = varset Mid.t
 
   type itysymbol = private {
-    its_pure : tysymbol;
-    its_args : tvsymbol list;
+    its_ts   : tysymbol;
     its_regs : region list;
     its_def  : ity option;
     its_inv  : bool;

src/whyml/mlw_typing.ml

@@ -142,7 +142,7 @@ let uc_find_ls uc p =
   Typing.find_ns (fun ls -> ls.ls_name) Theory.ns_find_ls p ns
 
 let get_id_ts = function
-  | PT pt -> pt.its_pure.ts_name
+  | PT pt -> pt.its_ts.ts_name
   | TS ts -> ts.ts_name
 
 let uc_find_ts uc p =
@@ -1274,7 +1274,7 @@ let add_type_invariant loc uc id params inv =
     let e = Loc.Located (loc, DuplicateTypeVar id) in
     Sstr.add_new e id acc, Typing.create_user_tv id in
   let _, tvl = Lists.map_fold_left add_tv Sstr.empty params in
-  let ty = ty_app its.its_pure (List.map ty_var tvl) in
+  let ty = ty_app its.its_ts (List.map ty_var tvl) in
   let res = create_vsymbol (id_fresh x) ty in
   let find = function
     | Qident { id = id } when id = x -> Some res
@@ -1284,9 +1284,9 @@ let add_type_invariant loc uc id params inv =
     t_label_add Split_goal.stop_split f in
   let inv = List.map mk_inv inv in
   let q = Mlw_ty.create_post res (t_and_simp_l inv) in
-  let q = if List.for_all2 tv_equal its.its_args tvl then q else
+  let q = if List.for_all2 tv_equal its.its_ts.ts_args tvl then q else
     let add mtv u v = Mtv.add u (ty_var v) mtv in
-    let mtv = List.fold_left2 add Mtv.empty tvl its.its_args in
+    let mtv = List.fold_left2 add Mtv.empty tvl its.its_ts.ts_args in
     t_ty_subst mtv Mvs.empty q in
   let uc = (count_term_tuples q; flush_tuples uc) in
   Mlw_module.add_invariant uc its q
@@ -1485,7 +1485,8 @@ let add_types ~wp uc tdl =
     let x = d.td_ident.id in
     let ts = Opt.get (Hstr.find tysymbols x) 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_args in
+    let vars =
+      List.fold_left2 add_tv Mstr.empty d.td_params ts.its_ts.ts_args in
     let get_ts = function
       | Qident { id = x } when Mstr.mem x def ->
           PT (Opt.get (Hstr.find tysymbols x))
@@ -1550,7 +1551,7 @@ let add_types ~wp uc tdl =
   (* detect pure type declarations *)
 
   let kn = get_known uc in
-  let check its = Mid.mem its.its_pure.ts_name kn 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 <> [] ||
@@ -1565,7 +1566,7 @@ let add_types ~wp uc tdl =
   in
   let mk_pure_decl (ts,csl) =
     let pjt = Hvs.create 3 in
-    let ty = ty_app ts.its_pure (List.map ty_var ts.its_args) in
+    let ty = ty_app ts.its_ts (List.map ty_var ts.its_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 ->
@@ -1580,13 +1581,13 @@ 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_pure, List.map mk_constr csl
+    ts.its_ts, 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_pure)
+      add_decl_with_tuples uc (Decl.create_ty_decl ts.its_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

src/whyml/mlw_wp.ml

@@ -354,7 +354,7 @@ let get_invariant km t =
     | Tyapp (ts,_) -> ts
     | _ -> assert false in
   let rec find_td = function
-    | (its,_,inv) :: _ when ts_equal ts its.its_pure -> inv
+    | (its,_,inv) :: _ when ts_equal ts its.its_ts -> inv
     | _ :: tdl -> find_td tdl
     | [] -> assert false in
   let pd = Mid.find ts.ts_name km in