----------------------------------------------------------------------
-- |
-- 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 :: Constraints -> Err (Constraints, MetaSubst)
unifyVal Constraints
cs0 = do
  let (Constraints
cs1,Constraints
cs2) = ((Val, Val) -> Bool) -> Constraints -> (Constraints, Constraints)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Val, Val) -> Bool
notSolvable Constraints
cs0 
  let ([Val]
us,[Val]
vs) = Constraints -> ([Val], [Val])
forall a b. [(a, b)] -> ([a], [b])
unzip Constraints
cs2
  let us' :: [Term]
us' = (Val -> Term) -> [Val] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Val -> Term
val2term [Val]
us
  let vs' :: [Term]
vs' = (Val -> Term) -> [Val] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Val -> Term
val2term [Val]
vs
  let (Unifier
ms,Constrs
cs) = Constrs -> Unifier -> (Unifier, Constrs)
unifyAll ([Term] -> [Term] -> Constrs
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
us' [Term]
vs') []
  (Constraints, MetaSubst) -> Err (Constraints, MetaSubst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraints
cs1 Constraints -> Constraints -> Constraints
forall a. [a] -> [a] -> [a]
++ [(Env -> Term -> Val
VClos [] Term
t, Env -> Term -> Val
VClos [] Term
u) | (Term
t,Term
u) <- Constrs
cs], 
          [(MetaId
m,          Env -> Term -> Val
VClos [] Term
t) | (MetaId
m,Term
t) <- Unifier
ms])
 where
   notSolvable :: (Val, Val) -> Bool
notSolvable (Val
v,Val
w) = case (Val
v,Val
w) of -- don't consider nonempty closures
     (VClos ((Ident, Val)
_:Env
_) Term
_,Val
_) -> Bool
True
     (Val
_,VClos ((Ident, Val)
_:Env
_) Term
_) -> Bool
True
     (Val, Val)
_ -> Bool
False

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

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

unify :: Term -> Term -> Unifier -> Err Unifier
unify :: Term -> Term -> Unifier -> Err Unifier
unify Term
e1 Term
e2 Unifier
g = 
 case (Term
e1, Term
e2) of 
  (Meta MetaId
s, Term
t) -> do
     Term
tg <- Unifier -> Term -> Err Term
subst_all Unifier
g Term
t
     let sg :: Term
sg = Term -> (Term -> Term) -> Maybe Term -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
e1 Term -> Term
forall a. a -> a
id (MetaId -> Unifier -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
s Unifier
g)
     if (Term
sg Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId -> Term
Meta MetaId
s) then Unifier -> MetaId -> Term -> Err Unifier
extend Unifier
g MetaId
s Term
tg else Term -> Term -> Unifier -> Err Unifier
unify Term
sg Term
tg Unifier
g 
  (Term
t, Meta MetaId
s) -> Term -> Term -> Unifier -> Err Unifier
unify Term
e2 Term
e1 Unifier
g
  (Q (ModuleName
_,Ident
a), Q (ModuleName
_,Ident
b)) | (Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b)  -> Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return Unifier
g ---- qualif?
  (QC (ModuleName
_,Ident
a), QC (ModuleName
_,Ident
b)) | (Ident
a Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
b)-> Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return Unifier
g ----
  (Vr Ident
x, Vr Ident
y) | (Ident
x Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
y)        -> Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return Unifier
g 
  (Abs BindType
_ Ident
x Term
b, Abs BindType
_ Ident
y Term
c)         -> do let c' :: Term
c' = [Ident] -> Substitution -> Term -> Term
substTerm [Ident
x] [(Ident
y,Ident -> Term
Vr Ident
x)] Term
c 
                                       Term -> Term -> Unifier -> Err Unifier
unify Term
b Term
c' Unifier
g
  (App Term
c Term
a, App Term
d Term
b)            -> case Term -> Term -> Unifier -> Err Unifier
unify Term
c Term
d Unifier
g of 
                                     Ok Unifier
g1 -> Term -> Term -> Unifier -> Err Unifier
unify Term
a Term
b Unifier
g1 
                                     Err Unifier
_     -> String -> Err Unifier
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"fail unify" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Term
e1))
  (RecType [Labelling]
xs,RecType [Labelling]
ys) | [Labelling]
xs [Labelling] -> [Labelling] -> Bool
forall a. Eq a => a -> a -> Bool
== [Labelling]
ys -> Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return Unifier
g
  (Term, Term)
_                             -> String -> Err Unifier
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"fail unify" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Term
e1))

extend :: Unifier -> MetaId -> Term -> Err Unifier
extend :: Unifier -> MetaId -> Term -> Err Unifier
extend Unifier
g MetaId
s Term
t | (Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId -> Term
Meta MetaId
s) = Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return Unifier
g  
             | MetaId -> Term -> Bool
occCheck MetaId
s Term
t  = String -> Err Unifier
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"occurs check" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Unqualified Integer
0 Term
t))
             | Bool
True          = Unifier -> Err Unifier
forall (m :: * -> *) a. Monad m => a -> m a
return ((MetaId
s, Term
t) (MetaId, Term) -> Unifier -> Unifier
forall a. a -> [a] -> [a]
: Unifier
g) 

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

substMetas :: [(MetaId,Term)] -> Term -> Term
substMetas :: Unifier -> Term -> Term
substMetas Unifier
subst Term
trm = case Term
trm of
   Meta MetaId
x -> case MetaId -> Unifier -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
x Unifier
subst of
     Just Term
t -> Term
t
     Maybe Term
_ -> Term
trm
   Term
_ -> (Term -> Term) -> Term -> Term
composSafeOp (Unifier -> Term -> Term
substMetas Unifier
subst) Term
trm

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

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

val2term :: Val -> Term
val2term :: Val -> Term
val2term Val
v = case Val
v of
  VClos Env
g Term
e   -> [Ident] -> Substitution -> Term -> Term
substTerm [] (((Ident, Val) -> (Ident, Term)) -> Env -> Substitution
forall a b. (a -> b) -> [a] -> [b]
map (\(Ident
x,Val
v) -> (Ident
x,Val -> Term
val2term Val
v)) Env
g) Term
e
  VApp Val
f Val
c    -> Term -> Term -> Term
App (Val -> Term
val2term Val
f) (Val -> Term
val2term Val
c)
  VCn (ModuleName, Ident)
c       -> (ModuleName, Ident) -> Term
Q (ModuleName, Ident)
c
  VGen MetaId
i Ident
x    -> Ident -> Term
Vr Ident
x
  VRecType [(Label, Val)]
xs -> [Labelling] -> Term
RecType (((Label, Val) -> Labelling) -> [(Label, Val)] -> [Labelling]
forall a b. (a -> b) -> [a] -> [b]
map (\(Label
l,Val
v) -> (Label
l,Val -> Term
val2term Val
v)) [(Label, Val)]
xs)
  Val
VType       -> Term
typeType