Nothing Special   »   [go: up one dir, main page]
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.

Sign up for GitHub

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

Jump to bottom

--functor and --agda cannot be used simultaneously #405

Closed
rachelambda opened this issue Dec 19, 2021 · 3 comments · Fixed by #406
Closed

--functor and --agda cannot be used simultaneously #405

rachelambda opened this issue Dec 19, 2021 · 3 comments · Fixed by #406
Assignees
@andreasabel
Labels
Agda Issues of the Agda backend bug position Concerning position information in parsed AST
Milestone
2.9.4

Comments

@rachelambda
Copy link
rachelambda commented Dec 19, 2021 •
edited by andreasabel
Loading

Using the --functor flag and the --agda flag simultaneously generates code which passes the agda typechecker but fails to compile. Here is a very simple example:

separator Exp ",";
Int. Exp ::= Integer

$ bnfc -m --functor --agda test.cf

Running make yield the following type errors:

[15 of 17] Compiling MAlonzo.Code.ASTTest ( MAlonzo/Code/ASTTest.hs, MAlonzo/Code/ASTTest.o )
Compilation error:

MAlonzo/Code/ASTTest.hs:22:17: error:
    • The constructor ‘AbsTest.Int’ should have 2 arguments, but has been given 1
    • In the pattern: AbsTest.Int a0
      In the declaration for pattern synonym ‘C6’
   |
22 | pattern C6 a0 = AbsTest.Int a0
   |                 ^^^^^^^^^^^^^^

MAlonzo/Code/ASTTest.hs:24:10: error:
    • Couldn't match type ‘Integer -> AbsTest.Exp' Integer’
                     with ‘AbsTest.Exp' AbsTest.BNFC'Position’
      Expected type: Integer -> T2
        Actual type: Integer -> Integer -> AbsTest.Exp' Integer
    • Probable cause: ‘AbsTest.Int’ is applied to too few arguments
      In the expression: AbsTest.Int
      In an equation for ‘check6’: check6 = AbsTest.Int
   |
24 | check6 = AbsTest.Int
   |          ^^^^^^^^^^^

MAlonzo/Code/ASTTest.hs:28:7: error:
    • The constructor ‘AbsTest.Int’ should have 2 arguments, but has been given 1
    • In the pattern: AbsTest.Int _
      In a case alternative: AbsTest.Int _ -> ()
      In the expression: case x of { AbsTest.Int _ -> () }
   |
28 |       AbsTest.Int _ -> ()
   |       ^^^^^^^^^^^^^

make: *** [Makefile:34: Main] Error 1

Looking at ASTTest.agda and AbsTest.hs we can see the issue:

  data Exp : Set where
    int : (x : Integer) → Exp

  {-# COMPILE GHC Exp = data AbsTest.Exp (AbsTest.Int) #-}
type Exp = Exp' BNFC'Position
data Exp' a = Int a Integer
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

-- | Start position (line, column) of something.

type BNFC'Position = C.Maybe (C.Int, C.Int)

All that really needs to be done is to parameterize the agda datatype, provide a translation of BNFC'Position in ASTTest.agda, correct the type signatures of agda functions handling the AST (and thereby also adding a dummy lambda to the COMPILE pragma because of the new implicit argument).

I'm currently looking into the codebase to see if I'd be able to fix this myself.
@rachelambda
Copy link
Author

It would seem that (to no ones surprise) solving this problem is harder than it first seemed, due to having to add parameters all over the agda backend to keep track of if the functor options is enabled and having to find some way to "intelligently" parameterize all types from categories correctly. I'm giving up on my own attempts.

@andreasabel andreasabel added Agda Issues of the Agda backend bug position Concerning position information in parsed AST labels Dec 21, 2021
@andreasabel
Copy link
Member
andreasabel commented Dec 21, 2021 •
edited
Loading

I think this isn't too hard to get to work.
(Maybe I originally abstained from implementing --functor for --agda since Agda did not have Agda.Builtin.Maybe then, which is needed to implement BNFC'Position. On the other hand, tuples are also needed and I added them manually... Maybe I just postponed --functor.)

On the Agda side, we could have:

data Exp' (A : Set) : Set where
    int : (a : A) (x : Integer) → Exp' A

BNFC'Position = Maybe (Pair Nat Nat)

Exp = Exp' BNFC'Position

This would limit polymorphism to level 0, but bind directly to the code that the Haskell backend produces.

@andreasabel andreasabel self-assigned this Dec 21, 2021
@andreasabel andreasabel added this to the 2.9.4 milestone Dec 21, 2021
andreasabel added a commit that referenced this issue Dec 21, 2021
@andreasabel
Fix #405: support --functor in the Agda backend
d3fd356 
This updates the generated abstract syntax (AST.agda) so that data
types are parametrized, and instantiated to #BNFCPosition.
andreasabel added a commit that referenced this issue Dec 21, 2021
@andreasabel
Testing #405: use --functor with --agda in system testsuite
7ded4a4
@andreasabel andreasabel mentioned this issue Dec 21, 2021
Merged
3 tasks
@rachelambda
Copy link
Author
rachelambda commented Dec 21, 2021 •
edited
Loading

While the PR you opened would close this particular issue, perhaps it would be nice to keep track of what features can and cannot be used simultaneously? It would be much nicer for BNFC to state that the combination is not supported than to discover later down the line, as was the case here.

andreasabel added a commit that referenced this issue Dec 22, 2021
@andreasabel
Re #405 (Agda/Functor): fix problem with underscores in category names
1eab993 
Underscores are placeholders in Agda, so e.g. the name Foo_' is
invalid, since ' by itself is not a valid name.
andreasabel added a commit that referenced this issue Dec 22, 2021
@andreasabel
Re #405: implement define for Agda/Functor by parametrizing Haskell's
80ccbfa 
Generalize `definedRules` to `definedRules'` using a configuration
record that is instantiated to both Haskell and Agda.
andreasabel added a commit that referenced this issue Dec 22, 2021
@andreasabel
CHANGELOG #405
af2cd4d
andreasabel added a commit that referenced this issue Dec 22, 2021
@andreasabel
Document --agda --functor (#405)
a964b7c 
Also, observe that the Agda backend needs at least Agda 2.6.0.
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
Fix #405: support --functor in the Agda backend
d1e5058 
This updates the generated abstract syntax (AST.agda) so that data
types are parametrized, and instantiated to #BNFCPosition.
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
Testing #405: use --functor with --agda in system testsuite
9e3a151
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
Re #405 (Agda/Functor): fix problem with underscores in category names
ce7dc51 
Underscores are placeholders in Agda, so e.g. the name Foo_' is
invalid, since ' by itself is not a valid name.
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
Re #405: implement define for Agda/Functor by parametrizing Haskell's
d9d4f4f 
Generalize `definedRules` to `definedRules'` using a configuration
record that is instantiated to both Haskell and Agda.
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
CHANGELOG #405
d16b12f
andreasabel added a commit that referenced this issue Dec 23, 2021
@andreasabel
Document --agda --functor (#405)
7d7b714 
Also, observe that the Agda backend needs at least Agda 2.6.0.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
Agda Issues of the Agda backend bug position Concerning position information in parsed AST
Projects
None yet
Milestone
2.9.4
Development

Successfully merging a pull request may close this issue.

Fix #405: support --functor in the Agda backend BNFC/bnfc
2 participants
@andreasabel @rachelambda