(* Rank 2 intersection types a la van Bakel-Barbanera-Fernandez.
   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.
*)

open "types_h";

fun monotype_subst sigma =
    let fun tsubst (mt as CVAR name) =
	    if name inset sigma
		then ?sigma name
	    else mt
	  | tsubst (CFUN (mt1, mt2)) = CFUN (tsubst mt1, tsubst mt2)
	  | tsubst mt = mt
    in
	tsubst
    end;

fun monotype_free (sigma, xname) =
    let fun free (mt as CVAR name) =
	    if name inset sigma
		then free (?sigma name)
	    else xname=name
	  | free (CFUN (mt1, mt2)) = free mt1 orelse free mt2
	  | free _ = false
    in
	free
    end;

fun monotype_unify sigma =
    let fun unify (mt, mt') =
	    if mt=mt'
		then sigma
	    else case mt of
		     CVAR name => if name inset sigma
				      then unify (?sigma name, mt')
				  else if monotype_free (sigma, name) mt'
				      then raise TUnify
				  else sigma ++ {name => mt'}
		   | _ => case mt' of
			      CVAR name' => if name' inset sigma
						then unify (mt, ?sigma name')
					    else if monotype_free (sigma, name') mt
						then raise TUnify
					    else sigma ++ {name' => mt}
			    | CFUN (mt'1, mt'2) =>
			      (case mt of
				   CFUN (mt1, mt2) =>
				   monotype_unify (unify (mt1, mt'1)) (mt2, mt'2)
				 | _ => raise TUnify)
			    | _ => raise TUnify
    in
	unify
    end;

fun monotype_from_inter sigma =
    let fun from_inter nil = raise TUnify
	  | from_inter [_] = sigma
	  | from_inter (mt::(l as [mt', ...])) =
	    monotype_from_inter (monotype_unify sigma (mt, mt')) l
    in
	from_inter
    end;

fun monotype_from_rank1 sigma =
    let val from_inter = monotype_from_inter sigma
	fun from_rank1 (l : rank1type) =
	    from_inter [if n=0
			    then mt
			else raise TUnify
		       | (n, mt) in list l]
    in
	from_rank1
    end;

fun monotype_from_rank1list sigma =
    let val from_rank1 = monotype_from_rank1 sigma
	fun from_rank1list nil = sigma
	  | from_rank1list (rank1::l) =
	    monotype_from_rank1list (from_rank1 rank1) l
    in
	from_rank1list
    end;

fun monotype_from_rank2 sigma =
    let val from_rank1list = monotype_from_rank1list sigma
	fun from_rank2 (rank1list, mt) =
	    from_rank1list rank1list
    in
	from_rank2
    end;

fun rank1type_unify_monotype sigma =
    let val munify = monotype_unify sigma
	fun unify (nil, _) = nil
	  | unify ((n, mt1)::l, mt) =
	    TSUBST (munify (mt1, mt), TCLOS (n, TNIL)) :: unify (l, mt)
    in
	fn (rank1type, mt) => TEXP (unify (rank1type, mt))
    end;

