Module Model

module Model: sig .. end

Model

type 'a printer = Format.formatter -> 'a -> unit

type 'a prec_printer = TermInner.prec -> 'a printer

type 'a to_sexp = 'a -> Sexp_lib.t

Decision Trees

A decision tree is a nested if/then/else used to describe functions over finite domains.

module DT: sig .. end

Helpers for Decision Trees

module DT_util: sig .. end

Models

type symbol_kind =

`\|`	`Symbol_prop`
`\|`	`Symbol_fun`
`\|`	`Symbol_utype`
`\|`	`Symbol_data`
`\|`	`Symbol_codata`

type ('t, 'ty) value_def = 't * ('t, 'ty) DT.t * symbol_kind

type ('t, 'ty) t = {

`values : ('t, 'ty) value_def list;`
`finite_types : ('ty * ID.t list) list;`
`potentially_spurious : bool;`	`(*`	the model might be spurious, i.e. some approximation made the translation unsound	`*)`

}

A model

type ('a, 'b) model = ('a, 'b) t

val empty : ('a, 'b) t

Empty model

val empty_copy : ('t, 'ty) t -> ('t, 'ty) t

empty_copy m is a empty model that has the same additional information (such as potentially_spurious) as m

val add_const : ('t, 'ty) t -> 't * 't * symbol_kind -> ('t, 'ty) t

Add a constant term interpretation

val add_value : ('t, 'ty) t ->
       't * ('t, 'ty) DT.t * symbol_kind -> ('t, 'ty) t

Add a value interpretation

val add_finite_type : ('t, 'ty) t -> 'ty -> ID.t list -> ('t, 'ty) t

Map the type to its finite domain.

val values : ('t, 'ty) t ->
       ('t * ('t, 'ty) DT.t * symbol_kind) Sequence.t

val finite_types : ('a, 'ty) t -> ('ty * ID.t list) Sequence.t

val fold : ?values:('acc -> 'a * ('a, 'b) DT.t * symbol_kind -> 'acc) ->
       ?finite_types:('acc -> 'b * ID.t list -> 'acc) ->
       'acc -> ('a, 'b) t -> 'acc

val iter : ?values:('a * ('a, 'b) DT.t * symbol_kind -> unit) ->
       ?finite_types:('b * ID.t list -> unit) -> ('a, 'b) t -> unit

val filter_map : values:('t1 * ('t1, 'ty1) DT.t * symbol_kind ->
               ('t2 * ('t2, 'ty2) DT.t * symbol_kind) option) ->
       finite_types:('ty1 * ID.t list -> ('ty2 * ID.t list) option) ->
       ('t1, 'ty1) t -> ('t2, 'ty2) t

val map : term:('t1 -> 't2) ->
       ty:('ty1 -> 'ty2) -> ('t1, 'ty1) t -> ('t2, 'ty2) t

val filter : ?values:('t * ('t, 'ty) DT.t * symbol_kind -> bool) ->
       ?finite_types:('ty * ID.t list -> bool) ->
       ('t, 'ty) t -> ('t, 'ty) t

val print : 't prec_printer -> 'ty printer -> ('t, 'ty) t printer

Debug printing

val to_sexp : 't to_sexp -> 'ty to_sexp -> ('t, 'ty) t to_sexp

S-expr output suitable for parsing from the caller

module Default: sig .. end