{-# 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
  , 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    -> Doc -> Prop -> Prop
forall p. Doc -> p -> p
dbg Doc
msg Prop
p
      where msg :: Doc
msg = String -> Doc
text String
"unsolved:" Doc -> Doc -> Doc
<+> Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
p
    SolvedIf [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 String
"solved:" Doc -> Doc -> Doc
<+> Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
p
                    [Prop]
_  -> Prop -> Doc
forall a. PP a => a -> Doc
pp Prop
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"~~~>" 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 Doc
msg 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 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
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