SortUnification.mli 2.29 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
(* This module implements sort inference. *)

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

(* The syntax of sorts is:

     sort ::= (sort, ..., sort) -> *

   where the arity (the number of sorts on the left-hand side of the arrow)
   can be zero. *)

type 'a structure =
  | Arrow of 'a list

type sort =
  | TVar of int
  | TNode of sort structure

32 33 34
type ground_sort =
  | GArrow of ground_sort list

35 36 37 38 39 40 41 42
(* -------------------------------------------------------------------------- *)

(* Sort unification. *)

type variable

val star: variable
val arrow: variable list -> variable
43 44
val fresh: unit -> variable

45 46 47 48
(* [domain] is the opposite of [arrow]. If [x] has been unified with an arrow,
   then [domain x] returns its domain. Otherwise, it returns [None]. Use with
   caution. *)
val domain: variable -> variable list option
49 50 51 52 53 54 55 56 57

exception Unify of variable * variable
exception Occurs of variable * variable
val unify: variable -> variable -> unit

(* Once unification is over, a unification variable can be decoded as a sort. *)

val decode: variable -> sort

58 59 60 61 62
(* Grounding a sort replaces all sort variables with the sort [*]. *)

val ground: sort -> ground_sort
val unground: ground_sort -> sort

63 64 65 66 67
(* -------------------------------------------------------------------------- *)

(* A sort can be printed. *)

val print: sort -> string