(************************************************************
   typing.ml		Created      : Sat Aug  9 01:48:11 2003
  			Last modified: Sat Aug 09 02:54:09 2003
  Compile: ocamlc typing.ml -o typing #
  FTP Directory: sources/ocaml #
************************************************************)
(**

  @author Takashi Masuyama <mamewo@dk9.so-net.ne.jp>

*)

exception UnifyError of string

type mini_type =
    Var of string
  | INT
  | STRING
  | Function of mini_type * mini_type
  | Pair of mini_type * mini_type

type substitution =
    Substitution of string * mini_type

(** for debug *)
let print_substs_domains =
  List.iter (fun (Substitution(id, _)) -> print_endline id)

let rec print_mini_type = function
  | Var v -> ("'"^v)
  | INT -> "int"
  | STRING -> "string"
  | Function (t1, t2) -> (print_mini_type t1)^" -> "^(print_mini_type t2)
  | Pair (t1, t2) -> (print_mini_type t1)^", "^(print_mini_type t2)

let rec occur_check var_id = function
    INT | STRING -> false
  | Var id -> id = var_id
  | Function (t1, t2) | Pair (t1, t2) ->
      (occur_check var_id t1) || (occur_check var_id t2)

let rec subst t substs = 
  match t with
    INT | STRING -> t
  | Var id2 ->
      (try 
	let Substitution(id, totype) =
	  List.find (fun (Substitution(id, _)) -> id = id2) substs in
	totype
      with Not_found ->
	t)
  | Function(t1, t2) ->
      Function((subst t1 substs), (subst t2 substs))
  | Pair (t1, t2) ->
      Pair((subst t1 substs), (subst t2 substs))
	
let rec uniqueness_check lst =
  match lst with
    [] | [_] -> true
  | hd::tl -> 
      (not (List.mem hd tl)) && uniqueness_check tl

let rec unify2 t1 t2 s1 s2 =
  let (substs1, fsttype) = unify t1 s1 in
  let tt2 = subst t2 substs1 in
  let ss2 = subst s2 substs1 in
  (* tt2 and ss2 doesn't contain domain of substs1 *)
  (* So, substs2 doesn't contain domain of substs1 *)
  let (substs2, sndtype) = unify tt2 ss2 in
  let sub = List.append substs1 substs2 in
  (* check *)
(*  print_endline "substs1 domain --------";*)
(*  print_substs_domains substs1;*)
(*  print_endline "substs2 domain --------";*)
(*  print_substs_domains substs2;*)
  if uniqueness_check sub then
    (sub, fsttype, sndtype)
  else
    failwith "unique algorithm bug?"
and unify t1 t2 =
  match (t1, t2) with
    (INT, INT)
  | (STRING, STRING) -> ([], t1)
  | (Var id1, Var id2) ->
      if id1 = id2 then ([], t1)
      else ([ Substitution (id1, t2) ], t2)
  | (Var id, t) | (t, Var id) ->
      if occur_check id t then
	raise (UnifyError "occur check")
      else ([ Substitution(id, t) ], t)
  | (Function(t1, t2), Function(s1, s2)) ->
      let (sub, fsttype, sndtype) = unify2 t1 t2 s1 s2 in
      (sub, Function(fsttype, sndtype))
  | (Pair(t1, t2), Pair(s1, s2)) ->
      let (sub, fsttype, sndtype) = unify2 t1 t2 s1 s2 in
      (sub, Pair(fsttype, sndtype))
  | _ -> raise (UnifyError ("inconpatible type: "^
		(print_mini_type t1)^" / "^(print_mini_type t2)))

let result = 
  let t1 = Function (Var "a", Var "a") in
  let t2 = Function (INT, Var "b") in
  unify t1 t2

(* fail *)
let result2 = 
  let t1 = Function (Var "a", Var "a") in
  let t2 = Function (INT, Function (INT, Var "b")) in
  unify t1 t2

let occur =
  let t1 = Var "a" in
  let t2 = Function (Var "a", INT) in
  unify t1 t2