{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass #-}
module Cryptol.TypeCheck.Solver.Types where

import Data.Map(Map)
import Data.Set(Set)

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

data Ctxt =
  SolverCtxt
  { Ctxt -> Map TVar Interval
intervals :: Map TVar Interval
  , Ctxt -> Set Prop
saturatedAsmps :: Set Prop
  }

instance Semigroup Ctxt where
  SolverCtxt Map TVar Interval
is1 Set Prop
as1 <> :: Ctxt -> Ctxt -> Ctxt
<> SolverCtxt Map TVar Interval
is2 Set Prop
as2 = Map TVar Interval -> Set Prop -> Ctxt
SolverCtxt (Map TVar Interval
is1 Map TVar Interval -> Map TVar Interval -> Map TVar Interval
forall a. Semigroup a => a -> a -> a
<> Map TVar Interval
is2) (Set Prop
as1 Set Prop -> Set Prop -> Set Prop
forall a. Semigroup a => a -> a -> a
<> Set Prop
as2)

instance Monoid Ctxt where
  mempty :: Ctxt
mempty = Map TVar Interval -> Set Prop -> Ctxt
SolverCtxt Map TVar Interval
forall a. Monoid a => a
mempty Set Prop
forall a. Monoid a => a
mempty


data Solved = SolvedIf [Prop]           -- ^ Solved, assuming the sub-goals.
            | Unsolved                  -- ^ We could not solve the goal.
            | Unsolvable                -- ^ 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
Solved
Unsolved elseTry :: Solved -> Solved -> Solved
`elseTry` Solved
x = Solved
x
Solved
x        `elseTry` Solved
_ = Solved
x

solveOpts :: [Solved] -> Solved
solveOpts :: [Solved] -> Solved
solveOpts [] = Solved
Unsolved
solveOpts (Solved
x : [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 Maybe a
Nothing a -> Solved
_  = Solved
Unsolved
matchThen (Just a
a) a -> Solved
f = a -> Solved
f a
a

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


instance PP Solved where
  ppPrec :: Int -> Solved -> Doc
ppPrec Int
_ Solved
res =
    case Solved
res of
      SolvedIf [Prop]
ps  -> String -> Doc
text String
"solved" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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))
      Solved
Unsolved     -> String -> Doc
text String
"unsolved"
      Solved
Unsolvable   -> String -> Doc
text String
"unsolvable"