Bind sequence and regular expression theories

This commit is contained in:
Frédéric Bour 2021-12-01 10:36:44 +01:00
parent b654b4d933
commit 4779f41ee4
4 changed files with 258 additions and 0 deletions

View File

@ -59,6 +59,8 @@ type (_, _) zarray = private Sort_zarray
type 'a zset = ('a, bool) zarray
type _ bitvector = private Sort_bitvector
type _ uninterpreted = private Sort_uninterpreted
type _ zseq = private Sort_sequence
type _ zre = private Sort_regexp
type 'ctx datatype_internal = ..
type 'ctx datatype_internal += Datatype_defined of Z3.Sort.sort
@ -151,6 +153,8 @@ module Sort : sig
val real : 'ctx context -> ('ctx, real) sort
val zarray : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'b) sort -> ('ctx, ('a, 'b) zarray) sort
val zset : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'a zset) sort
val zseq : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'a zseq) sort
val zre : 'ctx context -> ('ctx, 'a zseq) sort -> ('ctx, 'a zseq zre) sort
val bitvector : 'ctx context -> 'n natural -> ('ctx, 'n bitvector) sort
val uninterpreted : ('ctx, 'a) Uninterpreted.t -> ('ctx, 'a uninterpreted) sort
val datatype : ('ctx, 'a) datatype -> ('ctx, ('ctx, 'a) datatype) sort
@ -163,6 +167,8 @@ module Sort : sig
| Bitvector : 'n natural -> ('ctx, 'n bitvector) desc
| Uninterpreted : ('ctx, 'n) Uninterpreted.t -> ('ctx, 'n uninterpreted) desc
| Datatype : ('ctx, 'a) datatype -> ('ctx, ('ctx, 'a) datatype) desc
| Zseq : ('ctx, 'a) desc -> ('ctx, 'a zseq) desc
| Zre : ('ctx, 'a zseq) desc -> ('ctx, 'a zseq zre) desc
val make : 'ctx context -> ('ctx, 'a) desc -> ('ctx, 'a) sort
end = struct
@ -173,6 +179,8 @@ end = struct
let zset = Z3.Set.mk_sort
let bitvector ctx nat = Z3.BitVector.mk_sort ctx (Natural.to_int nat)
let uninterpreted = Uninterpreted.to_zsort
let zseq = Z3.Seq.mk_seq_sort
let zre = Z3.Seq.mk_re_sort
let datatype (Sort_datatype dt) =
match dt.internal with
| Datatype_defined sort -> sort
@ -186,6 +194,8 @@ end = struct
| Bitvector : 'n natural -> ('ctx, 'n bitvector) desc
| Uninterpreted : ('ctx, 'n) Uninterpreted.t -> ('ctx, 'n uninterpreted) desc
| Datatype : ('ctx, 'a) datatype -> ('ctx, ('ctx, 'a) datatype) desc
| Zseq : ('ctx, 'a) desc -> ('ctx, 'a zseq) desc
| Zre : ('ctx, 'a zseq) desc -> ('ctx, 'a zseq zre) desc
let rec make : type ctx a. ctx context -> (ctx, a) desc -> (ctx, a) sort =
fun ctx -> function
@ -200,6 +210,8 @@ end = struct
| Datatype_defined sort -> sort
| _ -> invalid_arg "Sort.make: datatype not yet defined"
end
| Zseq desc -> zseq ctx (make ctx desc)
| Zre desc -> zre ctx (make ctx desc)
end
(* Typed FuncDecl *)
@ -781,6 +793,81 @@ end = struct
let mul_no_underflow = Z3.BitVector.mk_mul_no_underflow
end
module Zseq : sig
val empty : 'ctx context -> ('ctx, 'a zseq) sort -> ('ctx, 'a zseq) expr
val unit : 'ctx context -> ('ctx, 'a) expr -> ('ctx, 'a zseq) expr
val concat : 'ctx context -> ('ctx, 'a zseq) expr list -> ('ctx, 'a zseq) expr
val is_prefix : 'ctx context -> ('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val is_suffix : 'ctx context -> ('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val contains : 'ctx context -> container:('ctx, 'a zseq) expr -> containee:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val extract : 'ctx context -> ('ctx, 'a zseq) expr -> offset:('ctx, integer) expr -> length:('ctx, integer) expr -> ('ctx, 'a zseq) expr
val replace : 'ctx context -> in_:('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr -> by:('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr
val at : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr -> ('ctx, 'a zseq) expr
val nth : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr -> ('ctx, 'a) expr
val length : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr
val index : 'ctx context -> in_:('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> from:('ctx, integer) expr -> ('ctx, integer) expr
val last_index : 'ctx context -> in_:('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, integer) expr
end = struct
let empty ctx sort = Z3.Seq.mk_seq_empty ctx sort
let unit ctx expr = Z3.Seq.mk_seq_unit ctx expr
let concat = Z3.Seq.mk_seq_concat
let is_prefix ctx base ~of_ = Z3.Seq.mk_seq_prefix ctx base of_
let is_suffix ctx base ~of_ = Z3.Seq.mk_seq_suffix ctx base of_
let contains ctx ~container ~containee = Z3.Seq.mk_seq_contains ctx container containee
let extract ctx base ~offset ~length = Z3.Seq.mk_seq_extract ctx base offset length
let replace ctx ~in_ replace ~by = Z3.Seq.mk_seq_replace ctx in_ replace by
let at = Z3.Seq.mk_seq_at
let nth ctx seq index = z3_i (Z3native.mk_seq_nth (z3_o ctx) (z3_o seq) (z3_o index))
let length = Z3.Seq.mk_seq_length
let index ctx ~in_ ~of_ ~from = Z3.Seq.mk_seq_index ctx in_ of_ from
let last_index ctx ~in_ ~of_ = z3_i (Z3native.mk_seq_last_index (z3_o ctx) (z3_o in_) (z3_o of_))
end
module Zre : sig
val seq_to_re : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq zre) expr
val seq_in_re : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq zre) expr -> ('ctx, bool) expr
val plus : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val star : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val option : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val union : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
val concat : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
val intersect : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
(*val range : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr -> ('ctx, 'a zre) expr*)
val loop : 'ctx context -> ?min:int -> ?max:int -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val complement : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val empty : 'ctx context -> ('ctx, 'a zre) sort -> ('ctx, 'a zre) expr
val full : 'ctx context -> ('ctx, 'a zre) sort -> ('ctx, 'a zre) expr
end = struct
let seq_to_re = Z3.Seq.mk_seq_to_re
let seq_in_re = Z3.Seq.mk_seq_in_re
let plus = Z3.Seq.mk_re_plus
let star = Z3.Seq.mk_re_star
let option = Z3.Seq.mk_re_option
let union = Z3.Seq.mk_re_union
let concat = Z3.Seq.mk_re_concat
let intersect ctx res = Z3.Seq.mk_re_intersect ctx (List.length res) res
(*let range = Z3.Seq.mk_re_range *)
let loop ctx ?(min=0) ?(max=0) re = Z3.Seq.mk_re_loop ctx re min max
let complement = Z3.Seq.mk_re_complement
let empty = Z3.Seq.mk_re_empty
let full = Z3.Seq.mk_re_full
end
(*module M_8 = Natural.Nth(struct let n = 8 end)
type _8 = M_8.n
let _8 = M_8.n
type zbyte = _8 bitvector
type zstring = zbyte zseq
module Zstring : sig
val of_string : 'ctx context -> string -> ('ctx, zstring) expr
val lt : 'ctx context -> ('ctx, zstring) expr -> ('ctx, zstring) expr -> ('ctx, bool) expr
val le : 'ctx context -> ('ctx, zstring) expr -> ('ctx, zstring) expr -> ('ctx, bool) expr
val to_int : 'ctx context -> ('ctx, zstring) expr -> ('ctx, integer) expr
val of_int : 'ctx context -> ('ctx, integer) expr -> ('ctx, zstring) expr
end*)
module Model : sig
val eval_expr : 'ctx model -> ('ctx, 'a) expr -> ('ctx, 'a) expr option
@ -837,6 +924,10 @@ end = struct
failwith "Ztl.Model: Uninterpreted sorts not supported yet"
| Datatype _ ->
failwith "Ztl.Model: Datatype sorts not supported yet"
| Zseq _ ->
failwith "Ztl.Model: Sequence sorts not supported yet"
| Zre _ ->
failwith "Ztl.Model: Regular expression sorts not supported yet"
and inject
: type ctx a. ctx context -> (ctx, a) Sort.desc -> a value -> (ctx, a) expr

