{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use tuple-section" #-}


module Embedder.Isabelle.Syntax where

import Data.Data ( Typeable, Data(..) )
import ReWire.Pretty
    ( (<+>), punctuate, vsep, brackets, comma, dquotes,
      parens, space, Doc, Pretty(..), text, empty, TextShow (..) )
import Data.List (intersperse)
import Data.Text as T (Text, pack, isPrefixOf, replicate, length, intercalate, unpack)
import qualified Prettyprinter as P
import Embedder.Builtins (Builtin (..), TyBuiltin (..), RWUserOp(..), rwu2s,
                        tb2s)

import Debug.Trace (trace)
import Data.Maybe (fromMaybe)

{- helpers -}

textS :: String -> Doc ann
textS :: forall ann. String -> Doc ann
textS = Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> (String -> Text) -> String -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack

bar :: [Doc ann] -> Doc ann
bar :: forall ann. [Doc ann] -> Doc ann
bar = Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
P.encloseSep (Doc ann
forall ann. Doc ann
space Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
space Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
space) Doc ann
forall a. Monoid a => a
mempty (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
" | ")

andS :: String
andS :: String
andS = String
"and"

($+$) :: Doc ann -> Doc ann -> Doc ann
Doc ann
a $+$ :: forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Doc ann
b = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.vcat [Doc ann
a, Doc ann
b]

tyAnn :: Doc ann -> Doc ann -> Doc ann
tyAnn :: forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn Doc ann
d Doc ann
t = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"::" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
t

printCon :: Text -> [Doc ann] -> Doc ann
printCon :: forall ann. Text -> [Doc ann] -> Doc ann
printCon Text
"->" [Doc ann
a,Doc ann
b] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<Rightarrow>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
b
printCon Text
"(,)" [Doc ann
a,Doc ann
b] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"," Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
b
printCon Text
"@" [] = Doc ann
"@"
printCon Text
"Tuple" [Doc ann]
ls = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma [Doc ann]
ls
printCon Text
"Nothing" [] = Doc ann
"None"
printCon Text
"Just" [Doc ann
a] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"Some" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
a
printCon Text
"Left" [Doc ann
a] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"inj\\<^sub>1" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
a
printCon Text
"Right" [Doc ann
a] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"inj\\<^sub>2" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
a
printCon Text
s [] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
s
printCon Text
s [Doc ann]
ls = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
s Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep [Doc ann]
ls

{- ------------------- Types ---------------------------------------- -}

-- TODO: refactor String ~> Text
-- TODO: Add type primitives? [prodS, sProdS, funS, cFunS, lFunS, sSumS]
-- TODO: Handle Modules?

-- | Names
type TName = Text

-- | Types
data Typ = Type { Typ -> Text
typeId :: TName,
                  Typ -> [Typ]
typeArgs :: [Typ] }
         | TBuiltin { Typ -> TyBuiltin
typeB :: TyBuiltin,
                      typeArgs :: [Typ] }
         | TNum { Typ -> Int
typeN :: Int }
         | TVar { typeId :: TName }
         deriving (Typ -> Typ -> Bool
(Typ -> Typ -> Bool) -> (Typ -> Typ -> Bool) -> Eq Typ
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Typ -> Typ -> Bool
== :: Typ -> Typ -> Bool
$c/= :: Typ -> Typ -> Bool
/= :: Typ -> Typ -> Bool
Eq, Eq Typ
Eq Typ =>
(Typ -> Typ -> Ordering)
-> (Typ -> Typ -> Bool)
-> (Typ -> Typ -> Bool)
-> (Typ -> Typ -> Bool)
-> (Typ -> Typ -> Bool)
-> (Typ -> Typ -> Typ)
-> (Typ -> Typ -> Typ)
-> Ord Typ
Typ -> Typ -> Bool
Typ -> Typ -> Ordering
Typ -> Typ -> Typ
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Typ -> Typ -> Ordering
compare :: Typ -> Typ -> Ordering
$c< :: Typ -> Typ -> Bool
< :: Typ -> Typ -> Bool
$c<= :: Typ -> Typ -> Bool
<= :: Typ -> Typ -> Bool
$c> :: Typ -> Typ -> Bool
> :: Typ -> Typ -> Bool
$c>= :: Typ -> Typ -> Bool
>= :: Typ -> Typ -> Bool
$cmax :: Typ -> Typ -> Typ
max :: Typ -> Typ -> Typ
$cmin :: Typ -> Typ -> Typ
min :: Typ -> Typ -> Typ
Ord, Int -> Typ -> ShowS
[Typ] -> ShowS
Typ -> String
(Int -> Typ -> ShowS)
-> (Typ -> String) -> ([Typ] -> ShowS) -> Show Typ
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Typ -> ShowS
showsPrec :: Int -> Typ -> ShowS
$cshow :: Typ -> String
show :: Typ -> String
$cshowList :: [Typ] -> ShowS
showList :: [Typ] -> ShowS
Show, Typeable, Typeable Typ
Typeable Typ =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Typ -> c Typ)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Typ)
-> (Typ -> Constr)
-> (Typ -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Typ))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ))
-> ((forall b. Data b => b -> b) -> Typ -> Typ)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r)
-> (forall u. (forall d. Data d => d -> u) -> Typ -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Typ -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Typ -> m Typ)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Typ -> m Typ)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Typ -> m Typ)
-> Data Typ
Typ -> Constr
Typ -> DataType
(forall b. Data b => b -> b) -> Typ -> Typ
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Typ -> u
forall u. (forall d. Data d => d -> u) -> Typ -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typ
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typ -> c Typ
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Typ)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typ -> c Typ
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Typ -> c Typ
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typ
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Typ
$ctoConstr :: Typ -> Constr
toConstr :: Typ -> Constr
$cdataTypeOf :: Typ -> DataType
dataTypeOf :: Typ -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Typ)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Typ)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ)
$cgmapT :: (forall b. Data b => b -> b) -> Typ -> Typ
gmapT :: (forall b. Data b => b -> b) -> Typ -> Typ
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Typ -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Typ -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Typ -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Typ -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Typ -> m Typ
Data)

data TypSig = TypSig {TypSig -> [Typ]
typSigArgs :: [Typ], TypSig -> Typ
typeSigCod :: Typ } deriving (TypSig -> TypSig -> Bool
(TypSig -> TypSig -> Bool)
-> (TypSig -> TypSig -> Bool) -> Eq TypSig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypSig -> TypSig -> Bool
== :: TypSig -> TypSig -> Bool
$c/= :: TypSig -> TypSig -> Bool
/= :: TypSig -> TypSig -> Bool
Eq, Eq TypSig
Eq TypSig =>
(TypSig -> TypSig -> Ordering)
-> (TypSig -> TypSig -> Bool)
-> (TypSig -> TypSig -> Bool)
-> (TypSig -> TypSig -> Bool)
-> (TypSig -> TypSig -> Bool)
-> (TypSig -> TypSig -> TypSig)
-> (TypSig -> TypSig -> TypSig)
-> Ord TypSig
TypSig -> TypSig -> Bool
TypSig -> TypSig -> Ordering
TypSig -> TypSig -> TypSig
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TypSig -> TypSig -> Ordering
compare :: TypSig -> TypSig -> Ordering
$c< :: TypSig -> TypSig -> Bool
< :: TypSig -> TypSig -> Bool
$c<= :: TypSig -> TypSig -> Bool
<= :: TypSig -> TypSig -> Bool
$c> :: TypSig -> TypSig -> Bool
> :: TypSig -> TypSig -> Bool
$c>= :: TypSig -> TypSig -> Bool
>= :: TypSig -> TypSig -> Bool
$cmax :: TypSig -> TypSig -> TypSig
max :: TypSig -> TypSig -> TypSig
$cmin :: TypSig -> TypSig -> TypSig
min :: TypSig -> TypSig -> TypSig
Ord, Int -> TypSig -> ShowS
[TypSig] -> ShowS
TypSig -> String
(Int -> TypSig -> ShowS)
-> (TypSig -> String) -> ([TypSig] -> ShowS) -> Show TypSig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypSig -> ShowS
showsPrec :: Int -> TypSig -> ShowS
$cshow :: TypSig -> String
show :: TypSig -> String
$cshowList :: [TypSig] -> ShowS
showList :: [TypSig] -> ShowS
Show, Typeable, Typeable TypSig
Typeable TypSig =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TypSig -> c TypSig)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TypSig)
-> (TypSig -> Constr)
-> (TypSig -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TypSig))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypSig))
-> ((forall b. Data b => b -> b) -> TypSig -> TypSig)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypSig -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypSig -> r)
-> (forall u. (forall d. Data d => d -> u) -> TypSig -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TypSig -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TypSig -> m TypSig)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypSig -> m TypSig)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TypSig -> m TypSig)
-> Data TypSig
TypSig -> Constr
TypSig -> DataType
(forall b. Data b => b -> b) -> TypSig -> TypSig
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TypSig -> u
forall u. (forall d. Data d => d -> u) -> TypSig -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypSig
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypSig -> c TypSig
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypSig)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypSig)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypSig -> c TypSig
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TypSig -> c TypSig
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypSig
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TypSig
$ctoConstr :: TypSig -> Constr
toConstr :: TypSig -> Constr
$cdataTypeOf :: TypSig -> DataType
dataTypeOf :: TypSig -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypSig)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TypSig)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypSig)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypSig)
$cgmapT :: (forall b. Data b => b -> b) -> TypSig -> TypSig
gmapT :: (forall b. Data b => b -> b) -> TypSig -> TypSig
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypSig -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TypSig -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TypSig -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypSig -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TypSig -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TypSig -> m TypSig
Data)

