module Cryptol.TypeCheck.Solver.Class
( classStep
, solveArithInst
, solveCmpInst
, expandProp
) where
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.Solver.Types
classStep :: Prop -> Solved
classStep p = case tNoUser p of
TCon (PC PArith) [ty] -> solveArithInst (tNoUser ty)
TCon (PC PCmp) [ty] -> solveCmpInst (tNoUser ty)
_ -> Unsolved
solveArithInst :: Type -> Solved
solveArithInst ty = case tNoUser ty of
TCon (TError _ e) _ -> Unsolvable e
TCon (TC TCSeq) [n, e] -> solveArithSeq n e
TCon (TC TCFun) [_,b] -> SolvedIf [ pArith b ]
TCon (TC (TCTuple _)) es -> SolvedIf [ pArith e | e <- es ]
TCon (TC TCBit) [] ->
Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
TRec fs -> SolvedIf [ pArith ety | (_,ety) <- fs ]
_ -> Unsolved
solveArithSeq :: Type -> Type -> Solved
solveArithSeq n ty = case tNoUser ty of
TCon (TC TCBit) [] -> SolvedIf [ pFin n ]
TVar {} -> Unsolved
_ -> SolvedIf [ pArith ty ]
solveCmpInst :: Type -> Solved
solveCmpInst ty = case tNoUser ty of
TCon (TError _ e) _ -> Unsolvable e
TCon (TC TCBit) [] -> SolvedIf []
TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pCmp a ]
TCon (TC (TCTuple _)) es -> SolvedIf (map pCmp es)
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Comparisons may not be performed on functions."
TRec fs -> SolvedIf [ pCmp e | (_,e) <- fs ]
_ -> Unsolved
expandProp :: Prop -> [Prop]
expandProp prop =
prop :
case tNoUser prop of
TCon (PC pc) [ty] ->
case (pc, tNoUser ty) of
(PArith, TCon (TC TCSeq) [n,a])
| TCon (TC TCBit) _ <- ty1 -> [pFin n]
| TCon _ _ <- ty1 -> expandProp (pArith ty1)
| TRec {} <- ty1 -> expandProp (pArith ty1)
where
ty1 = tNoUser a
(PArith, TCon (TC TCFun) [_,b]) -> expandProp (pArith b)
(PArith, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pArith) ts
(PArith, TRec fs) -> concatMap (expandProp . pArith. snd) fs
(PCmp, TCon (TC TCSeq) [n,a]) -> pFin n : expandProp (pCmp a)
(PCmp, TCon (TC (TCTuple _)) ts) -> concatMap (expandProp . pCmp) ts
(PCmp, TRec fs) -> concatMap (expandProp . pCmp . snd) fs
_ -> []
_ -> []