module Cryptol.TypeCheck.Solver.Types where

import Data.Map(Map)

import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Solver.Numeric.Interval

type Ctxt = Map TVar Interval

data Solved = SolvedIf [Prop]           -- ^ Solved, assuming the sub-goals.
            | Unsolved                  -- ^ We could not solve the goal.
            | Unsolvable TCErrorMessage -- ^ The goal can never be solved.
              deriving (Show)


elseTry :: Solved -> Solved -> Solved
Unsolved `elseTry` x = x
x        `elseTry` _ = x

solveOpts :: [Solved] -> Solved
solveOpts [] = Unsolved
solveOpts (x : xs) = x `elseTry` solveOpts xs

matchThen :: Maybe a -> (a -> Solved) -> Solved
matchThen Nothing _  = Unsolved
matchThen (Just a) f = f a

guarded :: Bool -> Solved -> Solved
guarded True x = x
guarded False _ = Unsolved


instance PP Solved where
  ppPrec _ res =
    case res of
      SolvedIf ps  -> text "solved" $$ nest 2 (vcat (map pp ps))
      Unsolved     -> text "unsolved"
      Unsolvable e -> text "unsolvable" <.> colon <+> text (tcErrorMessage e)