    -- |
    -- Module      :  Cryptol.TypeCheck.Solver.Class
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- Solving class constraints.

    {-# LANGUAGE PatternGuards, OverloadedStrings #-}
    module Cryptol.TypeCheck.Solver.Class
      ( classStep
      , solveZeroInst
      , solveLogicInst
      , solveArithInst
      , solveCmpInst
      , solveSignedCmpInst
      , solveLiteralInst
      , expandProp
      ) where

    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.SimpType (tAdd,tWidth)
    import Cryptol.TypeCheck.Solver.Types
    import Cryptol.TypeCheck.PP

    -- | Solve class constraints.
    -- If not, then we return 'Nothing'.
    -- If solved, then we return 'Just' a list of sub-goals.
    classStep :: Prop -> Solved
    classStep :: Prop -> Solved
    classStep p :: Prop
    p = case Prop -> Prop
    tNoUser Prop
    p of
      TCon (PC PLogic) [ty :: Prop
    ty] -> Prop -> Solved
    solveLogicInst (Prop -> Prop
    tNoUser Prop
    ty)
      TCon (PC PArith) [ty :: Prop
    ty] -> Prop -> Solved
    solveArithInst (Prop -> Prop
    tNoUser Prop
    ty)
      TCon (PC PCmp) [ty :: Prop
    ty]   -> Prop -> Solved
    solveCmpInst   (Prop -> Prop
    tNoUser Prop
    ty)
      _                     -> Solved
    Unsolved

    -- | Solve a Zero constraint by instance, if possible.
    solveZeroInst :: Type -> Solved
    solveZeroInst :: Prop -> Solved
    solveZeroInst ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- Zero Error -> fails
      TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

      -- Zero Bit
      TCon (TC TCBit) [] -> [Prop] -> Solved
    SolvedIf []

      -- Zero Integer
      TCon (TC TCInteger) [] -> [Prop] -> Solved
    SolvedIf []

      -- Zero (Z n)
      TCon (TC TCIntMod) [n :: Prop
    n] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop
    n Prop -> Prop -> Prop
    >== Prop
    tOne ]

      -- Zero a => Zero [n]a
      TCon (TC TCSeq) [_, a :: Prop
    a] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pZero Prop
    a ]

      -- Zero b => Zero (a -> b)
      TCon (TC TCFun) [_, b :: Prop
    b] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pZero Prop
    b ]

      -- (Zero a, Zero b) => Zero (a,b)
      TCon (TC (TCTuple _)) es :: [Prop]
    es -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pZero Prop
    e | Prop
    e <- [Prop]
    es ]

      -- (Zero a, Zero b) => Zero { x1 : a, x2 : b }
      TRec fs :: [(Ident, Prop)]
    fs -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pZero Prop
    ety | (_,ety :: Prop
    ety) <- [(Ident, Prop)]
    fs ]

      _ -> Solved
    Unsolved

    -- | Solve a Logic constraint by instance, if possible.
    solveLogicInst :: Type -> Solved
    solveLogicInst :: Prop -> Solved
    solveLogicInst ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- Logic Error -> fails
      TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

      -- Logic Bit
      TCon (TC TCBit) [] -> [Prop] -> Solved
    SolvedIf []

      -- Logic a => Logic [n]a
      TCon (TC TCSeq) [_, a :: Prop
    a] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pLogic Prop
    a ]

      -- Logic b => Logic (a -> b)
      TCon (TC TCFun) [_, b :: Prop
    b] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pLogic Prop
    b ]

      -- (Logic a, Logic b) => Logic (a,b)
      TCon (TC (TCTuple _)) es :: [Prop]
    es -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pLogic Prop
    e | Prop
    e <- [Prop]
    es ]

      -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
      TRec fs :: [(Ident, Prop)]
    fs -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pLogic Prop
    ety | (_,ety :: Prop
    ety) <- [(Ident, Prop)]
    fs ]

      _ -> Solved
    Unsolved

    -- | Solve an Arith constraint by instance, if possible.
    solveArithInst :: Type -> Solved
    solveArithInst :: Prop -> Solved
    solveArithInst ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- Arith Error -> fails
      TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

      -- Arith [n]e
      TCon (TC TCSeq) [n :: Prop
    n, e :: Prop
    e] -> Prop -> Prop -> Solved
    solveArithSeq Prop
    n Prop
    e

      -- Arith b => Arith (a -> b)
      TCon (TC TCFun) [_,b :: Prop
    b] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pArith Prop
    b ]

      -- (Arith a, Arith b) => Arith (a,b)
      TCon (TC (TCTuple _)) es :: [Prop]
    es -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pArith Prop
    e | Prop
    e <- [Prop]
    es ]

      -- Arith Bit fails
      TCon (TC TCBit) [] ->
        TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage "Arithmetic cannot be done on individual bits."

      -- Arith Integer
      TCon (TC TCInteger) [] -> [Prop] -> Solved
    SolvedIf []

      -- Arith (Z n)
      TCon (TC TCIntMod) [n :: Prop
    n] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop
    n Prop -> Prop -> Prop
    >== Prop
    tOne ]

      -- (Arith a, Arith b) => Arith { x1 : a, x2 : b }
      TRec fs :: [(Ident, Prop)]
    fs -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pArith Prop
    ety | (_,ety :: Prop
    ety) <- [(Ident, Prop)]
    fs ]

      _ -> Solved
    Unsolved

    -- | Solve an Arith constraint for a sequence.  The type passed here is the
    -- element type of the sequence.
    solveArithSeq :: Type -> Type -> Solved
    solveArithSeq :: Prop -> Prop -> Solved
    solveArithSeq n :: Prop
    n ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- fin n => Arith [n]Bit
      TCon (TC TCBit) [] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n ]

      -- variables are not solvable.
      TVar {} -> case Prop -> Prop
    tNoUser Prop
    n of
                    {- We are sure that the lenght is not `fin`, so the
                    special case for `Bit` does not apply.
                    Arith ty => Arith [n]ty -}
                    TCon (TC TCInf) [] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pArith Prop
    ty ]
                    _                  -> Solved
    Unsolved

      -- Arith ty => Arith [n]ty
      _ -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pArith Prop
    ty ]

    -- | Solve Cmp constraints.
    solveCmpInst :: Type -> Solved
    solveCmpInst :: Prop -> Solved
    solveCmpInst ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- Cmp Error -> fails
      TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

      -- Cmp Bit
      TCon (TC TCBit) [] -> [Prop] -> Solved
    SolvedIf []

      -- Cmp Integer
      TCon (TC TCInteger) [] -> [Prop] -> Solved
    SolvedIf []

      -- Cmp (Z n)
      TCon (TC TCIntMod) [n :: Prop
    n] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop
    n Prop -> Prop -> Prop
    >== Prop
    tOne ]

      -- (fin n, Cmp a) => Cmp [n]a
      TCon (TC TCSeq) [n :: Prop
    n,a :: Prop
    a] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop -> Prop
    pCmp Prop
    a ]

      -- (Cmp a, Cmp b) => Cmp (a,b)
      TCon (TC (TCTuple _)) es :: [Prop]
    es -> [Prop] -> Solved
    SolvedIf ((Prop -> Prop) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Prop
    pCmp [Prop]
    es)

      -- Cmp (a -> b) fails
      TCon (TC TCFun) [_,_] ->
        TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage "Comparisons may not be performed on functions."

      -- (Cmp a, Cmp b) => Cmp { x:a, y:b }
      TRec fs :: [(Ident, Prop)]
    fs -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pCmp Prop
    e | (_,e :: Prop
    e) <- [(Ident, Prop)]
    fs ]

      _ -> Solved
    Unsolved

    -- | Solve a SignedCmp constraint for a sequence.  The type passed here is the
    -- element type of the sequence.
    solveSignedCmpSeq :: Type -> Type -> Solved
    solveSignedCmpSeq :: Prop -> Prop -> Solved
    solveSignedCmpSeq n :: Prop
    n ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- (fin n, n >=1 ) => SignedCmp [n]Bit
      TCon (TC TCBit) [] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop
    n Prop -> Prop -> Prop
    >== Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum (1 :: Integer) ]

      -- variables are not solvable.
      TVar {} -> Solved
    Unsolved

      -- (fin n, SignedCmp ty) => SignedCmp [n]ty, when ty != Bit
      _ -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    n, Prop -> Prop
    pSignedCmp Prop
    ty ]

    -- | Solve SignedCmp constraints.
    solveSignedCmpInst :: Type -> Solved
    solveSignedCmpInst :: Prop -> Solved
    solveSignedCmpInst ty :: Prop
    ty = case Prop -> Prop
    tNoUser Prop
    ty of

      -- SignedCmp Error -> fails
      TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

      -- SignedCmp Bit
      TCon (TC TCBit) [] -> TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage "Signed comparisons may not be performed on bits"

      -- SignedCmp for sequences
      TCon (TC TCSeq) [n :: Prop
    n,a :: Prop
    a] -> Prop -> Prop -> Solved
    solveSignedCmpSeq Prop
    n Prop
    a

      -- (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
      TCon (TC (TCTuple _)) es :: [Prop]
    es -> [Prop] -> Solved
    SolvedIf ((Prop -> Prop) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Prop
    pSignedCmp [Prop]
    es)

      -- SignedCmp (a -> b) fails
      TCon (TC TCFun) [_,_] ->
        TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage "Signed comparisons may not be performed on functions."

      -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
      TRec fs :: [(Ident, Prop)]
    fs -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pSignedCmp Prop
    e | (_,e :: Prop
    e) <- [(Ident, Prop)]
    fs ]

      _ -> Solved
    Unsolved

    -- | Solve Literal constraints.
    solveLiteralInst :: Type -> Type -> Solved
    solveLiteralInst :: Prop -> Prop -> Solved
    solveLiteralInst val :: Prop
    val ty :: Prop
    ty
      | TCon (TError _ e :: TCErrorMessage
    e) _ <- Prop -> Prop
    tNoUser Prop
    val = TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e
      | Bool
    otherwise =
        case Prop -> Prop
    tNoUser Prop
    ty of

          -- Literal n Error -> fails
          TCon (TError _ e :: TCErrorMessage
    e) _ -> TCErrorMessage -> Solved
    Unsolvable TCErrorMessage
    e

          -- (fin val) => Literal val Integer
          TCon (TC TCInteger) [] -> [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    val ]

          -- (fin val, fin m, m >= val + 1) => Literal val (Z m)
          TCon (TC TCIntMod) [modulus :: Prop
    modulus] ->
            [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    val, Prop -> Prop
    pFin Prop
    modulus, Prop
    modulus Prop -> Prop -> Prop
    >== Prop -> Prop -> Prop
    tAdd Prop
    val Prop
    tOne ]

          -- (fin bits, bits => width n) => Literal n [bits]
          TCon (TC TCSeq) [bits :: Prop
    bits, elTy :: Prop
    elTy]
            | TCon (TC TCBit) [] <- Prop
    ety ->
                [Prop] -> Solved
    SolvedIf [ Prop -> Prop
    pFin Prop
    val, Prop -> Prop
    pFin Prop
    bits, Prop
    bits Prop -> Prop -> Prop
    >== Prop -> Prop
    tWidth Prop
    val ]
            | TVar _ <- Prop
    ety -> Solved
    Unsolved
            where ety :: Prop
    ety = Prop -> Prop
    tNoUser Prop
    elTy

          TVar _ -> Solved
    Unsolved

          _ -> TCErrorMessage -> Solved
    Unsolvable (TCErrorMessage -> Solved) -> TCErrorMessage -> Solved
    forall a b. (a -> b) -> a -> b
    $ String -> TCErrorMessage
    TCErrorMessage (String -> TCErrorMessage) -> String -> TCErrorMessage
    forall a b. (a -> b) -> a -> b
    $ Doc -> String
    forall a. Show a => a -> String
    show
             (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ "Type" Doc -> Doc -> Doc
    <+> Doc -> Doc
    quotes (Prop -> Doc
    forall a. PP a => a -> Doc
    pp Prop
    ty) Doc -> Doc -> Doc
    <+> "does not support literals."

    -- | Add propositions that are implied by the given one.
    -- The result contains the orignal proposition, and maybe some more.
    expandProp :: Prop -> [Prop]
    expandProp :: Prop -> [Prop]
    expandProp prop :: Prop
    prop =
      Prop
    prop Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    :
      case Prop -> Prop
    tNoUser Prop
    prop of

        TCon (PC pc :: PC
    pc) [ty :: Prop
    ty] ->
          case (PC
    pc, Prop -> Prop
    tNoUser Prop
    ty) of

            -- Arith [n]Bit => fin n
            -- (Arith [n]a, a/=Bit) => Arith a
            (PArith, TCon (TC TCSeq) [n :: Prop
    n,a :: Prop
    a])
              | TCon (TC TCBit) _ <- Prop
    ty1  -> [Prop -> Prop
    pFin Prop
    n]
              | TCon _ _          <- Prop
    ty1  -> Prop -> [Prop]
    expandProp (Prop -> Prop
    pArith Prop
    ty1)
              | TRec {}           <- Prop
    ty1  -> Prop -> [Prop]
    expandProp (Prop -> Prop
    pArith Prop
    ty1)
              where
              ty1 :: Prop
    ty1 = Prop -> Prop
    tNoUser Prop
    a

            -- Arith (a -> b) => Arith b
            (PArith, TCon (TC TCFun) [_,b :: Prop
    b]) -> Prop -> [Prop]
    expandProp (Prop -> Prop
    pArith Prop
    b)

            -- Arith (a,b) => (Arith a, Arith b)
            (PArith, TCon (TC (TCTuple _)) ts :: [Prop]
    ts) -> (Prop -> [Prop]) -> [Prop] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Prop -> [Prop]
    expandProp (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Prop -> Prop
    pArith) [Prop]
    ts

            -- Arith { x1 : a, x2 : b } => (Arith a, Arith b)
            (PArith, TRec fs :: [(Ident, Prop)]
    fs) -> ((Ident, Prop) -> [Prop]) -> [(Ident, Prop)] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Prop -> [Prop]
    expandProp (Prop -> [Prop])
    -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> [Prop]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Prop -> Prop
    pArith(Prop -> Prop) -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, Prop) -> Prop
    forall a b. (a, b) -> b
    snd) [(Ident, Prop)]
    fs

            -- Cmp [n]a => (fin n, Cmp a)
            (PCmp, TCon (TC TCSeq) [n :: Prop
    n,a :: Prop
    a]) -> Prop -> Prop
    pFin Prop
    n Prop -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    : Prop -> [Prop]
    expandProp (Prop -> Prop
    pCmp Prop
    a)

            -- Cmp (a,b) => (Cmp a, Cmp b)
            (PCmp, TCon (TC (TCTuple _)) ts :: [Prop]
    ts) -> (Prop -> [Prop]) -> [Prop] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Prop -> [Prop]
    expandProp (Prop -> [Prop]) -> (Prop -> Prop) -> Prop -> [Prop]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Prop -> Prop
    pCmp) [Prop]
    ts

            -- Cmp { x:a, y:b } => (Cmp a, Cmp b)
            (PCmp, TRec fs :: [(Ident, Prop)]
    fs) -> ((Ident, Prop) -> [Prop]) -> [(Ident, Prop)] -> [Prop]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Prop -> [Prop]
    expandProp (Prop -> [Prop])
    -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> [Prop]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Prop -> Prop
    pCmp (Prop -> Prop) -> ((Ident, Prop) -> Prop) -> (Ident, Prop) -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident, Prop) -> Prop
    forall a b. (a, b) -> b
    snd) [(Ident, Prop)]
    fs

            _ -> []

        _ -> []