{-# 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"