Skip to content

Commit 5db3d81

Browse files
filipeomfilipeom
committed
Type check expressions during construction
1 parent 794db70 commit 5db3d81

23 files changed

+727
-650
lines changed

‎doc/examples/product_mix.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ let read_int () = Scanf.scanf " %d" (fun x -> x)
55

66
let int x = Expr.value (Int x)
77

8-
let symbol x = Expr.symbol Symbol.(x @: Ty_int)
8+
let symbol x = Expr.symbol Symbol.(x @: Ty Ty_int)
99

1010
let ( = ) i1 i2 = Expr.relop Ty_bool Eq i1 i2
1111

‎src/smtml/altergo_mappings.default.ml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ module Fresh = struct
176176
let get_statistics _ = assert false
177177
end
178178

179-
let ty_to_aety (ty : Ty.t) : AEL.Ty.t =
179+
let ty_to_aety (Ty ty : Ty.t) : AEL.Ty.t =
180180
match ty with
181181
| Ty_bool -> Tbool
182182
| Ty_int -> Tint
@@ -187,10 +187,10 @@ module Fresh = struct
187187

188188
let aety_to_ty (ty : AEL.Ty.t) : Ty.t =
189189
match ty with
190-
| Tbool -> Ty_bool
191-
| Tint -> Ty_int
192-
| Treal -> Ty_real
193-
| Tbitv n -> Ty_bitv n
190+
| Tbool -> Ty Ty_bool
191+
| Tint -> Ty Ty_int
192+
| Treal -> Ty Ty_real
193+
| Tbitv n -> Ty (Ty_bitv n)
194194
| _ -> assert false
195195

196196
let sym_to_aeid Symbol.{ ty; name; _ } : AEL.Id.typed =
@@ -236,7 +236,7 @@ module Fresh = struct
236236
| Some q -> Real (Q.to_float q)
237237
| None -> (
238238
match (DM.Value.extract ~ops:DM.Bitv.ops v, ty) with
239-
| Some z, Ty_bitv n -> Bitv (Bitvector.make z n)
239+
| Some z, Ty (Ty_bitv n) -> Bitv (Bitvector.make z n)
240240
| _ ->
241241
Fmt.failwith "Altergo_mappings: dvalue_to_value(%a)"
242242
DM.Value.print v ) ) )
@@ -320,4 +320,4 @@ end
320320

321321
include Fresh.Make ()
322322

323-
let is_available = Internals.is_available
323+
let is_available = true

‎src/smtml/dolmenexpr_to_expr.ml‎

Lines changed: 43 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -156,9 +156,11 @@ module DolmenIntf = struct
156156

