module Cryptol.TypeCheck.SimpleSolver ( simplify , simplifyStep) where
import Cryptol.TypeCheck.Type hiding
( tSub, tMul, tDiv, tMod, tExp, tMin, tWidth
, tLenFromThen, tLenFromThenTo)
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst)
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
simplify :: Ctxt -> Prop -> Prop
simplify ctxt p =
case simplifyStep ctxt p of
Unsolvable e -> pError e
Unsolved -> dbg msg p
where msg = text "unsolved:" <+> pp p
SolvedIf ps -> dbg msg $ pAnd (map (simplify ctxt) ps)
where msg = case ps of
[] -> text "solved:" <+> pp p
_ -> pp p <+> text "~~~>" <+>
vcat (punctuate comma (map pp ps))
where
dbg msg x
| False = ppTrace msg x
| otherwise = x
simplifyStep :: Ctxt -> Prop -> Solved
simplifyStep ctxt prop =
case tNoUser prop of
TCon (PC PTrue) [] -> SolvedIf []
TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PFin) [ty] -> cryIsFinType ctxt ty
TCon (PC PEqual) [t1,t2] -> cryIsEqual ctxt t1 t2
TCon (PC PNeq) [t1,t2] -> cryIsNotEqual ctxt t1 t2
TCon (PC PGeq) [t1,t2] -> cryIsGeq ctxt t1 t2
_ -> Unsolved