-- |
-- 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

        _ -> []

    _ -> []