Created
June 30, 2022 20:28
-
-
Save Heimdell/c6ca1235a9f443f4fdf1ab548dc0484c to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type Cofree (f : * -> *) x = | |
| Cofree { x : a, f : f (Cofree f a) } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment