content: module SubtypeRelation(SubtypeRelation,empty,insert,subtype,lower,lub,glb) where
  
  import           Sort
  import           Utils
  
  import           Data.Graph.Inductive (Node)
  import qualified Data.Graph.Inductive as G
  import           Data.Graph.Inductive.PatriciaTree (Gr)
  import           Data.HashMap.Lazy (HashMap)
  import qualified Data.HashMap.Lazy as M
  import           Data.Maybe
  
  data SubtypeRelation = SubtypeRelation Node (HashMap Sort Node) (Gr Sort ()) deriving (Show,Eq)
  
  empty :: SubtypeRelation
  empty = SubtypeRelation 0 M.empty G.empty
  
  insert :: Sort -> Sort -> SubtypeRelation -> SubtypeRelation
  insert s1 s2 rel0 =
    let (n1, rel1) = insertSort s1 rel0
        (n2, rel2) = insertSort s2 rel1
    in withGraph (G.tc . G.insEdge (n1,n2,())) rel2
  
  withGraph :: (Gr Sort () -> Gr Sort ()) -> SubtypeRelation -> SubtypeRelation
  withGraph f (SubtypeRelation m nodes rel) = SubtypeRelation m nodes (f rel)
  {-# INLINE withGraph #-}
  
  insertSort :: Sort -> SubtypeRelation -> (Node,SubtypeRelation)
  insertSort s rel@(SubtypeRelation m nodes gr) =
    case M.lookup s nodes of
      Just n -> (n,rel)
      Nothing -> (m, SubtypeRelation (m+1) (M.insert s m nodes) (G.insNode (m,s) gr)) 
  
  lookupSort :: SubtypeRelation -> Sort -> Maybe Node
  lookupSort (SubtypeRelation _ nodes _) s = M.lookup s nodes
  
  subtype :: SubtypeRelation -> Sort -> Sort -> Bool
  subtype rel@(SubtypeRelation _ _ gr) s1 s2 = case (s1,s2) of
    (Bottom,_) -> True
    (_,Top) -> True
    (Lexical,Lexical) -> True
    (Numerical,Numerical) -> True
    (List x,List y) -> subtype rel x y
    (List x,Sort y) -> any (\ysub -> subtype rel (List x) ysub) (tail $ lower rel $ Sort y)
    (Option x,Option y) -> subtype rel x y
    (Option x,Sort y) -> any (\ysub -> subtype rel (Option x) ysub) (tail $ lower rel $ Sort y)
    (Tuple xs,Tuple ys)
      | eqLength xs ys -> and (zipWith (subtype rel) xs ys)
      | otherwise -> False
    (Tuple xs,Sort y) -> any (\ysub -> subtype rel (Tuple xs) ysub) (tail $ lower rel $ Sort y)
    (x,Sort y)
      | x == Sort y -> True
      | otherwise -> fromMaybe False $ do
          n1 <- lookupSort rel x 
          n2 <- lookupSort rel (Sort y)
          return $ G.hasEdge gr (n1, n2)
    (_,_) -> False
  
  lub :: SubtypeRelation -> Sort -> Sort -> Sort
  lub rel s1 s2 = case (s1,s2) of
    (Bottom,_) -> s2
    (_,Bottom) -> s1
    (Top,_) -> Top 
    (List x,List y) -> List (lub rel x y)
    (Option x,Option y) -> Option (lub rel x y)
    (Tuple xs,Tuple ys) -> Tuple (zipWith (lub rel) xs ys)
    (Lexical,Lexical) -> Lexical
    (Numerical,Numerical) -> Numerical
    (Sort _,_)
      | subtype rel s1 s2 -> s2
      | subtype rel s2 s1 -> s1
    (_,Sort _)
      | subtype rel s1 s2 -> s2
      | subtype rel s2 s1 -> s1
    _ -> Top
  
  glb :: SubtypeRelation -> Sort -> Sort -> Sort
  glb rel s1 s2 = case (s1,s2) of
    (Bottom,_) -> Bottom
    (_,Bottom) -> Bottom
    (Top,_) -> s2
    (_,Top) -> s1
    (List x,List y) -> List (glb rel x y)
    (Option x,Option y) -> Option (glb rel x y)
    (Tuple xs,Tuple ys) -> Tuple (zipWith (glb rel) xs ys)
    (Lexical,Lexical) -> Lexical
    (Numerical,Numerical) -> Numerical
    (Sort _,_)
      | subtype rel s1 s2 -> s1
      | subtype rel s2 s1 -> s2
    (_,Sort _)
      | subtype rel s1 s2 -> s1
      | subtype rel s2 s1 -> s2
    _ -> Bottom
  
  lower :: SubtypeRelation -> Sort -> [Sort]
  lower rel@(SubtypeRelation _ _ gr) s = case s of
    Bottom -> [Bottom]
    Top -> [Top]
    Lexical -> return Lexical
    Numerical -> return Numerical
    List x -> List <$> lower rel x
    Option x -> Option <$> lower rel x
    Tuple xs -> Tuple <$> permutations (lower rel <$> xs)
    Sort _ -> fromMaybe (return s) $ do
      n <- lookupSort rel s
      xs <- traverse (G.lab gr) (G.pre gr n)
      return (s:xs)
  
  