feat: Human-friendly metavariable printing #54

croyzor · 2024-11-11T19:04:53Z

Closes #3.

There are a couple of open questions here:

What's a better name than nameMap? I kind of like mnemonics as we use for the user-provided names of holes
What's your favourite factoring of the repeated req AskNames >>= \nm -> showRow nm pattern?

I have a hunch this could look nicer after we tackle #23.

New test case vec_length2.brat reveals an error, which I plan to fix in #38.
(This bit of code is driving me up the wall 😅)

acl-cqc · 2024-11-14T13:02:24Z

Naming. I reckon the current UserName should be QualName. Might as well be a newtype, rather than data, too, with the constructor also called QualName.

Then, the names here that we show to the user can be UserName...?

Failing that, hmmm, VarName? It's not good as many of our names can stand for variables. UserVarName is too long and directs me back down the QualName route. SourceCodeName, also too long - and we can't abbreviate to SrcName because we have Src's everywhere.

EDIT: VisName (yes short for visible), SurfaceName?

acl-cqc · 2024-12-03T19:29:44Z

brat/Brat/Checker/Helpers.hs

-ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showSig (rowToSig xs)
+ensureEmpty str xs = do
+  nm <- req AskNames
+  err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showRow nm xs


I guess there is no easy equivalent of format! that we can partially apply to give a function from (string to insert into the middle) -> (another string with that inserted) ?

Not as far as I'm aware 😔

acl-cqc · 2024-12-03T19:32:17Z

brat/Brat/Syntax/Core.hs

@@ -85,7 +85,7 @@ instance Show (Term d k) where
  show (VHole (name, _)) = '?' : name
  show Empty = "()"
  show (a :|: b) = bracket PJuxtPull a ++ ", " ++ bracket PJuxtPull b
-  show Pass = "pass"
+  show Pass = ".."


This is a drive-by fix - the surface syntax for the Pass operator is .., not pass

brat/Brat/Syntax/Common.hs

acl-cqc · 2024-12-03T19:36:13Z

brat/Brat/Syntax/Value.hs

   where
    arrow = case modey :: Modey m of
      Braty -> "->"
      Kerny -> "-o"

+instance MODEY m => Show (CTy m n) where
+  show = showWithMetas M.empty


This sounds like we'll end up showing CTy's without user-names by accident....do we really need it?

I think you're right. 9c5f374d addresses this and most of the other comments

acl-cqc · 2024-12-03T20:32:07Z

brat/Brat/Syntax/Value.hs

-   where
-    helper :: MODEY m => Some (Ro m n) -> String
-    helper (Some ro) = show ro
+instance MODEY m => Show (Ro m bot top) where


acl-cqc · 2024-12-03T20:38:18Z

brat/Brat/Syntax/Value.hs

-  show (NumValue 0 g) = show g
-  show (NumValue n Constant0) = show n
-  show (NumValue n g) = show n ++ " + " ++ show g
+instance ShowWithMetas x => ShowWithMetas (NumVal x) where


Hmmm, how about fmap-ing showWithMetas over the variable to give a NumVal String (or NumVal of something that can be Shown)

This does kinda work, in that it saves a bunch of code, but results in error messages containing significantly more quotes - as show on a string produces that string in quotes. So maybe not. Shame!

acl-cqc · 2024-12-03T20:41:09Z

brat/Brat/Syntax/Value.hs

@@ -602,3 +660,13 @@ stkLen (zx :<< _) = Sy (stkLen zx)
 numValIsConstant :: NumVal (VVar Z) -> Maybe Integer
 numValIsConstant (NumValue up Constant0) = pure up
 numValIsConstant _ = Nothing
+
+showRow :: ShowWithMetas ty => M.Map End String -> [(NamedPort e, ty)] -> String


Hmmm, this now looks a bit like

instance ShowWithMetas ty => ShowWithMetas [(NamedPort e, ty)]

Although just using showWithMetas when we used to use showRow might be quite a jump...

I'm not sure about replacing showRow like this... showRow definitely needs to showWithMetasbecause it's makes a user facing string, but I'm not sure that encompasses all uses of theRo` data structure

acl-cqc · 2024-12-04T09:27:32Z

brat/Brat/Syntax/Common.hs

