AST.hs

module AST where

import Data.Text qualified as Text
import Data.Text (Text)
import Data.Scientific

data Module = Module QName [Import] [Toplevel]

data Import = Import
  { from   :: [Name]
  , rename :: Maybe [Name]
  , names  :: Maybe [Name]
  }

data Toplevel
  = TopDecl Private Decl
  | NewType Private NewType
  deriving stock (Show, Eq, Ord)

data Private = Private | Public
  deriving stock (Show, Eq, Ord)

data NewType
  = Opaque Name [TArg] [Variant]
  deriving stock (Show, Eq, Ord)

data Variant
  = Variant Ctor [TField]
  deriving stock (Show, Eq, Ord)

data TField = TField Name Type
  deriving stock (Show, Eq, Ord)

data TArg = TArg Name (Maybe Kind)
  deriving stock (Show, Eq, Ord)

data Kind = Star | KArr Kind Kind
  deriving stock (Show, Eq, Ord)

data Prog
  = Var QName
  | App Prog Prog
  | Lam [Arg] Prog

  | Ann Prog Type

  | Rec [RDecl]
  | Get Prog Field
  | Upd Prog [RDecl]

  | Inj  Ctor  Prog
  | Mtc  Prog [Alt]

  | Let [Decl] Prog

  | Con Constant
  deriving stock (Show, Eq, Ord)

data RDecl
  = Decl Decl
  | Capt Name
  deriving stock (Show, Eq, Ord)

data Decl
  = Val Name (Maybe Type) Prog
  deriving stock (Show, Eq, Ord)

data Type
  = TCon QName
  | TVar Name
  | TApp Type Type
  | TArr Type Type
  deriving stock (Show, Eq, Ord)

data QName = QName [Name] Name
  deriving stock (Show, Eq, Ord)

data Name = Name Text Int
  deriving stock (Eq, Ord)

fromText :: Text -> Name
fromText = (`Name` 0)

instance Show Name where
  show (Name x 0) = Text.unpack x
  show (Name x i) = Text.unpack x <> "'" <> show i

data Ctor  = Ctor  QName deriving stock (Show, Eq, Ord)
data Field = Field Name  deriving stock (Show, Eq, Ord)

data Arg = Arg Name (Maybe Type)
  deriving stock (Show, Eq, Ord)

data Alt = Alt Pat Prog Prog
  deriving stock (Show, Eq, Ord)

data Pat
  = PVar Name
  | PPrj Ctor [PDecl]
  | PCon Constant
  deriving stock (Show, Eq, Ord)

data PDecl
  = PDecl Name Pat
  | PCapt Name
  deriving stock (Show, Eq, Ord)

data Constant
  = Number Scientific
  | String Text
  deriving stock (Show, Eq, Ord)

E.hs

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-star-is-type #-}

module E where

import Control.Applicative hiding (some)
import Data.Monoid (First (..))
import Data.Char
import Data.Scientific
import Data.Text qualified as Text
import Data.Text (Text)
import Data.Typeable
import Prettyprinter

import Text.Brick.DSL
import Text.Brick.Lexer qualified as Lexer
import Text.Brick.Lexer (SourcePos, Parser, runLexer, stringLit, asToken, nameLike, kw)

import AST

import Debug.Trace

arith :: M (Entity Lexeme SourcePos NewType)
-- arith :: M (Entity Lexeme SourcePos QuailifiedName)
arith = mdo

  pat <- rule "Pat"
    [ Pos !* aCtor !. "{"           !. "}" :=> \_ c _    _ -> PPrj c []
    , Pos !* aCtor !. "{" !* pdecls !. "}" :=> \_ c _ ds _ -> PPrj c ds
    ]

  pdecls <- pdecl `sepBy` sep

  pdecl <- rule "PDecl"
    [ Pos !* name               :=> \_ n     -> PCapt n
    , Pos !* name !. "=" !* pat :=> \_ n _ p -> PDecl n p
    ]

  constant <- rule "Constant"
    [ Pos !. "number" :=> \_ (LNumber s) -> Number s
    , Pos !. "string" :=> \_ (LString s) -> String s
    ]

  newType <- rule "NewType"
    [ Pos !. "type" !* ctor !* targs !. "=" !* variants :=> \_ _ c ns _ vs -> Opaque c ns vs
    , Pos !. "type" !* ctor          !. "=" !* variants :=> \_ _ c    _ vs -> Opaque c [] vs
    , Pos !. "type" !* ctor !* targs                    :=> \_ _ c ns      -> Opaque c ns []
    , Pos !. "type" !* ctor                             :=> \_ _ c         -> Opaque c [] []
    ]

  targs    <- some targ
  variants <- some variant

  targ <- rule "TArg"
    [ Pos        !* name                       :=> \_   n       -> TArg n Nothing
    , Pos !. "(" !* name !. ":" !* kind !. ")" :=> \_ _ n _ k _ -> TArg n (Just k)
    ]

  kind <- rule "Kind"
    [ Pos !* kindArrow :=> pass
    ]

  kindArrow <- rule "KArrow"
    [ Pos !* kindTerm !. "->" !* kindArrow :=> \_ d _ c -> KArr d c
    , Pos !* kindTerm                      :=> pass
    ]

  kindTerm <- rule "KTerm"
    [ Pos        !. "*"         :=> \_ _     -> Star
    , Pos !. "(" !* kind !. ")" :=> \_ _ k _ -> k
    ]

  variant <- rule "Variant"
    [ Pos !. "|" !* aCtor !. "{"           !. "}" :=> \_ _ c _ _ -> Variant c []
    , Pos !. "|" !* aCtor !. "{" !* fields !. "}" :=> \_ _ c _ fs _ -> Variant c fs
    ]

  fields <- tField `sepBy` sep

  tField <- rule "TField"
    [ Pos !* name !. ":" !* type_ :=> \_ n _ t -> TField n t
    ]

  type_ <- rule "Type"
    [ Pos !* typeArrow :=> pass
    ]

  typeArrow <- rule "TArrow"
    [ Pos !* typeApp !. "->" !* typeArrow :=> \_ d _ c -> TArr d c
    , Pos !* typeApp                      :=> pass
    ]

  typeApp <- rule "TApp"
    [ Pos !* typeApp !* typeTerm :=> \_ f x -> TApp f x
    , Pos !* typeTerm            :=> pass
    ]

  typeTerm <- rule "TTerm"
    [ Pos        !* name         :=> \_ n     -> TVar n
    , Pos        !* qCtor        :=> \_ n     -> TCon n
    , Pos !. "(" !* type_ !. ")" :=> \_ _ t _ -> t
    ]

  qCtor <- rule "QCtor"
    [ Pos !* ctor                 :=> \_ c               -> QName [] c
    , Pos !* ctor !. "." !* qCtor :=> \_ c _ (QName p n) -> QName (c : p) n
    ]

  qName <- rule "QName"
    [ Pos !* name                 :=> \_ c               -> QName [] c
    , Pos !* ctor !. "." !* qName :=> \_ c _ (QName p n) -> QName (c : p) n
    ]

  aCtor <- rule "ACtor"
    [ Pos !* qCtor :=> \_ c -> Ctor c
    ]

  ctor <- rule @_ @SourcePos "Ctor" [ Pos !. "ctor" :=> \_ (LCtor c) -> fromText c ]
  name <- rule               "Name" [ Pos !. "name" :=> \_ (LVar  c) -> fromText c ]

  sep <- rule "Separator"
    [ Pos !. "," :=> \_ _ -> ()
    , Pos !. ";" :=> \_ _ -> ()
    ]

  return newType

