things
This commit is contained in:
@@ -35,6 +35,12 @@ import Text.Printf
|
|||||||
import Core.Syntax
|
import Core.Syntax
|
||||||
----------------------------------------------------------------------------------
|
----------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
infer = undefined
|
||||||
|
check = undefined
|
||||||
|
checkCoreProg = undefined
|
||||||
|
checkCoreProgR = undefined
|
||||||
|
checkCoreExprR = undefined
|
||||||
|
|
||||||
-- | Annotated typing context -- I have a feeling we're going to want this in the
|
-- | Annotated typing context -- I have a feeling we're going to want this in the
|
||||||
-- future.
|
-- future.
|
||||||
type Context b = [(b, Type)]
|
type Context b = [(b, Type)]
|
||||||
@@ -74,6 +80,8 @@ instance IsRlpcError TypeError where
|
|||||||
-- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
|
-- throw any number of fatal or nonfatal errors. Run with @runErrorful@.
|
||||||
type HMError = Errorful TypeError
|
type HMError = Errorful TypeError
|
||||||
|
|
||||||
|
{--
|
||||||
|
|
||||||
-- | Assert that an expression unifies with a given type
|
-- | Assert that an expression unifies with a given type
|
||||||
--
|
--
|
||||||
-- >>> let e = [coreProg|3|]
|
-- >>> let e = [coreProg|3|]
|
||||||
@@ -276,3 +284,4 @@ demoContext =
|
|||||||
, ("False", TyCon "Bool")
|
, ("False", TyCon "Bool")
|
||||||
]
|
]
|
||||||
|
|
||||||
|
--}
|
||||||
|
|||||||
109
src/Core/Parse.y
109
src/Core/Parse.y
@@ -12,7 +12,6 @@ module Core.Parse
|
|||||||
, parseCoreProgR
|
, parseCoreProgR
|
||||||
, module Core.Lex -- temp convenience
|
, module Core.Lex -- temp convenience
|
||||||
, SrcError
|
, SrcError
|
||||||
, Module
|
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
|
|
||||||
@@ -34,7 +33,6 @@ import Data.Text qualified as T
|
|||||||
import Data.HashMap.Strict qualified as H
|
import Data.HashMap.Strict qualified as H
|
||||||
}
|
}
|
||||||
|
|
||||||
%name parseCore Module
|
|
||||||
%name parseCoreExpr StandaloneExpr
|
%name parseCoreExpr StandaloneExpr
|
||||||
%name parseCoreProg StandaloneProgram
|
%name parseCoreProg StandaloneProgram
|
||||||
%tokentype { Located CoreToken }
|
%tokentype { Located CoreToken }
|
||||||
@@ -44,7 +42,6 @@ import Data.HashMap.Strict qualified as H
|
|||||||
%token
|
%token
|
||||||
let { Located _ TokenLet }
|
let { Located _ TokenLet }
|
||||||
letrec { Located _ TokenLetrec }
|
letrec { Located _ TokenLetrec }
|
||||||
module { Located _ TokenModule }
|
|
||||||
where { Located _ TokenWhere }
|
where { Located _ TokenWhere }
|
||||||
case { Located _ TokenCase }
|
case { Located _ TokenCase }
|
||||||
of { Located _ TokenOf }
|
of { Located _ TokenOf }
|
||||||
@@ -73,18 +70,14 @@ import Data.HashMap.Strict qualified as H
|
|||||||
|
|
||||||
%%
|
%%
|
||||||
|
|
||||||
Module :: { Module Name }
|
|
||||||
Module : module conname where Program Eof { Module (Just ($2, [])) $4 }
|
|
||||||
| Program Eof { Module Nothing $1 }
|
|
||||||
|
|
||||||
Eof :: { () }
|
Eof :: { () }
|
||||||
Eof : eof { () }
|
Eof : eof { () }
|
||||||
| error { () }
|
| error { () }
|
||||||
|
|
||||||
StandaloneProgram :: { Program Name }
|
StandaloneProgram :: { Program Var }
|
||||||
StandaloneProgram : Program eof { $1 }
|
StandaloneProgram : Program eof { $1 }
|
||||||
|
|
||||||
Program :: { Program Name }
|
Program :: { Program Var }
|
||||||
Program : ScTypeSig ';' Program { insTypeSig $1 $3 }
|
Program : ScTypeSig ';' Program { insTypeSig $1 $3 }
|
||||||
| ScTypeSig OptSemi { singletonTypeSig $1 }
|
| ScTypeSig OptSemi { singletonTypeSig $1 }
|
||||||
| ScDef ';' Program { insScDef $1 $3 }
|
| ScDef ';' Program { insScDef $1 $3 }
|
||||||
@@ -104,97 +97,99 @@ OptSemi : ';' { () }
|
|||||||
| {- epsilon -} { () }
|
| {- epsilon -} { () }
|
||||||
|
|
||||||
ScTypeSig :: { (Name, Type) }
|
ScTypeSig :: { (Name, Type) }
|
||||||
ScTypeSig : Var '::' Type { ($1,$3) }
|
ScTypeSig : Id '::' Type { ($1, $3 TyKindType) }
|
||||||
|
|
||||||
ScDefs :: { [ScDef Name] }
|
ScDefs :: { [ScDef PsName] }
|
||||||
ScDefs : ScDef ';' ScDefs { $1 : $3 }
|
ScDefs : ScDef ';' ScDefs { $1 : $3 }
|
||||||
| ScDef ';' { [$1] }
|
| ScDef ';' { [$1] }
|
||||||
| ScDef { [$1] }
|
| ScDef { [$1] }
|
||||||
|
|
||||||
ScDef :: { ScDef Name }
|
ScDef :: { ScDef PsName }
|
||||||
ScDef : Var ParList '=' Expr { ScDef $1 $2 $4 }
|
ScDef : Id ParList '=' Expr { ScDef ($1,Nothing) $2 $4 }
|
||||||
-- hack to allow constructors to be compiled into scs
|
|
||||||
| Con ParList '=' Expr { ScDef $1 $2 $4 }
|
|
||||||
|
|
||||||
Type :: { Type }
|
Type :: { [(Name, Kind)] -> Kind -> Type }
|
||||||
Type : Type1 { $1 }
|
: Type1 '->' Type { \cases
|
||||||
|
g TyKindType ->
|
||||||
|
$1 g TyKindType :-> $3 g TyKindType
|
||||||
|
_ _ -> error "kind mismatch" }
|
||||||
|
| Type1 { $1 }
|
||||||
|
|
||||||
Type1 :: { Type }
|
-- do we want to allow symbolic names for tyvars and tycons?
|
||||||
|
|
||||||
|
Type1 :: { [(Name, Kind)] -> Kind -> Type }
|
||||||
Type1 : '(' Type ')' { $2 }
|
Type1 : '(' Type ')' { $2 }
|
||||||
| Type1 '->' Type { $1 :-> $3 }
|
| varname { \k -> TyVar $ MkVar $1 k }
|
||||||
-- do we want to allow symbolic names for tyvars and tycons?
|
| conname { \k -> TyCon $ MkTyCon $1 k }
|
||||||
| varname { TyVar $1 }
|
|
||||||
| conname { TyCon $1 }
|
|
||||||
|
|
||||||
ParList :: { [Name] }
|
ParList :: { [PsName] }
|
||||||
ParList : Var ParList { $1 : $2 }
|
ParList : varname ParList { ($1, Nothing) : $2 }
|
||||||
| {- epsilon -} { [] }
|
| {- epsilon -} { [] }
|
||||||
|
|
||||||
StandaloneExpr :: { Expr Name }
|
StandaloneExpr :: { Expr Var }
|
||||||
StandaloneExpr : Expr eof { $1 }
|
StandaloneExpr : Expr eof { $1 }
|
||||||
|
|
||||||
Expr :: { Expr Name }
|
Expr :: { Expr Var }
|
||||||
Expr : LetExpr { $1 }
|
Expr : LetExpr { $1 }
|
||||||
| 'λ' Binders '->' Expr { Lam $2 $4 }
|
| 'λ' Binders '->' Expr { Lam $2 $4 }
|
||||||
| Application { $1 }
|
| Application { $1 }
|
||||||
| CaseExpr { $1 }
|
| CaseExpr { $1 }
|
||||||
| Expr1 { $1 }
|
| Expr1 { $1 }
|
||||||
|
|
||||||
LetExpr :: { Expr Name }
|
LetExpr :: { Expr Var }
|
||||||
LetExpr : let '{' Bindings '}' in Expr { Let NonRec $3 $6 }
|
LetExpr : let '{' Bindings '}' in Expr { Let NonRec $3 $6 }
|
||||||
| letrec '{' Bindings '}' in Expr { Let Rec $3 $6 }
|
| letrec '{' Bindings '}' in Expr { Let Rec $3 $6 }
|
||||||
|
|
||||||
Binders :: { [Name] }
|
Binders :: { [Var] }
|
||||||
Binders : Var Binders { $1 : $2 }
|
Binders : Var Binders { $1 : $2 }
|
||||||
| Var { [$1] }
|
| Var { [$1] }
|
||||||
|
|
||||||
Application :: { Expr Name }
|
Application :: { Expr Var }
|
||||||
Application : Expr1 AppArgs { foldl' App $1 $2 }
|
Application : Application AppArg { App $1 $2 }
|
||||||
|
| Expr1 AppArg { App $1 $2 }
|
||||||
|
|
||||||
AppArgs :: { [Expr Name] }
|
AppArg :: { Expr Var }
|
||||||
AppArgs : Expr1 AppArgs { $1 : $2 }
|
: '@' Type1 { Type ($2 [] TyKindInferred) }
|
||||||
| Expr1 { [$1] }
|
| Expr1 { $1 }
|
||||||
|
|
||||||
CaseExpr :: { Expr Name }
|
CaseExpr :: { Expr Var }
|
||||||
CaseExpr : case Expr of '{' Alters '}' { Case $2 $5 }
|
CaseExpr : case Expr of '{' Alters '}' { Case $2 $5 }
|
||||||
|
|
||||||
Alters :: { [Alter Name] }
|
Alters :: { [Alter Var] }
|
||||||
Alters : Alter ';' Alters { $1 : $3 }
|
Alters : Alter ';' Alters { $1 : $3 }
|
||||||
| Alter ';' { [$1] }
|
| Alter ';' { [$1] }
|
||||||
| Alter { [$1] }
|
| Alter { [$1] }
|
||||||
|
|
||||||
Alter :: { Alter Name }
|
Alter :: { Alter Var }
|
||||||
Alter : alttag ParList '->' Expr { Alter (AltTag $1) $2 $4 }
|
Alter : alttag AltParList '->' Expr { Alter (AltTag $1) $2 $4 }
|
||||||
| Con ParList '->' Expr { Alter (AltData $1) $2 $4 }
|
| conname AltParList '->' Expr { Alter (AltData $1) $2 $4 }
|
||||||
|
|
||||||
Expr1 :: { Expr Name }
|
AltParList :: { [Var] }
|
||||||
|
: Var AltParList { $1 : $2 }
|
||||||
|
| {- epsilon -} { [] }
|
||||||
|
|
||||||
|
Expr1 :: { Expr Var }
|
||||||
Expr1 : litint { Lit $ IntL $1 }
|
Expr1 : litint { Lit $ IntL $1 }
|
||||||
| Id { Var $1 }
|
| Id { Var $1 }
|
||||||
| PackCon { $1 }
|
| PackCon { $1 }
|
||||||
| '(' Expr ')' { $2 }
|
| '(' Expr ')' { $2 }
|
||||||
|
|
||||||
PackCon :: { Expr Name }
|
PackCon :: { Expr Var }
|
||||||
PackCon : pack '{' litint litint '}' { Con $3 $4 }
|
PackCon : pack '{' litint litint '}' { Con $3 $4 }
|
||||||
|
|
||||||
Bindings :: { [Binding Name] }
|
Bindings :: { [Binding Var] }
|
||||||
Bindings : Binding ';' Bindings { $1 : $3 }
|
Bindings : Binding ';' Bindings { $1 : $3 }
|
||||||
| Binding ';' { [$1] }
|
| Binding ';' { [$1] }
|
||||||
| Binding { [$1] }
|
| Binding { [$1] }
|
||||||
|
|
||||||
Binding :: { Binding Name }
|
Binding :: { Binding Var }
|
||||||
Binding : Var '=' Expr { $1 := $3 }
|
Binding : Var '=' Expr { $1 := $3 }
|
||||||
|
|
||||||
Id :: { Name }
|
Id :: { Name }
|
||||||
Id : Var { $1 }
|
: varname { $1 }
|
||||||
| Con { $1 }
|
| conname { $1 }
|
||||||
|
|
||||||
Var :: { Name }
|
Var :: { Var }
|
||||||
Var : varname { $1 }
|
Var : '(' varname '::' Type ')' { MkVar $2 ($4 [] TyKindType) }
|
||||||
| varsym { $1 }
|
|
||||||
|
|
||||||
Con :: { Name }
|
|
||||||
Con : conname { $1 }
|
|
||||||
| consym { $1 }
|
|
||||||
|
|
||||||
{
|
{
|
||||||
|
|
||||||
@@ -205,13 +200,13 @@ parseError (Located _ t : _) =
|
|||||||
|
|
||||||
{-# WARNING parseError "unimpl" #-}
|
{-# WARNING parseError "unimpl" #-}
|
||||||
|
|
||||||
exprPragma :: [String] -> RLPC (Expr Name)
|
exprPragma :: [String] -> RLPC (Expr Var)
|
||||||
exprPragma ("AST" : e) = undefined
|
exprPragma ("AST" : e) = undefined
|
||||||
exprPragma _ = undefined
|
exprPragma _ = undefined
|
||||||
|
|
||||||
{-# WARNING exprPragma "unimpl" #-}
|
{-# WARNING exprPragma "unimpl" #-}
|
||||||
|
|
||||||
astPragma :: [String] -> RLPC (Expr Name)
|
astPragma :: [String] -> RLPC (Expr Var)
|
||||||
astPragma _ = undefined
|
astPragma _ = undefined
|
||||||
|
|
||||||
{-# WARNING astPragma "unimpl" #-}
|
{-# WARNING astPragma "unimpl" #-}
|
||||||
@@ -228,13 +223,13 @@ insScDef sc = programScDefs %~ (sc:)
|
|||||||
singletonScDef :: (Hashable b) => ScDef b -> Program b
|
singletonScDef :: (Hashable b) => ScDef b -> Program b
|
||||||
singletonScDef sc = insScDef sc mempty
|
singletonScDef sc = insScDef sc mempty
|
||||||
|
|
||||||
parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m Expr'
|
parseCoreExprR :: (Monad m) => [Located CoreToken] -> RLPCT m (Expr Var)
|
||||||
parseCoreExprR = hoistRlpcT generalise . parseCoreExpr
|
parseCoreExprR = hoistRlpcT generalise . parseCoreExpr
|
||||||
|
|
||||||
parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m Program'
|
parseCoreProgR :: forall m. (Monad m) => [Located CoreToken] -> RLPCT m (Program Var)
|
||||||
parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg)
|
parseCoreProgR = ddumpast <=< (hoistRlpcT generalise . parseCoreProg)
|
||||||
where
|
where
|
||||||
ddumpast :: Program' -> RLPCT m Program'
|
ddumpast :: (Program Var) -> RLPCT m (Program Var)
|
||||||
ddumpast p = do
|
ddumpast p = do
|
||||||
addDebugMsg "dump-parsed-core" . show $ p
|
addDebugMsg "dump-parsed-core" . show $ p
|
||||||
pure p
|
pure p
|
||||||
@@ -257,5 +252,7 @@ doTLPragma (Pragma pr) p = case pr of
|
|||||||
readt :: (Read a) => Text -> a
|
readt :: (Read a) => Text -> a
|
||||||
readt = read . T.unpack
|
readt = read . T.unpack
|
||||||
|
|
||||||
|
type PsName = (Name, Maybe Type)
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -8,38 +8,31 @@ Description : Core ASTs and the like
|
|||||||
-- for recursion-schemes
|
-- for recursion-schemes
|
||||||
{-# LANGUAGE DeriveTraversable, TypeFamilies #-}
|
{-# LANGUAGE DeriveTraversable, TypeFamilies #-}
|
||||||
module Core.Syntax
|
module Core.Syntax
|
||||||
( Expr(..)
|
(
|
||||||
, ExprF(..)
|
-- * Core AST
|
||||||
, ExprF'(..)
|
ExprF(..), ExprF'
|
||||||
, Type(..)
|
, ScDef(..), ScDef'
|
||||||
, pattern TyInt
|
, Program(..), Program'
|
||||||
, Lit(..)
|
, Type(..), Kind, pattern (:->), pattern TyInt
|
||||||
, pattern (:$)
|
, Alter(..), Alter', AltCon(..)
|
||||||
, pattern (:@)
|
, Rec(..), Lit(..)
|
||||||
, pattern (:->)
|
|
||||||
, Binding(..)
|
|
||||||
, AltCon(..)
|
|
||||||
, pattern (:=)
|
|
||||||
, Rec(..)
|
|
||||||
, Alter(..)
|
|
||||||
, Name
|
|
||||||
, Tag
|
|
||||||
, ScDef(..)
|
|
||||||
, Module(..)
|
|
||||||
, Program(..)
|
|
||||||
, Program'
|
|
||||||
, Pragma(..)
|
, Pragma(..)
|
||||||
, unliftScDef
|
-- ** Variables and identifiers
|
||||||
, programScDefs
|
, Name, Var(..), TyCon(..), Tag
|
||||||
, programTypeSigs
|
, Binding(..), pattern (:=)
|
||||||
, programDataTags
|
, type Binding'
|
||||||
, Expr'
|
-- ** Working with the fixed point of ExprF
|
||||||
, ScDef'
|
, Expr, Expr'
|
||||||
, Alter'
|
, pattern Con, pattern Var, pattern App, pattern Lam, pattern Let
|
||||||
, Binding'
|
, pattern Case, pattern Type, pattern Lit
|
||||||
, HasRHS(_rhs)
|
|
||||||
, HasLHS(_lhs)
|
-- * Misc
|
||||||
, Pretty(pretty)
|
, Pretty(pretty)
|
||||||
|
|
||||||
|
-- * Optics
|
||||||
|
, programScDefs, programTypeSigs, programDataTags
|
||||||
|
, formalising
|
||||||
|
, HasRHS(_rhs), HasLHS(_lhs)
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
----------------------------------------------------------------------------------
|
----------------------------------------------------------------------------------
|
||||||
@@ -47,8 +40,6 @@ import Data.Coerce
|
|||||||
import Data.Pretty
|
import Data.Pretty
|
||||||
import Data.List (intersperse)
|
import Data.List (intersperse)
|
||||||
import Data.Function ((&))
|
import Data.Function ((&))
|
||||||
import Data.Functor.Foldable
|
|
||||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
|
||||||
import Data.String
|
import Data.String
|
||||||
import Data.HashMap.Strict (HashMap)
|
import Data.HashMap.Strict (HashMap)
|
||||||
import Data.HashMap.Strict qualified as H
|
import Data.HashMap.Strict qualified as H
|
||||||
@@ -56,40 +47,74 @@ import Data.Hashable
|
|||||||
import Data.Text qualified as T
|
import Data.Text qualified as T
|
||||||
import Data.Char
|
import Data.Char
|
||||||
import Data.These
|
import Data.These
|
||||||
import Data.Bifoldable (bifoldr)
|
|
||||||
import GHC.Generics (Generic, Generically(..))
|
import GHC.Generics (Generic, Generically(..))
|
||||||
|
import Text.Show.Deriving
|
||||||
|
|
||||||
|
import Data.Fix hiding (cata, ana)
|
||||||
|
import Data.Bifoldable (bifoldr)
|
||||||
|
import Data.Functor.Foldable
|
||||||
|
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||||
|
|
||||||
-- Lift instances for the Core quasiquoters
|
-- Lift instances for the Core quasiquoters
|
||||||
import Language.Haskell.TH.Syntax (Lift)
|
import Misc.Lift1
|
||||||
import Control.Lens
|
import Control.Lens
|
||||||
----------------------------------------------------------------------------------
|
----------------------------------------------------------------------------------
|
||||||
|
|
||||||
data Expr b = Var Name
|
data ExprF b a = VarF Name
|
||||||
| Con Tag Int -- ^ Con Tag Arity
|
| ConF Tag Int -- ^ Con Tag Arity
|
||||||
| Case (Expr b) [Alter b]
|
| CaseF a [Alter b]
|
||||||
| Lam [b] (Expr b)
|
| LamF [b] a
|
||||||
| Let Rec [Binding b] (Expr b)
|
| LetF Rec [Binding b] a
|
||||||
| App (Expr b) (Expr b)
|
| AppF a a
|
||||||
| Lit Lit
|
| LitF Lit
|
||||||
deriving (Show, Read, Lift)
|
| TypeF Type
|
||||||
|
deriving (Functor, Foldable, Traversable)
|
||||||
|
|
||||||
deriving instance (Eq b) => Eq (Expr b)
|
type Expr b = Fix (ExprF b)
|
||||||
|
|
||||||
data Type = TyFun
|
data Type = TyFun
|
||||||
| TyVar Name
|
| TyVar Var
|
||||||
| TyApp Type Type
|
| TyApp Type Type
|
||||||
| TyCon Name
|
| TyCon TyCon
|
||||||
deriving (Show, Read, Lift, Eq)
|
| TyForall Var Type
|
||||||
|
| TyKindType
|
||||||
|
| TyKindInferred
|
||||||
|
deriving (Show, Eq, Lift)
|
||||||
|
|
||||||
|
type Kind = Type
|
||||||
|
|
||||||
|
data TyCon = MkTyCon Name Kind
|
||||||
|
deriving (Eq, Show, Lift)
|
||||||
|
|
||||||
|
data Var = MkVar Name Type
|
||||||
|
deriving (Eq, Show, Lift)
|
||||||
|
|
||||||
|
pattern Con :: Tag -> Int -> Expr b
|
||||||
|
pattern Con t a = Fix (ConF t a)
|
||||||
|
|
||||||
|
pattern Var :: Name -> Expr b
|
||||||
|
pattern Var b = Fix (VarF b)
|
||||||
|
|
||||||
|
pattern App :: Expr b -> Expr b -> Expr b
|
||||||
|
pattern App f x = Fix (AppF f x)
|
||||||
|
|
||||||
|
pattern Lam :: [b] -> Expr b -> Expr b
|
||||||
|
pattern Lam bs e = Fix (LamF bs e)
|
||||||
|
|
||||||
|
pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b
|
||||||
|
pattern Let r bs e = Fix (LetF r bs e)
|
||||||
|
|
||||||
|
pattern Case :: Expr b -> [Alter b] -> Expr b
|
||||||
|
pattern Case e as = Fix (CaseF e as)
|
||||||
|
|
||||||
|
pattern Type :: Type -> Expr b
|
||||||
|
pattern Type t = Fix (TypeF t)
|
||||||
|
|
||||||
|
pattern Lit :: Lit -> Expr b
|
||||||
|
pattern Lit t = Fix (LitF t)
|
||||||
|
|
||||||
pattern TyInt :: Type
|
pattern TyInt :: Type
|
||||||
pattern TyInt = TyCon "Int#"
|
pattern TyInt = TyCon (MkTyCon "Int#" TyKindType)
|
||||||
|
|
||||||
infixl 2 :$
|
|
||||||
pattern (:$) :: Expr b -> Expr b -> Expr b
|
|
||||||
pattern f :$ x = App f x
|
|
||||||
|
|
||||||
infixl 2 :@
|
|
||||||
pattern (:@) :: Type -> Type -> Type
|
|
||||||
pattern f :@ x = TyApp f x
|
|
||||||
|
|
||||||
infixr 1 :->
|
infixr 1 :->
|
||||||
pattern (:->) :: Type -> Type -> Type
|
pattern (:->) :: Type -> Type -> Type
|
||||||
@@ -97,46 +122,39 @@ pattern a :-> b = TyApp (TyApp TyFun a) b
|
|||||||
|
|
||||||
{-# COMPLETE Binding :: Binding #-}
|
{-# COMPLETE Binding :: Binding #-}
|
||||||
{-# COMPLETE (:=) :: Binding #-}
|
{-# COMPLETE (:=) :: Binding #-}
|
||||||
data Binding b = Binding b (Expr b)
|
|
||||||
deriving (Show, Read, Lift)
|
|
||||||
|
|
||||||
deriving instance (Eq b) => Eq (Binding b)
|
data Binding b = Binding b (Expr b)
|
||||||
|
|
||||||
infixl 1 :=
|
infixl 1 :=
|
||||||
pattern (:=) :: b -> Expr b -> Binding b
|
pattern (:=) :: b -> Expr b -> Binding b
|
||||||
pattern k := v = Binding k v
|
pattern k := v = Binding k v
|
||||||
|
|
||||||
data Alter b = Alter AltCon [b] (Expr b)
|
data Alter b = Alter AltCon [b] (Expr b)
|
||||||
deriving (Show, Read, Lift)
|
|
||||||
|
|
||||||
deriving instance (Eq b) => Eq (Alter b)
|
|
||||||
|
|
||||||
newtype Pragma = Pragma [T.Text]
|
newtype Pragma = Pragma [T.Text]
|
||||||
|
|
||||||
data Rec = Rec
|
data Rec = Rec
|
||||||
| NonRec
|
| NonRec
|
||||||
deriving (Show, Read, Eq, Lift)
|
deriving (Show, Eq, Lift)
|
||||||
|
|
||||||
data AltCon = AltData Name
|
data AltCon = AltData Name
|
||||||
| AltTag Tag
|
| AltTag Tag
|
||||||
| AltLit Lit
|
| AltLit Lit
|
||||||
| AltDefault
|
| AltDefault
|
||||||
deriving (Show, Read, Eq, Lift)
|
deriving (Show, Eq, Lift)
|
||||||
|
|
||||||
newtype Lit = IntL Int
|
newtype Lit = IntL Int
|
||||||
deriving (Show, Read, Eq, Lift)
|
deriving (Show, Eq, Lift)
|
||||||
|
|
||||||
type Name = T.Text
|
type Name = T.Text
|
||||||
type Tag = Int
|
type Tag = Int
|
||||||
|
|
||||||
data ScDef b = ScDef b [b] (Expr b)
|
data ScDef b = ScDef b [b] (Expr b)
|
||||||
deriving (Show, Lift)
|
|
||||||
|
|
||||||
unliftScDef :: ScDef b -> Expr b
|
unliftScDef :: ScDef b -> Expr b
|
||||||
unliftScDef (ScDef _ as e) = Lam as e
|
unliftScDef (ScDef _ as e) = Lam as e
|
||||||
|
|
||||||
data Module b = Module (Maybe (Name, [Name])) (Program b)
|
data Module b = Module (Maybe (Name, [Name])) (Program b)
|
||||||
deriving (Show, Lift)
|
|
||||||
|
|
||||||
data Program b = Program
|
data Program b = Program
|
||||||
{ _programScDefs :: [ScDef b]
|
{ _programScDefs :: [ScDef b]
|
||||||
@@ -144,12 +162,12 @@ data Program b = Program
|
|||||||
, _programDataTags :: HashMap b (Tag, Int)
|
, _programDataTags :: HashMap b (Tag, Int)
|
||||||
-- ^ map constructors to their tag and arity
|
-- ^ map constructors to their tag and arity
|
||||||
}
|
}
|
||||||
deriving (Show, Lift, Generic)
|
deriving (Generic)
|
||||||
deriving (Semigroup, Monoid)
|
deriving (Semigroup, Monoid)
|
||||||
via Generically (Program b)
|
via Generically (Program b)
|
||||||
|
|
||||||
makeLenses ''Program
|
makeLenses ''Program
|
||||||
makeBaseFunctor ''Expr
|
-- makeBaseFunctor ''Expr
|
||||||
pure []
|
pure []
|
||||||
|
|
||||||
-- this is a weird optic, stronger than Lens and Prism, but weaker than Iso.
|
-- this is a weird optic, stronger than Lens and Prism, but weaker than Iso.
|
||||||
@@ -169,13 +187,6 @@ type Binding' = Binding Name
|
|||||||
instance IsString (Expr b) where
|
instance IsString (Expr b) where
|
||||||
fromString = Var . fromString
|
fromString = Var . fromString
|
||||||
|
|
||||||
instance IsString Type where
|
|
||||||
fromString "" = error "IsString Type string may not be empty"
|
|
||||||
fromString s
|
|
||||||
| isUpper c = TyCon . fromString $ s
|
|
||||||
| otherwise = TyVar . fromString $ s
|
|
||||||
where (c:_) = s
|
|
||||||
|
|
||||||
----------------------------------------------------------------------------------
|
----------------------------------------------------------------------------------
|
||||||
|
|
||||||
class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
class HasRHS s t a b | s -> a, t -> b, s b -> t, t a -> s where
|
||||||
@@ -214,14 +225,39 @@ instance HasLHS (Binding b) (Binding b) b b where
|
|||||||
(\ (k := _) -> k)
|
(\ (k := _) -> k)
|
||||||
(\ (_ := e) k' -> k' := e)
|
(\ (_ := e) k' -> k' := e)
|
||||||
|
|
||||||
|
-- | This is not a valid isomorphism for expressions containing lambdas whose
|
||||||
|
-- bodies are themselves lambdas with multiple arguments:
|
||||||
|
--
|
||||||
|
-- >>> [coreExpr|\x -> \y z -> x|] ^. from (from formalising)
|
||||||
|
-- Lam ["x"] (Lam ["y"] (Lam ["z"] (Var "x")))
|
||||||
|
-- >>> [coreExpr|\x -> \y z -> x|]
|
||||||
|
-- Lam ["x"] (Lam ["y","z"] (Var "x"))
|
||||||
|
--
|
||||||
|
-- For this reason, it's best to consider 'formalising' as if it were two
|
||||||
|
-- unrelated unidirectional getters.
|
||||||
|
|
||||||
|
formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b)
|
||||||
|
formalising = iso sa bt where
|
||||||
|
sa :: Expr a -> Expr a
|
||||||
|
sa = ana \case
|
||||||
|
Lam [b] e -> LamF [b] e
|
||||||
|
Lam (b:bs) e -> LamF [b] (Lam bs e)
|
||||||
|
x -> project x
|
||||||
|
|
||||||
|
bt :: Expr b -> Expr b
|
||||||
|
bt = cata \case
|
||||||
|
LamF [b] (Lam bs e) -> Lam (b:bs) e
|
||||||
|
x -> embed x
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
-- TODO: print type sigs with corresponding scdefs
|
|
||||||
-- TODO: emit pragmas for datatags
|
|
||||||
instance (Hashable b, Pretty b) => Pretty (Program b) where
|
instance (Hashable b, Pretty b) => Pretty (Program b) where
|
||||||
pretty p = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
|
pretty p = (datatags <> "\n")
|
||||||
$+$ vlinesOf (programJoinedDefs . to prettyGroup) p
|
$+$ defs
|
||||||
where
|
where
|
||||||
|
datatags = ifoldrOf (programDataTags . ifolded) cataDataTag mempty p
|
||||||
|
defs = vlinesOf (programJoinedDefs . to prettyGroup) p
|
||||||
|
|
||||||
programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
|
programJoinedDefs :: Fold (Program b) (These (b, Type) (ScDef b))
|
||||||
programJoinedDefs = folding $ \p ->
|
programJoinedDefs = folding $ \p ->
|
||||||
foldMapOf programTypeSigs thisTs p
|
foldMapOf programTypeSigs thisTs p
|
||||||
@@ -234,7 +270,10 @@ instance (Hashable b, Pretty b) => Pretty (Program b) where
|
|||||||
H.singleton (sc ^. _lhs . _1) (That sc)
|
H.singleton (sc ^. _lhs . _1) (That sc)
|
||||||
|
|
||||||
prettyGroup :: These (b, Type) (ScDef b) -> Doc
|
prettyGroup :: These (b, Type) (ScDef b) -> Doc
|
||||||
prettyGroup = bifoldr ($$) ($$) mempty . bimap prettyTySig pretty
|
prettyGroup = bifoldr vcatWithSemi vcatWithSemi mempty
|
||||||
|
. bimap prettyTySig pretty
|
||||||
|
|
||||||
|
vcatWithSemi a b = (a <+> ";") $$ b
|
||||||
|
|
||||||
prettyTySig (n,t) = hsep [ttext n, "::", pretty t]
|
prettyTySig (n,t) = hsep [ttext n, "::", pretty t]
|
||||||
|
|
||||||
@@ -257,7 +296,7 @@ instance Pretty Type where
|
|||||||
prettyPrec 1 f <+> prettyPrec 2 x
|
prettyPrec 1 f <+> prettyPrec 2 x
|
||||||
|
|
||||||
instance (Pretty b) => Pretty (ScDef b) where
|
instance (Pretty b) => Pretty (ScDef b) where
|
||||||
pretty sc = hsep [name, as, "=", hang empty 1 e, ";"]
|
pretty sc = hsep [name, as, "=", hang empty 1 e]
|
||||||
where
|
where
|
||||||
name = ttext $ sc ^. _lhs . _1
|
name = ttext $ sc ^. _lhs . _1
|
||||||
as = sc & hsepOf (_lhs . _2 . each . to ttext)
|
as = sc & hsepOf (_lhs . _2 . each . to ttext)
|
||||||
@@ -298,3 +337,26 @@ explicitLayout as = vcat inner <+> "}" where
|
|||||||
inner = zipWith (<+>) delims (pretty <$> as)
|
inner = zipWith (<+>) delims (pretty <$> as)
|
||||||
delims = "{" : repeat ";"
|
delims = "{" : repeat ";"
|
||||||
|
|
||||||
|
instance Pretty TyCon
|
||||||
|
instance Pretty Var
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
deriveShow1 ''ExprF
|
||||||
|
|
||||||
|
instance Lift b => Lift1 (ExprF b) where
|
||||||
|
lift1 (VarF k) = liftCon 'VarF (lift k)
|
||||||
|
lift1 (AppF f x) = liftCon2 'AppF (lift f) (lift x)
|
||||||
|
lift1 (LamF b e) = liftCon2 'LamF (lift b) (lift e)
|
||||||
|
lift1 (LetF r bs e) = liftCon3 'LetF (lift r) (lift bs) (lift e)
|
||||||
|
lift1 (CaseF e as) = liftCon2 'CaseF (lift e) (lift as)
|
||||||
|
lift1 (TypeF t) = liftCon 'TypeF (lift t)
|
||||||
|
lift1 (LitF l) = liftCon 'LitF (lift l)
|
||||||
|
|
||||||
|
deriving instance (Show b, Show a) => Show (ExprF b a)
|
||||||
|
deriving instance Show b => Show (Binding b)
|
||||||
|
deriving instance Show b => Show (Alter b)
|
||||||
|
|
||||||
|
deriving instance Lift b => Lift (Binding b)
|
||||||
|
deriving instance Lift b => Lift (Alter b)
|
||||||
|
|
||||||
|
|||||||
2
src/Core/SystemF.hs
Normal file
2
src/Core/SystemF.hs
Normal file
@@ -0,0 +1,2 @@
|
|||||||
|
module Core.SystemF where
|
||||||
|
|
||||||
Reference in New Issue
Block a user