Dterm, Dexpr: allow destructible types for casts and constants

src/core/dterm.ml

@@ -103,6 +103,8 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with
       List.iter2 dty_unify dl1 dl2
   | _ -> raise Exit
 
+let dty_int  = Duty ty_int
+let dty_real = Duty ty_real
 let dty_bool = Duty ty_bool
 
 let protect_on x s = if x then "(" ^^ s ^^ ")" else s
@@ -184,7 +186,7 @@ and dpattern_node =
   | DPapp of lsymbol * dpattern list
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
-  | DPcast of dpattern * ty
+  | DPcast of dpattern * dty
 
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff | DTby | DTso
@@ -203,7 +205,7 @@ type dterm = {
 and dterm_node =
   | DTvar of string * dty
   | DTgvar of vsymbol
-  | DTconst of Number.constant * ty
+  | DTconst of Number.constant * dty
   | DTapp of lsymbol * dterm list
   | DTfapp of dterm * dterm
   | DTif of dterm * dterm * dterm
@@ -215,7 +217,7 @@ and dterm_node =
   | DTnot of dterm
   | DTtrue
   | DTfalse
-  | DTcast of dterm * ty
+  | DTcast of dterm * dty
   | DTuloc of dterm * Loc.position
   | DTlabel of dterm * Slab.t
 
@@ -317,8 +319,7 @@ let dpattern ?loc node =
         dp1.dp_dty, Mstr.union join dp1.dp_vars dp2.dp_vars
     | DPas (dp,{pre_name = n}) ->
         dp.dp_dty, Mstr.add_new (DuplicateVar n) n dp.dp_dty dp.dp_vars
-    | DPcast (dp,ty) ->
-        let dty = dty_of_ty ty in
+    | DPcast (dp,dty) ->
         dpat_expected_type dp dty;
         dty, dp.dp_vars in
   let dty, vars = Loc.try1 ?loc get_dty node in
@@ -395,8 +396,8 @@ let dterm tuc ?loc node =
         mk_dty (Some dty)
     | DTgvar vs ->
         mk_dty (Some (dty_of_ty vs.vs_ty))
-    | DTconst (_,ty) ->
-        mk_dty (Some (dty_of_ty ty))
+    | DTconst (_,dty) ->
+        mk_dty (Some dty)
     | DTapp (ls, dtl) when ls_equal ls ps_equ ->
        let swap, dtl =
          match dtl with
@@ -490,8 +491,7 @@ let dterm tuc ?loc node =
            there is no need to count these constructs as "formulas" which
            require explicit if-then-else conversion to bool *)
         mk_dty (Some dty_bool)
-    | DTcast (dt,ty) ->
-        let dty = dty_of_ty ty in
+    | DTcast (dt,dty) ->
         dterm_expected_dterm tuc dt dty
     | DTuloc (dt,_)
     | DTlabel (dt,_) ->
@@ -606,8 +606,8 @@ and try_term strict keep_loc uloc env prop dty node =
       t_var (Mstr.find_exn (UnboundVar n) n env)
   | DTgvar vs ->
       t_var vs
-  | DTconst (c,ty) ->
-      t_const c ty
+  | DTconst (c,dty) ->
+      t_const c (term_ty_of_dty ~strict dty)
   | DTapp (ls,[]) when ls_equal ls fs_bool_true ->
       if prop then t_true else t_bool_true
   | DTapp (ls,[]) when ls_equal ls fs_bool_false ->

src/core/dterm.mli

@@ -28,6 +28,8 @@ val dty_app : tysymbol -> dty list -> dty
 val dty_match : dty -> ty  -> unit (* raises Exit on failure *)
 val dty_unify : dty -> dty -> unit (* raises Exit on failure *)
 
+val dty_int  : dty
+val dty_real : dty
 val dty_bool : dty
 
 val dty_fold : (tysymbol -> 'a list -> 'a) ->
