    -- |
    -- Module      :  $Header$
    -- Copyright   :  (c) 2014-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe #-}
    module Cryptol.TypeCheck.Solver.Numeric.ImportExport
      ( ExportM
      , exportProp
      , exportType
      , runExportM
      , exportPropM
      , exportTypeM
      , importProp
      , importType
      ) where

    import           Cryptol.TypeCheck.Solver.Numeric.AST
    import qualified Cryptol.TypeCheck.AST as Cry
    import           MonadLib

    exportProp :: Cry.Prop -> Maybe Prop
    exportProp = runExportM . exportPropM

    exportType :: Cry.Prop -> Maybe Expr
    exportType = runExportM . exportTypeM

    runExportM :: ExportM a -> Maybe a
    runExportM = either (\_ -> Nothing) Just
               . runId
               . runExceptionT

    type ExportM = ExceptionT () Id

    exportPropM :: Cry.Prop -> ExportM Prop
    exportPropM ty =
      case ty of
        Cry.TUser _ _ t -> exportPropM t
        Cry.TRec {}     -> raise ()
        Cry.TVar {}     -> raise ()
        Cry.TCon (Cry.PC pc) ts ->
          mapM exportTypeM ts >>= \ets ->
          case (pc, ets) of
            (Cry.PFin,   [t])     -> return (Fin t)
            (Cry.PEqual, [t1,t2]) -> return (t1 :== t2)
            (Cry.PNeq,   [t1,t2]) -> return (Not (t1 :== t2))
            (Cry.PGeq,   [t1,t2]) -> return (t1 :>= t2)
            _                     -> raise ()
        Cry.TCon _ _ -> raise ()

    exportTypeM :: Cry.Type -> ExportM Expr
    exportTypeM ty =
      case ty of
        Cry.TUser _ _ t -> exportTypeM t
        Cry.TRec {}     -> raise ()
        Cry.TVar x      -> return $ Var $ UserName x
        Cry.TCon tc ts  ->
          case tc of
            Cry.TC Cry.TCInf     -> return (K Inf)
            Cry.TC (Cry.TCNum x) -> return (K (Nat x))
            Cry.TC _             -> raise ()

            Cry.TF f ->
              mapM exportTypeM ts >>= \ets ->
              case (f, ets) of
                (Cry.TCAdd, [t1,t2]) -> return (t1 :+ t2)
                (Cry.TCSub, [t1,t2]) -> return (t1 :- t2)
                (Cry.TCMul, [t1,t2]) -> return (t1 :* t2)
                (Cry.TCDiv, [t1,t2]) -> return (Div t1 t2)
                (Cry.TCMod, [t1,t2]) -> return (Mod t1 t2)
                (Cry.TCExp, [t1,t2]) -> return (t1 :^^ t2)
                (Cry.TCMin, [t1,t2]) -> return (Min t1 t2)
                (Cry.TCMax, [t1,t2]) -> return (Max t1 t2)
                (Cry.TCWidth, [t1])  -> return (Width t1)
                (Cry.TCLenFromThen,   [t1,t2,t3]) -> return (LenFromThen   t1 t2 t3)
                (Cry.TCLenFromThenTo, [t1,t2,t3]) -> return (LenFromThenTo t1 t2 t3)

                _ -> raise ()

            Cry.PC _ -> raise ()

    importProp :: Prop -> Maybe [Cry.Prop]
    importProp prop =
      case prop of
        PFalse    -> Nothing
        PTrue     -> Just []

        Not p     -> importProp =<< pNot p
        p1 :&& p2 -> do ps1 <- importProp p1
                        ps2 <- importProp p2
                        return (ps1 ++ ps2)
        _  :|| _  -> Nothing

        Fin expr -> do t <- importType expr
                       return [ Cry.pFin t ]

        e1 :==  e2 -> do t1 <- importType e1
                         t2 <- importType e2
                         return [t1 Cry.=#= t2]
        e1 :>=  e2 -> do t1 <- importType e1
                         t2 <- importType e2
                         return [t1 Cry.>== t2]
        _ :> _     -> Nothing
        e1 :==: e2 -> do t1 <- importType e1
                         t2 <- importType e2
                         -- XXX: Do we need to add fin?
                         return [t1 Cry.=#= t2]
        _ :>: _    -> Nothing

      where
      pNot p =
        case p of
          PFalse  -> Just PTrue
          PTrue   -> Nothing

          Not a   -> Just a
          _ :&& _ -> Nothing
          a :|| b -> Just (Not a :&& Not b)

          Fin a    -> Just (a :== K Inf)
          _ :== _  -> Nothing
          _ :>= _  -> Nothing
          a :>  b  -> Just (b :>= a)
          _ :==: _ -> Nothing
          a :>: b  -> Just (b :>= a)
          -- XXX: Do we need to add Fin on `a` and 'b'?

    importType :: Expr -> Maybe Cry.Type
    importType = go
      where
      go expr =
        case expr of
          Var x               -> case x of
                                   UserName v -> return (Cry.TVar v)
                                   _          -> Nothing
          K n                 -> case n of
                                   Nat x -> Just (Cry.tNum x)
                                   Inf   -> Just (Cry.tInf)
          x :+ y              -> op2 Cry.TCAdd x y
          x :- y              -> op2 Cry.TCSub x y
          x :* y              -> op2 Cry.TCMul x y
          Div x y             -> op2 Cry.TCDiv x y
          Mod x y             -> op2 Cry.TCMod x y
          x :^^ y             -> op2 Cry.TCExp x y
          Min x y             -> op2 Cry.TCMin x y
          Max x y             -> op2 Cry.TCMax x y
          Width x             -> op1 Cry.TCWidth x
          LenFromThen   x y z -> op3 Cry.TCLenFromThen x y z
          LenFromThenTo x y z -> op3 Cry.TCLenFromThenTo x y z

      app f xs = Cry.TCon (Cry.TF f) xs

      op1 f x =
        do t <- go x
           return (app f [t])

      op2 f x y =
        do t1 <- go x
           t2 <- go y
           return (app f [t1,t2])

      op3 f x y z =
        do t1 <- go x
           t2 <- go y
           t3 <- go z
           return (app f [t1,t2,t3])