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

{-# LANGUAGE Safe                                #-}

{-# LANGUAGE RecordWildCards                     #-}
{-# LANGUAGE PatternGuards                       #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric       #-}
{-# LANGUAGE OverloadedStrings                   #-}
module Cryptol.TypeCheck.AST
  ( module Cryptol.TypeCheck.AST
  , Name()
  , TFun(..)
  , Selector(..)
  , Import(..)
  , ImportSpec(..)
  , ExportType(..)
  , ExportSpec(..), isExportedBind, isExportedType
  , Pragma(..)
  , Fixity(..)
  , PrimMap(..)
  , TCErrorMessage(..)
  , module Cryptol.TypeCheck.Type
  ) where

import Cryptol.Parser.Position(Located)
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Exports(ExportSpec(..)
                                   , isExportedBind, isExportedType)
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
                          , Import(..), ImportSpec(..), ExportType(..)
                          , Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type

import GHC.Generics (Generic)
import Control.DeepSeq

import           Data.Map    (Map)
import qualified Data.Map    as Map
import qualified Data.IntMap as IntMap


-- | A Cryptol module.
data Module = Module { Module -> ModName
mName        :: !ModName
                     , Module -> ExportSpec Name
mExports     :: ExportSpec Name
                     , Module -> [Import]
mImports     :: [Import]

                     , Module -> Map Name TySyn
mTySyns      :: Map Name TySyn
                       -- ^ This is just the type-level type synonyms
                       -- of a module.

                     , Module -> Map Name Newtype
mNewtypes         :: Map Name Newtype
                     , Module -> Map Name AbstractType
mPrimTypes        :: Map Name AbstractType
                     , Module -> Map Name ModTParam
mParamTypes       :: Map Name ModTParam
                     , Module -> [Located Prop]
mParamConstraints :: [Located Prop]
                     , Module -> Map Name ModVParam
mParamFuns        :: Map Name ModVParam
                     , Module -> [DeclGroup]
mDecls            :: [DeclGroup]
                     } deriving (Int -> Module -> ShowS
[Module] -> ShowS
Module -> String
(Int -> Module -> ShowS)
-> (Module -> String) -> ([Module] -> ShowS) -> Show Module
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Module] -> ShowS
$cshowList :: [Module] -> ShowS
show :: Module -> String
$cshow :: Module -> String
showsPrec :: Int -> Module -> ShowS
$cshowsPrec :: Int -> Module -> ShowS
Show, (forall x. Module -> Rep Module x)
-> (forall x. Rep Module x -> Module) -> Generic Module
forall x. Rep Module x -> Module
forall x. Module -> Rep Module x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Module x -> Module
$cfrom :: forall x. Module -> Rep Module x
Generic, Module -> ()
(Module -> ()) -> NFData Module
forall a. (a -> ()) -> NFData a
rnf :: Module -> ()
$crnf :: Module -> ()
NFData)

-- | Is this a parameterized module?
isParametrizedModule :: Module -> Bool
isParametrizedModule :: Module -> Bool
isParametrizedModule m :: Module
m = Bool -> Bool
not (Map Name ModTParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> Map Name ModTParam
mParamTypes Module
m) Bool -> Bool -> Bool
&&
                              [Located Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> [Located Prop]
mParamConstraints Module
m) Bool -> Bool -> Bool
&&
                              Map Name ModVParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> Map Name ModVParam
mParamFuns Module
m))

-- | A type parameter of a module.
data ModTParam = ModTParam
  { ModTParam -> Name
mtpName   :: Name
  , ModTParam -> Kind
mtpKind   :: Kind
  , ModTParam -> Int
mtpNumber :: !Int -- ^ The number of the parameter in the module
                      -- This is used when we move parameters from the module
                      -- level to individual declarations
                      -- (type synonyms in particular)
  , ModTParam -> Maybe String
mtpDoc    :: Maybe String
  } deriving (Int -> ModTParam -> ShowS
[ModTParam] -> ShowS
ModTParam -> String
(Int -> ModTParam -> ShowS)
-> (ModTParam -> String)
-> ([ModTParam] -> ShowS)
-> Show ModTParam
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModTParam] -> ShowS
$cshowList :: [ModTParam] -> ShowS
show :: ModTParam -> String
$cshow :: ModTParam -> String
showsPrec :: Int -> ModTParam -> ShowS
$cshowsPrec :: Int -> ModTParam -> ShowS
Show,(forall x. ModTParam -> Rep ModTParam x)
-> (forall x. Rep ModTParam x -> ModTParam) -> Generic ModTParam
forall x. Rep ModTParam x -> ModTParam
forall x. ModTParam -> Rep ModTParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModTParam x -> ModTParam
$cfrom :: forall x. ModTParam -> Rep ModTParam x
Generic,ModTParam -> ()
(ModTParam -> ()) -> NFData ModTParam
forall a. (a -> ()) -> NFData a
rnf :: ModTParam -> ()
$crnf :: ModTParam -> ()
NFData)

