package dolmen_type

  1. Overview
  2. Docs

Source file tff_intf.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

(** External Typechecker interface for TFF

    This module defines the external typechcker interface, that is,
    the interface of an instantiated typechecker. *)

(** {1 Typechecker interface} *)

(** Typechecker interface *)
module type S = sig

  (** {2 Module aliases} *)
  module Tag: Dolmen.Intf.Tag.S
  module Ty: Dolmen.Intf.Ty.Tff
    with type 'a tag := 'a Tag.t
     and type path := Dolmen.Std.Path.t
  module T: Dolmen.Intf.Term.Tff
    with type ty := Ty.t
     and type ty_var := Ty.Var.t
     and type ty_const := Ty.Const.t
     and type 'a tag := 'a Tag.t
     and type path := Dolmen.Std.Path.t

  include Intf.Formulas
    with type ty := Ty.t
     and type ty_var := Ty.Var.t
     and type ty_cst := Ty.Const.t
     and type term := T.t
     and type term_var := T.Var.t
     and type term_cst := T.Const.t
     and type term_cstr := T.Cstr.t
     and type term_field := T.Field.t
     and type 'a ast_tag := 'a Tag.t

end