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