Type check theory and operator during expression constructor

README.md

@@ -127,8 +127,8 @@ module Z3 :
 val solver : Z3.t = <abstr>
 
 # let cond =
-    let a = Expr.symbol (Symbol.make Ty.Ty_bool "a") in
-    let b = Expr.symbol (Symbol.make Ty.Ty_bool "b") in
+    let a = Expr.symbol (Symbol.make (Ty.Ty Ty_bool) "a") in
+    let b = Expr.symbol (Symbol.make (Ty.Ty Ty_bool) "b") in
     Expr.(binop Ty_bool And a (unop Ty_bool Not b));;
 val cond : Expr.t = (bool.and a (bool.not b))
 

doc/examples.mld

@@ -72,7 +72,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
 

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
 

doc/index.mld

@@ -93,8 +93,8 @@ Example: Bitvector arithmetic
 {@ocaml[
 # open Smtml;;
 # let cond =
-  let x = Expr.symbol (Symbol.make (Ty_bitv 8) "x") in
-  let y = Expr.symbol (Symbol.make (Ty_bitv 8) "y") in
+  let x = Expr.symbol (Symbol.make (Ty (Ty_bitv 8)) "x") in
+  let y = Expr.symbol (Symbol.make (Ty (Ty_bitv 8)) "y") in
   let sum = Expr.binop (Ty_bitv 8) Add x y in
   let num = Expr.value (Bitv (Bitvector.of_int8 42)) in
   Expr.relop Ty_bool Eq sum num;;
@@ -123,7 +123,7 @@ val model : Model.t = (model
     (x i8 9)
     (y i8 33))
 # let x_val =
-  let x = Symbol.make (Ty_bitv 8) "x" in
+  let x = Symbol.make (Ty (Ty_bitv 8)) "x" in
   Model.evaluate model x;;
 val x_val : Value.t option = Some (Smtml.Value.Bitv <abstr>)
 ]}

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)