content: module Ditto.Match where
  import Ditto.Syntax
  import Ditto.Monad
  import Ditto.Throw
  import Ditto.Sub
  import Ditto.Whnf
  import Data.List
  import Control.Monad
  
  ----------------------------------------------------------------------
  
  data Match = MSolve PSub | MStuck [Name] | MClash
  data Cover = CMatch PSub RHS | CSplit [Name] | CMiss
  
  ----------------------------------------------------------------------
  
  munion :: Match -> Match -> Match
  munion (MSolve xs) (MSolve ys) = MSolve (xs ++ ys)
  munion (MStuck xs) (MStuck ys) = MStuck (xs `union` ys)
  munion MClash _ = MClash
  munion _ MClash = MClash
  munion (MStuck xs) _ = MStuck xs
  munion _ (MStuck ys) = MStuck ys
  
  ----------------------------------------------------------------------
  
  match1 :: Pat -> Pat -> TCM Match
  match1 (PVar x) p = return $ MSolve [(x, p)]
  match1 (PInacc _) _ = return $ MSolve []
  match1 (PCon x ps) (PCon y qs) | x == y = match ps qs
  match1 (PCon x _) (PCon y _) = return MClash
  match1 (PCon x ps) (PVar y) = return $ MStuck [y]
  match1 (PCon x ps) (PInacc (Just a)) = matchInacc x ps a
  match1 (PCon x ps) (PInacc Nothing) = throwGenErr "Undefined inaccessible in covering"
  
  matchInacc :: PName -> Pats -> Exp -> TCM Match
  matchInacc x ps a = whnf a >>= \case
    ECon _ y as -> match1 (PCon x ps) (PCon y (injectExps as))
    (viewSpine -> (EVar y, as)) -> return $ MStuck [y]
    _ -> throwGenErr "Ill-formed match"
  
  match :: Pats -> Pats -> TCM Match
  match [] [] = return $ MSolve []
  match ((i1, p):ps) ((i2, q):qs) | i1 == i2 = munion <$> match1 p q <*> match ps qs
  match ps@((Expl, _):_) ((Impl, _):qs) = match ps qs
  match []               ((Impl, _):qs) = match [] qs
  match ((i1, p):ps) ((i2, q):qs) | i1 /= i2 = throwGenErr "Implicit and explicit patterns mismatch"
  match _ _ = throwGenErr "Matching pattern clauses of different lengths"
  
  ----------------------------------------------------------------------
  
  cunion :: Cover -> Cover -> Cover
  cunion x@(CMatch _ _) _ = x
  cunion x@(CSplit _) _ = x
  cunion _ y = y
  
  ----------------------------------------------------------------------
  
  matchClause :: SClause -> Pats -> TCM Cover
  matchClause (ps, rhs) qs = match ps qs >>= \case
    MSolve rs -> return $ CMatch rs rhs
    MStuck xs -> return $ CSplit xs
    MClash -> return CMiss
  
  matchClauses :: SClauses -> Pats -> TCM Cover
  matchClauses cs qs = foldM (\ acc c -> cunion acc <$> matchClause c qs) CMiss cs
  
  ----------------------------------------------------------------------
  
  isCovered :: Cover -> Bool
  isCovered (CMatch _ _) = True
  isCovered _ = False
  
  reachable :: SClauses -> SClauses -> Pats -> TCM SClauses
  reachable prev [] qs = return []
  reachable prev (c:cs) qs = do
    prevUnreached <- not . isCovered <$> matchClauses prev qs
    currReached <- isCovered <$> matchClause c qs
    if prevUnreached && currReached then (c:) <$> rec else rec
    where rec = reachable (snoc prev c) cs qs
  
  reachableClauses :: SClauses -> Clauses -> TCM SClauses
  reachableClauses cs cs' = nub . concat <$> mapM (reachable [] cs) qss
    where qss = map (\(Clause _ qs _) -> qs) cs'
  
  unreachableClauses :: SClauses -> Clauses -> TCM SClauses
  unreachableClauses cs cs' = (cs \\) <$> reachableClauses cs cs'
  
  ----------------------------------------------------------------------