instance Pretty TypSig where
  pretty :: forall ann. TypSig -> Doc ann
pretty = TypSig -> Doc ann
forall ann. TypSig -> Doc ann
printTypSig

instance Pretty Typ where
  pretty :: forall ann. Typ -> Doc ann
pretty = Typ -> Doc ann
forall ann. Typ -> Doc ann
printType

tyAtomic :: Typ -> Bool
tyAtomic :: Typ -> Bool
tyAtomic = \ case
  Type Text
_ [] -> Bool
True
  Type Text
_ [Typ]
_ -> Bool
False
  TBuiltin TyBuiltin
_ [] -> Bool
True
  TBuiltin TyBuiltin
_ [Typ]
_ -> Bool
False
  TNum Int
_ -> Bool
True
  TVar Text
_ -> Bool
True

printType :: Typ -> Doc ann
printType :: forall ann. Typ -> Doc ann
printType Typ
t = case Typ
t of
  TVar Text
name -> Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ if Text -> Text -> Bool
isPrefixOf Text
"\'" Text
name Bool -> Bool -> Bool
|| Text -> Text -> Bool
isPrefixOf Text
"?\'" Text
name
                      then Text
name else Text
"\'" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
name
  TNum Int
nvar -> Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Int -> Text
forall a. TextShow a => a -> Text
showt Int
nvar
  TBuiltin TyBuiltin
b [Typ]
args -> TyBuiltin -> [Typ] -> Doc ann
forall ann. TyBuiltin -> [Typ] -> Doc ann
printTBuiltin TyBuiltin
b [Typ]
args
  Type Text
name [Typ]
args -> case Text
name of
    -- ReWire base types:
    Text
"()"   -> Doc ann
"unit"
    Text
"Bool" -> Doc ann
"bool"
    Text
"Maybe" -> case [Typ]
args of 
      [Typ
t1] -> Typ -> Doc ann
forall ann. Typ -> Doc ann
printType Typ
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"option"
      [Typ]
_ -> String -> Doc ann
forall a. HasCallStack => String -> a
error String
"printType: incorrect Maybe type"
    Text
"Either" -> case [Typ]
args of
      [Typ
t1,Typ
t2] -> Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<uplus>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
t2
      [Typ]
_ -> String -> Doc ann
forall a. HasCallStack => String -> a
error String
"printType: incorrect Either type"
    Text
"Vec" -> case [Typ]
args of
              (TNum Int
n:Type Text
"Bool" []:[Typ]
_) -> Text -> Doc ann
forall ann. Text -> Doc ann
text (Int -> Text
forall a. TextShow a => a -> Text
showt Int
n) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"word"
              (TNum Int
n:Typ
t:[Typ]
_) -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Text -> Doc ann
forall ann. Text -> Doc ann
text (Int -> Text
forall a. TextShow a => a -> Text
showt Int
n) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall ann. Typ -> Doc ann
printType Typ
t) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"cvec"
              [Typ]
_ -> String -> Doc ann
forall a. HasCallStack => String -> a
error String
"printType: incorrect Vec type"
    -- infix notations
    Text
"->" -> case [Typ]
args of
             [Typ
t1, Typ
t2] -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<Rightarrow>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall ann. Typ -> Doc ann
printType Typ
t2)
             [Typ]
_ -> String -> Doc ann
forall a. HasCallStack => String -> a
error String
"printType: incorrect arrow type"
    Text
nm | Text -> Bool
isTuple Text
nm -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
" \\<times>" ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Typ -> Doc ann) -> [Typ] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Doc ann
forall ann. Typ -> Doc ann
printType [Typ]
args
    -- standard isabelle `('a,'b) Type` notation
    Text
_ -> Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' Text
name [Typ]
args

printTyTuple :: [Typ] -> Doc ann
printTyTuple :: forall ann. [Typ] -> Doc ann
printTyTuple [] = Doc ann
forall a. Monoid a => a
mempty
printTyTuple (Typ
t:[Typ]
ts) = Typ -> Doc ann
forall ann. Typ -> Doc ann
printType Typ
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>  Doc ann
"\\<times>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Typ] -> Doc ann
forall ann. [Typ] -> Doc ann
printTyTuple [Typ]
ts)

pTyArg :: Typ -> Doc ann
pTyArg :: forall ann. Typ -> Doc ann
pTyArg Typ
t = if Typ -> Bool
tyAtomic Typ
t then
  Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t

printType' :: TName -> [Typ] -> Doc ann
printType' :: forall ann. Text -> [Typ] -> Doc ann
printType' Text
name [Typ]
args = case [Typ]
args of
           [] -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name
           [Typ
arg] -> let d :: Doc ann
d = Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
arg in
                      Doc ann
forall ann. Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name
           [Typ]
_ -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$
                       (Typ -> Doc ann) -> [Typ] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty [Typ]
args) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name

printTBuiltin :: TyBuiltin -> [Typ] -> Doc ann
printTBuiltin :: forall ann. TyBuiltin -> [Typ] -> Doc ann
printTBuiltin TyBuiltin
TyUnit [] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"unit"
printTBuiltin TyBuiltin
TyInteger [] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"int"
printTBuiltin TyBuiltin
TyString [] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"string"
printTBuiltin TyBuiltin
TyBool [] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"bool"
printTBuiltin TyBuiltin
TyFun [Typ
a,Typ
b] = Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"\\<Rightarrow>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
b
printTBuiltin TyBuiltin
TyReacT [Typ]
_ = String -> Doc ann -> Doc ann
forall a. String -> a -> a
trace String
"printTB: uneliminated monad transformer TyReacT" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"TyReacT"
printTBuiltin TyBuiltin
TyStateT [Typ]
_ = String -> Doc ann -> Doc ann
forall a. String -> a -> a
trace String
"printTB: uneliminated monad transformer TyStateT" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"TyStateT"
printTBuiltin TyBuiltin
TyIdentity [Typ]
_ = String -> Doc ann -> Doc ann
forall a. String -> a -> a
trace String
"printTB: uneliminated monad transformer Identity" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"TyIdentity"
printTBuiltin b :: TyBuiltin
b@TyBuiltin
TyState args :: [Typ]
args@[Typ
_,Typ
_] = Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' (TyBuiltin -> Text
tb2s TyBuiltin
b) [Typ]
args
printTBuiltin b :: TyBuiltin
b@TyBuiltin
TyRe args :: [Typ]
args@[Typ
_,Typ
_,Typ
_,Typ
_] = Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' (TyBuiltin -> Text
tb2s TyBuiltin
b) [Typ]
args
printTBuiltin b :: TyBuiltin
b@TyBuiltin
TyDev args :: [Typ]
args@[Typ
_,Typ
_] = Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' (TyBuiltin -> Text
tb2s TyBuiltin
b) [Typ]
args
printTBuiltin b :: TyBuiltin
b@TyBuiltin
TyStateDev args :: [Typ]
args@[Typ
_,Typ
_,Typ
_] = Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' (TyBuiltin -> Text
tb2s TyBuiltin
b) [Typ]
args
printTBuiltin TyBuiltin
TyProd [Typ
a,Typ
b] = Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"\\<times>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
b
printTBuiltin TyBuiltin
TyList [Typ
a] = Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"list"
printTBuiltin b :: TyBuiltin
b@TyBuiltin
TyVec args :: [Typ]
args@[Typ
_,Typ
_] = Text -> [Typ] -> Doc ann
forall ann. Text -> [Typ] -> Doc ann
printType' (TyBuiltin -> Text
tb2s TyBuiltin
b) [Typ]
args
printTBuiltin TyBuiltin
TyProxy [Typ
_] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"nat"
printTBuiltin TyBuiltin
TyFin [Typ
n] = Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"fin"
printTBuiltin TyBuiltin
TyPlus [Typ
a,Typ
b] = Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"+" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
b
printTBuiltin TyBuiltin
TyNeg [Typ
a] = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"-" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
a
printTBuiltin TyBuiltin
TyRef [Typ
a] = Typ -> Doc ann
forall ann. Typ -> Doc ann
pTyArg Typ
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"Ref"
printTBuiltin TyBuiltin
_ [Typ]
_ = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"??TyBuiltin??"

isTuple :: Text -> Bool
isTuple :: Text -> Bool
isTuple Text
c = Text
c Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text -> Text
T.replicate (Text -> Int
T.length Text
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) Text
"," Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

