package dolmen_type
Builtin functions manipulations
A convenient function for merging a list of builtin parser functions into a single builtin function.
Smtlib Indexed id helpers
type 'ret indexed = [
| `Not_indexed
| `Unary of string -> 'ret
| `Binary of string -> string -> 'ret
| `Ternary of string -> string -> string -> 'ret
| `Nary of int * (string list -> 'ret)
]
The type of indexed family of operators.
val parse_indexed :
string ->
string list ->
(string -> 'ret indexed) ->
err:(string -> int -> int -> 'ret) ->
k:(unit -> 'ret) ->
'ret
parse_id basename indexes f ~err ~k
uses the function f
to get an expected arity for the indexed identifier, and then tries and parse the index list according to the returned specification.
val bad_ty_index_arity :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
'env ->
string ->
int ->
int ->
[> `Ty of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> 'ty ]
Suitable err
function for parse_id
for typing sort indexed families.
val bad_term_index_arity :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
'env ->
string ->
int ->
int ->
[> `Term of Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> 'term ]
Suitable err
function for parse_id
for typing term indexed families.
Low-level helpers
type ('env, 'args, 'ret) helper =
(module Tff_intf.S with type env = 'env) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'args -> 'ret) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ret
val make_op0 : (_, unit, _) helper
make_op (module Type) env ast op arity args ret
checks that args is the empty list and returns Some (ret ())
, else it raises the appropriate exception from the typechecking module.
val make_op1 : (_, Dolmen.Std.Term.t, _) helper
Same as make_op0
but the returning function takes a term as argument.
val make_op2 : (_, Dolmen.Std.Term.t * Dolmen.Std.Term.t, _) helper
Same as make_op0
but the returning function takes a couple of terms as argument.
val make_op3 :
(_, Dolmen.Std.Term.t * Dolmen.Std.Term.t * Dolmen.Std.Term.t, _) helper
Same as make_op0
but the returning function takes a triple of terms as argument.
val make_op4 :
(_,
Dolmen.Std.Term.t
* Dolmen.Std.Term.t
* Dolmen.Std.Term.t
* Dolmen.Std.Term.t,
_)
helper
Same as make_op0
but the returning function takes a quadruple of terms as argument.
val make_opn : int -> (_, Dolmen.Std.Term.t list, _) helper
Same as make_op0
but takes an arity first, and the returning function takes a list of terms as argument. The list is guaranteed to have the same length as the given arity.
val make_assoc : (_, Dolmen.Std.Term.t list, _) helper
Ensures the list of arguments is at least of size 2 (used for associative symbols).
Fold application of a left-associative function on a list.
Fold application of a right-associative function on a list.
val make_chain : (_, Dolmen.Std.Term.t list, _) helper
Ensures the list of arguments is at least of size 2 (used for chainable symbols).
val map_chain :
(module Tff_intf.S with type T.t = 't) ->
('t -> 't -> 't) ->
't list ->
't
Map a function on succesive pairs of elements in the arguments lists, and build the resulting conjunction. map_chain (module Type) mk [t1; t2; ..; tn]
is Type.T._and [mk t1 t2; mk t2 t3; ..]
High level helpers
val app0 :
(module Tff_intf.S with type env = 'env) ->
?check:(Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
'ret ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ret
val app0_ast :
(module Tff_intf.S with type env = 'env) ->
?check:(Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'ret) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ret
val ty_app1 :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
('ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val ty_app1_ast :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val term_app1 :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
('term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app1_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val ty_app2 :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
('ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val ty_app2_ast :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val term_app2 :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app2_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val ty_app3 :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
('ty -> 'ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val ty_app3_ast :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'ty -> 'ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val term_app3 :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app3_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val ty_app4 :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
('ty -> 'ty -> 'ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val ty_app4_ast :
(module Tff_intf.S with type env = 'env and type Ty.t = 'ty) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'ty -> 'ty -> 'ty -> 'ty -> 'ty) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'ty
val term_app4 :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app4_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:
(Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t ->
unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_list :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
('term list -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_list_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term list -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_left :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_left_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_right :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_right_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_chain :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
('term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_chain_ast :
(module Tff_intf.S with type env = 'env and type T.t = 'term) ->
?check:(Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> unit) ->
'env ->
Intf.symbol ->
(Dolmen.Std.Term.t -> 'term -> 'term -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_cst :
(module Tff_intf.S
with type env = 'env
and type T.t = 'term
and type T.Const.t = 'cst) ->
'env ->
'cst ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_ho :
(module Thf_intf.S with type env = 'env and type T.t = 'term) ->
'env ->
'term ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term
val term_app_ho_ast :
(module Thf_intf.S with type env = 'env and type T.t = 'term) ->
'env ->
(Dolmen.Std.Term.t -> 'term) ->
Dolmen.Std.Term.t ->
Dolmen.Std.Term.t list ->
'term