instances for Fix

This commit is contained in:
crumbtoo
2024-02-26 14:29:57 -07:00
parent d9682561b8
commit 8c2ea566dc

View File

@@ -2,40 +2,43 @@
Module : Core.Syntax Module : Core.Syntax
Description : Core ASTs and the like Description : Core ASTs and the like
-} -}
-- {-# OPTIONS_GHC -freduction-depth=0 #-}
{-# LANGUAGE PatternSynonyms, OverloadedStrings #-} {-# LANGUAGE PatternSynonyms, OverloadedStrings #-}
{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TemplateHaskell #-}
-- for recursion-schemes -- for recursion-schemes
{-# LANGUAGE DeriveTraversable, TypeFamilies #-} {-# LANGUAGE DeriveTraversable, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Core.Syntax module Core.Syntax
-- ( (
-- -- * Core AST -- * Core AST
-- ExprF(..), ExprF' ExprF(..), ExprF'
-- , ScDef(..), ScDef' , ScDef(..), ScDef'
-- , Program(..), Program' , Program(..), Program'
-- , Type(..), Kind, pattern (:->), pattern TyInt , Type(..), Kind, pattern (:->), pattern TyInt
-- , Alter(..), Alter', AltCon(..) , Alter(..), Alter', AltCon(..)
-- , Rec(..), Lit(..) , pattern Binding, pattern Alter
-- , Pragma(..) , Rec(..), Lit(..)
-- -- ** Variables and identifiers , Pragma(..)
-- , Name, Var(..), Tag -- ** Variables and identifiers
-- , Binding(..), pattern (:=), pattern (:$) , Name, Var(..), Tag
-- , type Binding' , Binding(..), pattern (:=), pattern (:$)
-- -- ** Working with the fixed point of ExprF , type Binding'
-- , Expr, Expr' -- ** Working with the fixed point of ExprF
-- , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let , Expr, Expr'
-- , pattern Case, pattern Type, pattern Lit , pattern Con, pattern Var, pattern App, pattern Lam, pattern Let
, pattern Case, pattern Type, pattern Lit
-- -- * Misc -- * Misc
-- , Pretty(pretty) , Pretty(pretty)
-- -- * Optics -- * Optics
-- , programScDefs, programTypeSigs, programDataTags , programScDefs, programTypeSigs, programDataTags
-- , formalising , formalising
-- , HasRHS(_rhs), HasLHS(_lhs) , HasRHS(_rhs), HasLHS(_lhs)
-- , HasBinders(binders) , HasBinders(binders)
-- ) )
where where
---------------------------------------------------------------------------------- ----------------------------------------------------------------------------------
import Data.Coerce import Data.Coerce
@@ -47,6 +50,7 @@ import Data.HashMap.Strict (HashMap)
import Data.HashMap.Strict qualified as H import Data.HashMap.Strict qualified as H
import Data.Hashable import Data.Hashable
import Data.Foldable (traverse_) import Data.Foldable (traverse_)
import Data.Functor
import Data.Functor.Classes (Show1(..), showsPrec1, showsBinaryWith) import Data.Functor.Classes (Show1(..), showsPrec1, showsBinaryWith)
import Data.Text qualified as T import Data.Text qualified as T
import Data.Char import Data.Char
@@ -100,63 +104,71 @@ data Var = MkVar Name Type
instance Hashable Var where instance Hashable Var where
hashWithSalt s (MkVar n _) = hashWithSalt s n hashWithSalt s (MkVar n _) = hashWithSalt s n
-- pattern Con :: Tag -> Int -> Expr b pattern Con :: Tag -> Int -> Expr b
-- pattern Con t a = Fix (ConF t a) pattern Con t a = Fix (ConF t a)
-- pattern Var :: Name -> Expr b pattern Var :: Name -> Expr b
-- pattern Var b = Fix (VarF b) pattern Var b = Fix (VarF b)
-- pattern App :: Expr b -> Expr b -> Expr b pattern App :: Expr b -> Expr b -> Expr b
-- pattern App f x = Fix (AppF f x) pattern App f x = Fix (AppF f x)
-- pattern Lam :: [b] -> Expr b -> Expr b pattern Lam :: [b] -> Expr b -> Expr b
-- pattern Lam bs e = Fix (LamF bs e) pattern Lam bs e = Fix (LamF bs e)
-- pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b pattern Let :: Rec -> [Binding b] -> Expr b -> Expr b
-- pattern Let r bs e = Fix (LetF r bs e) pattern Let r bs e = Fix (LetF r bs e)
-- pattern Case :: Expr b -> [Alter b] -> Expr b pattern Case :: Expr b -> [Alter b] -> Expr b
-- pattern Case e as = Fix (CaseF e as) pattern Case e as = Fix (CaseF e as)
-- pattern Type :: Type -> Expr b pattern Type :: Type -> Expr b
-- pattern Type t = Fix (TypeF t) pattern Type t = Fix (TypeF t)
-- pattern Lit :: Lit -> Expr b pattern Lit :: Lit -> Expr b
-- pattern Lit t = Fix (LitF t) pattern Lit t = Fix (LitF t)
-- pattern TyInt :: Type pattern TyInt :: Type
-- pattern TyInt = TyCon "Int#" pattern TyInt = TyCon "Int#"
infixr 1 :-> infixr 1 :->
pattern (:->) :: Type -> Type -> Type pattern (:->) :: Type -> Type -> Type
pattern a :-> b = TyApp (TyApp TyFun a) b pattern a :-> b = TyApp (TyApp TyFun a) b
-- {-# COMPLETE Binding :: Binding #-}
-- {-# COMPLETE (:=) :: Binding #-}
data BindingF b a = BindingF b (ExprF b a) data BindingF b a = BindingF b (ExprF b a)
deriving (Functor, Foldable, Traversable) deriving (Functor, Foldable, Traversable)
type Binding b = BindingF b (ExprF b (Fix (ExprF b))) type Binding b = BindingF b (Fix (ExprF b))
type Binding' = Binding Name
-- collapse = foldFix embed -- collapse = foldFix embed
-- pattern Binding :: b -> Expr b -> Binding b pattern Binding :: b -> Expr b -> Binding b
-- pattern Binding k v <- Fix (BindingF k (undefined -> v)) pattern Binding k v <- BindingF k (wrapFix -> v)
-- where Binding k v = Fix (BindingF k undefined) where Binding k v = BindingF k (unwrapFix v)
-- infixl 1 := {-# COMPLETE (:=) #-}
-- pattern (:=) :: b -> Expr b -> Binding b {-# COMPLETE Binding #-}
-- pattern k := v = Binding k v
-- infixl 2 :$ infixl 1 :=
-- pattern (:$) :: Expr b -> Expr b -> Expr b pattern (:=) :: b -> Expr b -> Binding b
-- pattern f :$ x = App f x pattern k := v = Binding k v
infixl 2 :$
pattern (:$) :: Expr b -> Expr b -> Expr b
pattern f :$ x = App f x
data AlterF b a = AlterF AltCon [b] (ExprF b a) data AlterF b a = AlterF AltCon [b] (ExprF b a)
deriving (Functor, Foldable, Traversable) deriving (Functor, Foldable, Traversable)
type Alter b = AlterF b (ExprF b (Fix (ExprF b))) pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
pattern Alter con bs e <- AlterF con bs (wrapFix -> e)
where Alter con bs e = AlterF con bs (unwrapFix e)
type Alter b = AlterF b (Fix (ExprF b))
type Alter' = Alter Name
-- pattern Alter :: AltCon -> [b] -> Expr b -> Alter b -- pattern Alter :: AltCon -> [b] -> Expr b -> Alter b
-- pattern Alter con bs e <- Fix (AlterF con bs (undefined -> e)) -- pattern Alter con bs e <- Fix (AlterF con bs (undefined -> e))
@@ -267,18 +279,18 @@ instance HasLHS (ScDef b) (ScDef b) (b, [b]) (b, [b]) where
-- For this reason, it's best to consider 'formalising' as if it were two -- For this reason, it's best to consider 'formalising' as if it were two
-- unrelated unidirectional getters. -- unrelated unidirectional getters.
-- formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b) formalising :: Iso (Expr a) (Expr b) (Expr a) (Expr b)
-- formalising = iso sa bt where formalising = iso sa bt where
-- sa :: Expr a -> Expr a sa :: Expr a -> Expr a
-- sa = ana \case sa = ana \case
-- Lam [b] e -> LamF [b] e Lam [b] e -> LamF [b] e
-- Lam (b:bs) e -> LamF [b] (Lam bs e) Lam (b:bs) e -> LamF [b] (Lam bs e)
-- x -> project x x -> project x
-- bt :: Expr b -> Expr b bt :: Expr b -> Expr b
-- bt = cata \case bt = cata \case
-- LamF [b] (Lam bs e) -> Lam (b:bs) e LamF [b] (Lam bs e) -> Lam (b:bs) e
-- x -> embed x x -> embed x
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
@@ -494,19 +506,19 @@ class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where
-- => HasBinders (ExprF b a) (ExprF b' a') b b' where -- => HasBinders (ExprF b a) (ExprF b' a') b b' where
-- binders k = undefined -- binders k = undefined
instance HasBinders a a b b' instance HasBinders a a' b b'
=> HasBinders (ExprF b a) (ExprF b' a) b b' where => HasBinders (ExprF b a) (ExprF b' a') b b' where
binders :: forall f. (Applicative f) binders :: forall f. (Applicative f)
=> LensLike f (ExprF b a) (ExprF b' a) b b' => LensLike f (ExprF b a) (ExprF b' a') b b'
binders k = go where binders k = go where
go :: ExprF b a -> f (ExprF b' a')
go (LamF bs e) = LamF <$> traverse k bs <*> binders k e go (LamF bs e) = LamF <$> traverse k bs <*> binders k e
go (CaseF e as) = CaseF <$> binders k e <*> traverseOf eachbind k as go (CaseF e as) = CaseF <$> binders k e <*> eachbind as
go (LetF r bs e) = LetF r <$> traverseOf eachbind k bs <*> binders k e go (LetF r bs e) = LetF r <$> eachbind bs <*> binders k e
go f = bitraverse k pure f go f = bitraverse k (binders k) f
eachbind :: forall a a' b b'. HasBinders a a' b b' eachbind :: forall p. Bitraversable p => [p b a] -> f [p b' a']
=> Traversal [a] [a'] b b' eachbind bs = bitraverse k (binders k) `traverse` bs
eachbind = each . binders
instance HasBinders a a b b' instance HasBinders a a b b'
=> HasBinders (AlterF b a) (AlterF b' a) b b' where => HasBinders (AlterF b a) (AlterF b' a) b b' where
@@ -516,6 +528,10 @@ instance HasBinders a a b b'
instance HasBinders (BindingF b a) (BindingF b' a) b b' where instance HasBinders (BindingF b a) (BindingF b' a) b b' where
binders = undefined binders = undefined
instance (HasBinders (f b (Fix (f b))) (f b' (Fix (f b'))) b b')
=> HasBinders (Fix (f b)) (Fix (f b')) b b' where
binders k (Fix f) = Fix <$> binders k f
-- deriveEq1 ''ExprF -- deriveEq1 ''ExprF
-- deriving instance Eq b => Eq (Alter b) -- deriving instance Eq b => Eq (Alter b)