-- |
-- Module      : Minigent.TC.Solver
-- Copyright   : (c) Data61 2018-2019
--                   Commonwealth Science and Research Organisation (CSIRO)
--                   ABN 41 687 119 230
-- License     : BSD3
--
-- The solver portion of the type inference.
--
-- May be used qualified or unqualified.
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Minigent.TC.Solver
  ( Solver
  , runSolver
  , solve
  , substAssign
  ) where

import Minigent.TC.Normalise
import Minigent.TC.Simplify
import Minigent.TC.Unify
import Minigent.TC.Equate
import Minigent.TC.SinkFloat
import Minigent.TC.Assign
import Minigent.Fresh
import Minigent.Syntax
import Minigent.Syntax.Utils
import Minigent.Syntax.PrettyPrint

import qualified Minigent.Syntax.Utils.Rewrite as Rewrite

import Control.Applicative
import Control.Monad.Trans.Maybe
import Control.Monad.State
import Control.Monad.Writer
import Data.Maybe (fromMaybe)

import Debug.Trace

-- | A monad that combines writer effects for accumulating assignments to
--   unification variables, and fresh variables.
newtype Solver a = Solver (WriterT [Assign] (FreshT VarName IO) a)
        deriving ( Monad, Applicative, Functor
                 , MonadFresh VarName, MonadWriter [Assign]
                 )

-- | Given a set of axioms and a set of constraints to solve, attempt to
--   find assignments to satisfy all the constraints assuming the axioms.
--
--   Right now, only 'Share', 'Drop' and 'Escape' constraints on type
--   variables can be axioms.
--
--   Returns any constraints that could not be satisfied. So, an empty list
--   means that the solver successfully solved everything.
solve :: [Constraint] -> [Constraint] -> Solver [Constraint]
solve axs cs = do
  cs'' <- runMaybeT (Rewrite.run' solverRewrites cs)
  case cs'' of
    Nothing -> pure (normaliseConstraints cs)
    Just a  -> pure a
  where
    solverRewrites :: Rewrite.Rewrite' Solver [Constraint]
    solverRewrites = Rewrite.untilFixedPoint $
      -- Rewrite.debugNewline "SOLV" debugPrettyConstraints <>
      Rewrite.pre normaliseConstraints (
          -- debugStr "[simp]" <>
          Rewrite.lift (simplify axs) <>
          -- debugStr "[unify]" <>
          unify <>
          -- debugStr "[equate]" <>
          Rewrite.lift equate <>
          -- debugStr "[sink/float]" <>
          sinkFloat)

-- | Run a solver computation.
runSolver :: Solver a -> FreshT VarName IO (a,[Assign])
runSolver (Solver x) = runWriterT x

debugStr :: String -> Rewrite.Rewrite' Solver a
debugStr s = Rewrite.Rewrite $ \cs -> do
  _ <- (lift . Solver . lift . lift . traceIO $ s :: MaybeT Solver ())
  empty