    -- |
    -- 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 :: Expr -> Doc
    showParseable (EList es :: [Expr]
    es _) = Doc -> Doc
    parens (String -> Doc
    text "EList" Doc -> Doc -> Doc
    <+> [Expr] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [Expr]
    es)
      showParseable (ETuple es :: [Expr]
    es) = Doc -> Doc
    parens (String -> Doc
    text "ETuple" Doc -> Doc -> Doc
    <+> [Expr] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [Expr]
    es)
      showParseable (ERec ides :: [(Ident, Expr)]
    ides) = Doc -> Doc
    parens (String -> Doc
    text "ERec" Doc -> Doc -> Doc
    <+> [(Ident, Expr)] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [(Ident, Expr)]
    ides)
      showParseable (ESel e :: Expr
    e s :: Selector
    s) = Doc -> Doc
    parens (String -> Doc
    text "ESel" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e Doc -> Doc -> Doc
    <+> Selector -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Selector
    s)
      showParseable (ESet e :: Expr
    e s :: Selector
    s v :: Expr
    v) = Doc -> Doc
    parens (String -> Doc
    text "ESet" Doc -> Doc -> Doc
    <+>
                                    Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e Doc -> Doc -> Doc
    <+> Selector -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Selector
    s
                                                    Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    v)
      showParseable (EIf c :: Expr
    c t :: Expr
    t f :: Expr
    f) = Doc -> Doc
    parens (String -> Doc
    text "EIf" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    c Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    t Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    f)
      showParseable (EComp _ _ e :: Expr
    e mss :: [[Match]]
    mss) = Doc -> Doc
    parens (String -> Doc
    text "EComp" Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e Doc -> Doc -> Doc
    $$ [[Match]] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [[Match]]
    mss)
      showParseable (EVar n :: Name
    n) = Doc -> Doc
    parens (String -> Doc
    text "EVar" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Name
    n)
      showParseable (EApp fe :: Expr
    fe ae :: Expr
    ae) = Doc -> Doc
    parens (String -> Doc
    text "EApp" Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    fe Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    ae)
      showParseable (EAbs n :: Name
    n _ e :: Expr
    e) = Doc -> Doc
    parens (String -> Doc
    text "EAbs" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Name
    n Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e)
      showParseable (EWhere e :: Expr
    e dclg :: [DeclGroup]
    dclg) = Doc -> Doc
    parens (String -> Doc
    text "EWhere" Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e Doc -> Doc -> Doc
    $$ [DeclGroup] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [DeclGroup]
    dclg)
      showParseable (ETAbs tp :: TParam
    tp e :: Expr
    e) = Doc -> Doc
    parens (String -> Doc
    text "ETAbs" Doc -> Doc -> Doc
    <+> TParam -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable TParam
    tp
                                            Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e)
      showParseable (ETApp e :: Expr
    e t :: Type
    t) = Doc -> Doc
    parens (String -> Doc
    text "ETApp" Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e Doc -> Doc -> Doc
    $$ Doc -> Doc
    parens (String -> Doc
    text "ETyp" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Type
    t))
      --NOTE: erase all "proofs" for now (change the following two lines to change that)
      showParseable (EProofAbs {-p-}_ e :: Expr
    e) = Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
      showParseable (EProofApp e :: Expr
    e) = Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e --"(EProofApp " ++ showParseable e ++ ")"

    instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
      showParseable :: (a, b) -> Doc
    showParseable (x :: a
    x,y :: b
    y) = Doc -> Doc
    parens (a -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable a
    x Doc -> Doc -> Doc
    PP.<> Doc
    comma Doc -> Doc -> Doc
    PP.<> b -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable b
    y)

    instance ShowParseable Int where
      showParseable :: Int -> Doc
    showParseable i :: Int
    i = Int -> Doc
    int Int
    i

    instance ShowParseable Ident where
      showParseable :: Ident -> Doc
    showParseable i :: Ident
    i = String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> String
    forall a. Show a => a -> String
    show (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ Ident -> String
    unpackIdent Ident
    i

    instance ShowParseable Type where
      showParseable :: Type -> Doc
    showParseable (TUser n :: Name
    n lt :: [Type]
    lt t :: Type
    t) = Doc -> Doc
    parens (String -> Doc
    text "TUser" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Name
    n Doc -> Doc -> Doc
    <+> [Type] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [Type]
    lt Doc -> Doc -> Doc
    <+> Type -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Type
    t)
      showParseable (TRec lidt :: [(Ident, Type)]
    lidt) = Doc -> Doc
    parens (String -> Doc
    text "TRec" Doc -> Doc -> Doc
    <+> [(Ident, Type)] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [(Ident, Type)]
    lidt)
      showParseable t :: Type
    t = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> String
    forall a. Show a => a -> String
    show Type
    t

    instance ShowParseable Selector where
      showParseable :: Selector -> Doc
    showParseable (TupleSel n :: Int
    n _) = Doc -> Doc
    parens (String -> Doc
    text "TupleSel" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Int
    n)
      showParseable (RecordSel n :: Ident
    n _) = Doc -> Doc
    parens (String -> Doc
    text "RecordSel" Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Ident
    n)
      showParseable (ListSel n :: Int
    n _) = Doc -> Doc
    parens (String -> Doc
    text "ListSel" Doc -> Doc -> Doc
    <+> Int -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Int
    n)

    instance ShowParseable Match where
      showParseable :: Match -> Doc
    showParseable (From n :: Name
    n _ _ e :: Expr
    e) = Doc -> Doc
    parens (String -> Doc
    text "From" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Name
    n Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e)
      showParseable (Let d :: Decl
    d) = Doc -> Doc
    parens (String -> Doc
    text "MLet" Doc -> Doc -> Doc
    <+> Decl -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Decl
    d)

    instance ShowParseable Decl where
      showParseable :: Decl -> Doc
    showParseable d :: Decl
    d = Doc -> Doc
    parens (String -> Doc
    text "Decl" Doc -> Doc -> Doc
    <+> Name -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable (Decl -> Name
    dName Decl
    d)
                                  Doc -> Doc -> Doc
    $$ DeclDef -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable (Decl -> DeclDef
    dDefinition Decl
    d))

    instance ShowParseable DeclDef where
      showParseable :: DeclDef -> Doc
    showParseable DPrim = String -> Doc
    text (DeclDef -> String
    forall a. Show a => a -> String
    show DeclDef
    DPrim)
      showParseable (DExpr e :: Expr
    e) = Doc -> Doc
    parens (String -> Doc
    text "DExpr" Doc -> Doc -> Doc
    $$ Expr -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Expr
    e)

    instance ShowParseable DeclGroup where
      showParseable :: DeclGroup -> Doc
    showParseable (Recursive ds :: [Decl]
    ds) =
        Doc -> Doc
    parens (String -> Doc
    text "Recursive" Doc -> Doc -> Doc
    $$ [Decl] -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable [Decl]
    ds)
      showParseable (NonRecursive d :: Decl
    d) =
        Doc -> Doc
    parens (String -> Doc
    text "NonRecursive" Doc -> Doc -> Doc
    $$ Decl -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable Decl
    d)

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

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

    instance (ShowParseable a) => ShowParseable (Located a) where
      showParseable :: Located a -> Doc
    showParseable l :: Located a
    l = a -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable (Located a -> a
    forall a. Located a -> a
    thing Located a
    l)

    instance ShowParseable TParam where
      showParseable :: TParam -> Doc
    showParseable tp :: TParam
    tp = Doc -> Doc
    parens (String -> Doc
    text (Int -> String
    forall a. Show a => a -> String
    show (TParam -> Int
    tpUnique TParam
    tp)) Doc -> Doc -> Doc
    PP.<> Doc
    comma Doc -> Doc -> Doc
    PP.<> Maybe Name -> Doc
    maybeNameDoc (TParam -> Maybe Name
    tpName TParam
    tp))

    maybeNameDoc :: Maybe Name -> Doc
    maybeNameDoc :: Maybe Name -> Doc
    maybeNameDoc Nothing = Doc -> Doc
    doubleQuotes Doc
    empty
    maybeNameDoc (Just n :: Name
    n) = Ident -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable (Name -> Ident
    nameIdent Name
    n)

    instance ShowParseable Name where
      showParseable :: Name -> Doc
    showParseable n :: Name
    n = Doc -> Doc
    parens (String -> Doc
    text (Int -> String
    forall a. Show a => a -> String
    show (Name -> Int
    nameUnique Name
    n)) Doc -> Doc -> Doc
    PP.<> Doc
    comma Doc -> Doc -> Doc
    PP.<> Ident -> Doc
    forall t. ShowParseable t => t -> Doc
    showParseable (Name -> Ident
    nameIdent Name
    n))