{-
instance Pretty Ty where
      pretty t = case flattenTyApp t of
            (TyCon _ (n2s -> c)     : ts)
                  | isTupleCtor c               -> parens $ hsep $ punctuate comma $ map pretty ts
            (TyCon _ (n2s -> "->")  : [t1, t2])
                  | needsParens t1              -> parens (pretty t1) <+> text "->" <+> pretty t2
            (TyCon _ (n2s -> "->")  : [t1, t2]) -> pretty t1 <+> text "->" <+> pretty t2
            (TyCon _ (n2s -> "[_]") : [t'])     -> brackets $ pretty t'
            [TyCon _ n]                         -> text $ n2s n
            [TyVar _ _ n]                       -> text $ showt n
            [TyNat _ n]                         -> text $ showt n
            ts                                  -> hsep $ map mparens ts
            where needsParens :: Ty -> Bool
                  needsParens t = case flattenTyApp t of
                        (TyCon _ (n2s -> "->") : _) -> True
                        _                           -> False

-}


printTypSig :: TypSig -> Doc ann
printTypSig :: forall ann. TypSig -> Doc ann
printTypSig (TypSig [Typ]
args Typ
cod) =  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
" \\<Rightarrow>" ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Typ -> Doc ann) -> [Typ] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Typ -> Doc ann
forall ann. Typ -> Doc ann
printType [Typ]
args [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Typ -> Doc ann
forall ann. Typ -> Doc ann
printType Typ
cod]


-- | Types for Terms
data DTyp = Hide { DTyp -> Typ
typ :: Typ }
          | Disp { typ :: Typ }
      deriving (DTyp -> DTyp -> Bool
(DTyp -> DTyp -> Bool) -> (DTyp -> DTyp -> Bool) -> Eq DTyp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DTyp -> DTyp -> Bool
== :: DTyp -> DTyp -> Bool
$c/= :: DTyp -> DTyp -> Bool
/= :: DTyp -> DTyp -> Bool
Eq, Eq DTyp
Eq DTyp =>
(DTyp -> DTyp -> Ordering)
-> (DTyp -> DTyp -> Bool)
-> (DTyp -> DTyp -> Bool)
-> (DTyp -> DTyp -> Bool)
-> (DTyp -> DTyp -> Bool)
-> (DTyp -> DTyp -> DTyp)
-> (DTyp -> DTyp -> DTyp)
-> Ord DTyp
DTyp -> DTyp -> Bool
DTyp -> DTyp -> Ordering
DTyp -> DTyp -> DTyp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DTyp -> DTyp -> Ordering
compare :: DTyp -> DTyp -> Ordering
$c< :: DTyp -> DTyp -> Bool
< :: DTyp -> DTyp -> Bool
$c<= :: DTyp -> DTyp -> Bool
<= :: DTyp -> DTyp -> Bool
$c> :: DTyp -> DTyp -> Bool
> :: DTyp -> DTyp -> Bool
$c>= :: DTyp -> DTyp -> Bool
>= :: DTyp -> DTyp -> Bool
$cmax :: DTyp -> DTyp -> DTyp
max :: DTyp -> DTyp -> DTyp
$cmin :: DTyp -> DTyp -> DTyp
min :: DTyp -> DTyp -> DTyp
Ord, Int -> DTyp -> ShowS
[DTyp] -> ShowS
DTyp -> String
(Int -> DTyp -> ShowS)
-> (DTyp -> String) -> ([DTyp] -> ShowS) -> Show DTyp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DTyp -> ShowS
showsPrec :: Int -> DTyp -> ShowS
$cshow :: DTyp -> String
show :: DTyp -> String
$cshowList :: [DTyp] -> ShowS
showList :: [DTyp] -> ShowS
Show, Typeable, Typeable DTyp
Typeable DTyp =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DTyp -> c DTyp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DTyp)
-> (DTyp -> Constr)
-> (DTyp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DTyp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp))
-> ((forall b. Data b => b -> b) -> DTyp -> DTyp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r)
-> (forall u. (forall d. Data d => d -> u) -> DTyp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> DTyp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DTyp -> m DTyp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DTyp -> m DTyp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DTyp -> m DTyp)
-> Data DTyp
DTyp -> Constr
DTyp -> DataType
(forall b. Data b => b -> b) -> DTyp -> DTyp
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DTyp -> u
forall u. (forall d. Data d => d -> u) -> DTyp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DTyp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DTyp -> c DTyp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DTyp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DTyp -> c DTyp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DTyp -> c DTyp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DTyp
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DTyp
$ctoConstr :: DTyp -> Constr
toConstr :: DTyp -> Constr
$cdataTypeOf :: DTyp -> DataType
dataTypeOf :: DTyp -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DTyp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DTyp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DTyp)
$cgmapT :: (forall b. Data b => b -> b) -> DTyp -> DTyp
gmapT :: (forall b. Data b => b -> b) -> DTyp -> DTyp
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DTyp -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DTyp -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DTyp -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DTyp -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DTyp -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DTyp -> m DTyp
Data)



{- ------------------- Expressions ---------------------------------- -}

-- | Names
type VName = Text

-- | Names with Qualifiers
data QName = QName
    { QName -> Text
qname :: Text
    , QName -> [Text]
qualifiers :: [Text] }
  deriving (QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
/= :: QName -> QName -> Bool
Eq, Eq QName
Eq QName =>
(QName -> QName -> Ordering)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> QName)
-> (QName -> QName -> QName)
-> Ord QName
QName -> QName -> Bool
QName -> QName -> Ordering
QName -> QName -> QName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: QName -> QName -> Ordering
compare :: QName -> QName -> Ordering
$c< :: QName -> QName -> Bool
< :: QName -> QName -> Bool
$c<= :: QName -> QName -> Bool
<= :: QName -> QName -> Bool
$c> :: QName -> QName -> Bool
> :: QName -> QName -> Bool
$c>= :: QName -> QName -> Bool
>= :: QName -> QName -> Bool
$cmax :: QName -> QName -> QName
max :: QName -> QName -> QName
$cmin :: QName -> QName -> QName
min :: QName -> QName -> QName
Ord, Typeable, Typeable QName
Typeable QName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QName -> c QName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QName)
-> (QName -> Constr)
-> (QName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName))
-> ((forall b. Data b => b -> b) -> QName -> QName)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r)
-> (forall u. (forall d. Data d => d -> u) -> QName -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> QName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> Data QName
QName -> Constr
QName -> DataType
(forall b. Data b => b -> b) -> QName -> QName
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QName -> u
forall u. (forall d. Data d => d -> u) -> QName -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName -> m QName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
$ctoConstr :: QName -> Constr
toConstr :: QName -> Constr
$cdataTypeOf :: QName -> DataType
dataTypeOf :: QName -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QName)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
$cgmapT :: (forall b. Data b => b -> b) -> QName -> QName
gmapT :: (forall b. Data b => b -> b) -> QName -> QName
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QName -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QName -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QName -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QName -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName -> m QName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
Data)

instance Show QName where
    show :: QName -> String
show QName
q = Text -> String
unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> Text
intercalate Text
"." ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ QName -> [Text]
qualifiers QName
q [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [QName -> Text
qname QName
q]


data Term =
        LitString Text
      | LitNum Integer
      | LitWord Int Integer
      | LitVec [Term]
      | Free { Term -> Text
termName :: VName }
      | Prim { Term -> RWUserOp
primId :: RWUserOp }
      -- | lambda abstraction
      | Abs { Term -> [Text]
absVars :: [VName],
                Term -> Term
termId :: Term }
      -- | application
      | App { Term -> Term
funId :: Term,
               Term -> [Term]
argIds :: [Term] }
      | If { Term -> Term
ifId :: Term,
             Term -> Term
thenId :: Term,
             Term -> Term
elseId :: Term }
      | Case { termId :: Term,
               Term -> [(Pttrn, Term)]
caseSubst :: [(Pttrn, Term)] }
      | Let { Term -> [(Pttrn, Term)]
letSubst :: [(Pttrn, Term)],
              Term -> Term
inId :: Term }
      | IsaEq { Term -> Term
firstTerm :: Term,
                Term -> Term
secondTerm :: Term }
      | Tuplex [Term]
      | List   [Term]
      | RecordVal [(Text, Term)]
      | RecordUpdate Term [(Text, Term)]
      | RecordSel Text Term
      | TypAnnTerm { termId :: Term, 
                     Term -> Typ
typAnn :: Typ}
      deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Term -> Term -> Ordering
compare :: Term -> Term -> Ordering
$c< :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
>= :: Term -> Term -> Bool
$cmax :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
min :: Term -> Term -> Term
Ord, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Term -> ShowS
showsPrec :: Int -> Term -> ShowS
$cshow :: Term -> String
show :: Term -> String
$cshowList :: [Term] -> ShowS
showList :: [Term] -> ShowS
Show, Typeable, Typeable Term
Typeable Term =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Term -> c Term)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Term)
-> (Term -> Constr)
-> (Term -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Term))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term))
-> ((forall b. Data b => b -> b) -> Term -> Term)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r)
-> (forall u. (forall d. Data d => d -> u) -> Term -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Term -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Term -> m Term)
-> Data Term
Term -> Constr
Term -> DataType
(forall b. Data b => b -> b) -> Term -> Term
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
forall u. (forall d. Data d => d -> u) -> Term -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term -> c Term
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Term
$ctoConstr :: Term -> Constr
toConstr :: Term -> Constr
$cdataTypeOf :: Term -> DataType
dataTypeOf :: Term -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Term)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)
$cgmapT :: (forall b. Data b => b -> b) -> Term -> Term
gmapT :: (forall b. Data b => b -> b) -> Term -> Term
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Term -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Term -> m Term
Data)

