(* Unification on Formulas *)
(* Author: Carsten Schuermann *)

functor TomegaUnify
  (structure IntSyn' : INTSYN
   structure Tomega' : TOMEGA
     sharing Tomega'.IntSyn = IntSyn'
   structure Abstract : ABSTRACT
     sharing Abstract.IntSyn = IntSyn'
   structure TypeCheck : TYPECHECK
     sharing TypeCheck.IntSyn = IntSyn'
   structure Conv : CONV
     sharing Conv.IntSyn = IntSyn'
   structure Normalize : NORMALIZE
     sharing Normalize.IntSyn = IntSyn'
     sharing Normalize.Tomega = Tomega'
   structure Whnf : WHNF
     sharing Whnf.IntSyn = IntSyn'
   structure Print : PRINT
     sharing Print.IntSyn = IntSyn'
   structure TomegaPrint : TOMEGAPRINT
     sharing TomegaPrint.IntSyn = IntSyn'
     sharing TomegaPrint.Tomega = Tomega'
   structure Subordinate : SUBORDINATE
     sharing Subordinate.IntSyn = IntSyn'
   structure Weaken : WEAKEN
     sharing Weaken.IntSyn = IntSyn') : TOMEGAUNIFY = 
struct
  structure IntSyn = IntSyn'
  structure Tomega = Tomega'

  exception Unify of string 
  
  local 
    structure I = IntSyn'
    structure T = Tomega

    (* unifyFor (Psi, F1, F2) = R

       Invariant:
       If   F1, F2 contain free variables X1 ... Xn
       and  Psi |- F1 for
       and  Psi |- F2 for
       and  there exists an instantiation I for X1 ...Xn such that
       and  Psi[I] |- F1[I] = F2[I]
       then R = ()
       otherwise exception Unify is raised
    *) 

    fun unifyFor (Psi, F1, F2) = 
          unifyForN (Psi, 
		     Normalize.normalizeFor (F1, T.id), 
		     Normalize.normalizeFor (F2, T.id))
    and unifyForN (Psi, T.True, T.True) = ()
      | unifyForN (Psi, T.Ex (D1, F1), T.Ex (D2, F2)) = 
        (unifyDec (Psi, T.UDec D1, (T.UDec D2));
	 unifyFor(I.Decl (Psi, T.UDec D1), F1, F2))
      | unifyForN (Psi, T.All (D1, F1), T.All (D2, F2)) = 
	(unifyDec (Psi, D1, D2);
	 unifyFor(I.Decl (Psi, D1), F1, F2))
      | unifyForN (Psi, T.FVar (_, r), F) = 
	(r := SOME F)
      | unifyForN (Psi, F, T.FVar (_, r)) = 
	(r := SOME F)
      | unifyForN (Psi, _, _) = raise Unify "Formula mismatch"

   
    (* unifyDec (Psi, D1, D2) = R

       Invariant:
       If   D1, D2 contain free variables X1 ... Xn
       and  Psi |- D1 dec
       and  Psi |- D2 dec
       and  there exists an instantiation I for X1 ...Xn such that
       and  Psi[I] |- D1[I] = D2[I]
       then R = ()
       otherwise exception Unify is raised
    *) 
    and unifyDec (Psi, T.UDec D1, T.UDec D2) = 
          if Conv.convDec ((D1, I.id), (D2, I.id)) then () 
	  else raise Unify "Declaration mismatch"
      | unifyDec (Psi, T.PDec (_, F1), T.PDec (_, F2)) =
	  unifyFor (Psi, F1, F2)



  in
    val unifyFor = unifyFor
  end
end