    {-# 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    -> Doc -> Prop -> Prop
    forall {b}. Doc -> b -> b
    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 {b}. Doc -> b -> b
    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
    commaSep ((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 -> b -> b
    dbg Doc
    msg b
    x
          -- Change `False` to `True` below to enable extra tracing. Note that
          -- this is written with an extraneous `id` expression to suppress
          -- pattern-match coverage checking warnings in this one case.
        | Bool -> Bool
    forall a. a -> a
    id Bool
    False  = Doc -> b -> b
    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