-- |
-- 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 Data.Void
import Prettyprinter

import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (Ident,unpackIdent)
import Cryptol.Utils.RecordMap (canonicalFields)
import Cryptol.Parser.AST ( Located(..))
import Cryptol.ModuleSystem.Name


infixl 5 $$
($$) :: Doc a -> Doc a -> Doc a
$$ :: forall a. Doc a -> Doc a -> Doc a
($$) Doc a
x Doc a
y = forall ann. [Doc ann] -> Doc ann
sep [Doc a
x, Doc a
y]

text :: String -> Doc a
text :: forall a. String -> Doc a
text = forall a ann. Pretty a => a -> Doc ann
pretty

int :: Int -> Doc a
int :: forall a. Int -> Doc a
int = forall a ann. Pretty a => a -> Doc ann
pretty

-- 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 Void

instance ShowParseable Expr where
  showParseable :: Expr -> Doc Void
showParseable (ELocated Range
_ Expr
e) = forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e -- TODO? emit range information
  showParseable (EList [Expr]
es Type
_) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EList" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable [Expr]
es)
  showParseable (ETuple [Expr]
es) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ETuple" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable [Expr]
es)
  showParseable (ERec RecordMap Ident Expr
ides) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ERec" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable (forall a b. RecordMap a b -> [(a, b)]
canonicalFields RecordMap Ident Expr
ides))
  showParseable (ESel Expr
e Selector
s) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ESel" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Selector
s)
  showParseable (ESet Type
_ty Expr
e Selector
s Expr
v) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ESet" forall a. Doc a -> Doc a -> Doc a
<+>
                                forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Selector
s
                                                forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Expr
v)
  showParseable (EIf Expr
c Expr
t Expr
f) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EIf" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Expr
c forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
t forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
f)
  showParseable (EComp Type
_ Type
_ Expr
e [[Match]]
mss) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EComp" forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable [[Match]]
mss)
  showParseable (EVar Name
n) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EVar" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Name
n)
  showParseable (EApp Expr
fe Expr
ae) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EApp" forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
fe forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
ae)
  showParseable (EAbs Name
n Type
_ Expr
e) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EAbs" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Name
n forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e)
  showParseable (EWhere Expr
e [DeclGroup]
dclg) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EWhere" forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable [DeclGroup]
dclg)
  showParseable (ETAbs TParam
tp Expr
e) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ETAbs" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable TParam
tp
                                        forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e)
  showParseable (ETApp Expr
e Type
t) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ETApp" forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e forall a. Doc a -> Doc a -> Doc a
$$ forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"ETyp" forall a. Doc a -> Doc a -> Doc a
<+> forall t. ShowParseable t => t -> Doc Void
showParseable Type
t))
  --NOTE: erase all "proofs" for now (change the following two lines to change that)
  showParseable (EProofAbs {-p-}Type
_ Expr
e) = forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
  showParseable (EProofApp Expr
e) = forall t. ShowParseable t => t -> Doc Void
showParseable Expr
e --"(EProofApp " ++ showParseable e ++ ")"
  
  showParseable (EPropGuards [([Type], Expr)]
guards Type
_) = forall ann. Doc ann -> Doc ann
parens (forall a. String -> Doc a
text String
"EPropGuards" forall a. Doc a -> Doc a -> Doc a
$$ forall t. ShowParseable t => t -> Doc Void
showParseable [([Type], Expr)]
guards)

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

instance ShowParseable Int where
  showParseable :: Int -> Doc Void
showParseable Int
i = forall a. Int -> Doc a
int Int
i

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

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

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

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

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

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

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

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

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

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

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

maybeNameDoc :: Maybe Name -> Doc Void
maybeNameDoc :: Maybe Name -> Doc Void
maybeNameDoc Maybe Name
Nothing = forall ann. Doc ann -> Doc ann
dquotes forall a. Monoid a => a
mempty
maybeNameDoc (Just Name
n) = forall t. ShowParseable t => t -> Doc Void
showParseable (Name -> Ident
nameIdent Name
n)

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