module Cryptol.TypeCheck.Solver.Class
( classStep
, expandProp
) where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes(Goal(..), Solved(..))
classStep :: Goal -> Solved
classStep g = case goal g of
TCon (PC PArith) [ty] -> solveArithInst g (tNoUser ty)
TCon (PC PCmp) [ty] -> solveCmpInst g (tNoUser ty)
_ -> Unsolved
solved :: Goal -> [Prop] -> Solved
solved g ps = Solved Nothing [ g { goal = p } | p <- ps ]
solveArithInst :: Goal -> Type -> Solved
solveArithInst g ty = case ty of
TCon (TC TCSeq) [n, e] -> solveArithSeq g n e
TCon (TC TCFun) [_,b] -> solved g [ pArith b ]
TCon (TC (TCTuple _)) es -> solved g [ pArith e | e <- es ]
TCon (TC TCBit) [] -> Unsolvable
TRec fs -> solved g [ pArith ety | (_,ety) <- fs ]
_ -> Unsolved
solveArithSeq :: Goal -> Type -> Type -> Solved
solveArithSeq g n ty = case ty of
TCon (TC TCBit) [] -> solved g [ pFin n ]
TVar {} -> Unsolved
_ -> solved g [ pArith ty ]
solveCmpInst :: Goal -> Type -> Solved
solveCmpInst g ty = case ty of
TCon (TC TCBit) [] -> solved g []
TCon (TC TCSeq) [n,a] -> solved g [ pFin n, pCmp a ]
TCon (TC (TCTuple _)) es -> solved g (map pCmp es)
TCon (TC TCFun) [_,_] -> Unsolvable
TRec fs -> solved g [ 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
_ -> []
_ -> []