    {-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass #-}
    {-# LANGUAGE Safe #-}
    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
    $cshowsPrec :: Int -> Solved -> ShowS
    showsPrec :: Int -> Solved -> ShowS
    $cshow :: Solved -> String
    show :: Solved -> String
    $cshowList :: [Solved] -> ShowS
    showList :: [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 :: forall a. 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"