@@ -164,6 +174,8 @@ deriving instance Eq io => Eq (CType' io)
 instance Semigroup (CType' (PortName, ty)) where
  (ss :-> ts) <> (us :-> vs) = (ss <> us) :-> (ts <> vs)

+type UserNameMap = M.Map End String


How about calling this NamesForMetas or NamesForEnds? (Is "Metas" a new term in this PR and if so do we want to suddenly introduce it like so, or is it a term we've been using in the code previously?

I don't think "Metas" is a term used in the code base per se, but it certainly comes up when talking about the code base! Otherwise we'd refer to these as global Names? For this reason, I'm reluctant to call the things we call the Names "Names" 😅

Ok, I have come round to calling this UserNameMap (or UserNamesForEnds I guess). But I think we should probably rename ShowWithMetas to Show(With)UserNames.

acl-cqc

Ok, looking good, let's

separate out from fix: False positive in type equality #75 (or base off that if you think that'll resolve first!)
rename ShowWithMetas. Really it's "show with usernames for metas" so I think that's probably just ShowUserNames or ShowWithUserNames (how about ShowUserNamed ?)
what's going on with refactor: Use a structure with variable names and port names #23 ? Is that a tidyup of this? would it replace the yet-another-thing-in-the-store?
I will have a quick go about my NumVal fmap suggestion and see if it doesn't work

acl-cqc · 2025-01-13T16:59:54Z

brat/Brat/Checker/Helpers.hs

@@ -67,8 +69,10 @@ pull1PortRo :: MODEY m
 -- TODO: Make an `Error` constructor for this
 pull1PortRo _ p _ R0 = fail $ "Port not found: " ++ p
 pull1PortRo m p stuff (RPr (p', ty) ro)
- | p == p' = if portNameExists m p ro
-   then err (AmbiguousPortPull p (show (RPr (p', ty) ro)))
+ | p == p' = do


Good to keep the scope small, this doesn't cost you anything in line count:

Suggested change

| p == p' = do

| p == p' = if portNameExists m p ro

then do

names <- req AskNames

err (AmbiguousPortPull p (showWithMetas names (RPr (p', ty) ro)))

else pure ((p', ty), rebuildRo m ro (stuff <>> []))

acl-cqc · 2025-01-13T17:01:56Z

brat/Brat/Checker/Monad.hs

@@ -281,6 +283,12 @@ handler (Req s k) ctx g
                        if M.member e hset
                        then handler (k ()) (ctx { hopes = M.delete e hset }) g
                        else Left (dumbErr (InternalError ("Trying to remove unknown Hope: " ++ show e)))
+      NameMeta end name -> let names = userNames (store ctx) in
+                             case M.lookup end names of
+                               Just oldName -> error $ "Trying to name end (" ++ show end ++ ")\nas " ++ show name ++ " but it's already called " ++ oldName


The \n in the middle here looks a bit weird, is that what you want?

acl-cqc · 2025-01-13T17:03:05Z

brat/Brat/Checker/SolveHoles.hs

@@ -83,8 +83,11 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
  when (or [M.member ie hopes | InEnd ie <- ends]) $ typeErr "ends were in hopeset"
  case ends of
    [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
-    [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined
-    _es -> error "TODO: must wait for one or the other to become more defined"
+    -- variables are trivially the same, even if undefined, but the values may


Looks like this PR has got muddled up with #75

acl-cqc · 2025-01-13T17:06:27Z

brat/Brat/Checker/SolvePatterns.hs

@@ -193,6 +193,9 @@ unify l k r = do

 -- Solve a metavariable statically - don't do anything dynamic
 -- Once a metavariable is solved, we expect to not see it again in a normal form.
+--
+-- N.B. We should try harder to preserve order here for more comprehensible


How about a tracking issue with all the ways to improve error messages ;)

acl-cqc · 2025-01-13T17:10:14Z

brat/Brat/Compiler.hs

@@ -64,11 +66,11 @@ writeDot libDirs file out = do
  isMain _ = False
 -}

-newtype CompilingHoles = CompilingHoles [TypedHole]
+data CompilingHoles = CompilingHoles UserNameMap [TypedHole]


Worth adding a comment that this is an error. Or just rename to CompilingHolesError

acl-cqc · 2025-01-13T17:11:14Z

brat/Brat/Eval.hs

+  then pure (Right ())
+  else do
+    names <- req AskNames
+    let msg = TypeMismatch tm (showWithMetas names exp) (showWithMetas names act)


let msg = --> pure $ Left $

acl-cqc · 2025-01-13T17:13:38Z

brat/Brat/Syntax/Common.hs

@@ -164,6 +174,8 @@ deriving instance Eq io => Eq (CType' io)
 instance Semigroup (CType' (PortName, ty)) where
  (ss :-> ts) <> (us :-> vs) = (ss <> us) :-> (ts <> vs)

+type UserNameMap = M.Map End String


Ok, I have come round to calling this UserNameMap (or UserNamesForEnds I guess). But I think we should probably rename ShowWithMetas to Show(With)UserNames.

acl-cqc · 2025-01-13T17:21:43Z

brat/Brat/Checker/Monad.hs

@@ -281,6 +283,12 @@ handler (Req s k) ctx g
                        if M.member e hset
                        then handler (k ()) (ctx { hopes = M.delete e hset }) g
                        else Left (dumbErr (InternalError ("Trying to remove unknown Hope: " ++ show e)))
+      NameMeta end name -> let names = userNames (store ctx) in


How about making the name an extra Maybe parameter to Declare?

(I say Maybe - we could then even turn Nothings into integer indices, say, to make them more compact than the rather-complex VPar End notation. Using len nameMap or something)

acl-cqc · 2025-01-13T17:23:21Z

brat/Brat/Checker/Helpers.hs

@@ -125,18 +129,25 @@ pullPorts toPort showFn to_pull types =
      ([found], remaining) -> pure (found, remaining)
      (_, _) -> err $ AmbiguousPortPull p (showFn available)

-ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
+combineDisjointEnvs :: M.Map QualName v -> M.Map QualName v -> Checking (M.Map QualName v)


Isn't this still in Checker.hs as well? Is this one used?

acl-cqc · 2025-01-13T17:58:05Z

brat/Brat/Syntax/Value.hs

+  showWithMetas m (StrictMonoFun sm) = showWithMetas m sm
+
+instance ShowWithMetas x => Show (Fun00 x) where
+  show = showWithMetas M.empty


I am a bit worried about all these showWithMetas M.empty. Removing a few threw (so that use of Show raised an error) pointed me at many places where I could have been using showWithMetas with a UserNameMap from the Checking monad, as well as a few where that was not available (but in those cases, presumably it would be better to use the UserNameMap if it had been available, so at the least, good to make it obvious that we'd like to route the map in at some point).

Possibly we need it for tests. I wonder about declaring that in the test module though?

acl-cqc · 2025-01-13T18:15:58Z

You can see my playing around in branch acl/metas4humans, not all commits compile, but I got some mileage out of showRow' and showWithMetas' in 7bef03d and I reckon some more like that could help ease the pain slightly

croyzor requested a review from acl-cqc November 11, 2024 19:04

croyzor force-pushed the feat/metas4humans branch from e0963ab to 303025f Compare November 19, 2024 11:48

croyzor changed the base branch from main to refactor/qualname November 19, 2024 11:49

croyzor self-assigned this Nov 20, 2024

Base automatically changed from refactor/qualname to main November 25, 2024 17:09

croyzor force-pushed the feat/metas4humans branch from 303025f to 42e299d Compare November 25, 2024 17:26

croyzor force-pushed the feat/metas4humans branch from 42e299d to 4e06428 Compare December 3, 2024 16:00

acl-cqc reviewed Dec 4, 2024

View reviewed changes

acl-cqc mentioned this pull request Dec 6, 2024

[refactor] pullports again, with StateT + mapM #64

Merged

acl-cqc mentioned this pull request Jan 6, 2025

feat: *-kinded holes which are solved by BRAT #69

Merged

croyzor added 6 commits January 13, 2025 12:41

fix: False positive in type equality

93f4c73

test: Add bad-swap test case

7ddcd22

Human readable metas

6fbef1a

Drive-by: Fix pass show

1fa7401

More test cases

bebcac5

Rename nameMap -> userNames

ff0481d

croyzor force-pushed the feat/metas4humans branch from 4e06428 to ff0481d Compare January 13, 2025 14:07

Fewer Show instances, more ShowWithMetas instances

9c5f374

croyzor requested a review from acl-cqc January 13, 2025 14:46

acl-cqc reviewed Jan 13, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Human-friendly metavariable printing #54

feat: Human-friendly metavariable printing #54

croyzor commented Nov 11, 2024

acl-cqc commented Nov 14, 2024 •

edited

Loading

acl-cqc Dec 3, 2024

croyzor Jan 13, 2025

acl-cqc Dec 3, 2024

croyzor Dec 4, 2024

acl-cqc Dec 3, 2024

croyzor Jan 13, 2025

acl-cqc Dec 3, 2024

acl-cqc Dec 3, 2024

acl-cqc Jan 13, 2025

acl-cqc Dec 3, 2024

croyzor Jan 13, 2025

acl-cqc Dec 4, 2024

croyzor Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc left a comment

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc Jan 13, 2025

acl-cqc commented Jan 13, 2025

feat: Human-friendly metavariable printing #54

Are you sure you want to change the base?

feat: Human-friendly metavariable printing #54

Conversation

croyzor commented Nov 11, 2024

acl-cqc commented Nov 14, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

acl-cqc left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

acl-cqc commented Jan 13, 2025

acl-cqc commented Nov 14, 2024 •

edited

Loading