mirror of
https://github.com/github/semantic.git
synced 2024-11-24 08:54:07 +03:00
Rob Rix
GitHub
commit
fb1c27b595
@ -1,4 +1,4 @@
|
||||
{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeOperators, UndecidableInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
|
||||
module Analysis.Concrete
|
||||
( Concrete(..)
|
||||
, concrete
|
||||
@ -27,10 +27,11 @@ import qualified Data.IntMap as IntMap
|
||||
import qualified Data.IntSet as IntSet
|
||||
import Data.Loc
|
||||
import qualified Data.Map as Map
|
||||
import Data.Monoid (Alt(..))
|
||||
import Data.Name
|
||||
import qualified Data.Set as Set
|
||||
import Data.Term
|
||||
import Data.Text (Text, pack)
|
||||
import Data.Traversable (for)
|
||||
import Prelude hiding (fail)
|
||||
|
||||
type Precise = Int
|
||||
@ -40,25 +41,27 @@ newtype FrameId = FrameId { unFrameId :: Precise }
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Concrete
|
||||
= Closure Loc User (Term Core.Core User) Precise
|
||||
= Closure Loc User (Term Core.Core User) Env
|
||||
| Unit
|
||||
| Bool Bool
|
||||
| String Text
|
||||
| Obj Frame
|
||||
| Record Env
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
objectFrame :: Concrete -> Maybe Frame
|
||||
objectFrame (Obj frame) = Just frame
|
||||
objectFrame _ = Nothing
|
||||
recordFrame :: Concrete -> Maybe Env
|
||||
recordFrame (Record frame) = Just frame
|
||||
recordFrame _ = Nothing
|
||||
|
||||
data Frame = Frame
|
||||
{ frameEdges :: [(Core.Edge, Precise)]
|
||||
, frameSlots :: Env
|
||||
newtype Frame = Frame
|
||||
{ frameSlots :: Env
|
||||
}
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type Heap = IntMap.IntMap Concrete
|
||||
|
||||
data Edge = Lexical | Import
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
|
||||
-- | Concrete evaluation of a term to a value.
|
||||
--
|
||||
@ -74,7 +77,6 @@ concrete
|
||||
runFile :: ( Carrier sig m
|
||||
, Effect sig
|
||||
, Member Fresh sig
|
||||
, Member (Reader FrameId) sig
|
||||
, Member (State Heap) sig
|
||||
)
|
||||
=> File (Term Core.Core User)
|
||||
@ -82,38 +84,32 @@ runFile :: ( Carrier sig m
|
||||
runFile file = traverse run file
|
||||
where run = runReader (fileLoc file)
|
||||
. runFailWithLoc
|
||||
. runReader @Env mempty
|
||||
. fix (eval concreteAnalysis)
|
||||
|
||||
concreteAnalysis :: ( Carrier sig m
|
||||
, Member Fresh sig
|
||||
, Member (Reader Env) sig
|
||||
, Member (Reader Loc) sig
|
||||
, Member (Reader FrameId) sig
|
||||
, Member (State Heap) sig
|
||||
, MonadFail m
|
||||
)
|
||||
=> Analysis Precise Concrete m
|
||||
concreteAnalysis = Analysis{..}
|
||||
where alloc _ = fresh
|
||||
bind name addr = modifyCurrentFrame (updateFrameSlots (Map.insert name addr))
|
||||
lookupEnv n = do
|
||||
FrameId frameAddr <- ask
|
||||
val <- deref frameAddr
|
||||
heap <- get
|
||||
pure (val >>= lookupConcrete heap n)
|
||||
bind name addr m = local (Map.insert name addr) m
|
||||
lookupEnv n = asks (Map.lookup n)
|
||||
deref = gets . IntMap.lookup
|
||||
assign addr value = modify (IntMap.insert addr value)
|
||||
abstract _ name body = do
|
||||
loc <- ask
|
||||
FrameId parentAddr <- ask
|
||||
pure (Closure loc name body parentAddr)
|
||||
apply eval (Closure loc name body parentAddr) a = do
|
||||
frameAddr <- fresh
|
||||
assign frameAddr (Obj (Frame [(Core.Lexical, parentAddr)] mempty))
|
||||
local (const loc) . (frameAddr ...) $ do
|
||||
env <- asks (flip Map.restrictKeys (Set.delete name (foldMap Set.singleton body)))
|
||||
pure (Closure loc name body env)
|
||||
apply eval (Closure loc name body env) a = do
|
||||
local (const loc) $ do
|
||||
addr <- alloc name
|
||||
assign addr a
|
||||
bind name addr
|
||||
eval body
|
||||
local (const (Map.insert name addr env)) (eval body)
|
||||
apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function"
|
||||
unit = pure Unit
|
||||
bool b = pure (Bool b)
|
||||
@ -122,30 +118,24 @@ concreteAnalysis = Analysis{..}
|
||||
string s = pure (String s)
|
||||
asString (String s) = pure s
|
||||
asString v = fail $ "Cannot coerce " <> show v <> " to String"
|
||||
-- FIXME: differential inheritance (reference fields instead of copying)
|
||||
-- FIXME: copy non-lexical parents deeply?
|
||||
frame = do
|
||||
lexical <- asks unFrameId
|
||||
pure (Obj (Frame [(Core.Lexical, lexical)] mempty))
|
||||
-- FIXME: throw an error
|
||||
-- FIXME: support dynamic imports
|
||||
edge e addr = modifyCurrentFrame (\ (Frame ps fs) -> Frame ((e, addr) : ps) fs)
|
||||
addr ... m = local (const (FrameId addr)) m
|
||||
|
||||
updateFrameSlots f frame = frame { frameSlots = f (frameSlots frame) }
|
||||
|
||||
modifyCurrentFrame f = do
|
||||
addr <- asks unFrameId
|
||||
Just (Obj frame) <- deref addr
|
||||
assign addr (Obj (f frame))
|
||||
record fields = do
|
||||
fields' <- for fields $ \ (name, value) -> do
|
||||
addr <- alloc name
|
||||
assign addr value
|
||||
pure (name, addr)
|
||||
pure (Record (Map.fromList fields'))
|
||||
addr ... n = do
|
||||
val <- deref addr
|
||||
heap <- get
|
||||
pure (val >>= lookupConcrete heap n)
|
||||
|
||||
|
||||
lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise
|
||||
lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete
|
||||
where -- look up the name in a concrete value
|
||||
inConcrete = inFrame <=< maybeA . objectFrame
|
||||
inConcrete = inFrame <=< maybeA . recordFrame
|
||||
-- look up the name in a specific 'Frame', with slots taking precedence over parents
|
||||
inFrame (Frame ps fs) = maybeA (Map.lookup name fs) <|> getAlt (foldMap (Alt . inAddress . snd) ps)
|
||||
inFrame fs = maybeA (Map.lookup name fs) <|> (maybeA (Map.lookup "__semantic_super" fs) >>= inAddress)
|
||||
-- look up the name in the value an address points to, if we haven’t already visited it
|
||||
inAddress addr = do
|
||||
visited <- get
|
||||
@ -157,10 +147,8 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete
|
||||
maybeA = maybe empty pure
|
||||
|
||||
|
||||
runHeap :: (Carrier sig m, Member Fresh sig) => ReaderC FrameId (StateC Heap m) a -> m (Heap, a)
|
||||
runHeap m = do
|
||||
addr <- fresh
|
||||
runState (IntMap.singleton addr (Obj (Frame [] mempty))) (runReader (FrameId addr) m)
|
||||
runHeap :: StateC Heap m a -> m (Heap, a)
|
||||
runHeap = runState mempty
|
||||
|
||||
|
||||
-- | 'heapGraph', 'heapValueGraph', and 'heapAddressGraph' allow us to conveniently export SVGs of the heap:
|
||||
@ -168,16 +156,15 @@ runHeap m = do
|
||||
-- > λ let (heap, res) = concrete [ruby]
|
||||
-- > λ writeFile "/Users/rob/Desktop/heap.dot" (export (addressStyle heap) (heapAddressGraph heap))
|
||||
-- > λ :!dot -Tsvg < ~/Desktop/heap.dot > ~/Desktop/heap.svg
|
||||
heapGraph :: (Precise -> Concrete -> a) -> (Either Core.Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a
|
||||
heapGraph :: (Precise -> Concrete -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a
|
||||
heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h)
|
||||
where graph k v rest = (G.vertex (vertex k v) `G.connect` outgoing v) `G.overlay` rest
|
||||
outgoing = \case
|
||||
Unit -> G.empty
|
||||
Bool _ -> G.empty
|
||||
String _ -> G.empty
|
||||
Closure _ _ _ parentAddr -> edge (Left Core.Lexical) parentAddr
|
||||
Obj frame -> fromFrame frame
|
||||
fromFrame (Frame es ss) = foldr (G.overlay . uncurry (edge . Left)) (foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList ss)) es
|
||||
Closure _ _ _ env -> foldr (G.overlay . edge (Left Lexical)) G.empty env
|
||||
Record frame -> Map.foldrWithKey (\ k -> G.overlay . edge (Right k)) G.empty frame
|
||||
|
||||
heapValueGraph :: Heap -> G.Graph Concrete
|
||||
heapValueGraph h = heapGraph (const id) (const fromAddr) h
|
||||
@ -189,20 +176,20 @@ heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,)
|
||||
addressStyle :: Heap -> G.Style (EdgeType, Precise) Text
|
||||
addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes }
|
||||
where vertex (_, addr) = pack (show addr) <> " = " <> maybe "?" fromConcrete (IntMap.lookup addr heap)
|
||||
edgeAttributes _ (Slot name, _) = ["label" G.:= name]
|
||||
edgeAttributes _ (Edge Core.Import, _) = ["color" G.:= "blue"]
|
||||
edgeAttributes _ (Edge Core.Lexical, _) = ["color" G.:= "green"]
|
||||
edgeAttributes _ _ = []
|
||||
edgeAttributes _ (Slot name, _) = ["label" G.:= name]
|
||||
edgeAttributes _ (Edge Import, _) = ["color" G.:= "blue"]
|
||||
edgeAttributes _ (Edge Lexical, _) = ["color" G.:= "green"]
|
||||
edgeAttributes _ _ = []
|
||||
fromConcrete = \case
|
||||
Unit -> "()"
|
||||
Bool b -> pack $ show b
|
||||
String s -> pack $ show s
|
||||
Closure (Loc p (Span s e)) n _ _ -> "\\\\ " <> n <> " [" <> p <> ":" <> showPos s <> "-" <> showPos e <> "]"
|
||||
Obj _ -> "{}"
|
||||
Record _ -> "{}"
|
||||
showPos (Pos l c) = pack (show l) <> ":" <> pack (show c)
|
||||
|
||||
data EdgeType
|
||||
= Edge Core.Edge
|
||||
= Edge Edge
|
||||
| Slot User
|
||||
| Value Concrete
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
@ -11,6 +11,7 @@ module Analysis.Eval
|
||||
, Analysis(..)
|
||||
) where
|
||||
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Effect.Fail
|
||||
import Control.Effect.Reader
|
||||
import Control.Monad ((>=>))
|
||||
@ -18,7 +19,7 @@ import Data.Core as Core
|
||||
import Data.File
|
||||
import Data.Functor
|
||||
import Data.Loc
|
||||
import Data.Maybe (fromJust)
|
||||
import Data.Maybe (fromJust, fromMaybe)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Term
|
||||
@ -36,9 +37,17 @@ eval :: ( Carrier sig m
|
||||
eval Analysis{..} eval = \case
|
||||
Var n -> lookupEnv' n >>= deref' n
|
||||
Term c -> case c of
|
||||
Let n -> alloc n >>= bind n >> unit
|
||||
Rec (Named (Ignored n) b) -> do
|
||||
addr <- alloc n
|
||||
v <- bind n addr (eval (instantiate1 (pure n) b))
|
||||
v <$ assign addr v
|
||||
a :>> b -> eval a >> eval b
|
||||
Lam (Ignored n) b -> abstract eval n (instantiate1 (pure n) b)
|
||||
Named (Ignored n) a :>>= b -> do
|
||||
a' <- eval a
|
||||
addr <- alloc n
|
||||
assign addr a'
|
||||
bind n addr (eval (instantiate1 (pure n) b))
|
||||
Lam (Named (Ignored n) b) -> abstract eval n (instantiate1 (pure n) b)
|
||||
f :$ a -> do
|
||||
f' <- eval f
|
||||
a' <- eval a
|
||||
@ -50,11 +59,10 @@ eval Analysis{..} eval = \case
|
||||
if c' then eval t else eval e
|
||||
String s -> string s
|
||||
Load p -> eval p >>= asString >> unit -- FIXME: add a load command or something
|
||||
Edge e a -> ref a >>= edge e >> unit
|
||||
Frame -> frame
|
||||
Record fields -> traverse (traverse eval) fields >>= record
|
||||
a :. b -> do
|
||||
a' <- ref a
|
||||
a' ... eval b
|
||||
a' ... b >>= maybe (freeVariable (show b)) (deref' b)
|
||||
a := b -> do
|
||||
b' <- eval b
|
||||
addr <- ref a
|
||||
@ -70,147 +78,140 @@ eval Analysis{..} eval = \case
|
||||
ref = \case
|
||||
Var n -> lookupEnv' n
|
||||
Term c -> case c of
|
||||
Let n -> do
|
||||
addr <- alloc n
|
||||
addr <$ bind n addr
|
||||
If c t e -> do
|
||||
c' <- eval c >>= asBool
|
||||
if c' then ref t else ref e
|
||||
a :. b -> do
|
||||
a' <- ref a
|
||||
a' ... ref b
|
||||
a' ... b >>= maybe (freeVariable (show b)) pure
|
||||
Ann loc c -> local (const loc) (ref c)
|
||||
c -> invalidRef (show c)
|
||||
|
||||
|
||||
prog1 :: File (Term Core User)
|
||||
prog1 = fromBody . lam' foo $ block
|
||||
[ let' bar .= pure foo
|
||||
, Core.if' (pure bar)
|
||||
prog1 = fromBody $ lam (named' "foo")
|
||||
( named' "bar" :<- pure "foo"
|
||||
>>>= Core.if' (pure "bar")
|
||||
(Core.bool False)
|
||||
(Core.bool True)
|
||||
]
|
||||
where (foo, bar) = ("foo", "bar")
|
||||
(Core.bool True))
|
||||
|
||||
prog2 :: File (Term Core User)
|
||||
prog2 = fromBody $ fileBody prog1 $$ Core.bool True
|
||||
|
||||
prog3 :: File (Term Core User)
|
||||
prog3 = fromBody $ lams' [foo, bar, quux]
|
||||
(Core.if' (pure quux)
|
||||
(pure bar)
|
||||
(pure foo))
|
||||
where (foo, bar, quux) = ("foo", "bar", "quux")
|
||||
prog3 = fromBody $ lams [named' "foo", named' "bar", named' "quux"]
|
||||
(Core.if' (pure "quux")
|
||||
(pure "bar")
|
||||
(pure "foo"))
|
||||
|
||||
prog4 :: File (Term Core User)
|
||||
prog4 = fromBody $ block
|
||||
[ let' foo .= Core.bool True
|
||||
, Core.if' (pure foo)
|
||||
prog4 = fromBody
|
||||
( named' "foo" :<- Core.bool True
|
||||
>>>= Core.if' (pure "foo")
|
||||
(Core.bool True)
|
||||
(Core.bool False)
|
||||
]
|
||||
where foo = "foo"
|
||||
(Core.bool False))
|
||||
|
||||
prog5 :: File (Term Core User)
|
||||
prog5 = fromBody $ block
|
||||
[ let' "mkPoint" .= lam' "_x" (lam' "_y" (block
|
||||
[ let' "this" .= Core.frame
|
||||
, pure "this" Core.... let' "x" .= pure "_x"
|
||||
, pure "this" Core.... let' "y" .= pure "_y"
|
||||
, pure "this"
|
||||
prog5 = fromBody $ ann (do'
|
||||
[ Just (named' "mkPoint") :<- lams [named' "_x", named' "_y"] (ann (Core.record
|
||||
[ ("x", ann (pure "_x"))
|
||||
, ("y", ann (pure "_y"))
|
||||
]))
|
||||
, let' "point" .= pure "mkPoint" $$ Core.bool True $$ Core.bool False
|
||||
, pure "point" Core.... pure "x"
|
||||
, pure "point" Core.... pure "y" .= pure "point" Core.... pure "x"
|
||||
]
|
||||
, Just (named' "point") :<- ann (ann (ann (pure "mkPoint") $$ ann (Core.bool True)) $$ ann (Core.bool False))
|
||||
, Nothing :<- ann (ann (pure "point") Core.... "x")
|
||||
, Nothing :<- ann (ann (pure "point") Core.... "y") .= ann (ann (pure "point") Core.... "x")
|
||||
])
|
||||
|
||||
prog6 :: [File (Term Core User)]
|
||||
prog6 =
|
||||
[ File (Loc "dep" (locSpan (fromJust here))) $ block
|
||||
[ let' "dep" .= Core.frame
|
||||
, pure "dep" Core.... (let' "var" .= Core.bool True)
|
||||
]
|
||||
, File (Loc "main" (locSpan (fromJust here))) $ block
|
||||
[ File (Loc "dep" (locSpan (fromJust here))) $ Core.record
|
||||
[ ("dep", Core.record [ ("var", Core.bool True) ]) ]
|
||||
, File (Loc "main" (locSpan (fromJust here))) $ do' (map (Nothing :<-)
|
||||
[ load (Core.string "dep")
|
||||
, let' "thing" .= pure "dep" Core.... pure "var"
|
||||
]
|
||||
, Core.record [ ("thing", pure "dep" Core.... "var") ]
|
||||
])
|
||||
]
|
||||
|
||||
ruby :: File (Term Core User)
|
||||
ruby = fromBody . ann . block $
|
||||
[ ann (let' "Class" .= Core.frame)
|
||||
, ann (pure "Class" Core....
|
||||
(ann (let' "new" .= lam' "self" (block
|
||||
[ ann (let' "instance" .= Core.frame)
|
||||
, ann (pure "instance" Core.... Core.edge Import (pure "self"))
|
||||
, ann (pure "instance" $$$ "initialize")
|
||||
]))))
|
||||
ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' statements))
|
||||
where statements =
|
||||
[ Just "Class" :<- record
|
||||
[ (__semantic_super, Core.record [])
|
||||
, ("new", lam "self"
|
||||
( "instance" :<- record [ (__semantic_super, var "self") ]
|
||||
>>>= var "instance" $$$ "initialize"))
|
||||
]
|
||||
|
||||
, ann (let' "(Object)" .= Core.frame)
|
||||
, ann (pure "(Object)" Core.... ann (Core.edge Import (pure ("Class"))))
|
||||
, ann (let' "Object" .= Core.frame)
|
||||
, ann (pure "Object" Core.... block
|
||||
[ ann (Core.edge Import (pure "(Object)"))
|
||||
, ann (let' "nil?" .= lam' "_" false)
|
||||
, ann (let' "initialize" .= lam' "self" (pure "self"))
|
||||
, ann (let' __semantic_truthy .= lam' "_" (Core.bool True))
|
||||
])
|
||||
, Just "(Object)" :<- record [ (__semantic_super, var "Class") ]
|
||||
, Just "Object" :<- record
|
||||
[ (__semantic_super, var "(Object)")
|
||||
, ("nil?", lam "_" (var __semantic_global ... "false"))
|
||||
, ("initialize", lam "self" (var "self"))
|
||||
, (__semantic_truthy, lam "_" (bool True))
|
||||
]
|
||||
|
||||
, ann (pure "Class" Core.... Core.edge Import (pure "Object"))
|
||||
, Just "(NilClass)" :<- record
|
||||
-- FIXME: what should we do about multiple import edges like this
|
||||
[ (__semantic_super, var "Class")
|
||||
, (__semantic_super, var "(Object)")
|
||||
]
|
||||
, Just "NilClass" :<- record
|
||||
[ (__semantic_super, var "(NilClass)")
|
||||
, (__semantic_super, var "Object")
|
||||
, ("nil?", lam "_" (var __semantic_global ... "true"))
|
||||
, (__semantic_truthy, lam "_" (bool False))
|
||||
]
|
||||
|
||||
, ann (let' "(NilClass)" .= Core.frame)
|
||||
, ann (pure "(NilClass)" Core.... block
|
||||
[ ann (Core.edge Import (pure "Class"))
|
||||
, ann (Core.edge Import (pure "(Object)"))
|
||||
])
|
||||
, ann (let' "NilClass" .= Core.frame)
|
||||
, ann (pure "NilClass" Core.... block
|
||||
[ ann (Core.edge Import (pure "(NilClass)"))
|
||||
, ann (Core.edge Import (pure "Object"))
|
||||
, ann (let' "nil?" .= lam' "_" true)
|
||||
, ann (let' __semantic_truthy .= lam' "_" (Core.bool False))
|
||||
])
|
||||
, Just "(TrueClass)" :<- record
|
||||
[ (__semantic_super, var "Class")
|
||||
, (__semantic_super, var "(Object)")
|
||||
]
|
||||
, Just "TrueClass" :<- record
|
||||
[ (__semantic_super, var "(TrueClass)")
|
||||
, (__semantic_super, var "Object")
|
||||
]
|
||||
|
||||
, ann (let' "(TrueClass)" .= Core.frame)
|
||||
, ann (pure "(TrueClass)" Core.... block
|
||||
[ ann (Core.edge Import (pure "Class"))
|
||||
, ann (Core.edge Import (pure "(Object)"))
|
||||
])
|
||||
, ann (let' "TrueClass" .= Core.frame)
|
||||
, ann (pure "TrueClass" Core.... block
|
||||
[ ann (Core.edge Import (pure "(TrueClass)"))
|
||||
, ann (Core.edge Import (pure "Object"))
|
||||
])
|
||||
, Just "(FalseClass)" :<- record
|
||||
[ (__semantic_super, var "Class")
|
||||
, (__semantic_super, var "(Object)")
|
||||
]
|
||||
, Just "FalseClass" :<- record
|
||||
[ (__semantic_super, var "(FalseClass)")
|
||||
, (__semantic_super, var "Object")
|
||||
, (__semantic_truthy, lam "_" (bool False))
|
||||
]
|
||||
|
||||
, ann (let' "(FalseClass)" .= Core.frame)
|
||||
, ann (pure "(FalseClass)" Core.... block
|
||||
[ ann (Core.edge Import (pure "Class"))
|
||||
, ann (Core.edge Import (pure "(Object)"))
|
||||
])
|
||||
, ann (let' "FalseClass" .= Core.frame)
|
||||
, ann (pure "FalseClass" Core.... block
|
||||
[ ann (Core.edge Import (pure "(FalseClass)"))
|
||||
, ann (Core.edge Import (pure "Object"))
|
||||
, ann (let' __semantic_truthy .= lam' "_" (Core.bool False))
|
||||
])
|
||||
, Just "nil" :<- var "NilClass" $$$ "new"
|
||||
, Just "true" :<- var "TrueClass" $$$ "new"
|
||||
, Just "false" :<- var "FalseClass" $$$ "new"
|
||||
|
||||
, ann (let' "nil" .= pure "NilClass" $$$ "new")
|
||||
, ann (let' "true" .= pure "TrueClass" $$$ "new")
|
||||
, ann (let' "false" .= pure "FalseClass" $$$ "new")
|
||||
, Just "require" :<- lam "path" (Core.load (var "path"))
|
||||
|
||||
, ann (let' "require" .= lam' "path" (Core.load (pure "path")))
|
||||
]
|
||||
where -- _nil = pure "nil"
|
||||
true = pure "true"
|
||||
false = pure "false"
|
||||
self $$$ method = annWith callStack $ lam' "_x" (pure "_x" Core.... pure method $$ pure "_x") $$ self
|
||||
, Nothing :<- var "Class" ... __semantic_super .= var "Object"
|
||||
, Nothing :<- record (statements >>= \ (v :<- _) -> maybe [] (\ v -> [(v, var v)]) v)
|
||||
]
|
||||
self $$$ method = annWith callStack ("_x" :<- self >>>= var "_x" ... method $$ var "_x")
|
||||
record ... field = annWith callStack (record Core.... field)
|
||||
record bindings = annWith callStack (Core.record bindings)
|
||||
var x = annWith callStack (pure x)
|
||||
lam v b = annWith callStack (Core.lam (named' v) b)
|
||||
a >>> b = annWith callStack (a Core.>>> b)
|
||||
infixr 1 >>>
|
||||
v :<- a >>>= b = annWith callStack (named' v :<- a Core.>>>= b)
|
||||
infixr 1 >>>=
|
||||
do' bindings = fromMaybe Core.unit (foldr bind Nothing bindings)
|
||||
where bind (n :<- a) v = maybe (a >>>) ((>>>=) . (:<- a)) n <$> v <|> Just a
|
||||
bool b = annWith callStack (Core.bool b)
|
||||
a .= b = annWith callStack (a Core..= b)
|
||||
|
||||
__semantic_global = "__semantic_global"
|
||||
__semantic_super = "__semantic_super"
|
||||
__semantic_truthy = "__semantic_truthy"
|
||||
|
||||
|
||||
data Analysis address value m = Analysis
|
||||
{ alloc :: User -> m address
|
||||
, bind :: User -> address -> m ()
|
||||
, bind :: forall a . User -> address -> m a -> m a
|
||||
, lookupEnv :: User -> m (Maybe address)
|
||||
, deref :: address -> m (Maybe value)
|
||||
, assign :: address -> value -> m ()
|
||||
@ -221,7 +222,6 @@ data Analysis address value m = Analysis
|
||||
, asBool :: value -> m Bool
|
||||
, string :: Text -> m value
|
||||
, asString :: value -> m Text
|
||||
, frame :: m value
|
||||
, edge :: Edge -> address -> m ()
|
||||
, (...) :: forall a . address -> m a -> m a
|
||||
, record :: [(User, value)] -> m value
|
||||
, (...) :: address -> User -> m (Maybe address)
|
||||
}
|
||||
|
||||
@ -80,7 +80,7 @@ importGraphAnalysis :: ( Alternative m
|
||||
=> Analysis User Value m
|
||||
importGraphAnalysis = Analysis{..}
|
||||
where alloc = pure
|
||||
bind _ _ = pure ()
|
||||
bind _ _ m = m
|
||||
lookupEnv = pure . Just
|
||||
deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList
|
||||
assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty))
|
||||
@ -91,8 +91,7 @@ importGraphAnalysis = Analysis{..}
|
||||
apply eval (Value (Closure loc name body _) _) a = local (const loc) $ do
|
||||
addr <- alloc name
|
||||
assign addr a
|
||||
bind name addr
|
||||
eval body
|
||||
bind name addr (eval body)
|
||||
apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function"
|
||||
unit = pure mempty
|
||||
bool _ = pure mempty
|
||||
@ -100,9 +99,5 @@ importGraphAnalysis = Analysis{..}
|
||||
string s = pure (Value (String s) mempty)
|
||||
asString (Value (String s) _) = pure s
|
||||
asString _ = pure mempty
|
||||
frame = pure mempty
|
||||
edge Core.Import to = do -- FIXME: figure out some other way to do this
|
||||
Loc{locPath=from} <- ask
|
||||
() <$ pure (Value Abstract (Map.singleton from (Set.singleton to)))
|
||||
edge _ _ = pure ()
|
||||
_ ... m = m
|
||||
record fields = pure (Value Abstract (foldMap (valueGraph . snd) fields))
|
||||
_ ... m = pure (Just m)
|
||||
|
||||
@ -73,7 +73,7 @@ instance RightModule Polytype where
|
||||
|
||||
|
||||
forAll :: (Eq a, Carrier sig m, Member Polytype sig) => a -> m a -> m a
|
||||
forAll n body = send (PForAll (Data.Scope.bind1 n body))
|
||||
forAll n body = send (PForAll (abstract1 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
|
||||
@ -122,12 +122,11 @@ typecheckingAnalysis
|
||||
, Member Fresh sig
|
||||
, Member (State (Set.Set Constraint)) sig
|
||||
, Member (State (Heap User (Term Monotype Meta))) sig
|
||||
, MonadFail m
|
||||
)
|
||||
=> Analysis User (Term Monotype Meta) m
|
||||
typecheckingAnalysis = Analysis{..}
|
||||
where alloc = pure
|
||||
bind _ _ = pure ()
|
||||
bind _ _ m = m
|
||||
lookupEnv = pure . Just
|
||||
deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList
|
||||
assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty))
|
||||
@ -149,9 +148,8 @@ typecheckingAnalysis = Analysis{..}
|
||||
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
|
||||
record fields = pure (Term (Record (Map.fromList fields)))
|
||||
_ ... m = pure (Just m)
|
||||
|
||||
|
||||
data Constraint = Term Monotype Meta :===: Term Monotype Meta
|
||||
|
||||
@ -2,16 +2,19 @@
|
||||
ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
|
||||
module Data.Core
|
||||
( Core(..)
|
||||
, Edge(..)
|
||||
, let'
|
||||
, block
|
||||
, lam
|
||||
, lam'
|
||||
, lams
|
||||
, lams'
|
||||
, unlam
|
||||
, rec
|
||||
, (>>>)
|
||||
, unseq
|
||||
, unseqs
|
||||
, (>>>=)
|
||||
, unbind
|
||||
, unstatement
|
||||
, do'
|
||||
, unstatements
|
||||
, (:<-)(..)
|
||||
, lam
|
||||
, lams
|
||||
, unlam
|
||||
, ($$)
|
||||
, ($$*)
|
||||
, unapply
|
||||
@ -21,8 +24,7 @@ module Data.Core
|
||||
, if'
|
||||
, string
|
||||
, load
|
||||
, edge
|
||||
, frame
|
||||
, record
|
||||
, (...)
|
||||
, (.=)
|
||||
, ann
|
||||
@ -34,9 +36,11 @@ module Data.Core
|
||||
import Control.Applicative (Alternative (..))
|
||||
import Control.Effect.Carrier
|
||||
import Control.Monad.Module
|
||||
import Data.Bifunctor (Bifunctor (..))
|
||||
import Data.Foldable (foldl')
|
||||
import Data.List.NonEmpty
|
||||
import Data.List.NonEmpty (NonEmpty (..))
|
||||
import Data.Loc
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Stack
|
||||
@ -45,14 +49,18 @@ import Data.Text (Text)
|
||||
import GHC.Generics (Generic1)
|
||||
import GHC.Stack
|
||||
|
||||
data Edge = Lexical | Import
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Core f a
|
||||
= Let User
|
||||
-- | Recursive local binding of a name in a scope; strict evaluation of the name in the body will diverge.
|
||||
--
|
||||
-- Simultaneous (and therefore potentially mutually-recursive) bidnings can be made by binding a 'Record' recursively within 'Rec' and projecting from it with ':.'.
|
||||
= Rec (Named (Scope () f a))
|
||||
-- | Sequencing without binding; analogous to '>>' or '*>'.
|
||||
| f a :>> f a
|
||||
| Lam (Ignored User) (Scope () f a)
|
||||
-- | Sequencing with binding; analogous to '>>='.
|
||||
--
|
||||
-- Bindings made with :>>= are sequential, i.e. the name is not bound within the value, only within the consequence.
|
||||
| Named (f a) :>>= Scope () f a
|
||||
| Lam (Named (Scope () f a))
|
||||
-- | Function application; analogous to '$'.
|
||||
| f a :$ f a
|
||||
| Unit
|
||||
@ -61,18 +69,19 @@ data Core f a
|
||||
| String Text
|
||||
-- | Load the specified file (by path).
|
||||
| Load (f a)
|
||||
| Edge Edge (f a)
|
||||
-- | Allocation of a new frame.
|
||||
| Frame
|
||||
| f a :. f a
|
||||
-- | A record mapping some keys to some values.
|
||||
| Record [(User, f a)]
|
||||
-- | Projection from a record.
|
||||
| f a :. User
|
||||
-- | Assignment of a value to the reference returned by the lhs.
|
||||
| f a := f a
|
||||
| Ann Loc (f a)
|
||||
deriving (Foldable, Functor, Generic1, Traversable)
|
||||
|
||||
infixr 1 :>>
|
||||
infixl 9 :$
|
||||
infixl 4 :.
|
||||
infixr 1 :>>=
|
||||
infixl 8 :$
|
||||
infixl 9 :.
|
||||
infix 3 :=
|
||||
|
||||
instance HFunctor Core
|
||||
@ -83,48 +92,29 @@ deriving instance (Ord a, forall a . Eq a => Eq (f a)
|
||||
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Core f a)
|
||||
|
||||
instance RightModule Core where
|
||||
Let u >>=* _ = Let u
|
||||
(a :>> b) >>=* f = (a >>= f) :>> (b >>= f)
|
||||
Lam v b >>=* f = Lam v (b >>=* f)
|
||||
(a :$ b) >>=* f = (a >>= f) :$ (b >>= f)
|
||||
Unit >>=* _ = Unit
|
||||
Bool b >>=* _ = Bool b
|
||||
If c t e >>=* f = If (c >>= f) (t >>= f) (e >>= f)
|
||||
String s >>=* _ = String s
|
||||
Load b >>=* f = Load (b >>= f)
|
||||
Edge e b >>=* f = Edge e (b >>= f)
|
||||
Frame >>=* _ = Frame
|
||||
(a :. b) >>=* f = (a >>= f) :. (b >>= f)
|
||||
(a := b) >>=* f = (a >>= f) := (b >>= f)
|
||||
Ann l b >>=* f = Ann l (b >>= f)
|
||||
Rec b >>=* f = Rec ((>>=* f) <$> b)
|
||||
(a :>> b) >>=* f = (a >>= f) :>> (b >>= f)
|
||||
(a :>>= b) >>=* f = ((>>= f) <$> a) :>>= (b >>=* f)
|
||||
Lam b >>=* f = Lam ((>>=* f) <$> b)
|
||||
(a :$ b) >>=* f = (a >>= f) :$ (b >>= f)
|
||||
Unit >>=* _ = Unit
|
||||
Bool b >>=* _ = Bool b
|
||||
If c t e >>=* f = If (c >>= f) (t >>= f) (e >>= f)
|
||||
String s >>=* _ = String s
|
||||
Load b >>=* f = Load (b >>= f)
|
||||
Record fs >>=* f = Record (map (fmap (>>= f)) fs)
|
||||
(a :. b) >>=* f = (a >>= f) :. b
|
||||
(a := b) >>=* f = (a >>= f) := (b >>= f)
|
||||
Ann l b >>=* f = Ann l (b >>= f)
|
||||
|
||||
|
||||
let' :: (Carrier sig m, Member Core sig) => User -> m a
|
||||
let' = send . Let
|
||||
rec :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
|
||||
rec (Named u n) b = send (Rec (Named u (abstract1 n b)))
|
||||
|
||||
block :: (Foldable t, Carrier sig m, Member Core sig) => t (m a) -> m a
|
||||
block = maybe unit getBlock . foldMap (Just . Block)
|
||||
(>>>) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||
a >>> b = send (a :>> b)
|
||||
|
||||
newtype Block m a = Block { getBlock :: m a }
|
||||
|
||||
instance (Carrier sig m, Member Core sig) => Semigroup (Block m a) where
|
||||
Block a <> Block b = Block (send (a :>> b))
|
||||
|
||||
lam :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
|
||||
lam (Named u n) b = send (Lam u (bind1 n b))
|
||||
|
||||
lam' :: (Carrier sig m, Member Core sig) => User -> m User -> m User
|
||||
lam' u = lam (named' u)
|
||||
|
||||
lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a -> m a
|
||||
lams names body = foldr lam body names
|
||||
|
||||
lams' :: (Foldable t, Carrier sig m, Member Core sig) => t User -> m User -> m User
|
||||
lams' names body = foldr lam' body names
|
||||
|
||||
unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
|
||||
unlam n (Term sig) | Just (Lam v b) <- prj sig = pure (Named v n, instantiate (const (pure n)) b)
|
||||
unlam _ _ = empty
|
||||
infixr 1 >>>
|
||||
|
||||
unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||
unseq (Term sig) | Just (a :>> b) <- prj sig = pure (a, b)
|
||||
@ -136,16 +126,54 @@ unseqs = go
|
||||
Just (l, r) -> go l <> go r
|
||||
Nothing -> t :| []
|
||||
|
||||
(>>>=) :: (Eq a, Carrier sig m, Member Core sig) => (Named a :<- m a) -> m a -> m a
|
||||
Named u n :<- a >>>= b = send (Named u a :>>= abstract1 n b)
|
||||
|
||||
infixr 1 >>>=
|
||||
|
||||
unbind :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a)
|
||||
unbind n (Term sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
|
||||
unbind _ _ = empty
|
||||
|
||||
unstatement :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Maybe (Named a) :<- Term sig a, Term sig a)
|
||||
unstatement n t = first (first Just) <$> unbind n t <|> first (Nothing :<-) <$> unseq t
|
||||
|
||||
do' :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Maybe (Named a) :<- m a) -> m a
|
||||
do' bindings = fromMaybe unit (foldr bind Nothing bindings)
|
||||
where bind (n :<- a) v = maybe (a >>>) ((>>>=) . (:<- a)) n <$> v <|> Just a
|
||||
|
||||
unstatements :: (Member Core sig, RightModule sig) => Term sig a -> (Stack (Maybe (Named (Either Int a)) :<- Term sig (Either Int a)), Term sig (Either Int a))
|
||||
unstatements = unprefix (unstatement . Left) . fmap Right
|
||||
|
||||
data a :<- b = a :<- b
|
||||
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
|
||||
|
||||
infix 2 :<-
|
||||
|
||||
instance Bifunctor (:<-) where
|
||||
bimap f g (a :<- b) = f a :<- g b
|
||||
|
||||
|
||||
lam :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
|
||||
lam (Named u n) b = send (Lam (Named u (abstract1 n b)))
|
||||
|
||||
lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a -> m a
|
||||
lams names body = foldr lam body names
|
||||
|
||||
unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
|
||||
unlam n (Term sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
|
||||
unlam _ _ = empty
|
||||
|
||||
($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||
f $$ a = send (f :$ a)
|
||||
|
||||
infixl 9 $$
|
||||
infixl 8 $$
|
||||
|
||||
-- | Application of a function to a sequence of arguments.
|
||||
($$*) :: (Foldable t, Carrier sig m, Member Core sig) => m a -> t (m a) -> m a
|
||||
($$*) = foldl' ($$)
|
||||
|
||||
infixl 9 $$*
|
||||
infixl 8 $$*
|
||||
|
||||
unapply :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||
unapply (Term sig) | Just (f :$ a) <- prj sig = pure (f, a)
|
||||
@ -171,16 +199,13 @@ string = send . String
|
||||
load :: (Carrier sig m, Member Core sig) => m a -> m a
|
||||
load = send . Load
|
||||
|
||||
edge :: (Carrier sig m, Member Core sig) => Edge -> m a -> m a
|
||||
edge e b = send (Edge e b)
|
||||
record :: (Carrier sig m, Member Core sig) => [(User, m a)] -> m a
|
||||
record fs = send (Record fs)
|
||||
|
||||
frame :: (Carrier sig m, Member Core sig) => m a
|
||||
frame = send Frame
|
||||
|
||||
(...) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||
(...) :: (Carrier sig m, Member Core sig) => m a -> User -> m a
|
||||
a ... b = send (a :. b)
|
||||
|
||||
infixl 4 ...
|
||||
infixl 9 ...
|
||||
|
||||
(.=) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||
a .= b = send (a := b)
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Core.Parser
|
||||
( module Text.Trifecta
|
||||
, core
|
||||
@ -10,8 +11,9 @@ module Data.Core.Parser
|
||||
|
||||
import Control.Applicative
|
||||
import qualified Data.Char as Char
|
||||
import Data.Core (Core, Edge(..))
|
||||
import Data.Core ((:<-) (..), Core)
|
||||
import qualified Data.Core as Core
|
||||
import Data.Foldable (foldl')
|
||||
import Data.Name
|
||||
import Data.String
|
||||
import Data.Term
|
||||
@ -48,44 +50,51 @@ core :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
core = expr
|
||||
|
||||
expr :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
expr = atom `chainl1` go where
|
||||
go = choice [ (Core....) <$ dot
|
||||
, (Core.$$) <$ notFollowedBy dot
|
||||
]
|
||||
expr = ifthenelse <|> lambda <|> rec <|> load <|> assign
|
||||
|
||||
assign :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
assign = application <**> (symbolic '=' *> rhs <|> pure id) <?> "assignment"
|
||||
where rhs = flip (Core..=) <$> application
|
||||
|
||||
application :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
application = projection `chainl1` (pure (Core.$$))
|
||||
|
||||
projection :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
projection = foldl' (Core....) <$> atom <*> many (namedValue <$ dot <*> name)
|
||||
|
||||
atom :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
atom = choice
|
||||
[ comp
|
||||
, ifthenelse
|
||||
, edge
|
||||
, lit
|
||||
, ident
|
||||
, assign
|
||||
, parens expr
|
||||
]
|
||||
|
||||
comp :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
comp = braces (Core.block <$> sepEndByNonEmpty expr semi) <?> "compound statement"
|
||||
comp = braces (Core.do' <$> sepEndByNonEmpty statement semi) <?> "compound statement"
|
||||
|
||||
statement :: (TokenParsing m, Monad m) => m (Maybe (Named User) :<- Term Core User)
|
||||
statement
|
||||
= try ((:<-) . Just <$> name <* symbol "<-" <*> expr)
|
||||
<|> (Nothing :<-) <$> expr
|
||||
<?> "statement"
|
||||
|
||||
ifthenelse :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
ifthenelse = Core.if'
|
||||
<$ reserved "if" <*> core
|
||||
<* reserved "then" <*> core
|
||||
<* reserved "else" <*> core
|
||||
<$ reserved "if" <*> expr
|
||||
<* reserved "then" <*> expr
|
||||
<* reserved "else" <*> expr
|
||||
<?> "if-then-else statement"
|
||||
|
||||
assign :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
assign = (Core..=) <$> try (lvalue <* symbolic '=') <*> core <?> "assignment"
|
||||
rec :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
rec = Core.rec <$ reserved "rec" <*> name <* symbolic '=' <*> expr <?> "recursive binding"
|
||||
|
||||
edge :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
edge = kw <*> expr where kw = choice [ Core.edge Lexical <$ reserved "lexical"
|
||||
, Core.edge Import <$ reserved "import"
|
||||
, Core.load <$ reserved "load"
|
||||
]
|
||||
load :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
load = Core.load <$ reserved "load" <*> expr
|
||||
|
||||
lvalue :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
lvalue = choice
|
||||
[ Core.let' . namedValue <$ reserved "let" <*> name
|
||||
[ projection
|
||||
, ident
|
||||
, parens expr
|
||||
]
|
||||
@ -93,20 +102,22 @@ lvalue = choice
|
||||
-- * Literals
|
||||
|
||||
name :: (TokenParsing m, Monad m) => m (Named User)
|
||||
name = named' <$> identifier <?> "name" where
|
||||
name = named' <$> identifier <?> "name"
|
||||
|
||||
lit :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
lit = let x `given` n = x <$ reserved n in choice
|
||||
[ Core.bool True `given` "#true"
|
||||
, Core.bool False `given` "#false"
|
||||
, Core.unit `given` "#unit"
|
||||
, Core.frame `given` "#frame"
|
||||
, between (string "\"") (string "\"") (Core.string . fromString <$> many ('"' <$ string "\\\"" <|> noneOf "\""))
|
||||
, lambda
|
||||
, record
|
||||
, Core.string <$> stringLiteral
|
||||
] <?> "literal"
|
||||
|
||||
record :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
record = Core.record <$ reserved "#record" <*> braces (sepEndBy ((,) <$> identifier <* symbolic ':' <*> expr) comma)
|
||||
|
||||
lambda :: (TokenParsing m, Monad m) => m (Term Core User)
|
||||
lambda = Core.lam <$ lambduh <*> name <* arrow <*> core <?> "lambda" where
|
||||
lambda = Core.lam <$ lambduh <*> name <* arrow <*> expr <?> "lambda" where
|
||||
lambduh = symbolic 'λ' <|> symbolic '\\'
|
||||
arrow = symbol "→" <|> symbol "->"
|
||||
|
||||
|
||||
@ -8,19 +8,19 @@ module Data.Core.Pretty
|
||||
, prettyCore
|
||||
) where
|
||||
|
||||
import Control.Effect.Reader
|
||||
import Data.Core
|
||||
import Data.File
|
||||
import Data.Foldable (toList)
|
||||
import Data.Name
|
||||
import Data.Scope
|
||||
import Data.Stack
|
||||
import Data.Term
|
||||
import Data.Text.Prettyprint.Doc (Pretty (..), annotate, softline, (<+>))
|
||||
import qualified Data.Text.Prettyprint.Doc as Pretty
|
||||
import Data.Text.Prettyprint.Doc
|
||||
import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
|
||||
import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
|
||||
|
||||
showCore :: Term Core User -> String
|
||||
showCore = Pretty.renderString . Pretty.layoutSmart Pretty.defaultLayoutOptions . Pretty.unAnnotate . prettyCore Ascii
|
||||
showCore = Pretty.renderString . layoutSmart defaultLayoutOptions . unAnnotate . prettyCore Ascii
|
||||
|
||||
printCore :: Term Core User -> IO ()
|
||||
printCore p = Pretty.putDoc (prettyCore Unicode p) *> putStrLn ""
|
||||
@ -31,88 +31,91 @@ showFile = showCore . fileBody
|
||||
printFile :: File (Term Core User) -> IO ()
|
||||
printFile = printCore . fileBody
|
||||
|
||||
type AnsiDoc = Pretty.Doc Pretty.AnsiStyle
|
||||
type AnsiDoc = Doc Pretty.AnsiStyle
|
||||
|
||||
keyword, symbol, strlit, primitive :: AnsiDoc -> AnsiDoc
|
||||
keyword = annotate (Pretty.colorDull Pretty.Cyan)
|
||||
symbol = annotate (Pretty.color Pretty.Yellow)
|
||||
symbol = annotate (Pretty.color Pretty.Yellow)
|
||||
strlit = annotate (Pretty.colorDull Pretty.Green)
|
||||
primitive = keyword . mappend "#"
|
||||
|
||||
type Prec = Int
|
||||
|
||||
data Style = Unicode | Ascii
|
||||
|
||||
name :: User -> AnsiDoc
|
||||
name n = encloseIf (needsQuotation n) (symbol "#{") (symbol "}") (pretty n)
|
||||
|
||||
with :: (Member (Reader Prec) sig, Carrier sig m) => Prec -> m a -> m a
|
||||
with n = local (const n)
|
||||
|
||||
inParens :: (Member (Reader Prec) sig, Carrier sig m) => Prec -> m AnsiDoc -> m AnsiDoc
|
||||
inParens amount go = do
|
||||
prec <- ask
|
||||
body <- with amount go
|
||||
pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)
|
||||
name n = if needsQuotation n then enclose (symbol "#{") (symbol "}") (pretty n) else pretty n
|
||||
|
||||
prettyCore :: Style -> Term Core User -> AnsiDoc
|
||||
prettyCore style = run . runReader @Prec 0 . go
|
||||
prettyCore style = precBody . go . fmap name
|
||||
where go = \case
|
||||
Var v -> pure (name v)
|
||||
Var v -> atom v
|
||||
Term t -> case t of
|
||||
Let a -> pure $ keyword "let" <+> name a
|
||||
a :>> b -> do
|
||||
prec <- ask @Prec
|
||||
fore <- with 12 (go a)
|
||||
aft <- with 12 (go b)
|
||||
Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
|
||||
[ keyword "rec" <+> name x
|
||||
, symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b)))
|
||||
]
|
||||
|
||||
let open = symbol ("{" <> softline)
|
||||
close = symbol (softline <> "}")
|
||||
separator = ";" <> Pretty.line
|
||||
body = fore <> separator <> aft
|
||||
Lam (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
|
||||
[ lambda <> name x, arrow <+> withPrec 0 (go (instantiate1 (pure (name x)) b)) ]
|
||||
|
||||
pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
|
||||
Record fs -> atom . group . nest 2 $ vsep [ primitive "record", block ", " (map (uncurry keyValue) fs) ]
|
||||
|
||||
Lam n f -> inParens 11 $ do
|
||||
(x, body) <- bind n f
|
||||
pure (lambda <> name x <+> arrow <+> body)
|
||||
Unit -> atom $ primitive "unit"
|
||||
Bool b -> atom $ primitive (if b then "true" else "false")
|
||||
String s -> atom . strlit $ 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
|
||||
f :$ x -> prec 8 (withPrec 8 (go f) <+> withPrec 9 (go x))
|
||||
|
||||
f :$ x -> inParens 11 $ (<+>) <$> go f <*> go x
|
||||
If con tru fal -> prec 3 . group $ vsep
|
||||
[ keyword "if" <+> precBody (go con)
|
||||
, keyword "then" <+> precBody (go tru)
|
||||
, keyword "else" <+> precBody (go fal)
|
||||
]
|
||||
|
||||
If con tru fal -> do
|
||||
con' <- "if" `appending` go con
|
||||
tru' <- "then" `appending` go tru
|
||||
fal' <- "else" `appending` go fal
|
||||
pure $ Pretty.sep [con', tru', fal']
|
||||
Load p -> prec 3 (keyword "load" <+> withPrec 9 (go p))
|
||||
item :. body -> prec 9 (withPrec 9 (go item) <> symbol "." <> name body)
|
||||
|
||||
Load p -> "load" `appending` go p
|
||||
Edge Lexical n -> "lexical" `appending` go n
|
||||
Edge Import n -> "import" `appending` go n
|
||||
item :. body -> inParens 4 $ do
|
||||
f <- go item
|
||||
g <- go body
|
||||
pure (f <> symbol "." <> g)
|
||||
|
||||
lhs := rhs -> inParens 3 $ do
|
||||
f <- go lhs
|
||||
g <- go rhs
|
||||
pure (f <+> symbol "=" <+> g)
|
||||
lhs := rhs -> prec 3 . group . nest 2 $ vsep
|
||||
[ withPrec 4 (go lhs)
|
||||
, symbol "=" <+> align (withPrec 4 (go rhs))
|
||||
]
|
||||
|
||||
-- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
|
||||
Ann _ c -> go c
|
||||
where bind (Ignored x) f = (,) x <$> go (instantiate1 (pure x) f)
|
||||
statement ->
|
||||
let (bindings, return) = unstatements (Term statement)
|
||||
statements = toList (bindings :> (Nothing :<- return))
|
||||
names = zipWith (\ i (n :<- _) -> maybe (pretty @Int i) (name . namedName) n) [0..] statements
|
||||
statements' = map (prettyStatement names) statements
|
||||
in atom (block "; " statements')
|
||||
block _ [] = braces mempty
|
||||
block s ss = encloseSep "{ " " }" s ss
|
||||
keyValue x v = name x <+> symbol ":" <+> precBody (go v)
|
||||
prettyStatement names (Just (Named (Ignored u) _) :<- t) = name u <+> arrowL <+> precBody (go (either (names !!) id <$> t))
|
||||
prettyStatement names (Nothing :<- t) = precBody (go (either (names !!) id <$> t))
|
||||
lambda = case style of
|
||||
Unicode -> symbol "λ"
|
||||
Ascii -> symbol "\\"
|
||||
arrow = case style of
|
||||
Unicode -> symbol "→"
|
||||
Ascii -> symbol "->"
|
||||
arrowL = case style of
|
||||
Unicode -> symbol "←"
|
||||
Ascii -> symbol "<-"
|
||||
|
||||
|
||||
appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
|
||||
appending k item = (keyword k <+>) <$> item
|
||||
data Prec a = Prec
|
||||
{ precLevel :: Maybe Int
|
||||
, precBody :: a
|
||||
}
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
prec :: Int -> a -> Prec a
|
||||
prec = Prec . Just
|
||||
|
||||
atom :: a -> Prec a
|
||||
atom = Prec Nothing
|
||||
|
||||
withPrec :: Int -> Prec AnsiDoc -> AnsiDoc
|
||||
withPrec d (Prec d' a)
|
||||
| maybe False (d >) d' = parens a
|
||||
| otherwise = a
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
{-# LANGUAGE DeriveTraversable, ExistentialQuantification, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, MultiParamTypeClasses, OverloadedLists, OverloadedStrings, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
|
||||
{-# LANGUAGE DeriveTraversable, LambdaCase, OverloadedLists #-}
|
||||
module Data.Name
|
||||
( User
|
||||
, Named(..)
|
||||
@ -10,7 +10,6 @@ module Data.Name
|
||||
, reservedNames
|
||||
, isSimpleCharacter
|
||||
, needsQuotation
|
||||
, encloseIf
|
||||
) where
|
||||
|
||||
import qualified Data.Char as Char
|
||||
@ -45,18 +44,14 @@ instance Ord (Ignored a) where compare _ _ = EQ
|
||||
|
||||
|
||||
reservedNames :: HashSet String
|
||||
reservedNames = [ "#true", "#false", "let", "#frame", "if", "then", "else"
|
||||
, "lexical", "import", "#unit", "load"]
|
||||
reservedNames = [ "#true", "#false", "if", "then", "else"
|
||||
, "#unit", "load", "rec", "#record"]
|
||||
|
||||
-- | Returns true if any character would require quotation or if the
|
||||
-- name conflicts with a Core primitive.
|
||||
needsQuotation :: User -> Bool
|
||||
needsQuotation u = HashSet.member (unpack u) reservedNames || Text.any (not . isSimpleCharacter) u
|
||||
|
||||
encloseIf :: Monoid m => Bool -> m -> m -> m -> m
|
||||
encloseIf True l r x = l <> x <> r
|
||||
encloseIf False _ _ x = x
|
||||
|
||||
-- | A ‘simple’ character is, loosely defined, a character that is compatible
|
||||
-- with identifiers in most ASCII-oriented programming languages. This is defined
|
||||
-- as the alphanumeric set plus @$@ and @_@.
|
||||
|
||||
@ -6,12 +6,14 @@ module Data.Scope
|
||||
, Scope(..)
|
||||
, fromScope
|
||||
, toScope
|
||||
, bind1
|
||||
, bind
|
||||
, bindEither
|
||||
, abstract1
|
||||
, abstract
|
||||
, abstractEither
|
||||
, instantiate1
|
||||
, instantiate
|
||||
, instantiateEither
|
||||
, unprefix
|
||||
, unprefixEither
|
||||
) where
|
||||
|
||||
import Control.Applicative (liftA2)
|
||||
@ -20,6 +22,7 @@ import Control.Monad ((>=>), guard)
|
||||
import Control.Monad.Module
|
||||
import Control.Monad.Trans.Class
|
||||
import Data.Function (on)
|
||||
import Data.Stack
|
||||
|
||||
data Incr a b
|
||||
= Z a
|
||||
@ -86,14 +89,14 @@ toScope = Scope . fmap (fmap pure)
|
||||
|
||||
|
||||
-- | Bind occurrences of a variable in a term, producing a term in which the variable is bound.
|
||||
bind1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
|
||||
bind1 n = bind (guard . (== n))
|
||||
abstract1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
|
||||
abstract1 n = abstract (guard . (== n))
|
||||
|
||||
bind :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
|
||||
bind f = bindEither (matchMaybe f)
|
||||
abstract :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
|
||||
abstract f = abstractEither (matchMaybe f)
|
||||
|
||||
bindEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
|
||||
bindEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
|
||||
abstractEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
|
||||
abstractEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
|
||||
|
||||
|
||||
-- | Substitute a term for the free variable in a given term, producing a closed term.
|
||||
@ -105,3 +108,25 @@ instantiate f = instantiateEither (either f pure)
|
||||
|
||||
instantiateEither :: Monad f => (Either a b -> f c) -> Scope a f b -> f c
|
||||
instantiateEither f = unScope >=> incr (f . Left) (>>= f . Right)
|
||||
|
||||
|
||||
-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @t@ using a helper function.
|
||||
--
|
||||
-- This allows us to peel a prefix of syntax, typically binders, off of a term, returning a stack of prefixing values (e.g. variables) and the outermost subterm rejected by the function.
|
||||
unprefix
|
||||
:: (Int -> t -> Maybe (a, t)) -- ^ A function taking the 0-based index into the prefix & the current term, and optionally returning a pair of the prefixing value and the inner subterm.
|
||||
-> t -- ^ The initial term.
|
||||
-> (Stack a, t) -- ^ A stack of prefixing values & the final subterm.
|
||||
unprefix from = unprefixEither (matchMaybe . from)
|
||||
|
||||
-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @b@ within a @t@ using a helper function.
|
||||
--
|
||||
-- Compared to 'unprefix', this allows the helper function to extract inner terms of a different type, for example when @t@ is a right @b@-module.
|
||||
unprefixEither
|
||||
:: (Int -> t -> Either (a, t) b) -- ^ A function taking the 0-based index into the prefix & the current term, and returning either a pair of the prefixing value and the next inner subterm of type @t@, or the final inner subterm of type @b@.
|
||||
-> t -- ^ The initial term.
|
||||
-> (Stack a, b) -- ^ A stack of prefixing values & the final subterm.
|
||||
unprefixEither from = go (0 :: Int) Nil
|
||||
where go i bs t = case from i t of
|
||||
Left (b, t) -> go (succ i) (bs :> b) t
|
||||
Right b -> (bs, b)
|
||||
|
||||
@ -6,8 +6,10 @@ module Generators
|
||||
, variable
|
||||
, boolean
|
||||
, lambda
|
||||
, record
|
||||
, apply
|
||||
, ifthenelse
|
||||
, expr
|
||||
) where
|
||||
|
||||
import Prelude hiding (span)
|
||||
@ -16,7 +18,7 @@ import Hedgehog hiding (Var)
|
||||
import qualified Hedgehog.Gen as Gen
|
||||
import qualified Hedgehog.Range as Range
|
||||
|
||||
import Data.Core
|
||||
import qualified Data.Core as Core
|
||||
import Data.Name
|
||||
import Data.Term
|
||||
|
||||
@ -24,34 +26,51 @@ import Data.Term
|
||||
-- fresh names for variables, since the length of variable names is not an
|
||||
-- interesting property as they parse regardless.
|
||||
name :: MonadGen m => m (Named User)
|
||||
name = Gen.prune ((Named . Ignored <*> id) <$> names) where
|
||||
name = Gen.prune (named' <$> names) where
|
||||
names = Gen.text (Range.linear 1 10) Gen.lower
|
||||
|
||||
boolean :: MonadGen m => m (Term Core User)
|
||||
boolean = bool <$> Gen.bool
|
||||
boolean :: MonadGen m => m (Term Core.Core User)
|
||||
boolean = Core.bool <$> Gen.bool
|
||||
|
||||
variable :: MonadGen m => m (Term Core User)
|
||||
variable :: MonadGen m => m (Term Core.Core User)
|
||||
variable = pure . namedValue <$> name
|
||||
|
||||
ifthenelse :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
||||
ifthenelse bod = Gen.subterm3 boolean bod bod if'
|
||||
ifthenelse :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
|
||||
ifthenelse bod = Gen.subterm3 boolean bod bod Core.if'
|
||||
|
||||
apply :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
||||
apply :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
|
||||
apply gen = go where
|
||||
go = Gen.recursive
|
||||
Gen.choice
|
||||
[ Gen.subterm2 gen gen ($$)]
|
||||
[ Gen.subterm2 go go ($$) -- balanced
|
||||
, Gen.subtermM go (\x -> lam <$> name <*> pure x)
|
||||
[ Gen.subterm2 gen gen (Core.$$)]
|
||||
[ Gen.subterm2 go go (Core.$$) -- balanced
|
||||
, Gen.subtermM go (\x -> Core.lam <$> name <*> pure x)
|
||||
]
|
||||
|
||||
lambda :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
||||
lambda :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
|
||||
lambda bod = do
|
||||
arg <- name
|
||||
Gen.subterm bod (lam arg)
|
||||
Gen.subterm bod (Core.lam arg)
|
||||
|
||||
atoms :: MonadGen m => [m (Term Core User)]
|
||||
atoms = [boolean, variable, pure unit, pure frame]
|
||||
record :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
|
||||
record bod = Core.record <$> Gen.list (Range.linear 0 5) ((,) . namedValue <$> name <*> bod)
|
||||
|
||||
literal :: MonadGen m => m (Term Core User)
|
||||
literal = Gen.recursive Gen.choice atoms [lambda literal]
|
||||
atoms :: MonadGen m => [m (Term Core.Core User)]
|
||||
atoms = [variable, pure Core.unit, boolean, Core.string <$> Gen.text (Range.linear 1 10) Gen.lower]
|
||||
|
||||
literal :: MonadGen m => m (Term Core.Core User)
|
||||
literal = Gen.recursive Gen.choice atoms [lambda literal, record literal]
|
||||
|
||||
expr :: MonadGen m => m (Term Core.Core User)
|
||||
expr = Gen.recursive Gen.choice atoms
|
||||
[ Gen.subtermM expr (\x -> flip Core.rec x <$> name)
|
||||
, Gen.subterm2 expr expr (Core.>>>)
|
||||
, Gen.subtermM2 expr expr (\ x y -> (Core.>>>= y) . (Core.:<- x) <$> name)
|
||||
, lambda expr
|
||||
, Gen.subterm2 expr expr (Core.$$)
|
||||
, Gen.subterm3 expr expr expr Core.if'
|
||||
, Gen.subterm expr Core.load
|
||||
, record expr
|
||||
, Gen.subtermM expr (\ x -> (x Core....) . namedValue <$> name)
|
||||
, Gen.subterm2 expr expr (Core..=)
|
||||
]
|
||||
|
||||
@ -41,6 +41,7 @@ parserProps = testGroup "Parsing: roundtripping"
|
||||
, testProperty "if/then/else" . prop_roundtrips . Gen.ifthenelse $ Gen.variable
|
||||
, testProperty "lambda" . prop_roundtrips $ Gen.lambda Gen.literal
|
||||
, testProperty "function application" . prop_roundtrips $ Gen.apply Gen.variable
|
||||
, testProperty "expressions" . prop_roundtrips $ Gen.expr
|
||||
]
|
||||
|
||||
-- * Parser specs
|
||||
@ -68,7 +69,7 @@ assert_application_left_associative :: Assertion
|
||||
assert_application_left_associative = "f g h" `parsesInto` (f $$ g $$ h)
|
||||
|
||||
assert_push_left_associative :: Assertion
|
||||
assert_push_left_associative = "f.g.h" `parsesInto` (f ... g ... h)
|
||||
assert_push_left_associative = "f.g.h" `parsesInto` (f ... "g" ... "h")
|
||||
|
||||
assert_ascii_lambda_parse :: Assertion
|
||||
assert_ascii_lambda_parse = "\\a -> a" `parsesInto` lam (named' "a") a
|
||||
@ -79,12 +80,6 @@ assert_unicode_lambda_parse = "λa → a" `parsesInto` lam (named' "a") a
|
||||
assert_quoted_name_parse :: Assertion
|
||||
assert_quoted_name_parse = "#{(NilClass)}" `parsesInto` pure "(NilClass)"
|
||||
|
||||
assert_let_dot_precedence :: Assertion
|
||||
assert_let_dot_precedence = "let a = f.g.h" `parsesInto` (let' "a" .= (f ... g ... h))
|
||||
|
||||
assert_let_in_push_precedence :: Assertion
|
||||
assert_let_in_push_precedence = "f.let g = h" `parsesInto` (f ... (let' "g" .= h))
|
||||
|
||||
parserSpecs :: TestTree
|
||||
parserSpecs = testGroup "Parsing: simple specs"
|
||||
[ testCase "true/false" assert_booleans_parse
|
||||
@ -95,12 +90,12 @@ parserSpecs = testGroup "Parsing: simple specs"
|
||||
, testCase "lambda with ASCII syntax" assert_ascii_lambda_parse
|
||||
, testCase "lambda with unicode syntax" assert_unicode_lambda_parse
|
||||
, testCase "quoted names" assert_quoted_name_parse
|
||||
, testCase "let + dot precedence" assert_let_dot_precedence
|
||||
, testCase "let in push" assert_let_in_push_precedence
|
||||
]
|
||||
|
||||
assert_roundtrips :: File (Term Core User) -> Assertion
|
||||
assert_roundtrips (File _ core) = parseEither Parse.core (showCore core) @?= Right (stripAnnotations core)
|
||||
assert_roundtrips (File _ core) = case parseEither Parse.core (showCore core) of
|
||||
Right v -> v @?= stripAnnotations core
|
||||
Left e -> assertFailure e
|
||||
|
||||
parserExamples :: TestTree
|
||||
parserExamples = testGroup "Parsing: Eval.hs examples"
|
||||
|
||||
Loading…
Reference in New Issue
Block a user