mtpParam :: ModTParam -> TParam
mtpParam :: ModTParam -> TParam
mtpParam mtp :: ModTParam
mtp = $WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
TParam { tpUnique :: Int
tpUnique = Name -> Int
nameUnique (ModTParam -> Name
mtpName ModTParam
mtp)
                      , tpKind :: Kind
tpKind   = ModTParam -> Kind
mtpKind ModTParam
mtp
                      , tpFlav :: TPFlavor
tpFlav   = Name -> TPFlavor
TPModParam (ModTParam -> Name
mtpName ModTParam
mtp)
                      , tpInfo :: TVarInfo
tpInfo   = TVarInfo
desc
                      }
  where desc :: TVarInfo
desc = TVarInfo :: Range -> TVarSource -> TVarInfo
TVarInfo { tvarDesc :: TVarSource
tvarDesc   = Name -> TVarSource
TVFromModParam (ModTParam -> Name
mtpName ModTParam
mtp)
                        , tvarSource :: Range
tvarSource = Name -> Range
nameLoc (ModTParam -> Name
mtpName ModTParam
mtp)
                        }

-- | A value parameter of a module.
data ModVParam = ModVParam
  { ModVParam -> Name
mvpName   :: Name
  , ModVParam -> Schema
mvpType   :: Schema
  , ModVParam -> Maybe String
mvpDoc    :: Maybe String
  , ModVParam -> Maybe Fixity
mvpFixity :: Maybe Fixity
  } deriving (Int -> ModVParam -> ShowS
[ModVParam] -> ShowS
ModVParam -> String
(Int -> ModVParam -> ShowS)
-> (ModVParam -> String)
-> ([ModVParam] -> ShowS)
-> Show ModVParam
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModVParam] -> ShowS
$cshowList :: [ModVParam] -> ShowS
show :: ModVParam -> String
$cshow :: ModVParam -> String
showsPrec :: Int -> ModVParam -> ShowS
$cshowsPrec :: Int -> ModVParam -> ShowS
Show,(forall x. ModVParam -> Rep ModVParam x)
-> (forall x. Rep ModVParam x -> ModVParam) -> Generic ModVParam
forall x. Rep ModVParam x -> ModVParam
forall x. ModVParam -> Rep ModVParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModVParam x -> ModVParam
$cfrom :: forall x. ModVParam -> Rep ModVParam x
Generic,ModVParam -> ()
(ModVParam -> ()) -> NFData ModVParam
forall a. (a -> ()) -> NFData a
rnf :: ModVParam -> ()
$crnf :: ModVParam -> ()
NFData)