atomic :: Term -> Bool
atomic :: Term -> Bool
atomic = \ case
       LitString Text
_ -> Bool
True
       LitNum Integer
_    -> Bool
True
       LitWord Int
_ Integer
_ -> Bool
True
       LitVec [Term]
_    -> Bool
True
       Free Text
_      -> Bool
True
       Prim RWUserOp
_      -> Bool
True
       Abs [Text]
_ Term
e     -> Term -> Bool
atomic Term
e
       App Term
_ [Term]
_     -> Bool
False
       If {}       -> Bool
False
       Case Term
_ [(Pttrn, Term)]
_    -> Bool
False
       Let [(Pttrn, Term)]
bs Term
e    -> Term -> Bool
atomic Term
e Bool -> Bool -> Bool
&& ((Pttrn, Term) -> Bool) -> [(Pttrn, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term -> Bool
atomic (Term -> Bool) -> ((Pttrn, Term) -> Term) -> (Pttrn, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pttrn, Term) -> Term
forall a b. (a, b) -> b
snd) [(Pttrn, Term)]
bs
       IsaEq Term
_ Term
_   -> Bool
False
       Tuplex [Term]
es   -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
atomic [Term]
es
       List [Term]
es     -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
atomic [Term]
es
       TypAnnTerm Term
e Typ
_ -> Term -> Bool
atomic Term
e
       RecordVal [(Text, Term)]
fields -> [(Text, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length [(Text, Term)]
fields Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
4 Bool -> Bool -> Bool
&& ((Text, Term) -> Bool) -> [(Text, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term -> Bool
atomic (Term -> Bool) -> ((Text, Term) -> Term) -> (Text, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Term) -> Term
forall a b. (a, b) -> b
snd) [(Text, Term)]
fields 
       RecordUpdate {} -> Bool
True
       RecordSel {} -> Bool
True


selfGroup :: Term -> Bool
selfGroup :: Term -> Bool
selfGroup = \ case
       LitString Text
_ -> Bool
True
       LitNum Integer
_    -> Bool
True
       LitWord Int
_ Integer
_ -> Bool
True
       LitVec [Term]
_    -> Bool
True
       Free Text
_      -> Bool
True
       Prim RWUserOp
_      -> Bool
True
       Abs {}      -> Bool
False
       App Term
_ [Term]
_     -> Bool
False
       If {}       -> Bool
True
       Case Term
_ [(Pttrn, Term)]
_    -> Bool
True
       Let {}      -> Bool
True
       IsaEq Term
_ Term
_   -> Bool
False
       Tuplex [Term]
_    -> Bool
True
       List [Term]
_      -> Bool
True
       RecordVal {}     -> Bool
True
       RecordUpdate {}  -> Bool
True
       RecordSel {}     -> Bool
False
       TypAnnTerm {} -> Bool
True


--              | Put | Get
--              | Add | Sub | Mul | Div | Mod | Pow
--              | Eq | Gt | GtEq | Lt | LtEq
----------------------------------------------
--                Error | Extern
--              | Bind | Return
--              | Signal | Lift | Extrude
--              | VecFromList | VecReplicate | VecReverse | VecSlice | VecRSlice
--              | VecIndex | VecIndexProxy
--              | VecConcat
--              | VecMap | VecGenerate
--              | Finite | FiniteMinBound | FiniteMaxBound | ToFinite | ToFiniteMod | FromFinite
--              | NatVal
--              | Bits | Resize | BitSlice | BitIndex
--              | LAnd | LOr
--              | And | Or
--              | XOr | XNor
--              | LShift | RShift | RShiftArith
--              | LNot | Not
--              | RAnd | RNAnd | ROr | RNor | RXOr | RXNor
--              | MSBit

pArg :: Term -> Doc ann
pArg :: forall ann. Term -> Doc ann
pArg Term
a = if Term -> Bool
selfGroup Term
a then Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
a else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
a)

infixBuiltinList :: [Builtin]
infixBuiltinList :: [Builtin]
infixBuiltinList = [
  Builtin
Add, Builtin
Sub, Builtin
Mul, Builtin
Pow, Builtin
Div, Builtin
Mod,
  Builtin
Eq, Builtin
Gt, Builtin
GtEq, Builtin
Lt, Builtin
LtEq,
  Builtin
Bind,
  Builtin
VecIndex, Builtin
VecIndexProxy, Builtin
VecConcat,
  Builtin
LAnd, Builtin
LOr,
  Builtin
And, Builtin
Or, Builtin
XOr, Builtin
XNor,
  Builtin
LShift, Builtin
RShift, Builtin
RShiftArith
  ]

infixRWUserOpList :: [RWUserOp]
infixRWUserOpList :: [RWUserOp]
infixRWUserOpList = [
  RWUserOp
CompDot,
  RWUserOp
NEq,
  RWUserOp
BAnd, RWUserOp
BOr, RWUserOp
BXOr,
  RWUserOp
BindI, RWUserOp
BindS, RWUserOp
BindR, RWUserOp
BindRInf,
  RWUserOp
Seq, RWUserOp
SeqI, RWUserOp
SeqS, RWUserOp
SeqR, RWUserOp
SeqRInf,
  RWUserOp
RBindI, RWUserOp
RBindS, RWUserOp
RBindR, RWUserOp
RBindRInf,
  RWUserOp
FinAdd, RWUserOp
FinSub, RWUserOp
FinMul, RWUserOp
FinDiv, RWUserOp
FinEq, RWUserOp
FinLt,
  RWUserOp
WordSlice, RWUserOp
WordIndex, RWUserOp
WordIndexProxy, RWUserOp
WordIndexFin
  ]

prefixBuiltinList :: [Builtin]
prefixBuiltinList :: [Builtin]
prefixBuiltinList = [Builtin
Not]

prefixRWUserOpList :: [RWUserOp]
prefixRWUserOpList :: [RWUserOp]
prefixRWUserOpList = []

isInfix :: RWUserOp -> Bool
isInfix :: RWUserOp -> Bool
isInfix (RWBuiltin Builtin
b) = Builtin
b Builtin -> [Builtin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Builtin]
infixBuiltinList
isInfix RWUserOp
op = RWUserOp
op RWUserOp -> [RWUserOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RWUserOp]
infixRWUserOpList

isPrefix :: RWUserOp -> Bool
isPrefix :: RWUserOp -> Bool
isPrefix (RWBuiltin Builtin
b) = Builtin
b Builtin -> [Builtin] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Builtin]
prefixBuiltinList
isPrefix RWUserOp
op = RWUserOp
op RWUserOp -> [RWUserOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RWUserOp]
prefixRWUserOpList

textListRWOp :: [(RWUserOp,Text)]
textListRWOp :: [(RWUserOp, Text)]
textListRWOp = [
  (Builtin -> RWUserOp
RWBuiltin Builtin
Add, Text
"+"), (Builtin -> RWUserOp
RWBuiltin Builtin
Sub, Text
"-"), (Builtin -> RWUserOp
RWBuiltin Builtin
Mul, Text
"*"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
Pow, Text
"**"), (Builtin -> RWUserOp
RWBuiltin Builtin
Div, Text
"div"), (Builtin -> RWUserOp
RWBuiltin Builtin
Mod, Text
"mod"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
Gt, Text
">"), (Builtin -> RWUserOp
RWBuiltin Builtin
GtEq, Text
">="), (Builtin -> RWUserOp
RWBuiltin Builtin
Lt, Text
"<"), (Builtin -> RWUserOp
RWBuiltin Builtin
LtEq, Text
"<="),
  (Builtin -> RWUserOp
RWBuiltin Builtin
Bind, Text
"\\<bind>"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
VecIndex, Text
"!vf"), (Builtin -> RWUserOp
RWBuiltin Builtin
VecIndexProxy, Text
"!v"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
VecConcat, Text
"++"), (Builtin -> RWUserOp
RWBuiltin Builtin
VecSlice, Text
"slice"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
VecRSlice, Text
"rslice"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
VecGenerate, Text
"generate"), (Builtin -> RWUserOp
RWBuiltin Builtin
VecMap, Text
"map"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
VecReplicate, Text
"replicate"), (Builtin -> RWUserOp
RWBuiltin Builtin
VecReverse, Text
"reverse"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
LAnd, Text
"\\<and>w"), (Builtin -> RWUserOp
RWBuiltin Builtin
LOr, Text
"\\<or>w"), (Builtin -> RWUserOp
RWBuiltin Builtin
LNot, Text
"\\<not>w"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
And, Text
"&&"), (Builtin -> RWUserOp
RWBuiltin Builtin
Or, Text
"||"), (Builtin -> RWUserOp
RWBuiltin Builtin
Not, Text
"~~"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
XOr, Text
"xor"), (Builtin -> RWUserOp
RWBuiltin Builtin
XNor, Text
"~xor"),
  (Builtin -> RWUserOp
RWBuiltin Builtin
LShift, Text
"<<"), (Builtin -> RWUserOp
RWBuiltin Builtin
RShift, Text
">>"), (Builtin -> RWUserOp
RWBuiltin Builtin
RShiftArith, Text
">>>"),
  (RWUserOp
CompDot, Text
"o"),
  (RWUserOp
BXOr, Text
"x\\<or>"),
  (RWUserOp
RBindI, Text
"=<<I"), (RWUserOp
RBindS, Text
"=<<S"), (RWUserOp
RBindR, Text
"=<<R"), (RWUserOp
RBindRInf, Text
"=<<<R"),
  (RWUserOp
BindI, Text
"\\<bind>I"), (RWUserOp
BindS, Text
"\\<bind>S"), (RWUserOp
BindR, Text
"\\<bind>R"), (RWUserOp
BindRInf, Text
">>>=R"),
  (RWUserOp
Seq, Text
"\\<then>"), (RWUserOp
SeqI, Text
"\\<then>I"), (RWUserOp
SeqS, Text
"\\<then>S"), (RWUserOp
SeqR, Text
"\\<then>R"), (RWUserOp
SeqRInf, Text
">>>R"),
  (RWUserOp
FinAdd, Text
"+%"), (RWUserOp
FinSub, Text
"-%"), (RWUserOp
FinMul, Text
"*%"), (RWUserOp
FinDiv, Text
"div%"),
  (RWUserOp
FinEq, Text
"="), (RWUserOp
FinLt, Text
"<"),
  (RWUserOp
WordIndex, Text
"@!"), (RWUserOp
WordSlice, Text
"@@"),
  (RWUserOp
VecLastIndexProxy, Text
"lastIndexNat"),
  (RWUserOp
WordIndexProxy,Text
"!w"), (RWUserOp
WordIndexFin,Text
"!wf"),
  (RWUserOp
NEq, Text
"\\<noteq>"),
  (RWUserOp
Update, Text
"update")
  ]

{-
      (VecEmpty  , "empty"), (VecSingleton, "singleton"),
      (VecCons   , "cons"),  (VecSnoc     , "snoc"),
      (VecHead   , "head"),  (VecLastIndex, "lastIndex"),
      (VecLastIndexProxy, "lastIndex'"), (VecTake, "take"),
      (VecDrop   , "drop"),  (VecInit     , "init"),
      (VecTail   , "tail"),  (VecZipWith  , "zipWith"),
      (VecZipWith3, "zipWith3"), (VecPackLo, "packlo"),
      (VecPackHi , "packhi"), (VecUnpackLo, "unpacklo"),
      (VecUnpackHi, "unpackhi")]
-}


-- TODO: Need to handle vector-concat and word-concat separately
-- TODO: Similarly: liftS and liftR, bindS and bindR,
printApp :: Term -> [Term] -> Doc ann
-- handles operators with special formatting/parens
printApp :: forall ann. Term -> [Term] -> Doc ann
printApp (Prim (RWBuiltin Builtin
Eq)) [Term
a,Term
b] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
b
printApp (Prim RWUserOp
BAnd) (Term
a:[Term]
as) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<and>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
as)
printApp (Prim RWUserOp
BOr) (Term
a:[Term]
as) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<or>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
as)
printApp (Prim RWUserOp
CompDol) (Term
a:[Term]
bs) = Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty [Term]
bs)))
printApp (Prim (RWBuiltin Builtin
Bind)) (Term
a:[Term]
bs) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"\\<bind>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
bs)
-- handle standard operator forms (infix or not) uniformly
printApp (Prim RWUserOp
op) [Term]
args = RWUserOp -> [Term] -> Doc ann
forall ann. RWUserOp -> [Term] -> Doc ann
pOp RWUserOp
op [Term]
args
printApp (Free Text
"not") [Term
a] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"\\<not>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a
printApp (Free Text
"not") [] = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
"\\<lambda> x. \\<not> x"
printApp (Free Text
"Nothing") [] = Doc ann
"None"
printApp (Free Text
"Just") [Term
a] = Doc ann
"Some" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a
printApp (Free Text
"Left") [Term
a] = Doc ann
"inj\\<^sub>1" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a
printApp (Free Text
"Right") [Term
a] = Doc ann
"inj\\<^sub>2" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
a
printApp (Free Text
op) [Term]
args | Text -> Bool
isTuple Text
op = [Term] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
printTuple [Term]
args
printApp (Free Text
op) [Term]
args = Term -> [Term] -> Doc ann
forall ann. Term -> [Term] -> Doc ann
printApp' (Text -> Term
Free Text
op) [Term]
args
printApp Term
e [Term]
args = Term -> [Term] -> Doc ann
forall ann. Term -> [Term] -> Doc ann
printApp' Term
e [Term]
args


