restore support for literal constant

examples/hackers-delight.mlw

@@ -10,8 +10,8 @@ theory Utils
 
   use import bv.BV32
 
-  let constant one : t = 1
-  let constant two : t = 2
+  let constant one : t = (1:bool)
+  let constant two : t = (2:t)
   let constant lastbit : t = sub size_bv one
 
   function max (x y : t) : t = (if ult x y then y else x)

src/core/term.ml

@@ -826,12 +826,14 @@ let t_nat_const n =
 
 exception InvalidLiteralType of ty
 
-let t_const c ty =
+let check_literal c ty =
   let ts = match ty.ty_node with
     | Tyapp (ts,[]) -> ts
     | _ -> raise (InvalidLiteralType ty) in
-  begin match c with
+  match c with
     | Number.ConstInt c when not (ts_equal ts ts_int) ->
+       Format.eprintf "check literal %a of type %s@."
+                      Number.print_integer_constant c ts.ts_name.id_string;
         begin match ts.ts_def with
           | Range ir -> Number.check_range c ir
           | _ -> raise (InvalidLiteralType ty)
@@ -842,8 +844,8 @@ let t_const c ty =
           | _ -> raise (InvalidLiteralType ty)
         end
     | _ -> ()
-  end;
-  t_const c ty
+
+let t_const c ty = check_literal c ty; t_const c ty
 
 let t_if f t1 t2 =
   t_ty_check t2 t1.t_ty;
@@ -1675,4 +1677,3 @@ module TermTF = struct
   let tr_fold fnT fnF = tr_fold (t_selecti fnT fnF)
   let tr_map_fold fnT fnF = tr_map_fold (t_selecti fnT fnF)
 end
-

src/core/term.mli

@@ -201,6 +201,8 @@ val t_app_infer : lsymbol -> term list -> term
 val ls_arg_inst : lsymbol -> term list -> ty Mtv.t
 val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
 
+val check_literal : Number.constant -> ty -> unit
+
 val t_var : vsymbol -> term
 val t_const : Number.constant -> ty -> term
 val t_if : term -> term -> term -> term

src/mlw/dexpr.ml

@@ -224,8 +224,10 @@ let dity_real = Dapp (its_real, [], [])
 let dity_bool = Dapp (its_bool, [], [])
 let dity_unit = Dapp (its_unit, [], [])
 
+(*
 let dvty_int  = [], dity_int
 let dvty_real = [], dity_real
+*)
 let dvty_bool = [], dity_bool
 let dvty_unit = [], dity_unit
 
@@ -403,7 +405,7 @@ and dexpr_node =
   | DEpv of pvsymbol
   | DErs of rsymbol
   | DEls of lsymbol
-  | DEconst of Number.constant
+  | DEconst of Number.constant * dity
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * mask * dspec later * dexpr
   | DEany of dbinder list * mask * dspec later * dity
@@ -641,10 +643,7 @@ let dexpr ?loc node =
         specialize_rs rs
     | DEls ls ->
         specialize_ls ls
-    | DEconst (Number.ConstInt _) ->
-        dvty_int
-    | DEconst (Number.ConstReal _) ->
-        dvty_real
+    | DEconst (_, ity) -> [],ity
     | DEapp ({de_dvty = (arg::argl, res)}, de2) ->
         dexpr_expected_type de2 arg;
         argl, res
@@ -1139,8 +1138,8 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
       e_var (get_pv env n)
   | DEpv v ->
       e_var v
-  | DEconst c ->
-      e_const c
+  | DEconst(c,dity) ->
+     e_const c (ity_of_dity dity)
   | DEapp ({de_dvty = ([],_)} as de1, de2) ->
       let e1 = expr uloc env de1 in
       let e2 = expr uloc env de2 in

src/mlw/dexpr.mli

@@ -23,8 +23,12 @@ val dity_fresh : unit -> dity
 
 val dity_of_ity : ity -> dity
 
+val dity_int : dity
+val dity_real : dity
+
 type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
 
+
 (** Patterns *)
 
 type dpattern = private {
@@ -92,7 +96,7 @@ and dexpr_node =
   | DEpv of pvsymbol
   | DErs of rsymbol
   | DEls of lsymbol
-  | DEconst of Number.constant
+  | DEconst of Number.constant * dity
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * mask * dspec later * dexpr
   | DEany of dbinder list * mask * dspec later * dity

src/mlw/expr.ml

@@ -463,14 +463,12 @@ let e_var ({pv_ity = ity; pv_ghost = ghost} as v) =
   let eff = eff_ghostify ghost (eff_read_single v) in
   mk_expr (Evar v) ity MaskVisible eff
 
-let e_const c =
-  let ity = match c with
-    | Number.ConstInt  _ -> ity_int
-    | Number.ConstReal _ -> ity_real in
+let e_const c ity =
+  Term.check_literal c (ty_of_ity ity);
   mk_expr (Econst c) ity MaskVisible eff_empty
 
 let e_nat_const n =
-  e_const (Number.ConstInt (Number.int_const_dec (string_of_int n)))
+  e_const (Number.ConstInt (Number.int_const_dec (string_of_int n))) ity_int
 
 let e_ghostify gh ({e_effect = eff} as e) =
   if not gh then e else

src/mlw/expr.mli

@@ -190,7 +190,7 @@ val c_any : cty -> cexp
 
 val e_var : pvsymbol -> expr
 
-val e_const : Number.constant -> expr
+val e_const : Number.constant -> ity -> expr
 val e_nat_const : int -> expr
 
 val e_exec : cexp -> expr

src/mlw/pmodule.ml

@@ -829,7 +829,7 @@ let clone_ppat cl sm pp mask =
 
 let rec clone_expr cl sm e = e_label_copy e (match e.e_node with
   | Evar v -> e_var (sm_find_pv sm v)
-  | Econst c -> e_const c
+  | Econst c -> e_const c e.e_ity
   | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
   | Eassign asl ->
       let conv (r,f,v) =

src/parser/typing.ml

@@ -618,7 +618,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
         | e23 ->
             apply loc de1 op1 (dexpr muc denv e23) in
       chain "q1 " "q2 " loc (dexpr muc denv e1) op1 e23
-  | Ptree.Econst c -> DEconst c
+  | Ptree.Econst (Number.ConstInt _ as c) -> DEconst(c, dity_int)
+  | Ptree.Econst (Number.ConstReal _ as c) -> DEconst(c, dity_real)
   | Ptree.Erecord fl ->
       let ls_of_rs rs = match rs.rs_logic with
         | RLls ls -> ls | _ -> assert false in
@@ -747,7 +748,12 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
   | Ptree.Enamed (Lstr lab, e1) ->
       DElabel (dexpr muc denv e1, Slab.singleton lab)
   | Ptree.Ecast (e1, pty) ->
-      DEcast (dexpr muc denv e1, ity_of_pty muc pty))
+      let e1 = dexpr muc denv e1 in
+      let ity = ity_of_pty muc pty in
+      let dity = dity_of_ity ity in
+      match e1.de_node with
+      | DEconst (c, _) -> DEconst (c, dity)
+      | _ -> DEcast (e1, ity))
 
 and drec_defn muc denv fdl =
   let prep (id, gh, kind, bl, pty, msk, sp, e) =