From 03ed4cd3aeb1fe5174024253e77bf72af4604ffb Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:34:41 -0400 Subject: [PATCH 01/18] Analyze with names in User. --- semantic-core/src/Analysis/Concrete.hs | 23 +++++++++-------------- semantic-core/src/Analysis/Eval.hs | 23 +++++++++++------------ semantic-core/src/Analysis/ImportGraph.hs | 23 ++++++++++------------- semantic-core/src/Analysis/Typecheck.hs | 15 ++++++--------- 4 files changed, 36 insertions(+), 48 deletions(-) diff --git a/semantic-core/src/Analysis/Concrete.hs b/semantic-core/src/Analysis/Concrete.hs index a13cba65bb..46f9fdb447 100644 --- a/semantic-core/src/Analysis/Concrete.hs +++ b/semantic-core/src/Analysis/Concrete.hs @@ -22,7 +22,6 @@ import Control.Effect.State import Control.Monad ((<=<), guard) import qualified Data.Core as Core import Data.File -import Data.Foldable (foldl') import Data.Function (fix) import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet @@ -35,13 +34,13 @@ import Data.Text (Text, pack) import Prelude hiding (fail) type Precise = Int -type Env = Map.Map Name Precise +type Env = Map.Map User Precise newtype FrameId = FrameId { unFrameId :: Precise } deriving (Eq, Ord, Show) data Concrete - = Closure Loc Name (Term Core.Core Name) Precise + = Closure Loc User (Term Core.Core User) Precise | Unit | Bool Bool | String Text @@ -65,22 +64,20 @@ type Heap = IntMap.IntMap Concrete -- -- >>> map fileBody (snd (concrete [File (Loc "bool" emptySpan) (Core.bool True)])) -- [Right (Bool True)] -concrete :: [File (Term Core.Core Name)] -> (Heap, [File (Either (Loc, String) Concrete)]) +concrete :: [File (Term Core.Core User)] -> (Heap, [File (Either (Loc, String) Concrete)]) concrete = run . runFresh - . runNaming . runHeap . traverse runFile runFile :: ( Carrier sig m , Effect sig , Member Fresh sig - , Member Naming sig , Member (Reader FrameId) sig , Member (State Heap) sig ) - => File (Term Core.Core Name) + => File (Term Core.Core User) -> m (File (Either (Loc, String) Concrete)) runFile file = traverse run file where run = runReader (fileLoc file) @@ -143,7 +140,7 @@ concreteAnalysis = Analysis{..} assign addr (Obj (f frame)) -lookupConcrete :: Heap -> Name -> Concrete -> Maybe Precise +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 @@ -171,7 +168,7 @@ 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 Name -> Precise -> G.Graph a) -> Heap -> G.Graph a +heapGraph :: (Precise -> Concrete -> a) -> (Either Core.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 @@ -192,7 +189,7 @@ 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.:= fromName name] + edgeAttributes _ (Slot name, _) = ["label" G.:= name] edgeAttributes _ (Edge Core.Import, _) = ["color" G.:= "blue"] edgeAttributes _ (Edge Core.Lexical, _) = ["color" G.:= "green"] edgeAttributes _ _ = [] @@ -200,15 +197,13 @@ addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes } Unit -> "()" Bool b -> pack $ show b String s -> pack $ show s - Closure (Loc p (Span s e)) n _ _ -> "\\\\ " <> fromName n <> " [" <> p <> ":" <> showPos s <> "-" <> showPos e <> "]" + Closure (Loc p (Span s e)) n _ _ -> "\\\\ " <> n <> " [" <> p <> ":" <> showPos s <> "-" <> showPos e <> "]" Obj _ -> "{}" showPos (Pos l c) = pack (show l) <> ":" <> pack (show c) - fromName (User s) = s - fromName (Gen (Gensym ss i)) = foldl' (\ ss s -> ss <> "." <> s) (pack (show i)) ss data EdgeType = Edge Core.Edge - | Slot Name + | Slot User | Value Concrete deriving (Eq, Ord, Show) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index 049f8fb358..80f82be60e 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -20,20 +20,19 @@ import Data.Functor import Data.Loc import Data.Maybe (fromJust) import Data.Name +import Data.Scope import Data.Term import Data.Text (Text) import GHC.Stack import Prelude hiding (fail) -eval :: (Carrier sig m, Member Naming sig, Member (Reader Loc) sig, MonadFail m) => Analysis address value m -> (Term Core Name -> m value) -> Term Core Name -> m value +eval :: (Carrier sig m, Member (Reader Loc) sig, MonadFail m) => Analysis address value m -> (Term Core User -> m value) -> Term Core User -> m value eval Analysis{..} eval = \case Var n -> lookupEnv' n >>= deref' n Term c -> case c of - Let n -> alloc (User n) >>= bind (User n) >> unit + Let n -> alloc n >>= bind n >> unit a :>> b -> eval a >> eval b - Lam _ b -> do - n <- Gen <$> fresh - abstract eval n (instantiate (const (pure n)) b) + Lam (Ignored n) b -> abstract eval n (incr (const n) id <$> fromScope b) f :$ a -> do f' <- eval f a' <- eval a @@ -66,8 +65,8 @@ eval Analysis{..} eval = \case Var n -> lookupEnv' n Term c -> case c of Let n -> do - addr <- alloc (User n) - addr <$ bind (User n) addr + addr <- alloc n + addr <$ bind n addr If c t e -> do c' <- eval c >>= asBool if c' then ref t else ref e @@ -203,13 +202,13 @@ ruby = fromBody . ann . block $ data Analysis address value m = Analysis - { alloc :: Name -> m address - , bind :: Name -> address -> m () - , lookupEnv :: Name -> m (Maybe address) + { alloc :: User -> m address + , bind :: User -> address -> m () + , lookupEnv :: User -> m (Maybe address) , deref :: address -> m (Maybe value) , assign :: address -> value -> m () - , abstract :: (Term Core Name -> m value) -> Name -> Term Core Name -> m value - , apply :: (Term Core Name -> m value) -> value -> value -> m value + , abstract :: (Term Core User -> m value) -> User -> Term Core User -> m value + , apply :: (Term Core User -> m value) -> value -> value -> m value , unit :: m value , bool :: Bool -> m value , asBool :: value -> m Bool diff --git a/semantic-core/src/Analysis/ImportGraph.hs b/semantic-core/src/Analysis/ImportGraph.hs index 31e55dad3d..7247462f17 100644 --- a/semantic-core/src/Analysis/ImportGraph.hs +++ b/semantic-core/src/Analysis/ImportGraph.hs @@ -22,7 +22,6 @@ import Data.Loc import qualified Data.Map as Map import Data.Name import qualified Data.Set as Set -import Data.Stack import Data.Term import Data.Text (Text) import Prelude hiding (fail) @@ -42,29 +41,27 @@ instance Monoid Value where mempty = Value Abstract mempty data Semi - = Closure Loc Name (Term Core.Core Name) Name + = Closure Loc User (Term Core.Core User) User -- FIXME: Bound String values. | String Text | Abstract deriving (Eq, Ord, Show) -importGraph :: [File (Term Core.Core Name)] -> (Heap Name Value, [File (Either (Loc, String) Value)]) +importGraph :: [File (Term Core.Core User)] -> (Heap User Value, [File (Either (Loc, String) Value)]) importGraph = run . runFresh - . runNaming - . runHeap (Gen (Gensym (Nil :> "root") 0)) + . runHeap "__semantic_root" . traverse runFile runFile :: ( Carrier sig m , Effect sig , Member Fresh sig - , Member Naming sig - , Member (Reader (FrameId Name)) sig - , Member (State (Heap Name Value)) sig + , Member (Reader (FrameId User)) sig + , Member (State (Heap User Value)) sig ) - => File (Term Core.Core Name) + => File (Term Core.Core User) -> m (File (Either (Loc, String) Value)) runFile file = traverse run file where run = runReader (fileLoc file) @@ -75,12 +72,12 @@ runFile file = traverse run file -- FIXME: decompose into a product domain and two atomic domains importGraphAnalysis :: ( Alternative m , Carrier sig m - , Member (Reader (FrameId Name)) sig + , Member (Reader (FrameId User)) sig , Member (Reader Loc) sig - , Member (State (Heap Name Value)) sig + , Member (State (Heap User Value)) sig , MonadFail m ) - => Analysis Name Value m + => Analysis User Value m importGraphAnalysis = Analysis{..} where alloc = pure bind _ _ = pure () @@ -104,7 +101,7 @@ importGraphAnalysis = Analysis{..} asString (Value (String s) _) = pure s asString _ = pure mempty frame = pure mempty - edge Core.Import (User to) = do -- FIXME: figure out some other way to do this + 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 () diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs index cc7a2423b3..1329b6db6d 100644 --- a/semantic-core/src/Analysis/Typecheck.hs +++ b/semantic-core/src/Analysis/Typecheck.hs @@ -31,7 +31,6 @@ import Data.Maybe (fromJust) import Data.Name as Name import Data.Scope import qualified Data.Set as Set -import Data.Stack import Data.Term import Data.Void import GHC.Generics (Generic1) @@ -83,28 +82,26 @@ generalize :: Term Monotype Meta -> Term (Polytype :+: Monotype) Void generalize ty = fromJust (closed (forAlls (IntSet.toList (mvs ty)) (hoistTerm R ty))) -typecheckingFlowInsensitive :: [File (Term Core.Core Name)] -> (Heap Name (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))]) +typecheckingFlowInsensitive :: [File (Term Core.Core User)] -> (Heap User (Term Monotype Meta), [File (Either (Loc, String) (Term (Polytype :+: Monotype) Void))]) typecheckingFlowInsensitive = run . runFresh - . runNaming - . runHeap (Gen (Gensym (Nil :> "root") 0)) + . runHeap "__semantic_root" . fmap (fmap (fmap (fmap generalize))) . traverse runFile runFile :: ( Carrier sig m , Effect sig , Member Fresh sig - , Member Naming sig - , Member (State (Heap Name (Term Monotype Meta))) sig + , Member (State (Heap User (Term Monotype Meta))) sig ) - => File (Term Core.Core Name) + => File (Term Core.Core User) -> m (File (Either (Loc, String) (Term Monotype Meta))) runFile file = traverse run file where run = (\ m -> do (subst, t) <- m - modify @(Heap Name (Term Monotype Meta)) (substAll subst) + modify @(Heap User (Term Monotype Meta)) (substAll subst) pure (substAll subst <$> t)) . runState (mempty :: Substitution) . runReader (fileLoc file) @@ -119,7 +116,7 @@ runFile file = traverse run file v <$ for_ bs (unify v)) . convergeTerm (fix (cacheTerm . eval typecheckingAnalysis)) -typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap Name (Term Monotype Meta))) sig, MonadFail m) => Analysis Name (Term Monotype Meta) m +typecheckingAnalysis :: (Alternative m, Carrier sig m, 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 () From baa675f2355c3497fe51da642053dc77cf8ac7a7 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:35:57 -0400 Subject: [PATCH 02/18] :fire: prime. --- semantic-core/src/Data/Name.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index cf2bb4b2d4..42b4652480 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -14,7 +14,6 @@ module Data.Name , needsQuotation , encloseIf , Gensym(..) -, prime , fresh , namespace , Naming(..) @@ -114,10 +113,6 @@ instance Pretty Gensym where where (q, r) = i `divMod` 26 alphabet = ['a'..'z'] -prime :: Gensym -> Gensym -prime (Gensym s i) = Gensym s (succ i) - - fresh :: (Carrier sig m, Member Naming sig) => m Gensym fresh = send (Fresh pure) From 59f09cc679720d4fdc0d4998ac793d3d1f647845 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:37:13 -0400 Subject: [PATCH 03/18] :fire: NamingC & runNaming. --- semantic-core/src/Data/Name.hs | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index 42b4652480..13449d2696 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -17,15 +17,9 @@ module Data.Name , fresh , namespace , Naming(..) -, runNaming -, NamingC(..) ) where import Control.Effect.Carrier -import Control.Effect.Reader -import Control.Effect.State -import Control.Monad.Fail -import Control.Monad.IO.Class import qualified Data.Char as Char import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet @@ -133,15 +127,3 @@ instance HFunctor Naming where instance Effect Naming where handle state handler (Fresh k) = Fresh (handler . (<$ state) . k) handle state handler (Namespace s m k) = Namespace s (handler (m <$ state)) (handler . fmap k) - - -runNaming :: Functor m => NamingC m a -> m a -runNaming = runReader Nil . evalState 0 . runNamingC - -newtype NamingC m a = NamingC { runNamingC :: StateC Int (ReaderC (Stack Text) m) a } - deriving (Applicative, Functor, Monad, MonadFail, MonadIO) - -instance (Carrier sig m, Effect sig) => Carrier (Naming :+: sig) (NamingC m) where - eff (L (Fresh k)) = NamingC (asks Gensym <*> get <* modify (succ @Int) >>= runNamingC . k) - eff (L (Namespace s m k)) = NamingC (StateC (\ i -> local (:> s) (evalState 0 (runNamingC m)) >>= runState i . runNamingC . k)) - eff (R other) = NamingC (eff (R (R (handleCoercible other)))) From 62c09c308b6465c6b9b1ece192b9be4ef530ba14 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:37:51 -0400 Subject: [PATCH 04/18] :fire: Naming. --- semantic-core/src/Analysis/Concrete.hs | 2 +- semantic-core/src/Data/Name.hs | 25 ------------------------- 2 files changed, 1 insertion(+), 26 deletions(-) diff --git a/semantic-core/src/Analysis/Concrete.hs b/semantic-core/src/Analysis/Concrete.hs index 46f9fdb447..761a697dde 100644 --- a/semantic-core/src/Analysis/Concrete.hs +++ b/semantic-core/src/Analysis/Concrete.hs @@ -28,7 +28,7 @@ import qualified Data.IntSet as IntSet import Data.Loc import qualified Data.Map as Map import Data.Monoid (Alt(..)) -import Data.Name hiding (fresh) +import Data.Name import Data.Term import Data.Text (Text, pack) import Prelude hiding (fail) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index 13449d2696..7d74a70acf 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -14,12 +14,8 @@ module Data.Name , needsQuotation , encloseIf , Gensym(..) -, fresh -, namespace -, Naming(..) ) where -import Control.Effect.Carrier import qualified Data.Char as Char import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet @@ -106,24 +102,3 @@ instance Pretty Gensym where pretty (Gensym _ i) = pretty (alphabet !! r : if q > 0 then show q else "") where (q, r) = i `divMod` 26 alphabet = ['a'..'z'] - -fresh :: (Carrier sig m, Member Naming sig) => m Gensym -fresh = send (Fresh pure) - -namespace :: (Carrier sig m, Member Naming sig) => Text -> m a -> m a -namespace s m = send (Namespace s m pure) - - -data Naming m k - = Fresh (Gensym -> m k) - | forall a . Namespace Text (m a) (a -> m k) - -deriving instance Functor m => Functor (Naming m) - -instance HFunctor Naming where - hmap f (Fresh k) = Fresh (f . k) - hmap f (Namespace s m k) = Namespace s (f m) (f . k) - -instance Effect Naming where - handle state handler (Fresh k) = Fresh (handler . (<$ state) . k) - handle state handler (Namespace s m k) = Namespace s (handler (m <$ state)) (handler . fmap k) From 467292d5092dec0c5b24a0a5b0b207182ed49c14 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:38:25 -0400 Subject: [PATCH 05/18] :fire: Name. --- semantic-core/src/Data/Name.hs | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index 7d74a70acf..8ad789f945 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -2,7 +2,6 @@ module Data.Name ( User , Namespaced -, Name(..) , Named(..) , named , named' @@ -31,23 +30,6 @@ type User = Text -- This corresponds to the @Agent@ type synonym described in /I Am Not a Number—I Am a Free Variable/. type Namespaced a = Gensym -> a -data Name - -- | A locally-bound, machine-generatable name. - -- - -- This should be used for locals, function parameters, and similar names which can’t escape their defining scope. - = Gen Gensym - -- | A name provided by a user. - -- - -- This should be used for names which the user provided and which other code (other functions, other modules, other packages) could call, e.g. declaration names. - | User User - deriving (Eq, Ord, Show) - -instance Pretty Name where - pretty = \case - Gen p -> pretty p - User n -> pretty n - - -- | Annotates an @a@ with a 'User'-provided name, which is ignored for '==' and 'compare'. data Named a = Named (Ignored User) a deriving (Eq, Foldable, Functor, Ord, Show, Traversable) From cda5e3d80e5906256f8d804e06a64d39f49b6b16 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:38:58 -0400 Subject: [PATCH 06/18] :fire: Namespaced. --- semantic-core/src/Data/Name.hs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index 8ad789f945..9033364c0c 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -1,7 +1,6 @@ {-# LANGUAGE DeriveTraversable, ExistentialQuantification, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, MultiParamTypeClasses, OverloadedLists, OverloadedStrings, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-} module Data.Name ( User -, Namespaced , Named(..) , named , named' @@ -25,11 +24,6 @@ import Data.Text.Prettyprint.Doc (Pretty (..)) -- | User-specified and -relevant names. type User = Text --- | The type of namespaced actions, i.e. actions occurring within some outer name. --- --- This corresponds to the @Agent@ type synonym described in /I Am Not a Number—I Am a Free Variable/. -type Namespaced a = Gensym -> a - -- | Annotates an @a@ with a 'User'-provided name, which is ignored for '==' and 'compare'. data Named a = Named (Ignored User) a deriving (Eq, Foldable, Functor, Ord, Show, Traversable) From e5330918263c66f56065616458bfbe1316fda430 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 16:39:23 -0400 Subject: [PATCH 07/18] :fire: Gensym. --- semantic-core/src/Data/Name.hs | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs index 9033364c0c..d7f644669a 100644 --- a/semantic-core/src/Data/Name.hs +++ b/semantic-core/src/Data/Name.hs @@ -11,15 +11,12 @@ module Data.Name , isSimpleCharacter , needsQuotation , encloseIf -, Gensym(..) ) where import qualified Data.Char as Char import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet -import Data.Stack import Data.Text as Text (Text, any, unpack) -import Data.Text.Prettyprint.Doc (Pretty (..)) -- | User-specified and -relevant names. type User = Text @@ -69,12 +66,3 @@ isSimpleCharacter = \case '_' -> True '?' -> True -- common in Ruby c -> Char.isAlphaNum c - - -data Gensym = Gensym (Stack Text) Int - deriving (Eq, Ord, Show) - -instance Pretty Gensym where - pretty (Gensym _ i) = pretty (alphabet !! r : if q > 0 then show q else "") - where (q, r) = i `divMod` 26 - alphabet = ['a'..'z'] From f81384767a588501d2f6dacb6776dd07fc6af7a4 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Thu, 18 Jul 2019 22:00:45 -0400 Subject: [PATCH 08/18] Reformat the signature for eval. --- semantic-core/src/Analysis/Eval.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index 80f82be60e..ea51804d70 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -26,7 +26,13 @@ import Data.Text (Text) import GHC.Stack import Prelude hiding (fail) -eval :: (Carrier sig m, Member (Reader Loc) sig, MonadFail m) => Analysis address value m -> (Term Core User -> m value) -> Term Core User -> m value +eval :: ( Carrier sig m + , Member (Reader Loc) sig + , MonadFail m + ) + => Analysis address value m + -> (Term Core User -> m value) + -> (Term Core User -> m value) eval Analysis{..} eval = \case Var n -> lookupEnv' n >>= deref' n Term c -> case c of From 7d336c9d9adaa0777a418e2a6976ed4775905f79 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 08:43:31 -0400 Subject: [PATCH 09/18] Reformat a little. --- semantic-core/src/Analysis/Eval.hs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index ea51804d70..def9b7e719 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -115,7 +115,8 @@ prog5 :: File (Term Core User) prog5 = fromBody $ block [ let' "mkPoint" .= lam' "_x" (lam' "_y" (block [ let' "x" .= pure "_x" - , let' "y" .= pure "_y"])) + , let' "y" .= 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" @@ -125,9 +126,7 @@ prog6 :: [File (Term Core User)] prog6 = [ File (Loc "dep" (locSpan (fromJust here))) $ block [ let' "dep" .= Core.frame - , pure "dep" Core.... block - [ let' "var" .= Core.bool True - ] + , pure "dep" Core.... (let' "var" .= Core.bool True) ] , File (Loc "main" (locSpan (fromJust here))) $ block [ load (Core.string "dep") From 89cdd3bda3eadd3260734a5a2e2591afae41c566 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 08:46:02 -0400 Subject: [PATCH 10/18] Reformat the signature for typecheckingAnalysis. --- semantic-core/src/Analysis/Typecheck.hs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs index 95170ee67f..998dc301b6 100644 --- a/semantic-core/src/Analysis/Typecheck.hs +++ b/semantic-core/src/Analysis/Typecheck.hs @@ -116,7 +116,15 @@ runFile file = traverse run file v <$ for_ bs (unify v)) . convergeTerm (fix (cacheTerm . eval typecheckingAnalysis)) -typecheckingAnalysis :: (Alternative m, Carrier sig m, Member Fresh sig, Member (State (Set.Set Constraint)) sig, Member (State (Heap User (Term Monotype Meta))) sig, MonadFail m) => Analysis User (Term Monotype Meta) m +typecheckingAnalysis + :: ( Alternative m + , Carrier sig m + , 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 () From 835506030bcfc9aca4fa48fd560a583aadfeec48 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 09:42:10 -0400 Subject: [PATCH 11/18] Define a fixpoint over rank-n quantified mendler-style recursive functions. --- semantic-core/src/Analysis/Eval.hs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index def9b7e719..c3fbbe6a8c 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards #-} +{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables #-} module Analysis.Eval ( eval , prog1 @@ -9,6 +9,7 @@ module Analysis.Eval , prog6 , ruby , Analysis(..) +, fix ) where import Control.Effect.Fail @@ -26,6 +27,13 @@ import Data.Text (Text) import GHC.Stack import Prelude hiding (fail) +fix :: forall f a b + . ((forall x . (x -> a) -> f x -> b) -> (forall x . (x -> a) -> f x -> b)) + -> (forall x . (x -> a) -> f x -> b) +fix f = x + where x :: (x -> a) -> f x -> b + x = f x + eval :: ( Carrier sig m , Member (Reader Loc) sig , MonadFail m From 790f4e3084769105efac87e39191cd4a19c72594 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 09:44:25 -0400 Subject: [PATCH 12/18] Revert "Define a fixpoint over rank-n quantified mendler-style recursive functions." This reverts commit 835506030bcfc9aca4fa48fd560a583aadfeec48. --- semantic-core/src/Analysis/Eval.hs | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index c3fbbe6a8c..def9b7e719 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts, LambdaCase, OverloadedStrings, RankNTypes, RecordWildCards #-} module Analysis.Eval ( eval , prog1 @@ -9,7 +9,6 @@ module Analysis.Eval , prog6 , ruby , Analysis(..) -, fix ) where import Control.Effect.Fail @@ -27,13 +26,6 @@ import Data.Text (Text) import GHC.Stack import Prelude hiding (fail) -fix :: forall f a b - . ((forall x . (x -> a) -> f x -> b) -> (forall x . (x -> a) -> f x -> b)) - -> (forall x . (x -> a) -> f x -> b) -fix f = x - where x :: (x -> a) -> f x -> b - x = f x - eval :: ( Carrier sig m , Member (Reader Loc) sig , MonadFail m From d998f66133050a875e2856a0f4a252e2208804d3 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 09:58:10 -0400 Subject: [PATCH 13/18] Give fromScope a parameter to bind over the contents of the scope. --- semantic-core/src/Analysis/Eval.hs | 2 +- semantic-core/src/Data/Core/Pretty.hs | 2 +- semantic-core/src/Data/Scope.hs | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index def9b7e719..cfa2689a8a 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -38,7 +38,7 @@ eval Analysis{..} eval = \case Term c -> case c of Let n -> alloc n >>= bind n >> unit a :>> b -> eval a >> eval b - Lam (Ignored n) b -> abstract eval n (incr (const n) id <$> fromScope b) + Lam (Ignored n) b -> abstract eval n (fromScope (incr (const (pure n)) id) b) f :$ a -> do f' <- eval f a' <- eval a diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs index 57e70c7cb4..159643f9f6 100644 --- a/semantic-core/src/Data/Core/Pretty.hs +++ b/semantic-core/src/Data/Core/Pretty.hs @@ -106,7 +106,7 @@ prettyCore style = run . runReader @Prec 0 . go (pure . name) -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. Ann _ c -> go var c - where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f) + where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope sequenceA f) lambda = case style of Unicode -> symbol "λ" Ascii -> symbol "\\" diff --git a/semantic-core/src/Data/Scope.hs b/semantic-core/src/Data/Scope.hs index 3f591a2d22..e5544adaca 100644 --- a/semantic-core/src/Data/Scope.hs +++ b/semantic-core/src/Data/Scope.hs @@ -56,11 +56,11 @@ instance HFunctor (Scope a) where hmap f = Scope . f . fmap (fmap f) . unScope instance (Eq a, Eq b, forall a . Eq a => Eq (f a), Monad f) => Eq (Scope a f b) where - (==) = (==) `on` fromScope + (==) = (==) `on` fromScope sequenceA instance (Ord a, Ord b, forall a . Eq a => Eq (f a) , forall a . Ord a => Ord (f a), Monad f) => Ord (Scope a f b) where - compare = compare `on` fromScope + compare = compare `on` fromScope sequenceA deriving instance (Show a, Show b, forall a . Show a => Show (f a)) => Show (Scope a f b) @@ -78,8 +78,8 @@ instance RightModule (Scope a) where Scope m >>=* f = Scope (fmap (>>= f) <$> m) -fromScope :: Monad f => Scope a f b -> f (Incr a b) -fromScope = unScope >=> sequenceA +fromScope :: Monad f => (Incr a (f b) -> f c) -> Scope a f b -> f c +fromScope f = unScope >=> f toScope :: Applicative f => f (Incr a b) -> Scope a f b toScope = Scope . fmap (fmap pure) From a45c029d8606632ad67faffadf5653d868583f30 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 09:59:08 -0400 Subject: [PATCH 14/18] Simplify prettyCore.go. --- semantic-core/src/Data/Core/Pretty.hs | 39 +++++++++++++-------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs index 159643f9f6..f4b01d1a52 100644 --- a/semantic-core/src/Data/Core/Pretty.hs +++ b/semantic-core/src/Data/Core/Pretty.hs @@ -56,16 +56,15 @@ inParens amount go = do pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body) prettyCore :: Style -> Term Core User -> AnsiDoc -prettyCore style = run . runReader @Prec 0 . go (pure . name) - where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc - go var = \case - Var v -> var v +prettyCore style = run . runReader @Prec 0 . go + where go = \case + Var v -> pure (name v) Term t -> case t of Let a -> pure $ keyword "let" <+> name a a :>> b -> do prec <- ask @Prec - fore <- with 12 (go var a) - aft <- with 12 (go var b) + fore <- with 12 (go a) + aft <- with 12 (go b) let open = symbol ("{" <> softline) close = symbol (softline <> "}") @@ -76,37 +75,37 @@ prettyCore style = run . runReader @Prec 0 . go (pure . name) Lam n f -> inParens 11 $ do (x, body) <- bind n f - pure (lambda <> x <+> arrow <+> body) + pure (lambda <> name x <+> arrow <+> body) Frame -> pure $ primitive "frame" Unit -> pure $ primitive "unit" Bool b -> pure $ primitive (if b then "true" else "false") String s -> pure . strlit $ Pretty.viaShow s - f :$ x -> inParens 11 $ (<+>) <$> go var f <*> go var x + f :$ x -> inParens 11 $ (<+>) <$> go f <*> go x If con tru fal -> do - con' <- "if" `appending` go var con - tru' <- "then" `appending` go var tru - fal' <- "else" `appending` go var fal + con' <- "if" `appending` go con + tru' <- "then" `appending` go tru + fal' <- "else" `appending` go fal pure $ Pretty.sep [con', tru', fal'] - Load p -> "load" `appending` go var p - Edge Lexical n -> "lexical" `appending` go var n - Edge Import n -> "import" `appending` go var n + 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 var item - g <- go var body + f <- go item + g <- go body pure (f <> symbol "." <> g) lhs := rhs -> inParens 3 $ do - f <- go var lhs - g <- go var rhs + f <- go lhs + g <- go rhs pure (f <+> symbol "=" <+> g) -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. - Ann _ c -> go var c - where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope sequenceA f) + Ann _ c -> go c + where bind (Ignored x) f = (,) x <$> go (fromScope (incr (const (pure x)) id) f) lambda = case style of Unicode -> symbol "λ" Ascii -> symbol "\\" From 66c0bffc1741a43244ad8e0946af1b9ea0353860 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 10:59:02 -0400 Subject: [PATCH 15/18] Instantiate. --- semantic-core/src/Analysis/Eval.hs | 2 +- semantic-core/src/Data/Core/Pretty.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index cfa2689a8a..e42a7ec054 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -38,7 +38,7 @@ eval Analysis{..} eval = \case Term c -> case c of Let n -> alloc n >>= bind n >> unit a :>> b -> eval a >> eval b - Lam (Ignored n) b -> abstract eval n (fromScope (incr (const (pure n)) id) b) + Lam (Ignored n) b -> abstract eval n (instantiate1 (pure n) b) f :$ a -> do f' <- eval f a' <- eval a diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs index f4b01d1a52..92280c0fd7 100644 --- a/semantic-core/src/Data/Core/Pretty.hs +++ b/semantic-core/src/Data/Core/Pretty.hs @@ -105,7 +105,7 @@ prettyCore style = run . runReader @Prec 0 . go -- 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 (fromScope (incr (const (pure x)) id) f) + where bind (Ignored x) f = (,) x <$> go (instantiate1 (pure x) f) lambda = case style of Unicode -> symbol "λ" Ascii -> symbol "\\" From 53598bd6e98bff60388745b28ae6dc01aea7faaf Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 11:00:02 -0400 Subject: [PATCH 16/18] Revert "Give fromScope a parameter to bind over the contents of the scope." This reverts commit d998f66133050a875e2856a0f4a252e2208804d3. --- semantic-core/src/Data/Scope.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/semantic-core/src/Data/Scope.hs b/semantic-core/src/Data/Scope.hs index e5544adaca..3f591a2d22 100644 --- a/semantic-core/src/Data/Scope.hs +++ b/semantic-core/src/Data/Scope.hs @@ -56,11 +56,11 @@ instance HFunctor (Scope a) where hmap f = Scope . f . fmap (fmap f) . unScope instance (Eq a, Eq b, forall a . Eq a => Eq (f a), Monad f) => Eq (Scope a f b) where - (==) = (==) `on` fromScope sequenceA + (==) = (==) `on` fromScope instance (Ord a, Ord b, forall a . Eq a => Eq (f a) , forall a . Ord a => Ord (f a), Monad f) => Ord (Scope a f b) where - compare = compare `on` fromScope sequenceA + compare = compare `on` fromScope deriving instance (Show a, Show b, forall a . Show a => Show (f a)) => Show (Scope a f b) @@ -78,8 +78,8 @@ instance RightModule (Scope a) where Scope m >>=* f = Scope (fmap (>>= f) <$> m) -fromScope :: Monad f => (Incr a (f b) -> f c) -> Scope a f b -> f c -fromScope f = unScope >=> f +fromScope :: Monad f => Scope a f b -> f (Incr a b) +fromScope = unScope >=> sequenceA toScope :: Applicative f => f (Incr a b) -> Scope a f b toScope = Scope . fmap (fmap pure) From 90c6bea5f0fa00274e0bd2f38ee1155983e03911 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 11:08:23 -0400 Subject: [PATCH 17/18] Increase the precedence of $$. --- semantic-core/src/Data/Core.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs index e3a6d8c270..31f3912caf 100644 --- a/semantic-core/src/Data/Core.hs +++ b/semantic-core/src/Data/Core.hs @@ -71,7 +71,7 @@ data Core f a deriving (Foldable, Functor, Generic1, Traversable) infixr 1 :>> -infixl 2 :$ +infixl 9 :$ infixl 4 :. infix 3 := @@ -139,7 +139,7 @@ unseqs = go ($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a f $$ a = send (f :$ a) -infixl 2 $$ +infixl 9 $$ -- | Application of a function to a sequence of arguments. ($$*) :: (Foldable t, Carrier sig m, Member Core sig) => m a -> t (m a) -> m a From 02b955819cf1a67e736e1bd52311e4a6bc5799c2 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 19 Jul 2019 11:10:40 -0400 Subject: [PATCH 18/18] Correct prog5 to construct and return a new frame. --- semantic-core/src/Analysis/Eval.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs index e42a7ec054..a90df33753 100644 --- a/semantic-core/src/Analysis/Eval.hs +++ b/semantic-core/src/Analysis/Eval.hs @@ -114,8 +114,10 @@ prog4 = fromBody $ block prog5 :: File (Term Core User) prog5 = fromBody $ block [ let' "mkPoint" .= lam' "_x" (lam' "_y" (block - [ let' "x" .= pure "_x" - , let' "y" .= pure "_y" + [ let' "this" .= Core.frame + , pure "this" Core.... let' "x" .= pure "_x" + , pure "this" Core.... let' "y" .= pure "_y" + , pure "this" ])) , let' "point" .= pure "mkPoint" $$ Core.bool True $$ Core.bool False , pure "point" Core.... pure "x"