rwOpText :: RWUserOp -> Text
rwOpText :: RWUserOp -> Text
rwOpText RWUserOp
op = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe (Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
forall {a}. a
err (RWUserOp -> Maybe Text
rwu2s RWUserOp
op)) (RWUserOp -> [(RWUserOp, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup RWUserOp
op [(RWUserOp, Text)]
textListRWOp)
      where err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"rwOpText: no Isabelle notation for op: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RWUserOp -> String
forall a. Show a => a -> String
show RWUserOp
op

pOp :: RWUserOp -> [Term] -> Doc ann
pOp :: forall ann. RWUserOp -> [Term] -> Doc ann
pOp RWUserOp
op args :: [Term]
args@(Term
arg:[Term]
args') | RWUserOp -> Bool
isInfix RWUserOp
op = case [Term]
args' of
  [] -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.group (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op)) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
arg
  (Term
_:[Term]
_) -> if (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
atomic [Term]
args
           then Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.group (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
arg Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
args')
           else Term -> Doc ann
forall ann. Term -> Doc ann
pArg Term
arg Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
args'))
pOp RWUserOp
op args :: [Term]
args@(Term
_:[Term]
_) = if (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
atomic [Term]
args
  then Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.group (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
args)
  else Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
args))
pOp RWUserOp
op [] | RWUserOp -> Bool
isPrefix RWUserOp
op = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text
"\\<lambda> x. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RWUserOp -> Text
rwOpText RWUserOp
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" x"
pOp RWUserOp
op [] = Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
op)


printApp' :: Term -> [Term] ->  Doc ann
printApp' :: forall ann. Term -> [Term] -> Doc ann
printApp' Term
e [Term]
args = if (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
atomic [Term]
args
                  then Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.group (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg (Term
e Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args))
                  else Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall ann. Term -> Doc ann
pArg [Term]
args))

printTuple :: Pretty a => [a] -> Doc ann
printTuple :: forall a ann. Pretty a => [a] -> Doc ann
printTuple [a]
es =  Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ((a -> Doc ann) -> [a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [a]
es)

instance Pretty Term where
  pretty :: forall ann. Term -> Doc ann
pretty = Term -> Doc ann
forall ann. Term -> Doc ann
prettyTerm



      -- -- Additional notation: Bit=Bool, W n=Vec n Bit, extern, modify, length, len, fromList
      -- -- Additional notation: iter, iterSt
      -- -- Additional notation: id, const, (.), flip, ($), (&&), (||), not, otherwise, maybe, either, fst, snd, curry, uncurry, undefined, (=<<), (>>)
      -- Additional notation: empty, singleton, cons, snoc, head, lastIndex, lastIndex', take, drop, init, tail, zipWith, zipWith3, packlo, packhi, unpacklo, unpackhi, (!=) ; update
      --  -- Additional notation: ReWire.FiniteComp: +, -, *, div, ==, <, even, odd
      -- Additional notation: ReWire.Bits: zero, one, bit, lit, `xor`, (@@) ; bitSlice, (@.) ; bitIndex, rotR, rotL, (/=), even, odd, Lit=W128
      -- 


      -- | Primitives
      -- -- Defined Types/Data structs: Monad, MonadTrans, Ref a=Ref String, Proxy (n::Nat)=Proxy
      -- -- Imported Types/Data structs: type(+),type(Nat),Identity, ReacT, StateT, Integer, String, Bool, Vec=Vector, KnownNat, Finite
      -- | Prelude
      -- -- Data structures: Maybe a = Nothing | Just a, Either a b = Left a | Right b, Bool = True | False
      -- | Vectors
      -- -- Missing prims: VecUpdate, VecBulkUpdate, VecIterate, VecZip, VecFromList
      -- | Bits
      -- -- Missing prims: ToInteger,
      -- -- Not translated (directly): Bits, 
      -- ]


prettyTerm :: Term -> Doc ann
prettyTerm :: forall ann. Term -> Doc ann
prettyTerm = \ case
     Free Text
"not" -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
"\\<lambda> x. \\<not> x"
     Free Text
"Nothing" -> Doc ann
"None"
     Free Text
v -> -- trace ("print Free: " <> unpack v) $ 
                Text -> Doc ann
forall ann. Text -> Doc ann
text Text
v
     App Term
e [Term]
args -> --trace ("print App: " <> show e  <> " " <> show args) $ 
                   Term -> [Term] -> Doc ann
forall ann. Term -> [Term] -> Doc ann
printApp Term
e [Term]
args
     Tuplex [Term]
es -> [Term] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
printTuple [Term]
es
     List [Term]
es -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty [Term]
es)
     LitString Text
