{-# LANGUAGE PatternGuards, Trustworthy #-}
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