Record user names in Core.

2024-12-25 16:02:43 +03:00 · 2019-07-02 12:39:58 -04:00 · 2019-07-02 12:39:58 -04:00 · db2b72a133
commit db2b72a133
parent da7fd48cff
4 changed files with 113 additions and 107 deletions
--- a/semantic-core/src/Analysis/Eval.hs
+++ b/semantic-core/src/Analysis/Eval.hs
@ -29,10 +29,10 @@ eval :: (Carrier sig m, Member Naming sig, Member (Reader Loc) sig, MonadFail m)
 eval Analysis{..} eval = \case
  Var n -> lookupEnv' n >>= deref' n
  Core c -> case c of
-    Let n -> alloc n >>= bind n >> unit
+    Let n -> alloc (User n) >>= bind (User n) >> unit
    a :>> b -> eval a >> eval b
-    Lam b -> do
-      n <- Gen <$> gensym "lam"
+    Lam (Ignored n) b -> do
+      n <- Gen <$> gensym n
      abstract eval n (instantiate (const (pure n)) b)
    f :$ a -> do
      f' <- eval f
@ -66,8 +66,8 @@ eval Analysis{..} eval = \case
          Var n -> lookupEnv' n
          Core c -> case c of
            Let n -> do
-              addr <- alloc n
-              addr <$ bind n addr
+              addr <- alloc (User n)
+              addr <$ bind (User n) addr
            If c t e -> do
              c' <- eval c >>= asBool
              if c' then ref t else ref e
@ -78,127 +78,127 @@ eval Analysis{..} eval = \case
            c -> invalidRef (show c)


-prog1 :: File (Core Name)
-prog1 = fromBody . lam foo $ block
+prog1 :: File (Core User)
+prog1 = fromBody . lam' foo $ block
  [ let' bar .= pure foo
  , Core.if' (pure bar)
    (Core.bool False)
    (Core.bool True)
  ]
-  where (foo, bar) = (User "foo", User "bar")
+  where (foo, bar) = ("foo", "bar")

-prog2 :: File (Core Name)
+prog2 :: File (Core User)
 prog2 = fromBody $ fileBody prog1 $$ Core.bool True

-prog3 :: File (Core Name)
-prog3 = fromBody $ lams [foo, bar, quux]
+prog3 :: File (Core User)
+prog3 = fromBody $ lams' [foo, bar, quux]
  (Core.if' (pure quux)
    (pure bar)
    (pure foo))
-  where (foo, bar, quux) = (User "foo", User "bar", User "quux")
+  where (foo, bar, quux) = ("foo", "bar", "quux")

-prog4 :: File (Core Name)
+prog4 :: File (Core User)
 prog4 = fromBody
  $  let' foo .= Core.bool True
  <> Core.if' (pure foo)
    (Core.bool True)
    (Core.bool False)
-  where foo = User "foo"
+  where foo = "foo"

-prog5 :: File (Core Name)
+prog5 :: File (Core User)
 prog5 = fromBody $ block
