{-# LANGUAGE PatternGuards, Trustworthy #-} module Cryptol.TypeCheck.SimpleSolver ( simplify , simplifyStep) where import Cryptol.TypeCheck.Type hiding ( tSub, tMul, tDiv, tMod, tExp, tMin, 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 ( solveZeroInst, solveLogicInst, solveArithInst, solveCmpInst , solveSignedCmpInst, solveLiteralInst ) import Cryptol.Utils.Debug(ppTrace) import Cryptol.TypeCheck.PP simplify :: Ctxt -> Prop -> Prop simplify :: Ctxt -> Prop -> Prop simplify ctxt :: Ctxt ctxt p :: Prop p = case Ctxt -> Prop -> Solved simplifyStep Ctxt ctxt Prop p of Unsolvable e :: TCErrorMessage e -> TCErrorMessage -> Prop pError TCErrorMessage e Unsolved -> Doc -> Prop -> Prop forall p. Doc -> p -> p dbg Doc msg Prop p where msg :: Doc msg = String -> Doc text "unsolved:" Doc -> Doc -> Doc <+> Prop -> Doc forall a. PP a => a -> Doc pp Prop p SolvedIf ps :: [Prop] ps -> Doc -> Prop -> Prop forall p. Doc -> p -> p dbg Doc msg (Prop -> Prop) -> Prop -> Prop forall a b. (a -> b) -> a -> b $ [Prop] -> Prop pAnd ((Prop -> Prop) -> [Prop] -> [Prop] forall a b. (a -> b) -> [a] -> [b] map (Ctxt -> Prop -> Prop simplify Ctxt ctxt) [Prop] ps) where msg :: Doc msg = case [Prop] ps of [] -> String -> Doc text "solved:" Doc -> Doc -> Doc <+> Prop -> Doc forall a. PP a => a -> Doc pp Prop p _ -> Prop -> Doc forall a. PP a => a -> Doc pp Prop p Doc -> Doc -> Doc <+> String -> Doc text "~~~>" Doc -> Doc -> Doc <+> [Doc] -> Doc vcat (Doc -> [Doc] -> [Doc] punctuate Doc comma ((Prop -> Doc) -> [Prop] -> [Doc] forall a b. (a -> b) -> [a] -> [b] map Prop -> Doc forall a. PP a => a -> Doc pp [Prop] ps)) where dbg :: Doc -> p -> p dbg msg :: Doc msg x :: p x | Bool False = Doc -> p -> p forall p. Doc -> p -> p ppTrace Doc msg p x | Bool otherwise = p x simplifyStep :: Ctxt -> Prop -> Solved simplifyStep :: Ctxt -> Prop -> Solved simplifyStep ctxt :: Ctxt ctxt prop :: Prop prop = case Prop -> Prop tNoUser Prop prop of TCon (PC PTrue) [] -> [Prop] -> Solved SolvedIf [] TCon (PC PAnd) [l :: Prop l,r :: Prop r] -> [Prop] -> Solved SolvedIf [Prop l,Prop r] TCon (PC PZero) [ty :: Prop ty] -> Prop -> Solved solveZeroInst Prop ty TCon (PC PLogic) [ty :: Prop ty] -> Prop -> Solved solveLogicInst Prop ty TCon (PC PArith) [ty :: Prop ty] -> Prop -> Solved solveArithInst Prop ty TCon (PC PCmp) [ty :: Prop ty] -> Prop -> Solved solveCmpInst Prop ty TCon (PC PSignedCmp) [ty :: Prop ty] -> Prop -> Solved solveSignedCmpInst Prop ty TCon (PC PLiteral) [t1 :: Prop t1,t2 :: Prop t2] -> Prop -> Prop -> Solved solveLiteralInst Prop t1 Prop t2 TCon (PC PFin) [ty :: Prop ty] -> Ctxt -> Prop -> Solved cryIsFinType Ctxt ctxt Prop ty TCon (PC PEqual) [t1 :: Prop t1,t2 :: Prop t2] -> Ctxt -> Prop -> Prop -> Solved cryIsEqual Ctxt ctxt Prop t1 Prop t2 TCon (PC PNeq) [t1 :: Prop t1,t2 :: Prop t2] -> Ctxt -> Prop -> Prop -> Solved cryIsNotEqual Ctxt ctxt Prop t1 Prop t2 TCon (PC PGeq) [t1 :: Prop t1,t2 :: Prop t2] -> Ctxt -> Prop -> Prop -> Solved cryIsGeq Ctxt ctxt Prop t1 Prop t2 _ -> Solved Unsolved