txt -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.squotes (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.squotes (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
txt
     LitNum Integer
i -> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i
     LitWord Int
n Integer
i -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"w." Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i
     Abs [Text]
vs Term
e -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"\\<lambda>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Text -> Doc ann) -> [Text] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty [Text]
vs) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
e
     If Term
t Term
c Term
a  -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep [Doc ann
"if" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
t,
                                                Doc ann
"then" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
c,
                                                Doc ann
"else" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
a]
     Prim RWUserOp
b | RWUserOp -> Bool
isInfix RWUserOp
b -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ RWUserOp -> Text
rwOpText RWUserOp
b
     Prim RWUserOp
b | RWUserOp -> Bool
isPrefix RWUserOp
b -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text
"\\<lambda> x. " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RWUserOp -> Text
rwOpText RWUserOp
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" x"
     Prim RWUserOp
b -> Text -> Doc ann
forall ann. Text -> Doc ann
text (RWUserOp -> Text
rwOpText RWUserOp
b)
     Case Term
e [(Pttrn, Term)]
ps -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"case" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"of"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
bar ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ ((Pttrn, Term) -> Doc ann) -> [(Pttrn, Term)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Pttrn
p, Term
t) ->
               [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep [ Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty Pttrn
p Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"\\<Rightarrow>"
                    , Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
t]) [(Pttrn, Term)]
ps)
     TypAnnTerm Term
_e (TBuiltin TyBuiltin
TyProxy [TNum Int
n]) -> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n
     TypAnnTerm Term
e Typ
t -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
e) (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
                -- TODO: Could use conditional 'width' to align cases
     LitVec [Term]
_es -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"LitVec" -- something like 3w.[ a, b, c ]
     Let [(Pttrn, Term)]
_bs Term
_e -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"Let" -- not needed yet
     IsaEq Term
_e1 Term
_e2 -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"IsaEq" -- not needed yet
     RecordVal [(Text, Term)]
fields -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"(|" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma (((Text, Term) -> Doc ann) -> [(Text, Term)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Term) -> Doc ann
forall {a} {ann}. Pretty a => (Text, a) -> Doc ann
ppField [(Text, Term)]
fields)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"|)"
          where
          ppField :: (Text, a) -> Doc ann
ppField (Text
f, a
t) = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t

     RecordUpdate Term
rec [(Text, Term)]
fields -> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
rec Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"(|" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma (((Text, Term) -> Doc ann) -> [(Text, Term)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Term) -> Doc ann
forall {a} {ann}. Pretty a => (Text, a) -> Doc ann
ppUpd [(Text, Term)]
fields)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"|)"
          where
          ppUpd :: (Text, a) -> Doc ann
ppUpd (Text
f, a
t) = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
t

     RecordSel Text
f Term
t -> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
t Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"." Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f



{- ------------------- Patterns --------------------------------------- -}

data Pttrn = PttrnWildCard (Maybe Typ)
           | PttrnVar VName (Maybe Typ)
           | PttrnCon VName (Maybe Typ) [Pttrn]
           | PttrnTuple (Maybe Typ) [Pttrn]
           | PttrnAs (Maybe Typ) Pttrn VName
           | PttrnRecord (Maybe Typ) [(Text, Pttrn)]
        deriving (Pttrn -> Pttrn -> Bool
(Pttrn -> Pttrn -> Bool) -> (Pttrn -> Pttrn -> Bool) -> Eq Pttrn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pttrn -> Pttrn -> Bool
== :: Pttrn -> Pttrn -> Bool
$c/= :: Pttrn -> Pttrn -> Bool
/= :: Pttrn -> Pttrn -> Bool
Eq, Eq Pttrn
Eq Pttrn =>
(Pttrn -> Pttrn -> Ordering)
-> (Pttrn -> Pttrn -> Bool)
-> (Pttrn -> Pttrn -> Bool)
-> (Pttrn -> Pttrn -> Bool)
-> (Pttrn -> Pttrn -> Bool)
-> (Pttrn -> Pttrn -> Pttrn)
-> (Pttrn -> Pttrn -> Pttrn)
-> Ord Pttrn
Pttrn -> Pttrn -> Bool
Pttrn -> Pttrn -> Ordering
Pttrn -> Pttrn -> Pttrn
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Pttrn -> Pttrn -> Ordering
compare :: Pttrn -> Pttrn -> Ordering
$c< :: Pttrn -> Pttrn -> Bool
< :: Pttrn -> Pttrn -> Bool
$c<= :: Pttrn -> Pttrn -> Bool
<= :: Pttrn -> Pttrn -> Bool
$c> :: Pttrn -> Pttrn -> Bool
> :: Pttrn -> Pttrn -> Bool
$c>= :: Pttrn -> Pttrn -> Bool
>= :: Pttrn -> Pttrn -> Bool
$cmax :: Pttrn -> Pttrn -> Pttrn
max :: Pttrn -> Pttrn -> Pttrn
$cmin :: Pttrn -> Pttrn -> Pttrn
min :: Pttrn -> Pttrn -> Pttrn
Ord, Int -> Pttrn -> ShowS
[Pttrn] -> ShowS
Pttrn -> String
(Int -> Pttrn -> ShowS)
-> (Pttrn -> String) -> ([Pttrn] -> ShowS) -> Show Pttrn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pttrn -> ShowS
showsPrec :: Int -> Pttrn -> ShowS
$cshow :: Pttrn -> String
show :: Pttrn -> String
$cshowList :: [Pttrn] -> ShowS
showList :: [Pttrn] -> ShowS
Show, Typeable, Typeable Pttrn
Typeable Pttrn =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Pttrn -> c Pttrn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Pttrn)
-> (Pttrn -> Constr)
-> (Pttrn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Pttrn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pttrn))
-> ((forall b. Data b => b -> b) -> Pttrn -> Pttrn)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r)
-> (forall u. (forall d. Data d => d -> u) -> Pttrn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Pttrn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Pttrn -> m Pttrn)
-> Data Pttrn
Pttrn -> Constr
Pttrn -> DataType
(forall b. Data b => b -> b) -> Pttrn -> Pttrn
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Pttrn -> u
forall u. (forall d. Data d => d -> u) -> Pttrn -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pttrn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pttrn -> c Pttrn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pttrn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pttrn)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pttrn -> c Pttrn
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pttrn -> c Pttrn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pttrn
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pttrn
$ctoConstr :: Pttrn -> Constr
toConstr :: Pttrn -> Constr
$cdataTypeOf :: Pttrn -> DataType
dataTypeOf :: Pttrn -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pttrn)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pttrn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pttrn)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pttrn)
$cgmapT :: (forall b. Data b => b -> b) -> Pttrn -> Pttrn
gmapT :: (forall b. Data b => b -> b) -> Pttrn -> Pttrn
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pttrn -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Pttrn -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Pttrn -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pttrn -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pttrn -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pttrn -> m Pttrn
Data)

instance Pretty Pttrn where
  pretty :: forall ann. Pttrn -> Doc ann
pretty = \ case
    PttrnWildCard Maybe Typ
