solve issue with type range declarations

src/mlw/ity.ml

@@ -631,6 +631,11 @@ let create_alias_itysymbol id args def =
     ~aflg:(List.map (fun _ -> flg) args)
     ~rflg:(List.map (fun _ -> flg) regs) ~def:(Alias def)
 
+let create_range_itysymbol id ir =
+  let ts = create_tysymbol id [] (Range ir) in
+  mk_its ~ts ~nfr:false ~priv:false ~mut:false ~frg:false ~mfld:[] ~regs:[]
+    ~aflg:[] ~rflg:[] ~def:(Range ir)
+
 let fields_of_invariant ftv flds invl =
   if invl = [] then Mpv.empty, flds else
   let fvs = Mpv.fold (fun v _ s -> Svs.add v.pv_vs s) flds Svs.empty in

src/mlw/ity.mli

@@ -129,6 +129,9 @@ val create_rec_itysymbol : preid -> tvsymbol list -> itysymbol
 val create_alias_itysymbol : preid -> tvsymbol list -> ity -> itysymbol
 (** [create_alias_itysymbol id args def] creates a new type alias. *)
 
+val create_range_itysymbol : preid -> Number.int_range -> itysymbol
+(** [create_range_itysymbol id r] creates a new range type. *)
+
 val restore_its : tysymbol -> itysymbol
 (** raises [Not_found] if the argument is not a [its_ts] *)
 

src/mlw/pdecl.ml

