package inferno

  1. Overview
  2. Docs

Source file SolverSig.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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
(******************************************************************************)
(*                                                                            *)
(*                                  Inferno                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the MIT License, as described in the file LICENSE.               *)
(*                                                                            *)
(******************************************************************************)

(* This file defines some of the input signatures of the functor [Solver.Make]. *)

(* -------------------------------------------------------------------------- *)

(* The type of term variables is described to the solver as follows. *)

(* This signature is isomorphic to [Map.OrderedType] in OCaml's standard
   library. *)

(* BEGIN TEVAR *)
module type TEVAR = sig

  (* The type of term variables. *)
  type tevar

  (* A total ordering. *)
  val compare: tevar -> tevar -> int

(* END *)
end  
(* END TEVAR *)

(* -------------------------------------------------------------------------- *)

(* The structure of types *after decoding* is described to the solver as
   follows. *)

(* BEGIN OUTPUT *)
module type OUTPUT = sig

  (* The solver represents type variables via unique integer identifiers. *)
  type tyvar = int

  (* The solver works with first-order types whose structure is defined by
     the type ['a structure], as in the signature [Unifier.STRUCTURE]. *)
  type 'a structure

  (* The solver constructs decoded types of type [ty], and never deconstructs
     them. So, the operations that the solver requires are constructors for
     the type [ty]. *)
  type ty

  (* [variable v] is a representation of the type variable [v] as a decoded
     type. In other words, [variable] is an injection of [tyvar] into [ty]. *)
  val variable: tyvar -> ty

  (* [structure t] turns [t], an application of type constructor to children
     of type [ty], into something of type [ty]. In other words, when [variable]
     and [structure] are combined, we see that [ty] must contain the fixed point
     of the functor [\X. tyvar + t X]. *)
  val structure: ty structure -> ty

  (* If [v] is a type variable and [t] is a type, then [mu v t] is a
     representation of the recursive type [mu v.t]. This function is used in
     one of two situations: 1- the occurs check is disabled, so the solver
     produces recursive types; or 2- the occurs check is enabled, but the
     types carried by the exceptions [Unify] and [Cycle] can still be cyclic,
     and one may wish to decode and display them. *)
  val mu: tyvar -> ty -> ty

  (* A decoded type scheme consists of a list of quantifiers and a body. *)
  type scheme = tyvar list * ty

(* END *)
end
(* END OUTPUT *)
OCaml

Innovation. Community. Security.