data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
            | ETuple [Expr]             -- ^ Tuple value
            | ERec [(Ident,Expr)]       -- ^ Record value
            | ESel Expr Selector        -- ^ Elimination for tuple/record/list
            | ESet Expr Selector Expr   -- ^ Change the value of a field.

            | EIf Expr Expr Expr        -- ^ If-then-else
            | EComp Type Type Expr [[Match]]
                                        -- ^ List comprehensions
                                        --   The types cache the length of the
                                        --   sequence and its element type.

            | EVar Name                 -- ^ Use of a bound variable

            | ETAbs TParam Expr         -- ^ Function Value
            | ETApp Expr Type           -- ^ Type application

            | EApp Expr Expr            -- ^ Function application
            | EAbs Name Type Expr       -- ^ Function value


            {- | Proof abstraction.  Because we don't keep proofs around
                 we don't need to name the assumption, but we still need to
                 record the assumption.  The assumption is the `Type` term,
                 which should be of kind `KProp`.
             -}
            | EProofAbs {- x -} Prop Expr

            {- | If `e : p => t`, then `EProofApp e : t`,
                 as long as we can prove `p`.

                 We don't record the actual proofs, as they are not
                 used for anything.  It may be nice to keep them around
                 for sanity checking.
             -}

            | EProofApp Expr {- proof -}

            | EWhere Expr [DeclGroup]

              deriving (Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, (forall x. Expr -> Rep Expr x)
-> (forall x. Rep Expr x -> Expr) -> Generic Expr
forall x. Rep Expr x -> Expr
forall x. Expr -> Rep Expr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Expr x -> Expr
$cfrom :: forall x. Expr -> Rep Expr x
Generic, Expr -> ()
(Expr -> ()) -> NFData Expr
forall a. (a -> ()) -> NFData a
rnf :: Expr -> ()
$crnf :: Expr -> ()
NFData)


data Match  = From Name Type Type Expr
                                  -- ^ Type arguments are the length and element
                                  --   type of the sequence expression
            | Let Decl
              deriving (Int -> Match -> ShowS
[Match] -> ShowS
Match -> String
(Int -> Match -> ShowS)
-> (Match -> String) -> ([Match] -> ShowS) -> Show Match
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Match] -> ShowS
$cshowList :: [Match] -> ShowS
show :: Match -> String
$cshow :: Match -> String
showsPrec :: Int -> Match -> ShowS
$cshowsPrec :: Int -> Match -> ShowS
Show, (forall x. Match -> Rep Match x)
-> (forall x. Rep Match x -> Match) -> Generic Match
forall x. Rep Match x -> Match
forall x. Match -> Rep Match x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Match x -> Match
$cfrom :: forall x. Match -> Rep Match x
Generic, Match -> ()
(Match -> ()) -> NFData Match
forall a. (a -> ()) -> NFData a
rnf :: Match -> ()
$crnf :: Match -> ()
NFData)

data DeclGroup  = Recursive   [Decl]    -- ^ Mutually recursive declarations
                | NonRecursive Decl     -- ^ Non-recursive declaration
                  deriving (Int -> DeclGroup -> ShowS
[DeclGroup] -> ShowS
DeclGroup -> String
(Int -> DeclGroup -> ShowS)
-> (DeclGroup -> String)
-> ([DeclGroup] -> ShowS)
-> Show DeclGroup
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeclGroup] -> ShowS
$cshowList :: [DeclGroup] -> ShowS
show :: DeclGroup -> String
$cshow :: DeclGroup -> String
showsPrec :: Int -> DeclGroup -> ShowS
$cshowsPrec :: Int -> DeclGroup -> ShowS
Show, (forall x. DeclGroup -> Rep DeclGroup x)
-> (forall x. Rep DeclGroup x -> DeclGroup) -> Generic DeclGroup
forall x. Rep DeclGroup x -> DeclGroup
forall x. DeclGroup -> Rep DeclGroup x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DeclGroup x -> DeclGroup
$cfrom :: forall x. DeclGroup -> Rep DeclGroup x
Generic, DeclGroup -> ()
(DeclGroup -> ()) -> NFData DeclGroup
forall a. (a -> ()) -> NFData a
rnf :: DeclGroup -> ()
$crnf :: DeclGroup -> ()
NFData)

groupDecls :: DeclGroup -> [Decl]
groupDecls :: DeclGroup -> [Decl]
groupDecls dg :: DeclGroup
dg = case DeclGroup
dg of
  Recursive ds :: [Decl]
ds   -> [Decl]
ds
  NonRecursive d :: Decl
d -> [Decl
d]


