github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-11-24 08:54:07 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into module-laws

Browse Source
This commit is contained in:
Rob Rix 2019-08-06 13:34:36 -04:00 committed by GitHub
commit 5d47b21977
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 430 additions and 377 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

103
semantic-core/src/Analysis/Concrete.hs
View File

@ -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)

216
semantic-core/src/Analysis/Eval.hs
View File

@ -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)
}

13
semantic-core/src/Analysis/ImportGraph.hs
View File

@ -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)

10
semantic-core/src/Analysis/Typecheck.hs
View File

@ -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

163
semantic-core/src/Data/Core.hs
View File

@ -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)

61
semantic-core/src/Data/Core/Parser.hs
View File

@ -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 "->"

119
semantic-core/src/Data/Core/Pretty.hs
View File

@ -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

11
semantic-core/src/Data/Name.hs
View File

@ -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 @_@.

43
semantic-core/src/Data/Scope.hs
View File

@ -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)

53
semantic-core/test/Generators.hs
View File

@ -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..=)
]

15
semantic-core/test/Spec.hs
View File

@ -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"