Type check expressions during construction

Author: filipeom

doc/examples/product_mix.ml

@@ -5,7 +5,7 @@ let read_int () = Scanf.scanf " %d" (fun x -> x)
 
 let int x = Expr.value (Int x)
 
-let symbol x = Expr.symbol Symbol.(x @: Ty_int)
+let symbol x = Expr.symbol Symbol.(x @: Ty Ty_int)
 
 let ( = ) i1 i2 = Expr.relop Ty_bool Eq i1 i2
 

src/smtml/altergo_mappings.default.ml

@@ -221,10 +221,10 @@ module M = struct
     module Model = struct
       let aety_to_ty (ty : AEL.Ty.t) : Ty.t =
         match ty with
-        | Tbool -> Ty_bool
-        | Tint -> Ty_int
-        | Treal -> Ty_real
-        | Tbitv n -> Ty_bitv n
+        | Tbool -> Ty Ty_bool
+        | Tint -> Ty Ty_int
+        | Treal -> Ty Ty_real
+        | Tbitv n -> Ty (Ty_bitv n)
         | _ -> assert false
 
       let aeid_to_sym ((hs, tyl, ty) : AEL.Id.typed) =

src/smtml/dolmenexpr_to_expr.ml

@@ -150,9 +150,11 @@ module DolmenIntf = struct
 
     let to_ety (ty : DTy.t) : Ty.t =
       match ty with
-      | { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty_int
-      | { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty_real
-      | { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty_bool
+      | { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty Ty_int
+      | { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } ->
+        Ty Ty_real
+      | { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } ->
+        Ty Ty_bool
       | { ty_descr =
             TyApp
               ( { builtin = DBuiltin.Base
@@ -162,13 +164,13 @@ module DolmenIntf = struct
               , _ )
         ; _
         } ->
-        Ty_str
+        Ty Ty_str
       | { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->
-        Ty_bitv n
+        Ty (Ty_bitv n)
       | { ty_descr = TyApp ({ builtin = DBuiltin.Float (8, 24); _ }, _); _ } ->
-        Ty_fp 32
+        Ty (Ty_fp 32)
       | { ty_descr = TyApp ({ builtin = DBuiltin.Float (11, 53); _ }, _); _ } ->
-        Ty_fp 64
+        Ty (Ty_fp 64)
       | _ -> Fmt.failwith {|Unsupported dolmen type "%a"|} DTy.print ty
   end
 

src/smtml/dune

@@ -51,6 +51,7 @@
   symbol
   ty
   utils
+  utils_parse
   value
   z3_mappings)
  (private_modules lexer parser)