data Decl       = Decl { Decl -> Name
dName        :: !Name
                       , Decl -> Schema
dSignature   :: Schema
                       , Decl -> DeclDef
dDefinition  :: DeclDef
                       , Decl -> [Pragma]
dPragmas     :: [Pragma]
                       , Decl -> Bool
dInfix       :: !Bool
                       , Decl -> Maybe Fixity
dFixity      :: Maybe Fixity
                       , Decl -> Maybe String
dDoc         :: Maybe String
                       } deriving ((forall x. Decl -> Rep Decl x)
-> (forall x. Rep Decl x -> Decl) -> Generic Decl
forall x. Rep Decl x -> Decl
forall x. Decl -> Rep Decl x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Decl x -> Decl
$cfrom :: forall x. Decl -> Rep Decl x
Generic, Decl -> ()
(Decl -> ()) -> NFData Decl
forall a. (a -> ()) -> NFData a
rnf :: Decl -> ()
$crnf :: Decl -> ()
NFData, Int -> Decl -> ShowS
[Decl] -> ShowS
Decl -> String
(Int -> Decl -> ShowS)
-> (Decl -> String) -> ([Decl] -> ShowS) -> Show Decl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Decl] -> ShowS
$cshowList :: [Decl] -> ShowS
show :: Decl -> String
$cshow :: Decl -> String
showsPrec :: Int -> Decl -> ShowS
$cshowsPrec :: Int -> Decl -> ShowS
Show)

data DeclDef    = DPrim
                | DExpr Expr
                  deriving (Int -> DeclDef -> ShowS
[DeclDef] -> ShowS
DeclDef -> String
(Int -> DeclDef -> ShowS)
-> (DeclDef -> String) -> ([DeclDef] -> ShowS) -> Show DeclDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeclDef] -> ShowS
$cshowList :: [DeclDef] -> ShowS
show :: DeclDef -> String
$cshow :: DeclDef -> String
showsPrec :: Int -> DeclDef -> ShowS
$cshowsPrec :: Int -> DeclDef -> ShowS
Show, (forall x. DeclDef -> Rep DeclDef x)
-> (forall x. Rep DeclDef x -> DeclDef) -> Generic DeclDef
forall x. Rep DeclDef x -> DeclDef
forall x. DeclDef -> Rep DeclDef x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DeclDef x -> DeclDef
$cfrom :: forall x. DeclDef -> Rep DeclDef x
Generic, DeclDef -> ()
(DeclDef -> ()) -> NFData DeclDef
forall a. (a -> ()) -> NFData a
rnf :: DeclDef -> ()
$crnf :: DeclDef -> ()
NFData)


--------------------------------------------------------------------------------

-- | Construct a primitive, given a map to the unique names of the Cryptol
-- module.
ePrim :: PrimMap -> Ident -> Expr
ePrim :: PrimMap -> Ident -> Expr
ePrim pm :: PrimMap
pm n :: Ident
n = Name -> Expr
EVar (Ident -> PrimMap -> Name
lookupPrimDecl Ident
n PrimMap
pm)

-- | Make an expression that is `error` pre-applied to a type and a message.
eError :: PrimMap -> Type -> String -> Expr
eError :: PrimMap -> Prop -> String -> Expr
eError prims :: PrimMap
prims t :: Prop
t str :: String
str =
  Expr -> Expr -> Expr
EApp (Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> Ident -> Expr
ePrim PrimMap
prims (String -> Ident
packIdent "error")) Prop
t)
              (Int -> Prop
forall a. Integral a => a -> Prop
tNum (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str))) (PrimMap -> String -> Expr
eString PrimMap
prims String
str)

eString :: PrimMap -> String -> Expr
eString :: PrimMap -> String -> Expr
eString prims :: PrimMap
prims str :: String
str = [Expr] -> Prop -> Expr
EList ((Char -> Expr) -> String -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (PrimMap -> Char -> Expr
eChar PrimMap
prims) String
str) Prop
tChar

