content: -- |
  -- Module      : Minigent.TC
  -- Copyright   : (c) Data61 2018-2019
  --                   Commonwealth Science and Research Organisation (CSIRO)
  --                   ABN 41 687 119 230
  -- License     : BSD3
  --
  -- The top level type checking/inference module.
  --
  -- May be used qualified or unqualified.
  module Minigent.TC where
  
  import Minigent.Fresh
  
  import Minigent.TC.ConstraintGen
  import Minigent.TC.Solver
  
  import Minigent.Syntax
  import Minigent.Syntax.Utils
  import Minigent.Syntax.Utils.Rewrite(untilFixedPoint)
  import Minigent.Environment
  import Control.Monad.State
  import Control.Monad.Reader
  import qualified Data.Map as M
  import Debug.Trace
  
  import Minigent.Syntax.PrettyPrint
  
  -- | Run type checking/inference on the given definitions under the given 'GlobalEnvironments'.
  --
  --   Returns either a list of unsolved constraints (if inference fails) or a new definition
  --   with type signatures added to each subexpression and type applications expanded explicitly.
  tc :: GlobalEnvironments
     -> [(FunName, (VarName, Expr))]
     -> FreshT VarName IO [Either (FunName, [Constraint]) (FunName,(VarName,Expr))]
  tc envs = mapM check
    where
      check (f, (x, e)) = do
        (axs, e', c) <- runCG (cgFunction f x e) mempty envs
  
        (cs',ss) <- runSolver (solve axs [c])
        let subst = normaliseType (untilFixedPoint (foldMap substAssign ss))
        if null cs'
          then return $ Right (f, (x, exprTypes subst e'))
          else return $ Left (f, cs')
  