View File

@ -59,6 +59,10 @@ type _ bitvector = private Sort_bitvector
See [Uninterpreted] module for manipulating of uninterpreted sorts. *)
type _ uninterpreted = private Sort_uninterpreted
(** Representation of Z3 sequences and regular expressions *)
type _ zseq = private Sort_sequence
type _ zre = private Sort_regexp
type ('ctx, 'a) datatype =
Sort_datatype of { mutable internal: 'ctx datatype_internal }
and 'ctx datatype_internal
@ -128,6 +132,8 @@ module Sort : sig
val real : 'ctx context -> ('ctx, real) sort
val zarray : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'b) sort -> ('ctx, ('a, 'b) zarray) sort
val zset : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'a zset) sort
val zseq : 'ctx context -> ('ctx, 'a) sort -> ('ctx, 'a zseq) sort
val zre : 'ctx context -> ('ctx, 'a zseq) sort -> ('ctx, 'a zseq zre) sort
val bitvector : 'ctx context -> 'n natural -> ('ctx, 'n bitvector) sort
val uninterpreted : ('ctx, 'a) Uninterpreted.t -> ('ctx, 'a uninterpreted) sort
val datatype : ('ctx, 'a) datatype -> ('ctx, ('ctx, 'a) datatype) sort
@ -140,6 +146,8 @@ module Sort : sig
| Bitvector : 'n natural -> ('ctx, 'n bitvector) desc
| Uninterpreted : ('ctx, 'n) Uninterpreted.t -> ('ctx, 'n uninterpreted) desc
| Datatype : ('ctx, 'a) datatype -> ('ctx, ('ctx, 'a) datatype) desc
| Zseq : ('ctx, 'a) desc -> ('ctx, 'a zseq) desc
| Zre : ('ctx, 'a zseq) desc -> ('ctx, 'a zseq zre) desc
val make : 'ctx context -> ('ctx, 'a) desc -> ('ctx, 'a) sort
end
@ -387,6 +395,51 @@ module Bitvector : sig
(* repeat : context -> int -> Expr.term -> Expr.term*)
end
module Zseq : sig
val empty : 'ctx context -> ('ctx, 'a zseq) sort -> ('ctx, 'a zseq) expr
val unit : 'ctx context -> ('ctx, 'a) expr -> ('ctx, 'a zseq) expr
val concat : 'ctx context -> ('ctx, 'a zseq) expr list -> ('ctx, 'a zseq) expr
val is_prefix : 'ctx context -> ('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val is_suffix : 'ctx context -> ('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val contains : 'ctx context -> container:('ctx, 'a zseq) expr -> containee:('ctx, 'a zseq) expr -> ('ctx, bool) expr
val extract : 'ctx context -> ('ctx, 'a zseq) expr -> offset:('ctx, integer) expr -> length:('ctx, integer) expr -> ('ctx, 'a zseq) expr
val replace : 'ctx context -> in_:('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr -> by:('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr
val at : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr -> ('ctx, 'a zseq) expr
val nth : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr -> ('ctx, 'a) expr
val length : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, integer) expr
val index : 'ctx context -> in_:('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> from:('ctx, integer) expr -> ('ctx, integer) expr
val last_index : 'ctx context -> in_:('ctx, 'a zseq) expr -> of_:('ctx, 'a zseq) expr -> ('ctx, integer) expr
end
(*type _8
val _8 : _8 natural
type zbyte = _8 bitvector
type zstring = zbyte zseq
module Zstring : sig
val of_string : 'ctx context -> string -> ('ctx, zstring) expr
val lt : 'ctx context -> ('ctx, zstring) expr -> ('ctx, zstring) expr -> ('ctx, bool) expr
val le : 'ctx context -> ('ctx, zstring) expr -> ('ctx, zstring) expr -> ('ctx, bool) expr
val to_int : 'ctx context -> ('ctx, zstring) expr -> ('ctx, integer) expr
val of_int : 'ctx context -> ('ctx, integer) expr -> ('ctx, zstring) expr
end*)
module Zre : sig
val seq_to_re : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq zre) expr
val seq_in_re : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq zre) expr -> ('ctx, bool) expr
val plus : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val star : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val option : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val union : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
val concat : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
val intersect : 'ctx context -> ('ctx, 'a zre) expr list -> ('ctx, 'a zre) expr
(*val range : 'ctx context -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq) expr -> ('ctx, 'a zseq zre) expr*)
val loop : 'ctx context -> ?min:int -> ?max:int -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val complement : 'ctx context -> ('ctx, 'a zre) expr -> ('ctx, 'a zre) expr
val empty : 'ctx context -> ('ctx, 'a zre) sort -> ('ctx, 'a zre) expr
val full : 'ctx context -> ('ctx, 'a zre) sort -> ('ctx, 'a zre) expr
end
module Model : sig
val eval_expr : 'ctx model -> ('ctx, 'a) expr -> ('ctx, 'a) expr option

View File

@ -42,6 +42,10 @@ module type MONO = sig
See [Uninterpreted] module for manipulating of uninterpreted sorts. *)
type 'a uninterpreted = 'a Poly.uninterpreted
(** Representation of Z3 sequences and regular expressions *)
type 'a zseq = 'a Poly.zseq
type 'a zre = 'a Poly.zre
type 'a datatype = (ctx, 'a) Poly.datatype
(** Z3 uninterpreted sorts *)
@ -107,6 +111,8 @@ module type MONO = sig
val bitvector : 'n natural -> 'n bitvector sort
val uninterpreted : 'a Uninterpreted.t -> 'a uninterpreted sort
val datatype : 'a datatype -> 'a datatype sort
val zseq : 'a sort -> 'a zseq sort
val zre : 'a zseq sort -> 'a zseq zre sort
type 'a desc = (ctx, 'a) Poly.Sort.desc
val make : 'a desc -> 'a sort
@ -320,6 +326,38 @@ module type MONO = sig
(* repeat : context -> int -> Expr.term -> Expr.term*)
end
module Zseq : sig
val empty : 'a zseq sort -> 'a zseq expr
val unit : 'a expr -> 'a zseq expr
val concat : 'a zseq expr list -> 'a zseq expr
val is_prefix : 'a zseq expr -> of_:'a zseq expr -> bool expr
val is_suffix : 'a zseq expr -> of_:'a zseq expr -> bool expr
val contains : container:'a zseq expr -> containee:'a zseq expr -> bool expr
val extract : 'a zseq expr -> offset:integer expr -> length:integer expr -> 'a zseq expr
val replace : in_:'a zseq expr -> 'a zseq expr -> by:'a zseq expr -> 'a zseq expr
val at : 'a zseq expr -> integer expr -> 'a zseq expr
val nth : 'a zseq expr -> integer expr -> 'a expr
val length : 'a zseq expr -> integer expr
val index : in_:'a zseq expr -> of_:'a zseq expr -> from:integer expr -> integer expr
val last_index : in_:'a zseq expr -> of_:'a zseq expr -> integer expr
end
module Zre : sig
val seq_to_re : 'a zseq expr -> 'a zseq zre expr
val seq_in_re : 'a zseq expr -> 'a zseq zre expr -> bool expr
val plus : 'a zre expr -> 'a zre expr
val star : 'a zre expr -> 'a zre expr
val option : 'a zre expr -> 'a zre expr
val union : 'a zre expr list -> 'a zre expr
val concat : 'a zre expr list -> 'a zre expr
val intersect : 'a zre expr list -> 'a zre expr
(*val range : 'a zseq expr -> 'a zseq expr -> 'a zre expr*)
val loop : ?min:int -> ?max:int -> 'a zre expr -> 'a zre expr
val complement : 'a zre expr -> 'a zre expr
val empty : 'a zre sort -> 'a zre expr
val full : 'a zre sort -> 'a zre expr
end
module Model : sig
val eval_expr : model -> 'a expr -> 'a expr option
@ -386,6 +424,10 @@ struct
See [Uninterpreted] module for manipulating of uninterpreted sorts. *)
type 'a uninterpreted = 'a Poly.uninterpreted
(** Representation of Z3 sequences and regular expressions *)
type 'a zseq = 'a Poly.zseq
type 'a zre = 'a Poly.zre
type 'a datatype = (ctx, 'a) Poly.datatype
(** Z3 uninterpreted sorts *)
@ -454,6 +496,8 @@ struct
let bitvector x = Poly.Sort.bitvector context x
let uninterpreted = Poly.Sort.uninterpreted
let datatype = Poly.Sort.datatype
let zseq x = Poly.Sort.zseq context x
let zre x = Poly.Sort.zre context x
type 'a desc = (ctx, 'a) Poly.Sort.desc
let make x = Poly.Sort.make context x
@ -638,6 +682,38 @@ struct
(* repeat : context -> int -> Expr.term -> Expr.term*)
end
module Zseq = struct
let empty x = Poly.Zseq.empty context x
let unit x = Poly.Zseq.unit context x
let concat x = Poly.Zseq.concat context x
let is_prefix x = Poly.Zseq.is_prefix context x
let is_suffix x = Poly.Zseq.is_suffix context x
let contains ~container ~containee =
Poly.Zseq.contains context ~container ~containee
let extract x = Poly.Zseq.extract context x
let replace ~in_ = Poly.Zseq.replace context ~in_
let at x = Poly.Zseq.at context x
let nth x = Poly.Zseq.nth context x
let length x = Poly.Zseq.length context x
let index ~in_ = Poly.Zseq.index context ~in_
let last_index ~in_ = Poly.Zseq.last_index context ~in_
end
module Zre = struct
let seq_to_re x = Poly.Zre.seq_to_re context x
let seq_in_re x = Poly.Zre.seq_in_re context x
let plus x = Poly.Zre.plus context x
let star x = Poly.Zre.star context x
let option x = Poly.Zre.option context x
let union x = Poly.Zre.union context x
let concat x = Poly.Zre.concat context x
let intersect x = Poly.Zre.intersect context x
let loop ?min ?max x = Poly.Zre.loop context ?min ?max x
let complement x = Poly.Zre.complement context x
let empty x = Poly.Zre.empty context x
let full x = Poly.Zre.full context x
end
module Model = struct
let eval_expr = Poly.Model.eval_expr