sepBy
  :: forall (t :: *) (p :: *) a (sep :: *)
  .  (Typeable p, Typeable sep, Typeable a, Typeable t)
  => Entity t p a
  -> Entity t p sep
  -> M (Entity t p [a])
sepBy a@(MkEntity aName) sep'@(MkEntity sepName) = mdo
  res <- rule (aName <> "/" <> sepName)
    [ Pos !* a                :=> \_ x      -> [x]
    , Pos !* a !* sep' !* res :=> \_ x _ xs -> x : xs
    ]
  return res

some
  :: forall (t :: *) (p :: *) a
  .  (Typeable p, Typeable a, Typeable t)
  => Entity t p a
  -> M (Entity t p [a])
some a@(MkEntity aName) = mdo
  res <- rule (aName <> "+")
    [ Pos !* a        :=> \_ x    -> [x]
    , Pos !* a !* res :=> \_ x xs -> x : xs
    ]
  return res

pass :: i -> a -> a
pass = const id

ignore :: i -> a -> ()
ignore _ _ = ()

data Lexeme
  = LIgnored Text
  | LNumber  Scientific
  | LString  Text
  | LVar     Text
  | LCtor    Text

instance Show Lexeme where
  show = \case
    LIgnored t -> show t
    LNumber  n -> show n
    LString  t -> show t
    LVar     n -> Text.unpack n
    LCtor    n -> Text.unpack n

lexer :: String -> Text -> Either String [(Term, SourcePos, Lexeme)]
lexer = runLexer "$" (LIgnored "$")
  [ nameLike  "name"   startName restName LVar    reserved
  , nameLike  "ctor"   startCtor restCtor LCtor   reserved
  , terms LIgnored reserved
  ]
  where
    reserved = "-> . ( ) : , ; { } | type = *"
    startName c = isAlpha c && isLower c
    startCtor c = isAlpha c && isUpper c
    restName  c = isAlpha c && isLower c || isDigit c || c == ('_' :: Char)
    restCtor  c = isAlphaNum c || c `elem` ("-?!_" :: String)

terms :: (Text -> l) -> Text -> Parser (Term, SourcePos, l)
terms l txt = foldl (<|>) empty $ map (kw' l) do Text.words txt

kw' :: (Text -> l) -> Text -> Parser (Term, SourcePos, l)
kw' l t = kw t (MkTerm t) (l t)

input :: String -> Text -> [(Term, SourcePos, Lexeme)]
input f src = either error id $ lexer f src

-- test :: String -> Text -> (Either Component Ent)
test f src = runParser arith src $ input f src

pp :: (Functor f, Pretty (f Hide)) => f i -> IO ()
pp = print . pretty . fmap (const Hide)

data Hide = Hide

instance Show Hide where show _ = ""

angled, braced :: [Doc ann] -> Doc ann
braced = encloseSep "{" "}" ","
angled = encloseSep "<" ">" ","

located :: (Show i, Pretty (f i), Foldable f) => f i -> String
located fi = case getFirst (foldMap (First . Just) fi) of
  Just info -> show (pretty fi) <> " at " <> show info
  Nothing   -> error $ "structure with no info field: " <> show (pretty fi)

example.sml

type Cofree (f : * -> *) x =
  | Cofree { x : a, f : f (Cofree f a) }