Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(parsing): preserve whitespaces on Lam #1980

Merged
merged 5 commits into from
Aug 7, 2020

Conversation

german1608
Copy link
Collaborator

@german1608 german1608 commented Aug 6, 2020

This partially solves #1978


Lam is ready. I caught the whitespace that I thought would make more sense to write comments. Check the haddocks for more information. I did not catch the whitespace between a _lambda and an open parenthesis because I don't see why would somebody write comments there, but if you want me to handle the whitespace there as well please let me know.

An example of running this would be to:

$ dhall haskell-syntax-tree --noted <<< '\( {- A -} x {- B -} : {- C -} A) -> B'
...
    ( Lam 
        ( FunctionBinding 
            { fbSrc0 = Just 
                ( Src 
                    { srcStart = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 3
                        } 
                    , srcEnd = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 12
                        } 
                    , srcText = " {- A -} " 
                    } 
                )
            , fbVariable = "x" 
            , fbSrc1 = Just 
                ( Src 
                    { srcStart = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 13
                        } 
                    , srcEnd = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 22
                        } 
                    , srcText = " {- B -} " 
                    } 
                )
            , fbSrc2 = Just 
                ( Src 
                    { srcStart = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 23
                        } 
                    , srcEnd = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 32
                        } 
                    , srcText = " {- C -} " 
                    } 
                )
            , fbAnnotation = Note 
                ( Src 
                    { srcStart = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 32
                        } 
                    , srcEnd = SourcePos 
                        { sourceName = "(input)" 
                        , sourceLine = Pos 1
                        , sourceColumn = Pos 33
                        } 
                    , srcText = "A" 
                    } 
                ) 
                ( Var ( V "A" 0 ) )
            } 
        ) 
...

Regarding Pi, I noticed that there are two possible ways of creating it:

    -- | > Pi (FunctionBinding _ "_" _ _ A) B       ~        A  -> B
    --   > Pi (FunctionBinding _ x _ _ A) B         ~  ∀(x : A) -> B

but I feel that using FunctionBinding on the A -> B case isn't right because FunctionBinding should be used for the later case

I see we can do the following to tackle this:

  • A more strongly-typed solution is to add another constructor, say PiFree, that corresponds to A -> B. The counterpart of this approach is that we need to handle carefully other usages, although it's not so complicated
  • A weakly-typed solution is to use Either (NoBinding s a) (FunctionBinding s a) on the second parameter of the Pi constructor and use the Left constructor for the A -> B. NoBinding would include the prefix whitespace and A, although I don't need to handle that case on the jump-to-definition context.
  • Enforce Nothing on the FunctionBinding's Maybe Srcs on the A -> B.

Since it looks like preserving whitespace for Pi seems like more work than what I thought, I can add it in another PR to keep this one small

@german1608 german1608 marked this pull request as ready for review August 6, 2020 15:56
@german1608 german1608 force-pushed the feat/preserve-whitespace-on-lam-and-pi branch from 8e602ca to c567df7 Compare August 7, 2020 03:28
Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Regarding Pi:

Note that a Pi that has "_" as the type variable can also be written as ∀(_ : A) -> B. We could use that formatting when the binding contains any non-space comments.

I think it would also be useful for this discussion to have a motivating example that benefits from having comments on a Pi.

(And I somewhat feel that an issue #1978 would be the better, more permanent place for such discussions.)

dhall/src/Dhall/Normalize.hs Outdated Show resolved Hide resolved
dhall/src/Dhall/Syntax.hs Outdated Show resolved Hide resolved
Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

@mergify mergify bot merged commit 3c75ca3 into master Aug 7, 2020
@mergify mergify bot deleted the feat/preserve-whitespace-on-lam-and-pi branch August 7, 2020 16:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants