    -- |
    -- Module      :  Cryptol.TypeCheck.Parseable
    -- Copyright   :  (c) 2013-2017 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe                                #-}

    {-# LANGUAGE RecordWildCards                     #-}
    {-# LANGUAGE PatternGuards                       #-}
    {-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
    {-# LANGUAGE DeriveAnyClass, DeriveGeneric       #-}
    module Cryptol.TypeCheck.Parseable
      ( module Cryptol.TypeCheck.Parseable
      , ShowParseable(..)
      ) where

    import Cryptol.TypeCheck.AST
    import Cryptol.Utils.Ident (Ident,unpackIdent)
    import Cryptol.Parser.AST ( Located(..))
    import Cryptol.ModuleSystem.Name
    import Text.PrettyPrint hiding ((<>))
    import qualified Text.PrettyPrint as PP ((<>))

    -- ShowParseable prints out a cryptol program in a way that it's parseable by Coq (and likely other things)
    -- Used mainly for reasoning about the semantics of cryptol programs in Coq (https://github.com/GaloisInc/cryptol-semantics)
    class ShowParseable t where
      showParseable :: t -> Doc

    instance ShowParseable Expr where
      showParseable (EList es _) = parens (text "EList" <+> showParseable es)
      showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es)
      showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides)
      showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s)
      showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c $$ showParseable t $$ showParseable f)
      showParseable (EComp _ _ e mss) = parens (text "EComp" $$ showParseable e $$ showParseable mss)
      showParseable (EVar n) = parens (text "EVar" <+> showParseable n)
      showParseable (EApp fe ae) = parens (text "EApp" $$ showParseable fe $$ showParseable ae)
      showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n $$ showParseable e)
      showParseable (EWhere e dclg) = parens (text "EWhere" $$ showParseable e $$ showParseable dclg)
      showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp
                                            $$ showParseable e)
      showParseable (ETApp e t) = parens (text "ETApp" $$ showParseable e $$ parens (text "ETyp" <+> showParseable t))
      --NOTE: erase all "proofs" for now (change the following two lines to change that)
      showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
      showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")"

    instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
      showParseable (x,y) = parens (showParseable x PP.<> comma PP.<> showParseable y)

    instance ShowParseable Int where
      showParseable i = int i

    instance ShowParseable Ident where
      showParseable i = text $ show $ unpackIdent i

    instance ShowParseable Type where
      showParseable (TUser n lt t) = parens (text "TUser" <+> showParseable n <+> showParseable lt <+> showParseable t)
      showParseable (TRec lidt) = parens (text "TRec" <+> showParseable lidt)
      showParseable t = parens $ text $ show t

    instance ShowParseable Selector where
      showParseable (TupleSel n _) = parens (text "TupleSel" <+> showParseable n)
      showParseable (RecordSel n _) = parens (text "RecordSel" <+> showParseable n)
      showParseable (ListSel n _) = parens (text "ListSel" <+> showParseable n)

    instance ShowParseable Match where
      showParseable (From n _ _ e) = parens (text "From" <+> showParseable n <+> showParseable e)
      showParseable (Let d) = parens (text "MLet" <+> showParseable d)

    instance ShowParseable Decl where
      showParseable d = parens (text "Decl" <+> showParseable (dName d)
                                  $$ showParseable (dDefinition d))

    instance ShowParseable DeclDef where
      showParseable DPrim = text (show DPrim)
      showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e)

    instance ShowParseable DeclGroup where
      showParseable (Recursive ds) =
        parens (text "Recursive" $$ showParseable ds)
      showParseable (NonRecursive d) =
        parens (text "NonRecursive" $$ showParseable d)

    instance (ShowParseable a) => ShowParseable [a] where
      showParseable a = case a of
                          [] -> text "[]"
                          [x] -> brackets (showParseable x)
                          x : xs -> text "[" <+> showParseable x $$
                                    vcat [ comma <+> showParseable y | y <- xs ] $$
                                    text "]"

    instance (ShowParseable a) => ShowParseable (Maybe a) where
      showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow number
      showParseable (Just x) = showParseable x

    instance (ShowParseable a) => ShowParseable (Located a) where
      showParseable l = showParseable (thing l)

    instance ShowParseable TParam where
      showParseable tp = parens (text (show (tpUnique tp)) PP.<> comma PP.<> maybeNameDoc (tpName tp))

    maybeNameDoc :: Maybe Name -> Doc
    maybeNameDoc Nothing = doubleQuotes empty
    maybeNameDoc (Just n) = showParseable (nameIdent n)

    instance ShowParseable Name where
      showParseable n = parens (text (show (nameUnique n)) PP.<> comma PP.<> showParseable (nameIdent n))