eChar :: PrimMap -> Char -> Expr
eChar :: PrimMap -> Char -> Expr
eChar prims :: PrimMap
prims c :: Char
c = Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> Ident -> Expr
ePrim PrimMap
prims (String -> Ident
packIdent "number")) (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
v)) (Prop -> Prop
tWord (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
w))
  where v :: Int
v = Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c
        w :: Int
w = 8 :: Int


instance PP (WithNames Expr) where
  ppPrec :: Int -> WithNames Expr -> Doc
ppPrec prec :: Int
prec (WithNames expr :: Expr
expr nm :: NameMap
nm) =
    case Expr
expr of
      EList [] t :: Prop
t    -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
                    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "[]" Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
prec Prop
t

      EList es :: [Expr]
es _    -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [Expr]
es

      ETuple es :: [Expr]
es     -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [Expr]
es

      ERec fs :: [(Ident, Expr)]
fs       -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
                        [ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e | (f :: Ident
f,e :: Expr
e) <- [(Ident, Expr)]
fs ]

      ESel e :: Expr
e sel :: Selector
sel    -> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text "." Doc -> Doc -> Doc
<.> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel

      ESet e :: Expr
e sel :: Selector
sel v :: Expr
v  -> Doc -> Doc
braces (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e Doc -> Doc -> Doc
<+> "|" Doc -> Doc -> Doc
<+> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel Doc -> Doc -> Doc
<+> "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
v)

      EIf e1 :: Expr
e1 e2 :: Expr
e2 e3 :: Expr
e3  -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
                    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ String -> Doc
text "if"   Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e1
                          , String -> Doc
text "then" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e2
                          , String -> Doc
text "else" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e3 ]

      EComp _ _ e :: Expr
e mss :: [[Match]]
mss -> let arm :: [a] -> Doc
arm ms :: [a]
ms = String -> Doc
text "|" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [a]
ms)
                          in Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (([Match] -> Doc) -> [[Match]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Match] -> Doc
forall a. PP (WithNames a) => [a] -> Doc
arm [[Match]]
mss)

      EVar x :: Name
x        -> Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
x

      EAbs {}       -> let (xs :: [(Name, Prop)]
xs,e :: Expr
e) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs Expr
expr
                       in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [] [] [(Name, Prop)]
xs Expr
e

      EProofAbs {}  -> let (ps :: [Prop]
ps,e1 :: Expr
e1) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
expr
                           (xs :: [(Name, Prop)]
xs,e2 :: Expr
e2) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs Expr
e1
                       in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [] [Prop]
ps [(Name, Prop)]
xs Expr
e2

      ETAbs {}      -> let (ts :: [TParam]
ts,e1 :: Expr
e1) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs     Expr
expr
                           (ps :: [Prop]
ps,e2 :: Expr
e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
e1
                           (xs :: [(Name, Prop)]
xs,e3 :: Expr
e3) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs      Expr
e2
                       in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [TParam]
ts [Prop]
ps [(Name, Prop)]
xs Expr
e3

      -- infix applications
      EApp (EApp (EVar o :: Name
o) a :: Expr
a) b :: Expr
b
        | Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
o) ->
          Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr
a Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PPName a => a -> Doc
ppInfixName Name
o Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr
b

        | Bool
otherwise ->
          Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
o Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr
a Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr
b

      EApp e1 :: Expr
e1 e2 :: Expr
e2    -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
                    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$  Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e1 Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Expr
e2

      EProofApp e :: Expr
e   -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
                    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text "<>"

      ETApp e :: Expr
e t :: Prop
t     -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
                    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Prop
t

      EWhere e :: Expr
e ds :: [DeclGroup]
ds   -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
                     ( Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e Doc -> Doc -> Doc
$$ String -> Doc
text "where"
                                     Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DeclGroup -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [DeclGroup]
ds))
                                     Doc -> Doc -> Doc
$$ String -> Doc
text "" )

    where
    ppW :: a -> Doc
ppW x :: a
x   = NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm a
x
    ppWP :: Int -> a -> Doc
