mirror of
https://github.com/github/semantic.git
synced 2024-12-22 22:31:36 +03:00
Merge branch 'master' into the-point-of-no-carriage-return
This commit is contained in:
Rob Rix
GitHub
commit
a1e0e64204
@ -1,11 +1,8 @@
|
||||
{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, RecordWildCards, ScopedTypeVariables, TypeApplications #-}
|
||||
{-# LANGUAGE DeriveGeneric, DeriveTraversable, FlexibleContexts, FlexibleInstances, LambdaCase, OverloadedStrings, QuantifiedConstraints, RecordWildCards, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeOperators #-}
|
||||
module Analysis.Typecheck
|
||||
( Monotype (..)
|
||||
, Meta
|
||||
, Polytype (PForAll, PBool, PFree, PArr)
|
||||
, Scope
|
||||
, Analysis.Typecheck.bind
|
||||
, Analysis.Typecheck.instantiate
|
||||
, Polytype (..)
|
||||
, typecheckingFlowInsensitive
|
||||
, typecheckingAnalysis
|
||||
) where
|
||||
@ -13,15 +10,16 @@ module Analysis.Typecheck
|
||||
import Analysis.Eval
|
||||
import Analysis.FlowInsensitive
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Effect
|
||||
import Control.Effect.Carrier
|
||||
import Control.Effect.Fail
|
||||
import Control.Effect.Fresh as Fresh
|
||||
import Control.Effect.Reader hiding (Local)
|
||||
import Control.Effect.State
|
||||
import Control.Monad (unless)
|
||||
import Control.Monad.Module
|
||||
import qualified Data.Core as Core
|
||||
import Data.File
|
||||
import Data.Foldable (foldl', for_)
|
||||
import Data.Foldable (for_)
|
||||
import Data.Function (fix)
|
||||
import Data.Functor (($>))
|
||||
import qualified Data.IntMap as IntMap
|
||||
@ -29,102 +27,84 @@ import qualified Data.IntSet as IntSet
|
||||
import Data.List.NonEmpty (nonEmpty)
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe (fromJust, fromMaybe)
|
||||
import Data.Name as Name
|
||||
import Data.Scope
|
||||
import qualified Data.Set as Set
|
||||
import Data.Stack
|
||||
import Data.Term
|
||||
import Data.Void
|
||||
import GHC.Generics (Generic1)
|
||||
import Prelude hiding (fail)
|
||||
|
||||
data Monotype a
|
||||
= MBool
|
||||
| MUnit
|
||||
| MString
|
||||
| MMeta a
|
||||
| MFree Gensym
|
||||
| MArr (Monotype a) (Monotype a)
|
||||
| MRecord (Map.Map User (Monotype a))
|
||||
deriving (Eq, Functor, Ord, Show)
|
||||
data Monotype f a
|
||||
= Bool
|
||||
| Unit
|
||||
| String
|
||||
| Arr (f a) (f a)
|
||||
| Record (Map.Map User (f a))
|
||||
deriving (Foldable, Functor, Generic1, Traversable)
|
||||
|
||||
deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Monotype f a)
|
||||
deriving instance (Ord a, forall a . Eq a => Eq (f a)
|
||||
, forall a . Ord a => Ord (f a), Monad f) => Ord (Monotype f a)
|
||||
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Monotype f a)
|
||||
|
||||
instance HFunctor Monotype
|
||||
instance RightModule Monotype where
|
||||
Unit >>=* _ = Unit
|
||||
Bool >>=* _ = Bool
|
||||
String >>=* _ = String
|
||||
Arr a b >>=* f = Arr (a >>= f) (b >>= f)
|
||||
Record m >>=* f = Record ((>>= f) <$> m)
|
||||
|
||||
type Meta = Int
|
||||
|
||||
data Polytype
|
||||
= PForAll Scope
|
||||
| PUnit
|
||||
| PBool
|
||||
| PString
|
||||
| PBound Int
|
||||
| PFree Gensym
|
||||
| PArr Polytype Polytype
|
||||
| PRecord (Map.Map User Polytype)
|
||||
deriving (Eq, Ord, Show)
|
||||
newtype Polytype f a = PForAll (Scope () f a)
|
||||
deriving (Foldable, Functor, Generic1, Traversable)
|
||||
|
||||
newtype Scope = Scope Polytype
|
||||
deriving (Eq, Ord, Show)
|
||||
deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Polytype f a)
|
||||
deriving instance (Ord a, forall a . Eq a => Eq (f a)
|
||||
, forall a . Ord a => Ord (f a), Monad f) => Ord (Polytype f a)
|
||||
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Polytype f a)
|
||||
|
||||
forAll :: Gensym -> Polytype -> Polytype
|
||||
forAll n body = PForAll (Analysis.Typecheck.bind n body)
|
||||
instance HFunctor Polytype
|
||||
instance RightModule Polytype where
|
||||
PForAll b >>=* f = PForAll (b >>=* f)
|
||||
|
||||
forAlls :: Foldable t => t Gensym -> Polytype -> Polytype
|
||||
|
||||
forAll :: (Eq a, Carrier sig m, Member Polytype sig) => a -> m a -> m a
|
||||
forAll n body = send (PForAll (Data.Scope.bind1 n body))
|
||||
|
||||
forAlls :: (Eq a, Carrier sig m, Member Polytype sig, Foldable t) => t a -> m a -> m a
|
||||
forAlls ns body = foldr forAll body ns
|
||||
|
||||
generalize :: (Carrier sig m, Member Naming sig) => Monotype Meta -> m Polytype
|
||||
generalize ty = namespace "generalize" $ do
|
||||
Gensym root _ <- Name.fresh
|
||||
pure (forAlls (map (Gensym root) (IntSet.toList (mvs ty))) (fold root ty))
|
||||
where fold root = \case
|
||||
MUnit -> PUnit
|
||||
MBool -> PBool
|
||||
MString -> PString
|
||||
MMeta i -> PFree (Gensym root i)
|
||||
MFree n -> PFree n
|
||||
MArr a b -> PArr (fold root a) (fold root b)
|
||||
MRecord fs -> PRecord (fold root <$> fs)
|
||||
|
||||
-- | Bind occurrences of a 'Gensym' in a 'Polytype' term, producing a 'Scope' in which the 'Gensym' is bound.
|
||||
bind :: Gensym -> Polytype -> Scope
|
||||
bind name = Scope . substIn (\ i n -> if name == n then PBound i else PFree n) (const PBound)
|
||||
|
||||
-- | Substitute a 'Polytype' term for the free variable in a given 'Scope', producing a closed 'Polytype' term.
|
||||
instantiate :: Polytype -> Scope -> Polytype
|
||||
instantiate image (Scope body) = substIn (const PFree) (\ i j -> if i == j then image else PBound j) body
|
||||
|
||||
substIn :: (Int -> Gensym -> Polytype)
|
||||
-> (Int -> Int -> Polytype)
|
||||
-> Polytype
|
||||
-> Polytype
|
||||
substIn free bound = go 0
|
||||
where go i (PFree name) = free i name
|
||||
go i (PBound j) = bound i j
|
||||
go i (PForAll (Scope body)) = PForAll (Scope (go (succ i) body))
|
||||
go _ PUnit = PUnit
|
||||
go _ PBool = PBool
|
||||
go _ PString = PString
|
||||
go i (PArr a b) = PArr (go i a) (go i b)
|
||||
go i (PRecord fs) = PRecord (go i <$> fs)
|
||||
generalize :: Term Monotype Meta -> Term (Polytype :+: Monotype) Void
|
||||
generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty)))
|
||||
|
||||
|
||||
typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Monotype Meta), [File (Either (Loc, String) Polytype)])
|
||||
typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))])
|
||||
typecheckingFlowInsensitive
|
||||
= run
|
||||
. runFresh
|
||||
. runNaming
|
||||
. runHeap (Gen (Gensym (Nil :> "root") 0))
|
||||
. (>>= traverse (traverse (traverse generalize)))
|
||||
. fmap (fmap (fmap (fmap generalize)))
|
||||
. traverse runFile
|
||||
|
||||
runFile :: ( Carrier sig m
|
||||
, Effect sig
|
||||
, Member Fresh sig
|
||||
, Member Naming sig
|
||||
, Member (State (Heap Name (Monotype Meta))) sig
|
||||
, Member (State (Heap Name (Term Monotype Meta))) sig
|
||||
)
|
||||
=> File (Term Core.Core Name)
|
||||
-> m (File (Either (Loc, String) (Monotype Meta)))
|
||||
-> m (File (Either (Loc, String) (Term Monotype Meta)))
|
||||
runFile file = traverse run file
|
||||
where run
|
||||
= (\ m -> do
|
||||
(subst, t) <- m
|
||||
modify @(Heap Name (Monotype Meta)) (substAll subst)
|
||||
modify @(Heap Name (Term Monotype Meta)) (fmap (Set.map (substAll subst)))
|
||||
pure (substAll subst <$> t))
|
||||
. runState (mempty :: Substitution)
|
||||
. runReader (fileLoc file)
|
||||
@ -139,7 +119,7 @@ runFile file = traverse run file
|
||||
v <$ for_ bs (unify v))
|
||||
. convergeTerm (fix (cacheTerm . eval typecheckingAnalysis))
|
||||
|
||||
typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap Name (Monotype Meta))) sig, MonadFail m) => Analysis Name (Monotype Meta) m
|
||||
typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap Name (Term Monotype Meta))) sig, MonadFail m) => Analysis Name (Term Monotype Meta) m
|
||||
typecheckingAnalysis = Analysis{..}
|
||||
where alloc = pure
|
||||
bind _ _ = pure ()
|
||||
@ -152,108 +132,65 @@ typecheckingAnalysis = Analysis{..}
|
||||
arg <- meta
|
||||
assign addr arg
|
||||
ty <- eval body
|
||||
pure (MArr arg ty)
|
||||
pure (Term (Arr arg ty))
|
||||
apply _ f a = do
|
||||
_A <- meta
|
||||
_B <- meta
|
||||
unify (MArr _A _B) f
|
||||
unify (Term (Arr _A _B)) f
|
||||
unify _A a
|
||||
pure _B
|
||||
unit = pure MUnit
|
||||
bool _ = pure MBool
|
||||
asBool b = unify MBool b >> pure True <|> pure False
|
||||
string _ = pure MString
|
||||
asString s = unify MString s $> mempty
|
||||
unit = pure (Term Unit)
|
||||
bool _ = pure (Term Bool)
|
||||
asBool b = unify (Term Bool) b >> pure True <|> pure False
|
||||
string _ = pure (Term String)
|
||||
asString s = unify (Term String) s $> mempty
|
||||
frame = fail "unimplemented"
|
||||
edge _ _ = pure ()
|
||||
_ ... m = m
|
||||
|
||||
|
||||
data Constraint = Monotype Meta :===: Monotype Meta
|
||||
data Constraint = Term Monotype Meta :===: Term Monotype Meta
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
infix 4 :===:
|
||||
|
||||
data Solution
|
||||
= Int := Monotype Meta
|
||||
= Int := Term Monotype Meta
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
infix 5 :=
|
||||
|
||||
meta :: (Carrier sig m, Member Fresh sig) => m (Monotype Meta)
|
||||
meta = MMeta <$> Fresh.fresh
|
||||
meta :: (Carrier sig m, Member Fresh sig) => m (Term Monotype Meta)
|
||||
meta = pure <$> Fresh.fresh
|
||||
|
||||
unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Monotype Meta -> Monotype Meta -> m ()
|
||||
unify :: (Carrier sig m, Member (State (Set.Set Constraint)) sig) => Term Monotype Meta -> Term Monotype Meta -> m ()
|
||||
unify t1 t2
|
||||
| t1 == t2 = pure ()
|
||||
| otherwise = modify (<> Set.singleton (t1 :===: t2))
|
||||
|
||||
type Substitution = IntMap.IntMap (Monotype Meta)
|
||||
type Substitution = IntMap.IntMap (Term Monotype Meta)
|
||||
|
||||
solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Set Constraint -> m ()
|
||||
solve cs = for_ cs solve
|
||||
where solve = \case
|
||||
-- FIXME: how do we enforce proper subtyping? row polymorphism or something?
|
||||
MRecord f1 :===: MRecord f2 -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
|
||||
MArr a1 b1 :===: MArr a2 b2 -> solve (a1 :===: a2) *> solve (b1 :===: b2)
|
||||
MMeta m1 :===: MMeta m2 | m1 == m2 -> pure ()
|
||||
MMeta m1 :===: t2 -> do
|
||||
Term (Record f1) :===: Term (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
|
||||
Term (Arr a1 b1) :===: Term (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2)
|
||||
Var m1 :===: Var m2 | m1 == m2 -> pure ()
|
||||
Var m1 :===: t2 -> do
|
||||
sol <- solution m1
|
||||
case sol of
|
||||
Just (_ := t1) -> solve (t1 :===: t2)
|
||||
Nothing | m1 `IntSet.member` mvs t2 -> fail ("Occurs check failure: " <> show m1 <> " :===: " <> show t2)
|
||||
| otherwise -> modify (IntMap.insert m1 t2 . subst (m1 := t2))
|
||||
t1 :===: MMeta m2 -> solve (MMeta m2 :===: t1)
|
||||
| otherwise -> modify (IntMap.insert m1 t2 . fmap (substAll (IntMap.singleton m1 t2)))
|
||||
t1 :===: Var m2 -> solve (Var m2 :===: t1)
|
||||
t1 :===: t2 -> unless (t1 == t2) $ fail ("Type mismatch:\nexpected: " <> show t1 <> "\n actual: " <> show t2)
|
||||
|
||||
solution m = fmap (m :=) <$> gets (IntMap.lookup m)
|
||||
|
||||
substAll :: Substitutable t => Substitution -> t -> t
|
||||
substAll s a = foldl' (flip subst) a (map (uncurry (:=)) (IntMap.toList s))
|
||||
|
||||
mvs :: Foldable t => t Meta -> IntSet.IntSet
|
||||
mvs = foldMap IntSet.singleton
|
||||
|
||||
class FreeVariables t where
|
||||
mvs :: t -> IntSet.IntSet
|
||||
|
||||
instance FreeVariables (Monotype Meta) where
|
||||
mvs MUnit = mempty
|
||||
mvs MBool = mempty
|
||||
mvs MString = mempty
|
||||
mvs (MArr a b) = mvs a <> mvs b
|
||||
mvs (MMeta m) = IntSet.singleton m
|
||||
mvs (MFree _) = mempty
|
||||
mvs (MRecord fs) = foldMap mvs fs
|
||||
|
||||
instance FreeVariables Constraint where
|
||||
mvs (t1 :===: t2) = mvs t1 <> mvs t2
|
||||
|
||||
class Substitutable t where
|
||||
subst :: Solution -> t -> t
|
||||
|
||||
instance Substitutable (Monotype Meta) where
|
||||
subst s con = case con of
|
||||
MUnit -> MUnit
|
||||
MBool -> MBool
|
||||
MString -> MString
|
||||
MArr a b -> MArr (subst s a) (subst s b)
|
||||
MMeta m'
|
||||
| m := t <- s
|
||||
, m == m' -> t
|
||||
| otherwise -> MMeta m'
|
||||
MFree n -> MFree n
|
||||
MRecord fs -> MRecord (subst s <$> fs)
|
||||
|
||||
instance Substitutable Constraint where
|
||||
subst s (t1 :===: t2) = subst s t1 :===: subst s t2
|
||||
|
||||
instance Substitutable Solution where
|
||||
subst s (m := t) = m := subst s t
|
||||
|
||||
instance Substitutable a => Substitutable (IntMap.IntMap a) where
|
||||
subst s = IntMap.map (subst s)
|
||||
|
||||
instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
|
||||
subst s = Set.map (subst s)
|
||||
|
||||
instance Substitutable v => Substitutable (Map.Map k v) where
|
||||
subst s = fmap (subst s)
|
||||
substAll :: Monad t => IntMap.IntMap (t Meta) -> t Meta -> t Meta
|
||||
substAll s a = a >>= \ i -> fromMaybe (pure i) (IntMap.lookup i s)
|
||||
|
||||
@ -194,25 +194,8 @@ annWith :: (Carrier sig m, Member Core sig) => CallStack -> m a -> m a
|
||||
annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack)
|
||||
|
||||
|
||||
stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a
|
||||
stripAnnotations = iter id alg Var Var
|
||||
where alg t | Just c <- prj t, Ann _ b <- c = b
|
||||
| otherwise = Term t
|
||||
|
||||
|
||||
instance Syntax Core where
|
||||
foldSyntax go k h = \case
|
||||
Let a -> Let a
|
||||
a :>> b -> go h a :>> go h b
|
||||
Lam u b -> Lam u (foldSyntax go k h b)
|
||||
a :$ b -> go h a :$ go h b
|
||||
Unit -> Unit
|
||||
Bool b -> Bool b
|
||||
If c t e -> If (go h c) (go h t) (go h e)
|
||||
String s -> String s
|
||||
Load t -> Load (go h t)
|
||||
Edge e t -> Edge e (go h t)
|
||||
Frame -> Frame
|
||||
a :. b -> go h a :. go h b
|
||||
a := b -> go h a := go h b
|
||||
Ann loc t -> Ann loc (go h t)
|
||||
stripAnnotations :: (Member Core sig, HFunctor sig, forall g . Functor g => Functor (sig g)) => Term sig a -> Term sig a
|
||||
stripAnnotations (Var v) = Var v
|
||||
stripAnnotations (Term t)
|
||||
| Just c <- prj t, Ann _ b <- c = stripAnnotations b
|
||||
| otherwise = Term (hmap stripAnnotations t)
|
||||
|
||||
@ -11,7 +11,6 @@ module Data.Core.Pretty
|
||||
import Control.Effect.Reader
|
||||
import Data.Core
|
||||
import Data.File
|
||||
import Data.Functor.Const
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Term
|
||||
@ -56,57 +55,58 @@ inParens amount go = do
|
||||
body <- with amount go
|
||||
pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)
|
||||
|
||||
prettify :: (Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m)
|
||||
=> Style
|
||||
-> Core (Const (m AnsiDoc)) a
|
||||
-> m AnsiDoc
|
||||
prettify style = \case
|
||||
Let a -> pure $ keyword "let" <+> name a
|
||||
Const a :>> Const b -> do
|
||||
prec <- ask @Prec
|
||||
fore <- with 12 a
|
||||
aft <- with 12 b
|
||||
prettyCore :: Style -> Term Core User -> AnsiDoc
|
||||
prettyCore style = run . runReader @Prec 0 . go (pure . name)
|
||||
where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc
|
||||
go var = \case
|
||||
Var v -> var v
|
||||
Term t -> case t of
|
||||
Let a -> pure $ keyword "let" <+> name a
|
||||
a :>> b -> do
|
||||
prec <- ask @Prec
|
||||
fore <- with 12 (go var a)
|
||||
aft <- with 12 (go var b)
|
||||
|
||||
let open = symbol ("{" <> softline)
|
||||
close = symbol (softline <> "}")
|
||||
separator = ";" <> Pretty.line
|
||||
body = fore <> separator <> aft
|
||||
let open = symbol ("{" <> softline)
|
||||
close = symbol (softline <> "}")
|
||||
separator = ";" <> Pretty.line
|
||||
body = fore <> separator <> aft
|
||||
|
||||
pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
|
||||
pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
|
||||
|
||||
Lam n f -> inParens 11 $ do
|
||||
(x, body) <- bind n f
|
||||
pure (lambda <> x <+> arrow <+> body)
|
||||
Lam n f -> inParens 11 $ do
|
||||
(x, body) <- bind n f
|
||||
pure (lambda <> x <+> arrow <+> body)
|
||||
|
||||
Frame -> pure $ primitive "frame"
|
||||
Unit -> pure $ primitive "unit"
|
||||
Bool b -> pure $ primitive (if b then "true" else "false")
|
||||
String s -> pure . strlit $ Pretty.viaShow s
|
||||
Frame -> pure $ primitive "frame"
|
||||
Unit -> pure $ primitive "unit"
|
||||
Bool b -> pure $ primitive (if b then "true" else "false")
|
||||
String s -> pure . strlit $ Pretty.viaShow s
|
||||
|
||||
Const f :$ Const x -> inParens 11 $ (<+>) <$> f <*> x
|
||||
f :$ x -> inParens 11 $ (<+>) <$> go var f <*> go var x
|
||||
|
||||
If (Const con) (Const tru) (Const fal) -> do
|
||||
con' <- "if" `appending` con
|
||||
tru' <- "then" `appending` tru
|
||||
fal' <- "else" `appending` fal
|
||||
pure $ Pretty.sep [con', tru', fal']
|
||||
If con tru fal -> do
|
||||
con' <- "if" `appending` go var con
|
||||
tru' <- "then" `appending` go var tru
|
||||
fal' <- "else" `appending` go var fal
|
||||
pure $ Pretty.sep [con', tru', fal']
|
||||
|
||||
Load (Const p) -> "load" `appending` p
|
||||
Edge Lexical (Const n) -> "lexical" `appending` n
|
||||
Edge Import (Const n) -> "import" `appending` n
|
||||
Const item :. Const body -> inParens 4 $ do
|
||||
f <- item
|
||||
g <- body
|
||||
pure (f <> symbol "." <> g)
|
||||
Load p -> "load" `appending` go var p
|
||||
Edge Lexical n -> "lexical" `appending` go var n
|
||||
Edge Import n -> "import" `appending` go var n
|
||||
item :. body -> inParens 4 $ do
|
||||
f <- go var item
|
||||
g <- go var body
|
||||
pure (f <> symbol "." <> g)
|
||||
|
||||
Const lhs := Const rhs -> inParens 3 $ do
|
||||
f <- lhs
|
||||
g <- rhs
|
||||
pure (f <+> symbol "=" <+> g)
|
||||
lhs := rhs -> inParens 3 $ do
|
||||
f <- go var lhs
|
||||
g <- go var rhs
|
||||
pure (f <+> symbol "=" <+> g)
|
||||
|
||||
-- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
|
||||
Ann _ (Const c) -> c
|
||||
where bind (Ignored x) f = let x' = name x in (,) x' <$> local (x':) (getConst (unScope f))
|
||||
-- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
|
||||
Ann _ c -> go var c
|
||||
where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f)
|
||||
lambda = case style of
|
||||
Unicode -> symbol "λ"
|
||||
Ascii -> symbol "\\"
|
||||
@ -117,8 +117,3 @@ prettify style = \case
|
||||
|
||||
appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
|
||||
appending k item = (keyword k <+>) <$> item
|
||||
|
||||
prettyCore :: Style -> Term Core User -> AnsiDoc
|
||||
prettyCore s = run . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) bound (pure . name)
|
||||
where bound (Z _) = asks (head @AnsiDoc)
|
||||
bound (S n) = local (tail @AnsiDoc) n
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
module Data.Scope
|
||||
( Incr(..)
|
||||
, incr
|
||||
, closed
|
||||
, Scope(..)
|
||||
, fromScope
|
||||
, toScope
|
||||
@ -44,6 +45,10 @@ incr :: (a -> c) -> (b -> c) -> Incr a b -> c
|
||||
incr z s = \case { Z a -> z a ; S b -> s b }
|
||||
|
||||
|
||||
closed :: Traversable f => f a -> Maybe (f b)
|
||||
closed = traverse (const Nothing)
|
||||
|
||||
|
||||
newtype Scope a f b = Scope { unScope :: f (Incr a (f b)) }
|
||||
deriving (Foldable, Functor, Traversable)
|
||||
|
||||
|
||||
@ -1,18 +1,12 @@
|
||||
{-# LANGUAGE DeriveTraversable, FlexibleInstances, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeOperators, UndecidableInstances #-}
|
||||
{-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, StandaloneDeriving, UndecidableInstances #-}
|
||||
module Data.Term
|
||||
( Term(..)
|
||||
, Syntax(..)
|
||||
, iter
|
||||
, cata
|
||||
, interpret
|
||||
, hoistTerm
|
||||
) where
|
||||
|
||||
import Control.Effect.Carrier
|
||||
import Control.Monad (ap)
|
||||
import Control.Monad.Module
|
||||
import Data.Coerce (coerce)
|
||||
import Data.Functor.Const
|
||||
import Data.Scope
|
||||
|
||||
data Term sig a
|
||||
= Var a
|
||||
@ -50,44 +44,7 @@ instance RightModule sig => Carrier sig (Term sig) where
|
||||
eff = Term
|
||||
|
||||
|
||||
class (HFunctor sig, forall g . Functor g => Functor (sig g)) => Syntax sig where
|
||||
foldSyntax :: (forall x y . (x -> m y) -> f x -> n y)
|
||||
-> (forall a . Incr () (n a) -> m (Incr () (n a)))
|
||||
-> (a -> m b)
|
||||
-> sig f a
|
||||
-> sig n b
|
||||
|
||||
instance Syntax (Scope ()) where
|
||||
foldSyntax go bound free = Scope . go (bound . fmap (go free)) . unScope
|
||||
|
||||
instance (Syntax l, Syntax r) => Syntax (l :+: r) where
|
||||
foldSyntax go bound free (L l) = L (foldSyntax go bound free l)
|
||||
foldSyntax go bound free (R r) = R (foldSyntax go bound free r)
|
||||
|
||||
|
||||
iter :: forall m n sig a b
|
||||
. Syntax sig
|
||||
=> (forall a . m a -> n a)
|
||||
-> (forall a . sig n a -> n a)
|
||||
-> (forall a . Incr () (n a) -> m (Incr () (n a)))
|
||||
-> (a -> m b)
|
||||
-> Term sig a
|
||||
-> n b
|
||||
iter var alg bound = go
|
||||
where go :: forall x y . (x -> m y) -> Term sig x -> n y
|
||||
go free = \case
|
||||
Var a -> var (free a)
|
||||
Term t -> alg (foldSyntax go bound free t)
|
||||
|
||||
cata :: Syntax sig
|
||||
=> (a -> b)
|
||||
-> (forall a . sig (Const b) a -> b)
|
||||
-> (Incr () b -> a)
|
||||
-> (x -> a)
|
||||
-> Term sig x
|
||||
-> b
|
||||
cata var alg k h = getConst . iter (coerce var) (Const . alg) (coerce k) (Const . h)
|
||||
|
||||
|
||||
interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b
|
||||
interpret = iter id send
|
||||
hoistTerm :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => (forall m x . sig m x -> sig' m x) -> Term sig a -> Term sig' a
|
||||
hoistTerm f = go
|
||||
where go (Var v) = Var v
|
||||
go (Term t) = Term (f (hmap (hoistTerm f) t))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user