Records #203

robrix · 2019-07-22T17:41:08Z

This PR replaces much of the frame machinery with a more principled approach based on first-class records (labelled products).

Depends on Scope safety #184.
Depends on Fold over Core without iter #200.
Depends on Types as syntax #201.
Depends on 🔥 Naming, Name, & Gensym #202.

robrix

Ready for review.

robrix · 2019-07-23T20:01:31Z

semantic-core/src/Analysis/Concrete.hs


 concreteAnalysis :: ( Carrier sig m
                    , Member Fresh sig
+                    , Member (Reader Env) sig


Rather than modelling the local environment explicitly in the heap, we resume using an Env for it, and modelling non-local scopes explicitly with records. Computation of scope graphs is still possible by instrumenting binds (among other things), but we get to enjoy a much simpler implementation of name binding and lookup.

robrix · 2019-07-23T20:04:02Z

semantic-core/src/Analysis/Eval.hs

+    Rec (Named (Ignored n) b) -> do
+      addr <- alloc n
+      v <- bind n addr (eval (instantiate1 (pure n) b))
+      v <$ assign addr v


Rec implements recursive bindings of the form rec x = y s.t. occurrences of x within y are bound to the result of y. It’s not strictly requisite given mutable variables, but it’s hella convenient, and easier to analyze than the equivalent mutation-based knot-tying.

robrix · 2019-07-23T20:04:33Z

semantic-core/src/Analysis/Eval.hs

+      a' <- eval a
+      addr <- alloc n
+      assign addr a'
+      bind n addr (eval (instantiate1 (pure n) b))


We once more support local variables using :>>=.

robrix · 2019-07-23T20:05:30Z

semantic-core/src/Analysis/Eval.hs

    a :. b -> do
      a' <- ref a
-      a' ... eval b
+      a' ... b >>= maybe (freeVariable (show b)) (deref' b)


Projection simply selects (the address of) a field out of a record, rather than pushing into a frame.

robrix · 2019-07-23T20:06:42Z

semantic-core/src/Analysis/Eval.hs

+          , Just "NilClass" :<- record
+            [ (__semantic_super, var "(NilClass)")
+            , (__semantic_super, var "Object")
+            , ("nil?", lam "_" (var __semantic_global ... "true"))


We look true up in __semantic_global (which is bound recursively) because it hasn’t been defined yet.

robrix · 2019-07-23T20:21:19Z

semantic-core/src/Data/Scope.hs

-, bindEither
+, abstract1
+, abstract
+, abstractEither


I renamed these to match bound.

semantic-core/src/Data/Scope.hs

robrix · 2019-07-23T20:23:10Z

semantic-core/test/Generators.hs

+  , Gen.subterm expr Core.load
+  , record expr
+  , Gen.subtermM expr (\ x -> (x Core....) . namedValue <$> name)
+  , Gen.subterm2 expr expr (Core..=)


This should be exhaustive.

robrix · 2019-07-23T20:23:27Z

semantic-core/test/Spec.hs

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


These don’t make sense any more.

robrix · 2019-07-23T20:24:10Z

semantic-core/test/Spec.hs

-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


This gives us better error messages, tho sadly I can’t seem to find a way to do the same in tripping.

patrickt · 2019-08-06T14:31:49Z

semantic-core/src/Analysis/Concrete.hs

 runFile file = traverse run file
  where run = runReader (fileLoc file)
            . runFailWithLoc
+            . runReader (mempty :: Env)


Slight nitpick: I prefer runReader @Env mempty, since I love a good visible type annotation.

Fixed in dd6d9a0.

patrickt · 2019-08-06T14:32:03Z

semantic-core/src/Analysis/Concrete.hs

-          heap <- get
-          pure (val >>= lookupConcrete heap n)
+        bind name addr m = local (Map.insert name addr) m
+        lookupEnv n = asks (Map.lookup n)


Wow, way way way way better.

patrickt · 2019-08-06T14:32:31Z

semantic-core/src/Analysis/Concrete.hs

 import qualified Data.IntMap as IntMap
 import qualified Data.IntSet as IntSet
 import           Data.Loc
 import qualified Data.Map as Map


I wonder whether strict maps are preferable? Probably something we should file an issue about.

I’m not particularly interested in the performance of the concrete analysis at the moment given that we’re only intending to use it for validation, but we can revisit that later, for sure.

patrickt · 2019-08-06T14:34:03Z

semantic-core/src/Analysis/Concrete.hs

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


We have a top-level define for __semantic_super somewhere, can we use it here?

It’s not top-level, and I’m actually pretty sure that I don’t want this to live in here long-term; it should be encoded in the compilers, so that different languages can specify their own lookup strategies. This will be important for e.g. method_missing’s semantics.

patrickt · 2019-08-06T14:54:31Z

semantic-core/src/Analysis/Concrete.hs

-          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 -> foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList frame)


Suggested change

Record frame -> foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList frame)

