Module Syn_term.Make

Parameters

Signature

type const = A.const
type id = A.id
type ty = A.ty
type var = A.var
type pattern =
| P_or of pattern * pattern
| P_var of var
| P_construct of {
c : id;
ty : ty;
args : pattern list;
lbls : id list option;
}
| P_tuple of ty * pattern list
| P_record of ty * (id * pattern) list
| P_any of ty
| P_alias of var * pattern
| P_true
| P_false
| P_const of const * ty
type t =
| Const of const * ty
| If of t * t * t
| Let of Syn_term_intf.rec_flag * binding list * t
| Apply of ty * t * t list
| Fun of ty * var * t
| Ident of var
| Construct of {
c : id;
ty : ty;
args : t list;
lbls : id list option;
}
| Tuple of ty * t list
| Field of {
data_ty : ty;
ty : ty;
f : id;
t : t;
}
| Record of ty * (id * t) list * t option
| Match of {
loc : Imandra_util.Iloc.t option;
ty : ty;
lhs : t;
bs : t vb list;
}
| Let_match of {
loc : Imandra_util.Iloc.t option;
flg : Syn_term_intf.rec_flag;
bs : t vb list;
body : t;
}
| True
| False
| As of t * ty
and binding = var * t
and 't vb = {
pat : pattern;
when_ : 't option;
expr : 't;
}
val pattern_ty : pattern -> ty
val var : var -> t
val apply : ty:ty -> t -> t list -> t
val equal_const : const -> const -> bool
val equal_id : id -> id -> bool
val equal_var : var -> var -> bool
val equal_ty : ty -> ty -> bool
val equal : t -> t -> bool