{-# 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, cryIsPrime)
import Cryptol.TypeCheck.Solver.Class
( solveZeroInst, solveLogicInst, solveRingInst
, solveIntegralInst, solveFieldInst, solveRoundInst
, solveEqInst, solveCmpInst, solveSignedCmpInst
, solveLiteralInst
, solveLiteralLessThanInst
, solveValidFloat, solveFLiteralInst
)
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
simplify :: Ctxt -> Prop -> Prop
simplify :: Ctxt -> Prop -> Prop
simplify Ctxt
ctxt Prop
p =
case Ctxt -> Prop -> Solved
simplifyStep Ctxt
ctxt Prop
p of
Solved
Unsolvable -> case Prop -> Maybe Prop
tIsError Prop
p of
Maybe Prop
Nothing -> Prop -> Prop
tError Prop
p
Maybe Prop
_ -> Prop
p
Solved
Unsolved -> forall {b}. Doc -> b -> b
dbg Doc
msg Prop
p
where msg :: Doc
msg = String -> Doc
text String
"unsolved:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Prop
p
SolvedIf [Prop]
ps -> forall {b}. Doc -> b -> b
dbg Doc
msg forall a b. (a -> b) -> a -> b
$ [Prop] -> Prop
pAnd (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 String
"solved:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Prop
p
[Prop]
_ -> forall a. PP a => a -> Doc
pp Prop
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"~~~>" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [Prop]
ps)
where
dbg :: Doc -> b -> b
dbg Doc
msg b
x
| forall a. a -> a
id Bool
False = forall {b}. Doc -> b -> b
ppTrace Doc
msg b
x
| Bool
otherwise = b
x
simplifyStep :: Ctxt -> Prop -> Solved
simplifyStep :: Ctxt -> Prop -> Solved
simplifyStep Ctxt
ctxt Prop
prop =
case Prop -> Prop
tNoUser Prop
prop of
TCon (PC PC
PTrue) [] -> [Prop] -> Solved
SolvedIf []
TCon (PC PC
PAnd) [Prop
l,Prop
r] -> [Prop] -> Solved
SolvedIf [Prop
l,Prop
r]
TCon (PC PC
PZero) [Prop
ty] -> Prop -> Solved
solveZeroInst Prop
ty
TCon (PC PC
PLogic) [Prop
ty] -> Prop -> Solved
solveLogicInst Prop
ty
TCon (PC PC
PRing) [Prop
ty] -> Prop -> Solved
solveRingInst Prop
ty
TCon (PC PC
PField) [Prop
ty] -> Prop -> Solved
solveFieldInst Prop
ty
TCon (PC PC
PIntegral) [Prop
ty] -> Prop -> Solved
solveIntegralInst Prop
ty
TCon (PC PC
PRound) [Prop
ty] -> Prop -> Solved
solveRoundInst Prop
ty
TCon (PC PC
PEq) [Prop
ty] -> Prop -> Solved
solveEqInst Prop
ty
TCon (PC PC
PCmp) [Prop
ty] -> Prop -> Solved
solveCmpInst Prop
ty
TCon (PC PC
PSignedCmp) [Prop
ty] -> Prop -> Solved
solveSignedCmpInst Prop
ty
TCon (PC PC
PLiteral) [Prop
t1,Prop
t2] -> Prop -> Prop -> Solved
solveLiteralInst Prop
t1 Prop
t2
TCon (PC PC
PLiteralLessThan) [Prop
t1,Prop
t2] -> Prop -> Prop -> Solved
solveLiteralLessThanInst Prop
t1 Prop
t2
TCon (PC PC
PFLiteral) [Prop
t1,Prop
t2,Prop
t3,Prop
t4] -> Prop -> Prop -> Prop -> Prop -> Solved
solveFLiteralInst Prop
t1 Prop
t2 Prop
t3 Prop
t4
TCon (PC PC
PValidFloat) [Prop
t1,Prop
t2] -> Prop -> Prop -> Solved
solveValidFloat Prop
t1 Prop
t2
TCon (PC PC
PPrime) [Prop
ty] -> Ctxt -> Prop -> Solved
cryIsPrime Ctxt
ctxt Prop
ty
TCon (PC PC
PFin) [Prop
ty] -> Ctxt -> Prop -> Solved
cryIsFinType Ctxt
ctxt Prop
ty
TCon (PC PC
PEqual) [Prop
t1,Prop
t2] -> Ctxt -> Prop -> Prop -> Solved
cryIsEqual Ctxt
ctxt Prop
t1 Prop
t2
TCon (PC PC
PNeq) [Prop
t1,Prop
t2] -> Ctxt -> Prop -> Prop -> Solved
cryIsNotEqual Ctxt
ctxt Prop
t1 Prop
t2
TCon (PC PC
PGeq) [Prop
t1,Prop
t2] -> Ctxt -> Prop -> Prop -> Solved
cryIsGeq Ctxt
ctxt Prop
t1 Prop
t2
Prop
_ -> Solved
Unsolved