Nothing -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"_"
    PttrnWildCard (Just Typ
t) -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"_") (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
    PttrnVar Text
name Maybe Typ
Nothing -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name
    PttrnVar Text
name (Just Typ
t) -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name) (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
    PttrnCon Text
name Maybe Typ
Nothing [Pttrn]
ps -> Text -> [Doc ann] -> Doc ann
forall ann. Text -> [Doc ann] -> Doc ann
printCon Text
name ((Pttrn -> Doc ann) -> [Pttrn] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty [Pttrn]
ps)
    PttrnCon Text
name (Just Typ
t) [Pttrn]
ps -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Text -> [Doc ann] -> Doc ann
forall ann. Text -> [Doc ann] -> Doc ann
printCon Text
name ((Pttrn -> Doc ann) -> [Pttrn] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty [Pttrn]
ps)) (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
    PttrnTuple Maybe Typ
Nothing [Pttrn]
ps -> [Pttrn] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
printTuple [Pttrn]
ps
    PttrnTuple (Just Typ
t) [Pttrn]
ps -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn ([Pttrn] -> Doc ann
forall a ann. Pretty a => [a] -> Doc ann
printTuple [Pttrn]
ps) (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
    PttrnAs Maybe Typ
Nothing Pttrn
p Text
n -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty Pttrn
p Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
n
    PttrnAs (Just Typ
t) Pttrn
p Text
n -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty Pttrn
p Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
n)) (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
    PttrnRecord Maybe Typ
Nothing [(Text, Pttrn)]
fields -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"(|" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma (((Text, Pttrn) -> Doc ann) -> [(Text, Pttrn)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Pttrn) -> Doc ann
forall {a} {ann}. Pretty a => (Text, a) -> Doc ann
ppField [(Text, Pttrn)]
fields)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"|)"
      where
        ppField :: (Text, a) -> Doc ann
ppField (Text
f, a
p) = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
p
    PttrnRecord (Just Typ
t) [(Text, Pttrn)]
fields -> Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
tyAnn (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"(|" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma (((Text, Pttrn) -> Doc ann) -> [(Text, Pttrn)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Pttrn) -> Doc ann
forall {a} {ann}. Pretty a => (Text, a) -> Doc ann
ppField [(Text, Pttrn)]
fields)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
")|)") (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)
      where
        ppField :: (Text, a) -> Doc ann
ppField (Text
f, a
p) = Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
p






{- ------------------- Definitions ------------------------------------ -}



{- ------------------- Funs/Primrecs ---------------------------------- -}



{- ------------------- Datatypes and Type Synonyms -------------------- -}


data DatatypeConstructor = DatatypeConstructor {
      DatatypeConstructor -> Text
constructorName :: Text,
      DatatypeConstructor -> [Typ]
constructorArgs :: [Typ] }
  deriving (DatatypeConstructor -> DatatypeConstructor -> Bool
(DatatypeConstructor -> DatatypeConstructor -> Bool)
-> (DatatypeConstructor -> DatatypeConstructor -> Bool)
-> Eq DatatypeConstructor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DatatypeConstructor -> DatatypeConstructor -> Bool
== :: DatatypeConstructor -> DatatypeConstructor -> Bool
$c/= :: DatatypeConstructor -> DatatypeConstructor -> Bool
/= :: DatatypeConstructor -> DatatypeConstructor -> Bool
Eq, Eq DatatypeConstructor
Eq DatatypeConstructor =>
(DatatypeConstructor -> DatatypeConstructor -> Ordering)
-> (DatatypeConstructor -> DatatypeConstructor -> Bool)
-> (DatatypeConstructor -> DatatypeConstructor -> Bool)
-> (DatatypeConstructor -> DatatypeConstructor -> Bool)
-> (DatatypeConstructor -> DatatypeConstructor -> Bool)
-> (DatatypeConstructor
    -> DatatypeConstructor -> DatatypeConstructor)
-> (DatatypeConstructor
    -> DatatypeConstructor -> DatatypeConstructor)
-> Ord DatatypeConstructor
DatatypeConstructor -> DatatypeConstructor -> Bool
DatatypeConstructor -> DatatypeConstructor -> Ordering
DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DatatypeConstructor -> DatatypeConstructor -> Ordering
compare :: DatatypeConstructor -> DatatypeConstructor -> Ordering
$c< :: DatatypeConstructor -> DatatypeConstructor -> Bool
< :: DatatypeConstructor -> DatatypeConstructor -> Bool
$c<= :: DatatypeConstructor -> DatatypeConstructor -> Bool
<= :: DatatypeConstructor -> DatatypeConstructor -> Bool
$c> :: DatatypeConstructor -> DatatypeConstructor -> Bool
> :: DatatypeConstructor -> DatatypeConstructor -> Bool
$c>= :: DatatypeConstructor -> DatatypeConstructor -> Bool
>= :: DatatypeConstructor -> DatatypeConstructor -> Bool
$cmax :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
max :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
$cmin :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
min :: DatatypeConstructor -> DatatypeConstructor -> DatatypeConstructor
Ord, Int -> DatatypeConstructor -> ShowS
[DatatypeConstructor] -> ShowS
DatatypeConstructor -> String
(Int -> DatatypeConstructor -> ShowS)
-> (DatatypeConstructor -> String)
-> ([DatatypeConstructor] -> ShowS)
-> Show DatatypeConstructor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DatatypeConstructor -> ShowS
showsPrec :: Int -> DatatypeConstructor -> ShowS
$cshow :: DatatypeConstructor -> String
show :: DatatypeConstructor -> String
$cshowList :: [DatatypeConstructor] -> ShowS
showList :: [DatatypeConstructor] -> ShowS
Show, Typeable, Typeable DatatypeConstructor
Typeable DatatypeConstructor =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> DatatypeConstructor
 -> c DatatypeConstructor)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DatatypeConstructor)
-> (DatatypeConstructor -> Constr)
-> (DatatypeConstructor -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DatatypeConstructor))
-> ((forall b. Data b => b -> b)
    -> DatatypeConstructor -> DatatypeConstructor)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> DatatypeConstructor -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DatatypeConstructor -> m DatatypeConstructor)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DatatypeConstructor -> m DatatypeConstructor)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DatatypeConstructor -> m DatatypeConstructor)
-> Data DatatypeConstructor
DatatypeConstructor -> Constr
DatatypeConstructor -> DataType
(forall b. Data b => b -> b)
-> DatatypeConstructor -> DatatypeConstructor
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u
forall u.
(forall d. Data d => d -> u) -> DatatypeConstructor -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DatatypeConstructor
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DatatypeConstructor
-> c DatatypeConstructor
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DatatypeConstructor)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DatatypeConstructor
-> c DatatypeConstructor
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> DatatypeConstructor
-> c DatatypeConstructor
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DatatypeConstructor
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DatatypeConstructor
$ctoConstr :: DatatypeConstructor -> Constr
toConstr :: DatatypeConstructor -> Constr
$cdataTypeOf :: DatatypeConstructor -> DataType
dataTypeOf :: DatatypeConstructor -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DatatypeConstructor)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DatatypeConstructor)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DatatypeConstructor)
$cgmapT :: (forall b. Data b => b -> b)
-> DatatypeConstructor -> DatatypeConstructor
gmapT :: (forall b. Data b => b -> b)
-> DatatypeConstructor -> DatatypeConstructor
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DatatypeConstructor -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> DatatypeConstructor -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> DatatypeConstructor -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DatatypeConstructor -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DatatypeConstructor -> m DatatypeConstructor
Data)


instance Pretty DatatypeConstructor where
  pretty :: forall ann. DatatypeConstructor -> Doc ann
pretty = DatatypeConstructor -> Doc ann
forall ann. DatatypeConstructor -> Doc ann
printDatatypeConstructor

printDatatypeConstructor :: DatatypeConstructor -> Doc ann
printDatatypeConstructor :: forall ann. DatatypeConstructor -> Doc ann
printDatatypeConstructor (DatatypeConstructor Text
name [Typ]
args) =
  Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.hsep ((Typ -> Doc ann) -> [Typ] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Doc ann -> Doc ann) -> (Typ -> Doc ann) -> Typ -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty) [Typ]
args)

{-
datatype ('a,'b) tuplist = 
      ConsA "'a" "('a,'b) tuplist"  
      | TailB
      | TailA "'a \\<Rightarrow> ('a,'b) tuplist"
      | Empty
-}



{- --------------- Toplevel Declarations ----------------------------- -}


data Decl =
    Datatype {
      Decl -> Text
datatypeName :: Text,
      Decl -> [Text]
datatypeTVars :: [TName],
      Decl -> [DatatypeConstructor]
datatypeConstructors :: [DatatypeConstructor] }
  | Record { 
      Decl -> Text
recordName :: Text, 
      Decl -> [Text]
recordTVars :: [Text], 
      Decl -> [(Text, Typ)]
recordFields :: [(Text, Typ)] }
  | TypeSynonym Text [Text] Typ
  | Definition {
      Decl -> Text
definitionName :: Text,
      Decl -> TypSig
definitionType :: TypSig,
      Decl -> [Term]
definitionVars :: [Term],
      Decl -> Term
definitionTerm :: Term }
  | Fun { Decl -> [(Text, TypSig, [([Pttrn], Term)])]
funEquations :: [(Text, TypSig, [([Pttrn], Term)])] }
    deriving (Decl -> Decl -> Bool
(Decl -> Decl -> Bool) -> (Decl -> Decl -> Bool) -> Eq Decl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Decl -> Decl -> Bool
== :: Decl -> Decl -> Bool
$c/= :: Decl -> Decl -> Bool
/= :: Decl -> Decl -> Bool
Eq, Eq Decl
Eq Decl =>
(Decl -> Decl -> Ordering)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Decl)
-> (Decl -> Decl -> Decl)
-> Ord Decl
Decl -> Decl -> Bool
Decl -> Decl -> Ordering
Decl -> Decl -> Decl
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Decl -> Decl -> Ordering
compare :: Decl -> Decl -> Ordering
$c< :: Decl -> Decl -> Bool
< :: Decl -> Decl -> Bool
$c<= :: Decl -> Decl -> Bool
<= :: Decl -> Decl -> Bool
$c> :: Decl -> Decl -> Bool
> :: Decl -> Decl -> Bool
$c>= :: Decl -> Decl -> Bool
>= :: Decl -> Decl -> Bool
$cmax :: Decl -> Decl -> Decl
max :: Decl -> Decl -> Decl
$cmin :: Decl -> Decl -> Decl
min :: Decl -> Decl -> Decl
Ord, 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
$cshowsPrec :: Int -> Decl -> ShowS
showsPrec :: Int -> Decl -> ShowS
$cshow :: Decl -> String
show :: Decl -> String
$cshowList :: [Decl] -> ShowS
showList :: [Decl] -> ShowS
Show, Typeable, Typeable Decl
Typeable Decl =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Decl -> c Decl)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Decl)
-> (Decl -> Constr)
-> (Decl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Decl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Decl))
-> ((forall b. Data b => b -> b) -> Decl -> Decl)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r)
-> (forall u. (forall d. Data d => d -> u) -> Decl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Decl -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Decl -> m Decl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Decl -> m Decl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Decl -> m Decl)
-> Data Decl
Decl -> Constr
Decl -> DataType
(forall b. Data b => b -> b) -> Decl -> Decl
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Decl -> u
forall u. (forall d. Data d => d -> u) -> Decl -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Decl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Decl -> c Decl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Decl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Decl)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Decl -> c Decl
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Decl -> c Decl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Decl
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Decl
$ctoConstr :: Decl -> Constr
toConstr :: Decl -> Constr
$cdataTypeOf :: Decl -> DataType
dataTypeOf :: Decl -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Decl)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Decl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Decl)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Decl)
$cgmapT :: (forall b. Data b => b -> b) -> Decl -> Decl
gmapT :: (forall b. Data b => b -> b) -> Decl -> Decl
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Decl -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Decl -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Decl -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Decl -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Decl -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Decl -> m Decl
Data)

