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

    module Cryptol.Prims.Syntax
      ( TFun(..)
      , ECon(..)
      , eBinOpPrec
      , tBinOpPrec
      , ppPrefix
      ) where

    import           Cryptol.Utils.PP
    import qualified Data.Map as Map

    -- | Built-in types.
    data TFun

      = TCAdd                 -- ^ @ : Num -> Num -> Num @
      | TCSub                 -- ^ @ : Num -> Num -> Num @
      | TCMul                 -- ^ @ : Num -> Num -> Num @
      | TCDiv                 -- ^ @ : Num -> Num -> Num @
      | TCMod                 -- ^ @ : Num -> Num -> Num @
      | TCLg2                 -- ^ @ : Num -> Num @
      | TCExp                 -- ^ @ : Num -> Num -> Num @
      | TCWidth               -- ^ @ : Num -> Num @
      | TCMin                 -- ^ @ : Num -> Num -> Num @
      | TCMax                 -- ^ @ : Num -> Num -> Num @

      -- Computing the lengths of explicit enumerations
      | TCLenFromThen         -- ^ @ : Num -> Num -> Num -> Num@
        -- Example: @[ 1, 5 .. ] :: [lengthFromThen 1 5 b][b]@

      | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@
        -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@

        deriving (Show, Eq, Ord, Bounded, Enum)

    -- | Built-in constants.
    data ECon

      = ECTrue
      | ECFalse

      | ECDemote -- ^ Converts a numeric type into its corresponding value.

      -- Arith
      | ECPlus | ECMinus | ECMul | ECDiv | ECMod
      | ECExp | ECLg2 | ECNeg

      -- Cmp
      | ECLt | ECGt | ECLtEq | ECGtEq | ECEq | ECNotEq
      | ECFunEq | ECFunNotEq
      | ECMin | ECMax

      -- Logic
      | ECAnd | ECOr | ECXor | ECCompl | ECZero
      | ECShiftL | ECShiftR | ECRotL | ECRotR

      -- Sequences
      | ECCat  | ECSplitAt
      | ECJoin | ECSplit
      | ECReverse | ECTranspose

      | ECAt | ECAtRange | ECAtBack | ECAtRangeBack

      -- Static word sequences
      | ECFromThen | ECFromTo | ECFromThenTo

      -- Infinite word sequences
      | ECInfFrom | ECInfFromThen

      -- Run-time error
      | ECError

      -- Polynomials
      | ECPMul | ECPDiv | ECPMod

      -- Random values
      | ECRandom
        deriving (Eq,Ord,Show,Bounded,Enum)

    eBinOpPrec :: Map.Map ECon  (Assoc,Int)
    tBinOpPrec :: Map.Map TFun  (Assoc,Int)

    (eBinOpPrec, tBinOpPrec) = (mkMap e_table, mkMap t_table)
      where
      mkMap t = Map.fromList [ (op,(a,n)) | ((a,ops),n) <- zip t [0..] , op <- ops ]

      -- lowest to highest
      e_table =
        [ (LeftAssoc,  [ ECOr  ])
        , (LeftAssoc,  [ ECXor ])
        , (LeftAssoc,  [ ECAnd ])

        , (NonAssoc,   [ ECEq, ECNotEq, ECFunEq, ECFunNotEq ])
        , (NonAssoc,   [ ECLt, ECGt, ECLtEq, ECGtEq ])

        , (RightAssoc, [ ECCat ])
        , (LeftAssoc,  [ ECShiftL, ECShiftR, ECRotL, ECRotR ])

        , (LeftAssoc,  [ ECPlus, ECMinus ])
        , (LeftAssoc,  [ ECMul, ECDiv, ECMod ])
        , (RightAssoc, [ ECExp ])

        , (LeftAssoc,  [ ECAt, ECAtRange, ECAtBack, ECAtRangeBack ])
        ]

      t_table =
        [ (LeftAssoc,   [ TCAdd, TCSub ])
        , (LeftAssoc,   [ TCMul, TCDiv, TCMod ])
        , (RightAssoc,  [ TCExp ])
        ]

    instance PP TFun where
      ppPrec _ tcon =
        case tcon of
          TCAdd             -> text "+"
          TCSub             -> text "-"
          TCMul             -> text "*"
          TCDiv             -> text "/"
          TCMod             -> text "%"
          TCLg2             -> text "lg2"
          TCExp             -> text "^^"
          TCWidth           -> text "width"
          TCMin             -> text "min"
          TCMax             -> text "max"

          TCLenFromThen     -> text "lengthFromThen"
          TCLenFromThenTo   -> text "lengthFromThenTo"

    instance PP ECon where
      ppPrec _ con =
        case con of
          ECTrue        -> text "True"
          ECFalse       -> text "False"
          ECPlus        -> text "+"
          ECMinus       -> text "-"
          ECMul         -> text "*"
          ECDiv         -> text "/"
          ECMod         -> text "%"
          ECExp         -> text "^^"
          ECLg2         -> text "lg2"
          ECNeg         -> text "-"
          ECLt          -> text "<"
          ECGt          -> text ">"
          ECLtEq        -> text "<="
          ECGtEq        -> text ">="
          ECEq          -> text "=="
          ECNotEq       -> text "!="
          ECFunEq       -> text "==="
          ECFunNotEq    -> text "!=="
          ECAnd         -> text "&&"
          ECOr          -> text "||"
          ECXor         -> text "^"
          ECCompl       -> text "~"
          ECShiftL      -> text "<<"
          ECShiftR      -> text ">>"
          ECRotL        -> text "<<<"
          ECRotR        -> text ">>>"
          ECCat         -> text "#"
          ECAt          -> text "@"
          ECAtRange     -> text "@@"
          ECAtBack      -> text "!"
          ECAtRangeBack -> text "!!"
          ECMin         -> text "min"
          ECMax         -> text "max"

          ECSplitAt     -> text "splitAt"
          ECZero        -> text "zero"
          ECJoin        -> text "join"
          ECSplit       -> text "split"
          ECReverse     -> text "reverse"
          ECTranspose   -> text "transpose"

          ECDemote      -> text "demote"

          ECFromThen    -> text "fromThen"
          ECFromTo      -> text "fromTo"
          ECFromThenTo  -> text "fromThenTo"

          ECInfFrom     -> text "infFrom"
          ECInfFromThen -> text "infFromThen"

          ECError       -> text "error"

          ECPMul        -> text "pmult"
          ECPDiv        -> text "pdiv"
          ECPMod        -> text "pmod"

          ECRandom      -> text "random"

    ppPrefix :: ECon -> Doc
    ppPrefix con = optParens (Map.member con eBinOpPrec) (pp con)