View File

@ -42,6 +42,10 @@ module type MONO = sig
See [Uninterpreted] module for manipulating of uninterpreted sorts. *)
type 'a uninterpreted = 'a Poly.uninterpreted
(** Representation of Z3 sequences and regular expressions *)
type 'a zseq = 'a Poly.zseq
type 'a zre = 'a Poly.zre
type 'a datatype = (ctx, 'a) Poly.datatype
(** Z3 uninterpreted sorts *)
@ -107,6 +111,8 @@ module type MONO = sig
val bitvector : 'n natural -> 'n bitvector sort
val uninterpreted : 'a Uninterpreted.t -> 'a uninterpreted sort
val datatype : 'a datatype -> 'a datatype sort
val zseq : 'a sort -> 'a zseq sort
val zre : 'a zseq sort -> 'a zseq zre sort
type 'a desc = (ctx, 'a) Poly.Sort.desc
val make : 'a desc -> 'a sort
@ -320,6 +326,38 @@ module type MONO = sig
(* repeat : context -> int -> Expr.term -> Expr.term*)
end
module Zseq : sig
val empty : 'a zseq sort -> 'a zseq expr
val unit : 'a expr -> 'a zseq expr
val concat : 'a zseq expr list -> 'a zseq expr
val is_prefix : 'a zseq expr -> of_:'a zseq expr -> bool expr
val is_suffix : 'a zseq expr -> of_:'a zseq expr -> bool expr
val contains : container:'a zseq expr -> containee:'a zseq expr -> bool expr
val extract : 'a zseq expr -> offset:integer expr -> length:integer expr -> 'a zseq expr
val replace : in_:'a zseq expr -> 'a zseq expr -> by:'a zseq expr -> 'a zseq expr
val at : 'a zseq expr -> integer expr -> 'a zseq expr
val nth : 'a zseq expr -> integer expr -> 'a expr
val length : 'a zseq expr -> integer expr
val index : in_:'a zseq expr -> of_:'a zseq expr -> from:integer expr -> integer expr
val last_index : in_:'a zseq expr -> of_:'a zseq expr -> integer expr
end
module Zre : sig
val seq_to_re : 'a zseq expr -> 'a zseq zre expr
val seq_in_re : 'a zseq expr -> 'a zseq zre expr -> bool expr
val plus : 'a zre expr -> 'a zre expr
val star : 'a zre expr -> 'a zre expr
val option : 'a zre expr -> 'a zre expr
val union : 'a zre expr list -> 'a zre expr
val concat : 'a zre expr list -> 'a zre expr
val intersect : 'a zre expr list -> 'a zre expr
(*val range : 'a zseq expr -> 'a zseq expr -> 'a zre expr*)
val loop : ?min:int -> ?max:int -> 'a zre expr -> 'a zre expr
val complement : 'a zre expr -> 'a zre expr
val empty : 'a zre sort -> 'a zre expr
val full : 'a zre sort -> 'a zre expr
end
module Model : sig
val eval_expr : model -> 'a expr -> 'a expr option