Record frame -> Map.foldrWithKey (\k v -> G.overlay (edge v (Right k)) G.empty frame

Great suggestion! Fixed in 28404ae.

patrickt · 2019-08-06T15:16:22Z

semantic-core/src/Data/Core/Parser.hs

+application = projection `chainl1` (pure (Core.$$))
+
+projection :: (TokenParsing m, Monad m) => m (Term Core User)
+projection = foldl' (Core....) <$> atom <*> many (namedValue <$ dot <*> name)


patrickt · 2019-08-06T15:17:49Z

semantic-core/src/Data/Core/Parser.hs

+
+statement :: (TokenParsing m, Monad m) => m (Maybe (Named User) Core.:<- Term Core User)
+statement
+  =   try ((Core.:<-) . Just <$> name <* symbol "<-" <*> expr)


Nitpick: I would give (Core.:<-) its own prefix name here, as that particular punctuation cluster is tough to read when prefixed with Core (or just import it unqualified)

Fixed in 78bd32e.

patrickt · 2019-08-06T15:20:56Z

semantic-core/src/Data/Core/Parser.hs

-  , between (string "\"") (string "\"") (Core.string . fromString <$> many ('"' <$ string "\\\"" <|> noneOf "\""))
-  , lambda
+  , record
+  , token (between (string "\"") (string "\"") (Core.string . fromString <$> many (escape <|> (noneOf "\"" <?> "non-escaped character"))))


Two questions: how does this differ from stringLiteral from the parsers package? Can we make its differences explicit in a comment?
Secondly, and nitpickingly, I prefer char for single-character parsers.

That exists?? I was looking for it but didn’t find it. TIL, thank you! 🙇

Fixed in 372ed98.

patrickt · 2019-08-06T15:21:35Z

semantic-core/src/Data/Core/Pretty.hs

+withPrec :: Int -> Prec AnsiDoc -> AnsiDoc
+withPrec d (Prec d' a)
+  | maybe False (d >) d' = parens a
+  | otherwise            = a


Loving this. Definitely an improvement on my first stabs at it.

semantic-core/src/Data/Scope.hs

@patrickt

🎩 @patrickt.

@patrickt

🎩 @patrickt.

robrix added 30 commits July 19, 2019 11:45

Simplify how we instantiate in unlam.

0115512

Move encloseIf back into Data.Core.Pretty.

ebafd64

Generalize encloseIf to any Semigroup.

de51991

Use Named to represent the binder.

83cd925

Define records of simultaneously-bound fields.

218c8f3

Define a smart constructor for records.

00beb2d

Define a recursive binder.

e259bc0

Define a smart constructor for recursive bindings.

f373ca4

Redefine records as a flat list of bindings.

1398c99

🔥 a redundant where clause.

2606e1e

Parse recursive bindings.

3459b3b

Prefix records during pretty-printing.

972a52d

Parse records.

79f5737

Define a smart-constructor for :>>.

cbf9f43

Reintroduce assignment syntax.

8c06d7b

Use >>> to define Block’s Semigroup instance.

a10cdc9

Give fixity & precedence for >>>.

15a125b

Define a smart constructor for local bindings.

6f5e578

📝 :>>=.

e809a29

Move unseq & unseqs up under >>>.

38efb33

Give fixity & precedence for :<-.

ef24642

📝 :..

bff499e

Correct the docs for Record.

f24ef8b

🔥 redundant parens.

b5a0624

🔥 Let & Frame.

db448e6

Define prog5 using lams.

1d50aec

🔥 lam'/lams'.

2a5c181

Bind the global scope recursively.

c175bc3

🔥 a bunch of redundant prefixes.

c9b328e

Define a helper for binding multiple local variables in a sequence.

94546f7

robrix added 4 commits July 23, 2019 15:44

Alignment.

15430ba

Simplify the projection rule.

41a31d1

Parse whitespace following string literals.

7c24672

Move Edge into Concrete.

a0bf65f

robrix commented Jul 23, 2019

View reviewed changes

robrix marked this pull request as ready for review July 23, 2019 20:24

robrix requested a review from a team July 23, 2019 20:24

This was referenced Jul 25, 2019

Sequence values in the abstract domain #204

Merged

Factor annotations out of Core #208

Merged

Generalize analyses over the term type #209

Merged

Scope graphs #211

Merged

robrix changed the base branch from gen-x to master August 6, 2019 15:14

Merge branch 'master' into records

339585f

robrix mentioned this pull request Aug 6, 2019

Rename User to Name #219

Merged

8 tasks

patrickt reviewed Aug 6, 2019

View reviewed changes

robrix added 12 commits August 6, 2019 11:55

Rename un/unEither to unprefix/unprefixEither.

93eba20

📝 unprefix.

7b0a415

📝 unprefix’s purpose.

ab07e5a

📝 unprefix’s parameters.

e2ec37e

Subterm.

eb2ede6

📝 unprefixEither.

7c686d1

📝 the parameters to unprefixEither.

0d2f05a

Type application.

dd6d9a0

foldrWithKey.

28404ae

🎩 @patrickt.

Pull the rhs into a where clause.

b80dd53

Don’t prefix :<-.

78bd32e

Avoid rolling our own string literal parser.

372ed98

🎩 @patrickt.

patrickt approved these changes Aug 6, 2019

View reviewed changes

robrix merged commit fb1c27b into master Aug 6, 2019

robrix deleted the records branch August 6, 2019 17:34

	Record frame -> foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList frame)
	Record frame -> Map.foldrWithKey (\k v -> G.overlay (edge v (Right k)) G.empty frame

Records #203

Records #203

Uh oh!

Conversation

robrix commented Jul 22, 2019 • edited by patrickt Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robrix left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

robrix commented Jul 22, 2019 •

edited by patrickt

Loading