(* Rank 2 intersection types a la van Bakel-Barbanera-Fernandez, headers.
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

datatype monotype = CVAR of string
  | CBASE of string
  | CDB of int
  | CFUN of monotype * monotype;

type qtype = int * monotype; (* (n, T) is forall alpha1, ..., alphan . T *)

type rank1type = qtype list; (* non-empty list of qtypes, interpreted as intersection. *)

type rank2type = rank1type list * monotype; (* ([T1, ..., Tn], T) is T1 -> ... -> Tn -> T *)

type tsubst = string -m> monotype;

exception TUnify;

extern val monotype_subst : tsubst -> monotype -> monotype;
extern val monotype_free : tsubst * string -> monotype -> bool;
extern val monotype_unify : tsubst -> monotype * monotype -> tsubst;

extern val monotype_from_rank1 : tsubst -> rank1type -> tsubst;
extern val monotype_from_rank2 : tsubst -> rank2type -> tsubst;

type basis = string -m> rank1type; (* typing context, mapping identifiers to types *)

datatype t_op = TNIL
  | TSUBST of tsubst * t_op
  | TEXP of t_op list (* TEXP [op1, ..., opn]: build intersection of n distinct copies
		       of type; copies being types with their free CVAR's renamed to
		       fresh CVAR's; then apply opi on copy i. *)
  | TCLOS of int * t_op;

extern val rank1type_unify_monotype : tsubst -> rank1type * monotype -> t_op;