instance Pretty Decl where
  pretty :: forall ann. Decl -> Doc ann
pretty = \ case
    Datatype Text
name [Text]
tvs [DatatypeConstructor]
cons ->
      Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"datatype" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty (Text -> [Typ] -> Typ
Type Text
name ((Text -> Typ) -> [Text] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Typ
TVar [Text]
tvs)) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align (Doc ann
"="
          Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.vsep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
" |" ((DatatypeConstructor -> Doc ann)
-> [DatatypeConstructor] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map DatatypeConstructor -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. DatatypeConstructor -> Doc ann
pretty [DatatypeConstructor]
cons))) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
P.line
    Record Text
name [Text]
tvs [(Text, Typ)]
fields ->
      Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
P.nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"record" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty (Text -> [Typ] -> Typ
Type Text
name ((Text -> Typ) -> [Text] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Typ
TVar [Text]
tvs)) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"="
          Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.vsep (((Text, Typ) -> Doc ann) -> [(Text, Typ)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
f, Typ
t) -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"::" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
t)) [(Text, Typ)]
fields) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
P.line
    TypeSynonym Text
name [Text]
args Typ
ty ->
      Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"type_synonym" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty (Text -> [Typ] -> Typ
Type Text
name ((Text -> Typ) -> [Text] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Typ
TVar [Text]
args)) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Typ -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Typ -> Doc ann
pretty Typ
ty) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
P.line
    Definition Text
name TypSig
ty [Term]
vs Term
t ->
        (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"definition" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
          Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
P.align (Doc ann
"::" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.fillSep [ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (TypSig -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypSig -> Doc ann
pretty TypSig
ty) , Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"where"]) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$
         Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
P.nest Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ((Term -> Doc ann) -> [Term] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty [Term]
vs) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$
                     Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
t)))
        Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
P.line
    f :: Decl
f@(Fun {}) -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"fun"
          Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.vcat (Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
intersperse (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"and") ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$
                    ((Text, TypSig, [([Pttrn], Term)]) -> Doc ann)
-> [(Text, TypSig, [([Pttrn], Term)])] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Text
name, TypSig
tp, [([Pttrn], Term)]
_) -> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
name Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"::"
                          Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (TypSig -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypSig -> Doc ann
pretty TypSig
tp) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
empty)
                        (Decl -> [(Text, TypSig, [([Pttrn], Term)])]
funEquations Decl
f))
          Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"where" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$
       Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
P.nest Int
2 (let eqs :: [(Text, ([Pttrn], Term))]
eqs = ((Text, TypSig, [([Pttrn], Term)]) -> [(Text, ([Pttrn], Term))])
-> [(Text, TypSig, [([Pttrn], Term)])] -> [(Text, ([Pttrn], Term))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Text
name, TypSig
_, [([Pttrn], Term)]
e) -> (([Pttrn], Term) -> (Text, ([Pttrn], Term)))
-> [([Pttrn], Term)] -> [(Text, ([Pttrn], Term))]
forall a b. (a -> b) -> [a] -> [b]
map (\ ([Pttrn], Term)
e' -> (Text
name, ([Pttrn], Term)
e')) [([Pttrn], Term)]
e)
                            (Decl -> [(Text, TypSig, [([Pttrn], Term)])]
funEquations Decl
f)
                     eqs' :: [Doc ann]
eqs' = ((Text, ([Pttrn], Term)) -> Doc ann)
-> [(Text, ([Pttrn], Term))] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Text
n, ([Pttrn]
vs, Term
t)) -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
dquotes (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
                           [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep ((Pttrn -> Doc ann) -> [Pttrn] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Pttrn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pttrn -> Doc ann
pretty [Pttrn]
vs) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
                           Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term -> Doc ann
pretty Term
t)) [(Text, ([Pttrn], Term))]
eqs
                 in [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
bar [Doc ann]
forall {ann}. [Doc ann]
eqs')
          Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
P.line
    -- f@(Fun {}) -> text "function"
    --       <+> P.vcat (intersperse (text "and") $
    --                 map (\ (name, tp, _) -> text name <+> text "::"
    --                       <+> dquotes (pretty tp) <+> empty)
    --                     (funEquations f))
    --       <+> text "where" $+$
    --    P.nest 2 (let eqs = concatMap (\ (name, _, e) -> map (\ e' -> (name, e')) e)
    --                         (funEquations f)
    --                  eqs' = map (\ (n, (vs, t)) -> dquotes (text n <+>
    --                        P.sep (map pretty vs) <+>
    --                        text "=" <+> pretty t)) eqs
    --              in bar eqs')
    --       <> P.line <> "  by auto"
    --       <> P.line



{- --------------- Theory File --------------------------------------- -}

data Theory = Theory
  { Theory -> Text
thyName :: Text
  , Theory -> [Text]
imports :: [Text]
  , Theory -> [Decl]
decls :: [Decl]
  -- , graph :: Graph
  -- , tree :: [Tree Vertex]
  } deriving (Theory -> Theory -> Bool
(Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool) -> Eq Theory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Theory -> Theory -> Bool
== :: Theory -> Theory -> Bool
$c/= :: Theory -> Theory -> Bool
/= :: Theory -> Theory -> Bool
Eq, Eq Theory
Eq Theory =>
(Theory -> Theory -> Ordering)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Theory)
-> (Theory -> Theory -> Theory)
-> Ord Theory
Theory -> Theory -> Bool
Theory -> Theory -> Ordering
Theory -> Theory -> Theory
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Theory -> Theory -> Ordering
compare :: Theory -> Theory -> Ordering
$c< :: Theory -> Theory -> Bool
< :: Theory -> Theory -> Bool
$c<= :: Theory -> Theory -> Bool
<= :: Theory -> Theory -> Bool
$c> :: Theory -> Theory -> Bool
> :: Theory -> Theory -> Bool
$c>= :: Theory -> Theory -> Bool
>= :: Theory -> Theory -> Bool
$cmax :: Theory -> Theory -> Theory
max :: Theory -> Theory -> Theory
$cmin :: Theory -> Theory -> Theory
min :: Theory -> Theory -> Theory
Ord, Int -> Theory -> ShowS
[Theory] -> ShowS
Theory -> String
(Int -> Theory -> ShowS)
-> (Theory -> String) -> ([Theory] -> ShowS) -> Show Theory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Theory -> ShowS
showsPrec :: Int -> Theory -> ShowS
$cshow :: Theory -> String
show :: Theory -> String
$cshowList :: [Theory] -> ShowS
showList :: [Theory] -> ShowS
Show, Typeable)


instance Pretty Theory where
  pretty :: forall ann. Theory -> Doc ann
pretty thy :: Theory
thy@(Theory {}) =
        Theory -> Doc ann
forall ann. Theory -> Doc ann
mkHeader Theory
thy
    Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Theory -> Doc ann
forall ann. Theory -> Doc ann
printDecls Theory
thy
    Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Theory -> Doc ann
forall ann. Theory -> Doc ann
mkFooter Theory
thy

printDecls :: Theory -> Doc ann
printDecls :: forall ann. Theory -> Doc ann
printDecls t :: Theory
t@(Theory{}) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ((Decl -> Doc ann) -> [Decl] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Decl -> Doc ann
pretty ([Decl] -> [Doc ann]) -> [Decl] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Theory -> [Decl]
decls Theory
t)

mkHeader :: Theory -> Doc ann
mkHeader :: forall ann. Theory -> Doc ann
mkHeader t :: Theory
t@(Theory {}) =
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.sep [Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"theory", Text -> Doc ann
forall ann. Text -> Doc ann
text (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Theory -> Text
thyName Theory
t]
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
P.nest Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
P.vcat (Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"imports" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Text -> Doc ann) -> [Text] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Doc ann
forall ann. Text -> Doc ann
text (Theory -> [Text]
imports Theory
t)))
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"begin" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Doc ann
forall a. Monoid a => a
mempty


mkFooter :: Theory -> Doc ann
mkFooter :: forall ann. Theory -> Doc ann
mkFooter Theory
_ = Doc ann
forall a. Monoid a => a
mempty Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
$+$ Text -> Doc ann
forall ann. Text -> Doc ann
text Text
"end"