{-# 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