@@ -48,7 +50,7 @@ and dpattern_node =
   | DPapp of lsymbol * dpattern list
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
-  | DPcast of dpattern * ty
+  | DPcast of dpattern * dty
 
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff | DTby | DTso
@@ -67,7 +69,7 @@ type dterm = private {
 and dterm_node =
   | DTvar of string * dty
   | DTgvar of vsymbol
-  | DTconst of Number.constant * ty
+  | DTconst of Number.constant * dty
   | DTapp of lsymbol * dterm list
   | DTfapp of dterm * dterm
   | DTif of dterm * dterm * dterm
@@ -79,7 +81,7 @@ and dterm_node =
   | DTnot of dterm
   | DTtrue
   | DTfalse
-  | DTcast of dterm * ty
+  | DTcast of dterm * dty
   | DTuloc of dterm * Loc.position
   | DTlabel of dterm * Slab.t
 

src/mlw/dexpr.ml

@@ -362,7 +362,7 @@ type dpattern_node =
   | DPapp  of rsymbol * dpattern list
   | DPas   of dpattern * preid * bool
   | DPor   of dpattern * dpattern
-  | DPcast of dpattern * ity
+  | DPcast of dpattern * dity
 
 (** Specifications *)
 
@@ -618,7 +618,7 @@ let drec_defn denv0 prel =
     denv_add_rec denv denv0.frozen id (argl,res) in
   let denv1 = List.fold_left add denv0 prel in
   let parse (id,gh,pk,bl,res,msk,pre) =
-    let dsp, dvl, de = pre (denv_add_args denv1 bl) in
+    let dsp, dvl, de = pre denv1 in
     dexpr_expected_type de res;
     (id,gh,pk,bl,res,msk,dsp,dvl,de) in
   let fdl = List.map parse prel in
@@ -668,8 +668,8 @@ let dpattern ?loc node =
         let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
         let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
         mk_dpat (PPas (pat, id, gh)) dity vars
-    | DPcast (dp, ity) ->
-        dpat_expected_type dp (dity_of_ity ity);
+    | DPcast (dp, dity) ->
+        dpat_expected_type dp dity;
         dp
   in
   Loc.try1 ?loc dpat node

src/mlw/dexpr.mli

@@ -46,7 +46,7 @@ type dpattern_node =
   | DPapp  of rsymbol * dpattern list
   | DPas   of dpattern * preid * bool
   | DPor   of dpattern * dpattern
-  | DPcast of dpattern * ity
+  | DPcast of dpattern * dity
 
 (** Binders *)
 

src/parser/typing.ml

@@ -131,6 +131,13 @@ let ty_of_pty tuc pty =
   in
   get_ty pty
 
+let dty_of_pty tuc pty =
+  Dterm.dty_of_ty (ty_of_pty tuc pty)
+
+let dty_of_opt tuc = function
+  | Some pty -> dty_of_pty tuc pty
+  | None -> Dterm.dty_fresh ()
+
 let ity_of_pty muc pty =
   let rec get_ity = function
     | PTtyvar {id_str = x} ->
@@ -150,6 +157,13 @@ let ity_of_pty muc pty =
   in
   get_ity pty
 
+let dity_of_pty muc pty =
+  Dexpr.dity_of_ity (ity_of_pty muc pty)
+
+let dity_of_opt muc = function
+  | Some pty -> dity_of_pty muc pty
+  | None -> Dexpr.dity_fresh ()
+
 (** typing using destructive type variables
 
     parsed trees        intermediate trees       typed trees
@@ -191,16 +205,13 @@ let rec dpattern tuc { pat_desc = desc; pat_loc = loc } =
         DPapp (cs,fl)
     | Ptree.Pas (p, x, false) -> DPas (dpattern tuc p, create_user_id x)
     | Ptree.Por (p, q) -> DPor (dpattern tuc p, dpattern tuc q)
-    | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, ty_of_pty tuc ty)
+    | Ptree.Pcast (p, ty) -> DPcast (dpattern tuc p, dty_of_pty tuc ty)
     | Ptree.Pvar (_, true) | Ptree.Pas (_, _, true) -> Loc.errorm ~loc
         "ghost variables are only allowed in programs")
 
 let quant_var tuc (loc, id, gh, ty) =
   if gh then Loc.errorm ~loc "ghost variables are only allowed in programs";
-  let ty = match ty with
-    | Some ty -> dty_of_ty (ty_of_pty tuc ty)
-    | None    -> dty_fresh () in
-  Opt.map create_user_id id, ty, Some loc
+  Opt.map create_user_id id, dty_of_opt tuc ty, Some loc
 
 let loc_cutoff loc13 loc23 loc2 =
   let f,l,b,e = Loc.get loc13 in
@@ -293,9 +304,9 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
             apply loc de1 op1 (dterm tuc gvars at denv e23) in
       chain loc (dterm tuc gvars at denv e1) op1 e23
   | Ptree.Tconst (Number.ConstInt _ as c) ->
-      DTconst (c, ty_int)
+      DTconst (c, dty_int)
   | Ptree.Tconst (Number.ConstReal _ as c) ->