@@ -35,6 +35,9 @@ let mk_itd s f c i = {
 let create_alias_decl id args ity =
   mk_itd (create_alias_itysymbol id args ity) [] [] []
 
+let create_range_decl id ir =
+  mk_itd (create_range_itysymbol id ir) [] [] []
+
 let check_field stv f =
   let loc = f.pv_vs.vs_name.id_loc in
   let ftv = ity_freevars Stv.empty f.pv_ity in
@@ -294,10 +297,42 @@ let mk_decl = let r = ref 0 in fun node pure ->
 
 let create_type_decl dl =
   if dl = [] then invalid_arg "Pdecl.create_type_decl";
-  let add_itd ({itd_its = s} as itd) (abst,defn,rest) =
+  let add_itd ({itd_its = s} as itd) (abst,defn,rest,metas) =
     match itd.itd_fields, itd.itd_constructors with
     | [], [] when s.its_def <> NoDef ->
-        abst, defn, create_ty_decl s.its_ts :: rest
+        begin
+          match s.its_def with
+          | Alias _ -> abst, defn, create_ty_decl s.its_ts :: rest, metas
+          | Range ir ->
+             let ts = s.its_ts in
+             let td = create_ty_decl ts in
+             let nm = ts.ts_name.id_string ^ "'int" in
+             let id = id_derive nm ts.ts_name in
+             let pj = create_fsymbol id [ty_app ts []] ty_int in
+             let pjd = create_param_decl pj in
+             let meta = Theory.(meta_range,[MAts ts; MAls pj]) in
+             (* create max attribute *)
+             let nm = ts.ts_name.id_string ^ "'maxInt" in
+             let id = id_derive nm ts.ts_name in
+             let lsmaxInt = create_fsymbol id [] ty_int  in
+             let t =
+               t_const Number.(ConstInt (int_const_dec (BigInt.to_string ir.ir_upper)))
+                       ty_int
+             in
+             let maxInt_decl = create_logic_decl [make_ls_defn lsmaxInt [] t] in
+             (* create min attribute *)
+             let nm = ts.ts_name.id_string ^ "'minInt" in
+             let id = id_derive nm ts.ts_name in
+             let lsminInt = create_fsymbol id [] ty_int  in
+             let t =
+               t_const Number.(ConstInt (int_const_dec (BigInt.to_string ir.ir_lower)))
+                       ty_int
+             in
+             let minInt_decl = create_logic_decl [make_ls_defn lsminInt [] t] in
+             abst, defn, td :: pjd :: maxInt_decl :: minInt_decl :: rest, meta :: metas
+          | Float _ -> assert false (* TODO *)
+          | NoDef -> assert false
+        end
     | fl, _ when itd.itd_invariant <> [] ->
         let {id_string = nm; id_loc = loc} = s.its_ts.ts_name in
         let u = create_vsymbol (id_fresh "self")
@@ -313,13 +348,13 @@ let create_type_decl dl =
         let inv = t_subst sbs (t_and_simp_l itd.itd_invariant) in
         let inv = t_forall_close [u] [] inv in
         let inv = create_prop_decl Paxiom pr inv in
-        create_ty_decl s.its_ts :: abst, defn, proj @ inv :: rest
+        create_ty_decl s.its_ts :: abst, defn, proj @ inv :: rest, metas
     | fl, [] ->
         let get_ld s ldd = match s.rs_logic with
           | RLls s -> create_param_decl s :: ldd
           | _ -> assert false in
         let rest = List.fold_right get_ld fl rest in
-        create_ty_decl s.its_ts :: abst, defn, rest
+        create_ty_decl s.its_ts :: abst, defn, rest, metas
     | fl, cl ->
         let add s f = Mpv.add (Opt.get f.rs_field) f s in
         let mf = List.fold_left add Mpv.empty fl in
@@ -329,10 +364,11 @@ let create_type_decl dl =
         let get_cs s = match s.rs_logic with
           | RLls cs -> cs, List.map get_pj s.rs_cty.cty_args
           | _ -> assert false in
-        abst, (s.its_ts, List.map get_cs cl) :: defn, rest in
-  let abst,defn,rest = List.fold_right add_itd dl ([],[],[]) in
+        abst, (s.its_ts, List.map get_cs cl) :: defn, rest, metas
+  in
+  let abst,defn,rest,metas = List.fold_right add_itd dl ([],[],[],[]) in
   let defn = if defn = [] then [] else [create_data_decl defn] in
-  mk_decl (PDtype dl) (abst @ defn @ rest)
+  mk_decl (PDtype dl) (abst @ defn @ rest), metas
 
 (* TODO: share with Eliminate_definition *)
 let rec t_insert hd t = match t.t_node with

src/mlw/pdecl.mli

@@ -66,6 +66,9 @@ val create_rec_variant_decl :
 val create_alias_decl : preid -> tvsymbol list -> ity -> its_defn
 (** [create_alias_decl id args def] creates a new alias type declaration. *)
 
+val create_range_decl : preid -> Number.int_range -> its_defn
+(** [create_range_decl id ir] creates a new range type declaration. *)
+
 (** {2 Module declarations} *)
 
 type pdecl = private {
@@ -82,7 +85,8 @@ and pdecl_node = private
   | PDexn  of xsymbol
   | PDpure
 
-val create_type_decl : its_defn list -> pdecl
+val create_type_decl :
+  its_defn list -> pdecl * (Theory.meta * Theory.meta_arg list) list
 
 val create_let_decl : let_defn -> pdecl
 

src/mlw/pmodule.ml

@@ -327,7 +327,9 @@ let unit_module =
   let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
   let uc = use_export uc (tuple_module 0) in
   let td = create_alias_decl (id_fresh "unit") [] ity_unit in
-  close_module (add_pdecl_raw uc (create_type_decl [td]))
+  let d,metas = create_type_decl [td] in
+  assert (metas = []);
+  close_module (add_pdecl_raw uc d)
 
 let create_module env ?(path=[]) n =
   let m = empty_module env n path in
@@ -925,7 +927,11 @@ let clone_pdecl inst cl uc d = match d.pd_node with
   | PDtype tdl ->
       let tdl, vcl = clone_type_decl inst cl tdl uc.muc_known in
       if tdl = [] then List.fold_left add_vc uc vcl else
-      add_pdecl ~vc:false uc (create_type_decl tdl)
+        let d,metas = create_type_decl tdl in
+      List.fold_left
+        (fun uc (m,a) -> add_meta uc m a)
+        (add_pdecl ~vc:false uc d)
+        metas
   | PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
       (* refine only [val] symbols *)
       if c.c_node <> Cany then raise (BadInstance rs.rs_name);

src/parser/typing.ml

@@ -786,6 +786,14 @@ let type_term_pure muc lvm denv e =
 let type_fmla_pure muc lvm denv e =
   Dterm.fmla ~strict:true ~keep_loc:true (type_pure muc lvm denv e)
 
+let check_public ~loc d name =
+  if d.td_vis <> Public || d.td_mut then
+    Loc.errorm ~loc
+               "%s types cannot be abstract, private, or mutable"
+               name;
+  if d.td_inv <> [] then
+    Loc.errorm ~loc "%s types cannot have invariants" name
+
 let add_types muc tdl =
   let add m ({td_ident = {id_str = x}; td_loc = loc} as d) =
     Mstr.add_new (Loc.Located (loc, ClashSymbol x)) x d m in
@@ -797,20 +805,14 @@ let add_types muc tdl =
     let args = List.map (fun id -> tv_of_string id.id_str) d.td_params in
     match d.td_def with
     | TDalias pty ->
-        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
-          "Alias types cannot be abstract, private, or mutable";
-        if d.td_inv <> [] then Loc.errorm ~loc
-          "Alias types cannot have invariants";
-        let alias = Sstr.add x alias in
-        let ity = parse ~loc ~alias ~alg pty in
-        if not (Hstr.mem htd x) then
-        let itd = create_alias_decl id args ity in
-        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
+       check_public ~loc d "Alias";
+       let alias = Sstr.add x alias in
+       let ity = parse ~loc ~alias ~alg pty in
+       if not (Hstr.mem htd x) then
+         let itd = create_alias_decl id args ity in
+         Hstr.add hts x itd.itd_its; Hstr.add htd x itd
     | TDalgebraic csl ->
-        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
-          "Algebraic types cannot be abstract, private, or mutable";
-        if d.td_inv <> [] then Loc.errorm ~loc
-          "Algebraic types cannot have invariants";
+       check_public ~loc d "Algebraic";
         let hfd = Hstr.create 5 in
         let alias = Sstr.empty in
         let alg = Mstr.add x (id,args) alg in
@@ -864,10 +866,7 @@ let add_types muc tdl =
 (*      if not (Hstr.mem htd x) then *)
         begin match try Some (Hstr.find hts x) with Not_found -> None with
         | Some s ->
-            if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
-              "Recursive types cannot be abstract, private, or mutable";
-            if d.td_inv <> [] then Loc.errorm ~loc
-              "Recursive types cannot have invariants";
+           check_public ~loc d "Recursive";
             let get_fd (mut, fd) = if mut then Loc.errorm ~loc
               "Recursive types cannot have mutable fields" else fd in
             Hstr.add htd x (create_rec_record_decl s (List.map get_fd fl))
@@ -880,9 +879,24 @@ let add_types muc tdl =
             let type_inv f = type_fmla_pure muc gvars Dterm.denv_empty f in
             let invl = List.map type_inv d.td_inv in
             let itd = create_plain_record_decl ~priv ~mut id args fl invl in
-            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end
-    | TDrange _ -> assert false (* TODO *)
-    | TDfloat _ -> assert false (* TODO *)
+            Hstr.add hts x itd.itd_its; Hstr.add htd x itd
+        end
+    | TDrange (lo,hi) ->
+       check_public ~loc d "Range";
+(*
+        let alias = Sstr.add x alias in
+        let ity = parse ~loc ~alias ~alg pty in
+        if not (Hstr.mem htd x) then
+        let itd = create_alias_decl id args ity in
+        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
+ *)
+       let ir = { Number.ir_lower = lo;
+                  Number.ir_upper = hi } in
+       let itd = create_range_decl id ir in
+       Hstr.add hts x itd.itd_its; Hstr.add htd x itd
+    | TDfloat _ ->
+       check_public ~loc d "Float";
+       assert false (* TODO *)
 
   and parse ~loc ~alias ~alg pty =
     let rec down = function
@@ -914,7 +928,11 @@ let add_types muc tdl =
 
   Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
   let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
-  add_pdecl ~vc:true muc (create_type_decl tdl)
+  let d,metas = create_type_decl tdl in
+  List.fold_left
+    (fun uc (m,a) -> add_meta uc m a)
+    (add_pdecl ~vc:true muc d)
+    metas
 
 let tyl_of_params {muc_theory = tuc} pl =
   let ty_of_param (loc,_,gh,ty) =