ppWP x :: Int
x  = NameMap -> Int -> a -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
x

ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc
ppLam :: NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam nm :: NameMap
nm prec :: Int
prec [] [] [] e :: Expr
e = NameMap -> Int -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
prec Expr
e
ppLam nm :: NameMap
nm prec :: Int
prec ts :: [TParam]
ts ps :: [Prop]
ps xs :: [(Name, Prop)]
xs e :: Expr
e =
  Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
sep [ String -> Doc
text "\\" Doc -> Doc -> Doc
<.> Doc
tsD Doc -> Doc -> Doc
<+> Doc
psD Doc -> Doc -> Doc
<+> Doc
xsD Doc -> Doc -> Doc
<+> String -> Doc
text "->"
      , NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 Expr
e
      ]
  where
  ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ts NameMap
nm

  tsD :: Doc
tsD = if [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
ts then Doc
empty else Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Doc
ppT [TParam]
ts
  psD :: Doc
psD = if [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps then Doc
empty else Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
ppP [Prop]
ps
  xsD :: Doc
xsD = if [(Name, Prop)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Prop)]
xs then Doc
empty else [Doc] -> Doc
sep    ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Prop) -> Doc) -> [(Name, Prop)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Prop) -> Doc
forall a a. (PP a, PP (WithNames a)) => (a, a) -> Doc
ppArg [(Name, Prop)]
xs

  ppT :: TParam -> Doc
ppT = NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
  ppP :: Prop -> Doc
ppP = NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
  ppArg :: (a, a) -> Doc
ppArg (x :: a
x,t :: a
t) = Doc -> Doc
parens (a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 a
t)


splitWhile :: (a -> Maybe (b,a)) -> a -> ([b],a)
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile f :: a -> Maybe (b, a)
f e :: a
e = case a -> Maybe (b, a)
f a
e of
                   Nothing     -> ([], a
e)
                   Just (x :: b
x,e1 :: a
e1) -> let (xs :: [b]
xs,e2 :: a
e2) = (a -> Maybe (b, a)) -> a -> ([b], a)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile a -> Maybe (b, a)
f a
e1
                                  in (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs,a
e2)

splitAbs :: Expr -> Maybe ((Name,Type), Expr)
splitAbs :: Expr -> Maybe ((Name, Prop), Expr)
splitAbs (EAbs x :: Name
x t :: Prop
t e :: Expr
e)         = ((Name, Prop), Expr) -> Maybe ((Name, Prop), Expr)
forall a. a -> Maybe a
Just ((Name
x,Prop
t), Expr
e)
splitAbs _                    = Maybe ((Name, Prop), Expr)
forall a. Maybe a
Nothing

splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs (ETAbs t :: TParam
t e :: Expr
e)         = (TParam, Expr) -> Maybe (TParam, Expr)
forall a. a -> Maybe a
Just (TParam
t, Expr
e)
splitTAbs _                   = Maybe (TParam, Expr)
forall a. Maybe a
Nothing

splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs (EProofAbs p :: Prop
p e :: Expr
e) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
p,Expr
e)
splitProofAbs _               = Maybe (Prop, Expr)
forall a. Maybe a
Nothing

splitTApp :: Expr -> Maybe (Type,Expr)
splitTApp :: Expr -> Maybe (Prop, Expr)
splitTApp (ETApp e :: Expr
e t :: Prop
t) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
t, Expr
e)
splitTApp _           = Maybe (Prop, Expr)
forall a. Maybe a
Nothing

splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp (EProofApp e :: Expr
e) = ((), Expr) -> Maybe ((), Expr)
forall a. a -> Maybe a
Just ((), Expr
e)
splitProofApp _ = Maybe ((), Expr)
forall a. Maybe a
Nothing