-      DTconst (c, ty_real)
+      DTconst (c, dty_real)
   | Ptree.Tlet (x, e1, e2) ->
       let id = create_user_id x in
       let e1 = dterm tuc gvars at denv e1 in
@@ -370,12 +381,10 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
   | Ptree.Tnamed (Lstr lab, e1) ->
       DTlabel (dterm tuc gvars at denv e1, Slab.singleton lab)
   | Ptree.Tcast ({term_desc = Ptree.Tconst c}, pty) ->
-      let ty = ty_of_pty tuc pty in
-      DTconst (c, ty)
+      DTconst (c, dty_of_pty tuc pty)
   | Ptree.Tcast (e1, pty) ->
       let d1 = dterm tuc gvars at denv e1 in
-      let ty = ty_of_pty tuc pty in
-      DTcast (d1, ty))
+      DTcast (d1, dty_of_pty tuc pty))
 
 (** typing program expressions *)
 
@@ -435,7 +444,7 @@ let rec dpattern muc { pat_desc = desc; pat_loc = loc } =
         DPapp (cs,fl)
     | Ptree.Ptuple pl ->
         DPapp (rs_tuple (List.length pl), List.map (dpattern muc) pl)
-    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, ity_of_pty muc pty)
+    | Ptree.Pcast (p, pty) -> DPcast (dpattern muc p, dity_of_pty muc pty)
     | Ptree.Pas (p, x, gh) -> DPas (dpattern muc p, create_user_id x, gh)
     | Ptree.Por (p, q) -> DPor (dpattern muc p, dpattern muc q))
 
@@ -543,16 +552,11 @@ let dinvariant muc f lvm _xsm old = dpre muc f lvm old
 
 (* abstract values *)
 
-let dbinder muc id gh pty =
-  let id = Opt.map create_user_id id in
-  let dity = match pty with
-    | Some pty -> dity_of_ity (ity_of_pty muc pty)
-    | None -> dity_fresh () in
-  id, gh, dity
+let dparam muc (_,id,gh,pty) =
+  Opt.map create_user_id id, gh, dity_of_pty muc pty
 
-let dparam muc (_,id,gh,pty) = dbinder muc id gh (Some pty)
-
-let dbinder muc (_,id,gh,pty) = dbinder muc id gh pty
+let dbinder muc (_,id,gh,opt) =
+  Opt.map create_user_id id, gh, dity_of_opt muc opt
 
 (* expressions *)
 
@@ -669,10 +673,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
         | ({term_loc = loc},_)::_ ->
             Loc.errorm ~loc "unexpected 'variant' clause"
         | _ -> dspec muc sp in
+      let dity = dity_of_opt muc pty in
       let denv = denv_add_args denv bl in
-      let dity = match pty with
-        | Some pty -> dity_of_ity (ity_of_pty muc pty)
-        | None -> dity_fresh () in
       let denv = denv_add_exn denv old_mark_id dity in
       DEfun (bl, dity, msk, ds, dexpr muc denv e)
   | Ptree.Eany (pl, kind, pty, msk, sp) ->
@@ -758,7 +760,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       DEghost (dexpr muc denv e1)
   | Ptree.Eexn (id, pty, mask, e1) ->
       let id = create_user_id id in
-      let dity = dity_of_ity (ity_of_pty muc pty) in
+      let dity = dity_of_pty muc pty in
       let denv = denv_add_exn denv id dity in
       DEexn (id, dity, mask, dexpr muc denv e1)
   | Ptree.Eabsurd ->
@@ -783,21 +785,18 @@ 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 ({expr_desc = Ptree.Econst c}, pty) ->
-      let ity = ity_of_pty muc pty in
-      DEconst (c, dity_of_ity ity)
+      DEconst (c, dity_of_pty muc pty)
   | Ptree.Ecast (e1, pty) ->
       let d1 = dexpr muc denv e1 in
-      let ity = ity_of_pty muc pty in
-      DEcast (d1, dity_of_ity ity)
+      DEcast (d1, dity_of_pty muc pty)
   end
 
 and drec_defn muc denv fdl =
   let prep (id, gh, kind, bl, pty, msk, sp, e) =
     let bl = List.map (dbinder muc) bl in
-    let dity = match pty with
-      | Some pty -> dity_of_ity (ity_of_pty muc pty)
-      | None -> dity_fresh () in
+    let dity = dity_of_opt muc pty in
     let pre denv =
+      let denv = denv_add_args denv bl in
       let denv = denv_add_exn denv old_mark_id dity in
       let dv = dvariant muc sp.sp_variant in
       dspec muc sp, dv, dexpr muc denv e in