----------------------------------------------------------------------
-- |
-- Module      : Unify
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/04/21 16:22:31 $ 
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.4 $
--
-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
--
-- brute-force adaptation of the old-GF program AR 21\/12\/2001 ---
-- the only use is in 'TypeCheck.splitConstraints'
-----------------------------------------------------------------------------

module GF.Grammar.Unify (unifyVal) where

import GF.Grammar
import GF.Data.Operations

import GF.Text.Pretty
import Data.List (partition)

unifyVal :: Constraints -> Err (Constraints,MetaSubst)
unifyVal cs0 = do
  let (cs1,cs2) = partition notSolvable cs0 
  let (us,vs) = unzip cs2
  let us' = map val2term us
  let vs' = map val2term vs
  let (ms,cs) = unifyAll (zip us' vs') []
  return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs], 
          [(m,          VClos [] t) | (m,t) <- ms])
 where
   notSolvable (v,w) = case (v,w) of -- don't consider nonempty closures
     (VClos (_:_) _,_) -> True
     (_,VClos (_:_) _) -> True
     _ -> False

type Unifier = [(MetaId, Term)]
type Constrs = [(Term, Term)]

unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
unifyAll [] g = (g, [])
unifyAll ((a@(s, t)) : l) g =
  let (g1, c) = unifyAll l g
  in case unify s t g1 of
       Ok g2  -> (g2, c)
       _      -> (g1, a : c)

unify :: Term -> Term -> Unifier -> Err Unifier
unify e1 e2 g = 
 case (e1, e2) of 
  (Meta s, t) -> do
     tg <- subst_all g t
     let sg = maybe e1 id (lookup s g)
     if (sg == Meta s) then extend g s tg else unify sg tg g 
  (t, Meta s) -> unify e2 e1 g
  (Q (_,a), Q (_,b)) | (a == b)  -> return g ---- qualif?
  (QC (_,a), QC (_,b)) | (a == b)-> return g ----
  (Vr x, Vr y) | (x == y)        -> return g 
  (Abs _ x b, Abs _ y c)         -> do let c' = substTerm [x] [(y,Vr x)] c 
                                       unify b c' g
  (App c a, App d b)            -> case unify c d g of 
                                     Ok g1 -> unify a b g1 
                                     _     -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))
  (RecType xs,RecType ys) | xs == ys -> return g
  _                             -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))

extend :: Unifier -> MetaId -> Term -> Err Unifier
extend g s t | (t == Meta s) = return g  
             | occCheck s t  = Bad (render ("occurs check" <+> ppTerm Unqualified 0 t))
             | True          = return ((s, t) : g) 

subst_all :: Unifier -> Term -> Err Term
subst_all s u =
 case (s,u) of
  ([], t)  -> return t
  (a : l, t) -> do
     t' <- (subst_all l t) --- successive substs - why ?
     return $ substMetas [a] t'

substMetas :: [(MetaId,Term)] -> Term -> Term
substMetas subst trm = case trm of
   Meta x -> case lookup x subst of
     Just t -> t
     _ -> trm
   _ -> composSafeOp (substMetas subst) trm

substTerm  :: [Ident] -> Substitution -> Term -> Term
substTerm ss g c = case c of
  Vr x        -> maybe c id $ lookup x g
  App f a     -> App (substTerm ss g f) (substTerm ss g a)
  Abs b x t   -> let y = mkFreshVarX ss x in 
                   Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
  Prod b x a t  -> let y = mkFreshVarX ss x in 
                   Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
  _           -> c

occCheck :: MetaId -> Term -> Bool
occCheck s u = case u of
    Meta v  -> s == v
    App c a -> occCheck s c || occCheck s a
    Abs _ x b -> occCheck s b
    _       -> False

val2term :: Val -> Term
val2term v = case v of
  VClos g e   -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
  VApp f c    -> App (val2term f) (val2term c)
  VCn c       -> Q c
  VGen i x    -> Vr x
  VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs)
  VType       -> typeType