-  [ let' (User "mkPoint") .= lam (User "_x") (lam (User "_y") (block
-    [ let' (User "x") .= pure (User "_x")
-    , let' (User "y") .= pure (User "_y")]))
-  , let' (User "point") .= pure (User "mkPoint") $$ Core.bool True $$ Core.bool False
-  , pure (User "point") Core.... pure (User "x")
-  , pure (User "point") Core.... pure (User "y") .= pure (User "point") Core.... pure (User "x")
+  [ let' "mkPoint" .= lam' "_x" (lam' "_y" (block
+    [ let' "x" .= pure "_x"
+    , 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"
  ]

-prog6 :: [File (Core Name)]
+prog6 :: [File (Core User)]
 prog6 =
  [ File (Loc "dep"  (locSpan (fromJust here))) $ block
-    [ let' (User "dep") .= Core.frame
-    , pure (User "dep") Core.... block
-      [ let' (User "var") .= Core.bool True
+    [ let' "dep" .= Core.frame
+    , pure "dep" Core.... block
+      [ let' "var" .= Core.bool True
      ]
    ]
  , File (Loc "main" (locSpan (fromJust here))) $ block
    [ load (Core.string "dep")
-    , let' (User "thing") .= pure (User "dep") Core.... pure (User "var")
+    , let' "thing" .= pure "dep" Core.... pure "var"
    ]
  ]

-ruby :: File (Core Name)
+ruby :: File (Core User)
 ruby = fromBody . ann . block $
-  [ ann (let' (User "Class") .= Core.frame)
-  , ann (pure (User "Class") Core....
-    (ann (let' (User "new") .= lam (User "self") (block
-      [ ann (let' (User "instance") .= Core.frame)
-      , ann (pure (User "instance") Core.... Core.edge Import (pure (User "self")))
-      , ann (pure (User "instance") $$$ "initialize")
+  [ 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")
      ]))))

-  , ann (let' (User "(Object)") .= Core.frame)
-  , ann (pure (User "(Object)") Core.... ann (Core.edge Import (pure (User "Class"))))
-  , ann (let' (User "Object") .= Core.frame)
-  , ann (pure (User "Object") Core.... block
-    [ ann (Core.edge Import (pure (User "(Object)")))
-    , ann (let' (User "nil?") .= lam (User "_") false)
-    , ann (let' (User "initialize") .= lam (User "self") (pure (User "self")))
-    , ann (let' __semantic_truthy .= lam (User "_") (Core.bool True))
+  , 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))
    ])

-  , ann (pure (User "Class") Core.... Core.edge Import (pure (User "Object")))
+  , ann (pure "Class" Core.... Core.edge Import (pure "Object"))

-  , ann (let' (User "(NilClass)") .= Core.frame)
-  , ann (pure (User "(NilClass)") Core.... block
-    [ ann (Core.edge Import (pure (User "Class")))
-    , ann (Core.edge Import (pure (User "(Object)")))
+  , ann (let' "(NilClass)" .= Core.frame)
+  , ann (pure "(NilClass)" Core.... block
+    [ ann (Core.edge Import (pure "Class"))
+    , ann (Core.edge Import (pure "(Object)"))
    ])
-  , ann (let' (User "NilClass") .= Core.frame)
-  , ann (pure (User "NilClass") Core.... block
-    [ ann (Core.edge Import (pure (User "(NilClass)")))
-    , ann (Core.edge Import (pure (User "Object")))
-    , ann (let' (User "nil?") .= lam (User "_") true)
-    , ann (let' __semantic_truthy .= lam (User "_") (Core.bool False))
+  , 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))
    ])

-  , ann (let' (User "(TrueClass)") .= Core.frame)
-  , ann (pure (User "(TrueClass)") Core.... block
-    [ ann (Core.edge Import (pure (User "Class")))
-    , ann (Core.edge Import (pure (User "(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' (User "TrueClass") .= Core.frame)
-  , ann (pure (User "TrueClass") Core.... block
-    [ ann (Core.edge Import (pure (User "(TrueClass)")))
-    , ann (Core.edge Import (pure (User "Object")))
+  , ann (let' "TrueClass" .= Core.frame)
+  , ann (pure "TrueClass" Core.... block
+    [ ann (Core.edge Import (pure "(TrueClass)"))
+    , ann (Core.edge Import (pure "Object"))
    ])

-  , ann (let' (User "(FalseClass)") .= Core.frame)
-  , ann (pure (User "(FalseClass)") Core.... block
-    [ ann (Core.edge Import (pure (User "Class")))
-    , ann (Core.edge Import (pure (User "(Object)")))
+  , ann (let' "(FalseClass)" .= Core.frame)
+  , ann (pure "(FalseClass)" Core.... block
+    [ ann (Core.edge Import (pure "Class"))
+    , ann (Core.edge Import (pure "(Object)"))
    ])
-  , ann (let' (User "FalseClass") .= Core.frame)
-  , ann (pure (User "FalseClass") Core.... block
-    [ ann (Core.edge Import (pure (User "(FalseClass)")))
-    , ann (Core.edge Import (pure (User "Object")))
-    , ann (let' __semantic_truthy .= lam (User "_") (Core.bool False))
+  , 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))
    ])

-  , ann (let' (User "nil")   .= pure (User "NilClass")   $$$ "new")
-  , ann (let' (User "true")  .= pure (User "TrueClass")  $$$ "new")
-  , ann (let' (User "false") .= pure (User "FalseClass") $$$ "new")
+  , ann (let' "nil"   .= pure "NilClass"   $$$ "new")
+  , ann (let' "true"  .= pure "TrueClass"  $$$ "new")
+  , ann (let' "false" .= pure "FalseClass" $$$ "new")

-  , ann (let' (User "require") .= lam (User "path") (Core.load (pure (User "path"))))
+  , ann (let' "require" .= lam' "path" (Core.load (pure "path")))
  ]
-  where -- _nil  = pure (User "nil")
-        true  = pure (User "true")
-        false = pure (User "false")
-        self $$$ method = annWith callStack $ lam (User "_x") (pure (User "_x") Core.... pure (User method) $$ pure (User "_x")) $$ self
+  where -- _nil  = pure "nil"
+        true  = pure "true"
+        false = pure "false"
+        self $$$ method = annWith callStack $ lam' "_x" (pure "_x" Core.... pure method $$ pure "_x") $$ self

-        __semantic_truthy = User "__semantic_truthy"
+        __semantic_truthy = "__semantic_truthy"


 data Analysis address value m = Analysis
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@ -7,7 +7,9 @@ module Data.Core
 , let'
 , block
 , lam
+, lam'
 , lams
+, lams'
 , unlam
 , unseq
 , unseqs
@ -62,10 +64,10 @@ instance Monad Core where


 data CoreF f a
-  = Let Name
+  = Let User
  -- | Sequencing without binding; analogous to '>>' or '*>'.
  | f a :>> f a
-  | Lam (Scope () f a)
+  | Lam (Ignored User) (Scope (Named ()) f a)
  -- | Function application; analogous to '$'.
  | f a :$ f a
  | Unit
@ -94,7 +96,7 @@ infix  3 :=
 infixl 4 :.


-let' :: Name -> Core a
+let' :: User -> Core a
 let' = Core . Let

 block :: Foldable t => t (Core a) -> Core a
@ -102,16 +104,22 @@ block cs
  | null cs   = unit
  | otherwise = foldr1 (<>) cs

-lam :: Eq a => a -> Core a -> Core a
-lam n b = Core (Lam (bind matching b))
-  where matching x | x == n    = Just ()
+lam :: Eq a => Named a -> Core a -> Core a
+lam (Named u n) b = Core (Lam u (bind matching b))
+  where matching x | x == n    = Just (Named u ())
                   | otherwise = Nothing

-lams :: (Eq a, Foldable t) => t a -> Core a -> Core a
+lam' :: User -> Core User -> Core User
+lam' u = lam (named u u)
+
+lams :: (Eq a, Foldable t) => t (Named a) -> Core a -> Core a
 lams names body = foldr lam body names

-unlam :: Alternative m => a -> Core a -> m (a, Core a)
-unlam n (Core (Lam b)) = pure (n, instantiate (const (pure n)) b)
+lams' :: Foldable t => t User -> Core User -> Core User
+lams' names body = foldr lam' body names
+
+unlam :: Alternative m => a -> Core a -> m (Named a, Core a)
+unlam n (Core (Lam v b)) = pure (Named v n, instantiate (const (pure n)) b)
 unlam _ _                = empty

 unseq :: Alternative m => Core a -> m (Core a, Core a)
@ -181,7 +189,7 @@ annWith callStack = maybe id (fmap Core . Ann) (stackLoc callStack)
 iter :: forall m n a b
     .  (forall a . m a -> n a)
     -> (forall a . CoreF n a -> n a)
-     -> (forall a . Incr () (n a) -> m (Incr () (n a)))
+     -> (forall a . Incr (Named ()) (n a) -> m (Incr (Named ()) (n a)))
     -> (a -> m b)
     -> Core a
     -> n b
@ -193,13 +201,13 @@ iter var alg k = go

 cata :: (a -> b)
     -> (forall a . CoreF (Const b) a -> b)
-     -> (Incr () b -> a)
+     -> (Incr (Named ()) b -> a)
     -> (x -> a)
     -> Core x
     -> b
 cata var alg k h = getConst . iter (coerce var) (coerce alg) (coerce k) (Const . h)

-foldCoreF :: (forall a . Incr () (n a) -> m (Incr () (n a)))
+foldCoreF :: (forall a . Incr (Named ()) (n a) -> m (Incr (Named ()) (n a)))
          -> (forall x y . (x -> m y) -> f x -> n y)
          -> (a -> m b)
          -> CoreF f a
@ -207,7 +215,7 @@ foldCoreF :: (forall a . Incr () (n a) -> m (Incr () (n a)))
 foldCoreF k go h = \case
  Let a -> Let a
  a :>> b -> go h a :>> go h b
-  Lam b -> Lam (foldScope k go h b)
+  Lam u b -> Lam u (foldScope k go h b)
  a :$ b -> go h a :$ go h b
  Unit -> Unit
  Bool b -> Bool b
--- a/semantic-core/src/Data/Core/Parser.hs
+++ b/semantic-core/src/Data/Core/Parser.hs
@ -85,15 +85,15 @@ edge = kw <*> expr where kw = choice [ Core.edge Lexical <$ reserved "lexical"

 lvalue :: (TokenParsing m, Monad m) => m (Core Name)
 lvalue = choice
-  [ Core.let' <$ reserved "let" <*> name
+  [ Core.let' . namedValue <$ reserved "let" <*> name
  , ident
  , parens expr
  ]

 -- * Literals

-name :: (TokenParsing m, Monad m) => m Name
-name = User <$> identifier <?> "name" where
+name :: (TokenParsing m, Monad m) => m (Named User)
+name = (named <*> id) <$> identifier <?> "name" where

 lit :: (TokenParsing m, Monad m) => m (Core Name)
 lit = let x `given` n = x <$ reserved n in choice
@ -105,9 +105,9 @@ lit = let x `given` n = x <$ reserved n in choice
  ] <?> "literal"

 lambda :: (TokenParsing m, Monad m) => m (Core Name)
-lambda = Core.lam <$ lambduh <*> name <* arrow <*> core <?> "lambda" where
+lambda = Core.lam <$ lambduh <*> (fmap User <$> name) <* arrow <*> core <?> "lambda" where
  lambduh = symbolic 'λ' <|> symbolic '\\'
  arrow   = symbol "→"   <|> symbol "->"

 ident :: (Monad m, TokenParsing m) => m (Core Name)
-ident = pure <$> name <?> "identifier"
+ident = pure . User . namedValue <$> name <?> "identifier"
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@ -57,12 +57,12 @@ inParens amount go = do
  body <- with amount go
  pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)

-prettify :: (Member Naming sig, Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m)
+prettify :: (Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m)
         => Style
         -> CoreF (Const (m AnsiDoc)) a
         -> m AnsiDoc
 prettify style = \case
-  Let a -> pure $ keyword "let" <+> name a
+  Let a -> pure $ keyword "let" <+> name (User a)
  Const a :>> Const b -> do
    prec <- ask @Prec
    fore <- with 12 a
@ -75,8 +75,8 @@ prettify style = \case

    pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)

-  Lam f -> inParens 11 $ do
-    (x, body) <- bind f
+  Lam n f -> inParens 11 $ do
+    (x, body) <- bind n f
    pure (lambda <> x <+> arrow <+> body)

  Frame    -> pure $ primitive "frame"
@ -107,9 +107,7 @@ prettify style = \case

  -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
  Ann _ (Const c) -> c
-  where bind f = do
-          x <- name . Gen <$> gensym ""
-          (,) x <$> local (x:) (getConst (unScope f))
+  where bind (Ignored x) f = let x' = name (User x) in (,) x' <$> local (x':) (getConst (unScope f))
        lambda = case style of
          Unicode -> symbol "λ"
          Ascii   -> symbol "\\"
@ -122,6 +120,6 @@ appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
 appending k item = (keyword k <+>) <$> item

 prettyCore :: Style -> Core Name -> AnsiDoc
-prettyCore s = run . runNaming . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) k (pure . name)
-  where k (Z ()) = asks head
+prettyCore s = run . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) k (pure . name)
+  where k (Z n) = pure (name (User (namedName n)))
        k (S n) = local (tail @AnsiDoc) n