--functor and --agda cannot be used simultaneously

[rachelambda]

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]

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]

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.

[rachelambda]

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.