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 (Int -> Solved -> ShowS
[Solved] -> ShowS
Solved -> String
(Int -> Solved -> ShowS)
-> (Solved -> String) -> ([Solved] -> ShowS) -> Show Solved
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solved] -> ShowS
$cshowList :: [Solved] -> ShowS
show :: Solved -> String
$cshow :: Solved -> String
showsPrec :: Int -> Solved -> ShowS
$cshowsPrec :: Int -> Solved -> ShowS
Show)


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

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

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

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


instance PP Solved where
  ppPrec :: Int -> Solved -> Doc
ppPrec _ res :: Solved
res =
    case Solved
res of
      SolvedIf ps :: [Prop]
ps  -> String -> Doc
text "solved" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
forall a. PP a => a -> Doc
pp [Prop]
ps))
      Unsolved     -> String -> Doc
text "unsolved"
      Unsolvable e :: TCErrorMessage
e -> String -> Doc
text "unsolvable" Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
<+> String -> Doc
text (TCErrorMessage -> String
tcErrorMessage TCErrorMessage
e)