-- | Deconstruct an expression, typically polymorphic, into
-- the types and proofs to which it is applied.
-- Since we don't store the proofs, we just return
-- the number of proof applications.
-- The first type is the one closest to the expr.
splitExprInst :: Expr -> (Expr, [Type], Int)
splitExprInst :: Expr -> (Expr, [Prop], Int)
splitExprInst e :: Expr
e = (Expr
e2, [Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
ts, [()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
ps)
  where
  (ps :: [()]
ps,e1 :: Expr
e1) = (Expr -> Maybe ((), Expr)) -> Expr -> ([()], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((), Expr)
splitProofApp Expr
e
  (ts :: [Prop]
ts,e2 :: Expr
e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitTApp Expr
e1




instance PP Expr where
  ppPrec :: Int -> Expr -> Doc
ppPrec n :: Int
n t :: Expr
t = NameMap -> Int -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty Int
n Expr
t


instance PP (WithNames Match) where
  ppPrec :: Int -> WithNames Match -> Doc
ppPrec _ (WithNames mat :: Match
mat nm :: NameMap
nm) =
    case Match
mat of
      From x :: Name
x _ _ e :: Expr
e -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x Doc -> Doc -> Doc
<+> String -> Doc
text "<-" Doc -> Doc -> Doc
<+> NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e
      Let d :: Decl
d      -> String -> Doc
text "let" Doc -> Doc -> Doc
<+> NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Decl
d

instance PP Match where
  ppPrec :: Int -> Match -> Doc
ppPrec = NameMap -> Int -> Match -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

instance PP (WithNames DeclGroup) where
  ppPrec :: Int -> WithNames DeclGroup -> Doc
ppPrec _ (WithNames dg :: DeclGroup
dg nm :: NameMap
nm) =
    case DeclGroup
dg of
      Recursive ds :: [Decl]
ds    -> String -> Doc
text "/* Recursive */"
                      Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat ((Decl -> Doc) -> [Decl] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm) [Decl]
ds)
                      Doc -> Doc -> Doc
$$ String -> Doc
text ""
      NonRecursive d :: Decl
d  -> String -> Doc
text "/* Not recursive */"
                      Doc -> Doc -> Doc
$$ NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Decl
d
                      Doc -> Doc -> Doc
$$ String -> Doc
text ""

instance PP DeclGroup where
  ppPrec :: Int -> DeclGroup -> Doc
ppPrec = NameMap -> Int -> DeclGroup -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

instance PP (WithNames Decl) where
  ppPrec :: Int -> WithNames Decl -> Doc
ppPrec _ (WithNames Decl { .. } nm :: NameMap
nm) =
    Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> NameMap -> Schema -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Schema
dSignature  Doc -> Doc -> Doc
$$
    (if [Pragma] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pragma]
dPragmas
        then Doc
empty
        else String -> Doc
text "pragmas" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((Pragma -> Doc) -> [Pragma] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pragma -> Doc
forall a. PP a => a -> Doc
pp [Pragma]
dPragmas)
    ) Doc -> Doc -> Doc
$$
    Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> NameMap -> DeclDef -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm DeclDef
dDefinition

instance PP (WithNames DeclDef) where
  ppPrec :: Int -> WithNames DeclDef -> Doc
ppPrec _ (WithNames DPrim _)      = String -> Doc
text "<primitive>"
  ppPrec _ (WithNames (DExpr e :: Expr
e) nm :: NameMap
nm) = NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e

instance PP Decl where
  ppPrec :: Int -> Decl -> Doc
ppPrec = NameMap -> Int -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

instance PP Module where
  ppPrec :: Int -> Module -> Doc
ppPrec = NameMap -> Int -> Module -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty

instance PP (WithNames Module) where
  ppPrec :: Int -> WithNames Module -> Doc
ppPrec _ (WithNames Module { .. } nm :: NameMap
nm) =
    String -> Doc
text "module" Doc -> Doc -> Doc
<+> ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
mName Doc -> Doc -> Doc
$$
    -- XXX: Print exports?
    [Doc] -> Doc
vcat ((Import -> Doc) -> [Import] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Import -> Doc
forall a. PP a => a -> Doc
pp [Import]
mImports) Doc -> Doc -> Doc
$$
    -- XXX: Print tysyns
    -- XXX: Print abstarct types/functions
    [Doc] -> Doc
vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> DeclGroup -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames ([TParam] -> NameMap -> NameMap
addTNames [TParam]
mps NameMap
nm)) [DeclGroup]
mDecls)
    where mps :: [TParam]
mps = (ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems Map Name ModTParam
mParamTypes)