157157
let to_ety (ty : DTy.t) : Ty.t =
158158
match ty with
159-
| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty_int
160-
| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty_real
161-
| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty_bool
159+
| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty Ty_int
160+
| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } ->
161+
Ty Ty_real
162+
| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } ->
163+
Ty Ty_bool
162164
| { ty_descr =
163165
TyApp
164166
( { builtin = DBuiltin.Base
@@ -168,13 +170,13 @@ module DolmenIntf = struct
168170
, _ )
169171
; _
170172
} ->
171-
Ty_str
173+
Ty Ty_str
172174
| { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->
173-
Ty_bitv n
175+
Ty (Ty_bitv n)
174176
| { ty_descr = TyApp ({ builtin = DBuiltin.Float (8, 24); _ }, _); _ } ->
175-
Ty_fp 32
177+
Ty (Ty_fp 32)
176178
| { ty_descr = TyApp ({ builtin = DBuiltin.Float (11, 53); _ }, _); _ } ->
177-
Ty_fp 64
179+
Ty (Ty_fp 64)
178180
| _ -> Fmt.failwith {|Unsupported dolmen type "%a"|} DTy.print ty
179181
end
180182

@@ -352,23 +354,24 @@ end
352354

353355
let tty_of_etype (e : Ty.t) : DTy.t =
354356
match e with
355-
| Ty_int -> DTy.int
356-
| Ty_real -> DTy.real
357-
| Ty_bool -> DTy.bool
358-
| Ty_str -> Builtin.string_ty
359-
| Ty_bitv 8 -> DTy.bitv 8
360-
| Ty_bitv 32 -> DTy.bitv 32
361-
| Ty_bitv 64 -> DTy.bitv 64
362-
| Ty_fp 32 -> Builtin.float32_ty
363-
| Ty_fp 64 -> Builtin.float64_ty
364-
| Ty_fp _ | Ty_bitv _ | Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp ->
357+
| Ty Ty_int -> DTy.int
358+
| Ty Ty_real -> DTy.real
359+
| Ty Ty_bool -> DTy.bool
360+
| Ty Ty_str -> Builtin.string_ty
361+
| Ty (Ty_bitv 8) -> DTy.bitv 8
362+
| Ty (Ty_bitv 32) -> DTy.bitv 32
363+
| Ty (Ty_bitv 64) -> DTy.bitv 64
364+
| Ty (Ty_fp 32) -> Builtin.float32_ty
365+
| Ty (Ty_fp 64) -> Builtin.float64_ty
366+
| Ty (Ty_fp _ | Ty_bitv _ | Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp)
367+
->
365368
Fmt.failwith {|Unsupported type "%a"|} Ty.pp e
366369

367370
let tty_to_etype (ty : DTy.t) : Ty.t =
368371
match ty with
369-
| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty_int
370-
| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty_real
371-
| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty_bool
372+
| { ty_descr = TyApp ({ builtin = DBuiltin.Int; _ }, _); _ } -> Ty Ty_int
373+
| { ty_descr = TyApp ({ builtin = DBuiltin.Real; _ }, _); _ } -> Ty Ty_real
374+
| { ty_descr = TyApp ({ builtin = DBuiltin.Prop; _ }, _); _ } -> Ty Ty_bool
372375
| { ty_descr =
373376
TyApp
374377
( { builtin = DBuiltin.Base
@@ -378,12 +381,13 @@ let tty_to_etype (ty : DTy.t) : Ty.t =
378381
, _ )
379382
; _
380383
} ->
381-
Ty_str
382-
| { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } -> Ty_bitv n
384+
Ty Ty_str
385+
| { ty_descr = TyApp ({ builtin = DBuiltin.Bitv n; _ }, _); _ } ->
386+
Ty (Ty_bitv n)
383387
| { ty_descr = TyApp ({ builtin = DBuiltin.Float (8, 24); _ }, _); _ } ->
384-
Ty_fp 32
388+
Ty (Ty_fp 32)
385389
| { ty_descr = TyApp ({ builtin = DBuiltin.Float (11, 53); _ }, _); _ } ->
386-
Ty_fp 64
390+
Ty (Ty_fp 64)
387391
| _ -> Fmt.failwith {|Unsupported dolmen type "%a"|} DTy.print ty
388392

389393
module SHT = Hashtbl.Make (struct
@@ -827,60 +831,60 @@ let encode_val : Value.t -> expr = function
827831
| Num (F64 x) -> Fp.encode_val C64 x
828832
| v -> Fmt.failwith {|Unsupported value "%a"|} Value.pp v
829833

830-
let encode_unop (ty : Ty.t) =
834+
let encode_unop (Ty ty as ty_ : Ty.t) =
831835
match ty with
832836
| Ty_int -> I.encode_unop
833837
| Ty_real -> Real.encode_unop
834838
| Ty_bool -> Boolean.encode_unop
835839
| Ty_str -> Str.encode_unop
836840
| Ty_bitv _ -> Bv.encode_unop
837841
| Ty_fp _ -> Fp.encode_unop
838-
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as op ->
839-
Fmt.failwith {|Trying to encode unsupported op of type %a|} Ty.pp op
842+
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) ->
843+
Fmt.failwith {|Trying to encode unsupported op of type %a|} Ty.pp ty_
840844

841-
let encode_binop (ty : Ty.t) =
845+
let encode_binop (Ty ty as ty_ : Ty.t) =
842846
match ty with
843847
| Ty_int -> I.encode_binop
844848
| Ty_real -> Real.encode_binop
845849
| Ty_bool -> Boolean.encode_binop
846850
| Ty_str -> Str.encode_binop
847851
| Ty_bitv _ -> Bv.encode_binop
848852
| Ty_fp _ -> Fp.encode_binop
849-
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as op ->
850-
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp op
853+
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) ->
854+
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp ty_
851855

852-
let encode_triop (ty : Ty.t) =
856+
let encode_triop (Ty ty as ty_ : Ty.t) =
853857
match ty with
854858
| Ty_int -> I.encode_triop
855859
| Ty_real -> Real.encode_triop
856860
| Ty_bool -> Boolean.encode_triop
857861
| Ty_str -> Str.encode_triop
858862
| Ty_bitv _ -> Bv.encode_triop
859863
| Ty_fp _ -> Fp.encode_triop
860-
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as op ->
861-
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp op
864+
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) ->
865+
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp ty_
862866

863-
let encode_relop (ty : Ty.t) =
867+
let encode_relop (Ty ty as ty_ : Ty.t) =
864868
match ty with
865869
| Ty_int -> I.encode_relop
866870
| Ty_real -> Real.encode_relop
867871
| Ty_bool -> Boolean.encode_relop
868872
| Ty_str -> Str.encode_relop
869873
| Ty_bitv _ -> Bv.encode_relop
870874
| Ty_fp _ -> Fp.encode_relop
871-
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as op ->
872-
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp op
875+
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) ->
876+
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp ty_
873877

874-
let encode_cvtop (ty : Ty.t) =
878+
let encode_cvtop (Ty ty as ty_ : Ty.t) =
875879
match ty with
876880
| Ty_int -> I.encode_cvtop
877881
| Ty_real -> Real.encode_cvtop
878882
| Ty_bool -> Boolean.encode_cvtop
879883
| Ty_str -> Str.encode_cvtop
880884
| Ty_bitv sz -> Bv.encode_cvtop sz
881885
| Ty_fp sz -> Fp.encode_cvtop sz
882-
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as op ->
883-
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp op
886+
| (Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) ->
887+
Fmt.failwith "Trying to encode unsupported op of type %a" Ty.pp ty_
884888

885889
let encode_expr_acc ?(record_sym = fun acc _ -> acc) acc e =
886890
let rec aux acc (e : Expr.t) =

0 commit comments

Comments
 (0)