crude support for custom infix operators

src/Agda2Hs/Compile/Function.hs

@@ -15,7 +15,7 @@ import qualified Language.Haskell.Exts.Build as Hs
 import Agda.Compiler.Backend
 import Agda.Compiler.Common
 
-import Agda.Syntax.Common ( NamedArg, namedArg )
+import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Literal
 import Agda.Syntax.Scope.Base ( BindingSource(LambdaBound) )
@@ -29,6 +29,7 @@ import Agda.TypeChecking.Sort ( ifIsSort )
 import Agda.Utils.Functor ( (<&>) )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Pretty ( prettyShow )
+import Agda.Utils.Lens ((^.))
 import Agda.Utils.List ( snoc )
 import Agda.Utils.Monad
 
@@ -89,7 +90,33 @@ negSucIntPat _ _ _ = __IMPOSSIBLE__
 -- The bool argument says whether we also want the type signature or just the body
 compileFun, compileFun' :: Bool -> Definition -> C [Hs.Decl ()]
 -- initialize locals when first stepping into a function
-compileFun withSig def@Defn{..} = withFunctionLocals defName $ compileFun' withSig def
+compileFun withSig def@Defn{..} = setCurrentRangeQ defName $ do
+  -- check if the function is an operator with custom fixity,
+  -- then compile the function
+  maybePrependFixity $ withFunctionLocals defName $ compileFun' withSig def
+  where
+    Function{..} = theDef
+    m = qnameModule defName
+    n = qnameName defName
+    f@(Fixity _ lvl assoc) = n ^. lensFixity
+    x = hsName $ prettyShow n
+
+    checkFixityLevel :: FixityLevel -> C (Maybe Int)
+    checkFixityLevel Unrelated = pure Nothing
+    checkFixityLevel (Related lvl) =
+      if lvl /= fromInteger (round lvl) || lvl < 0
+        then genericDocError =<< text "Invalid fixity" <+> pretty lvl
+                             <+> text "for operator" <+> prettyTCM defName
+        else pure (Just (round lvl))
+
+    maybePrependFixity comp | f /= noFixity = do
+      hsLvl <- checkFixityLevel lvl
+      let hsAssoc = case assoc of
+            NonAssoc   -> Hs.AssocNone ()
+            LeftAssoc  -> Hs.AssocLeft ()
+            RightAssoc -> Hs.AssocRight ()
+      (Hs.InfixDecl () hsAssoc hsLvl [Hs.VarOp () x]:) <$> comp
+    maybePrependFixity comp = comp
 -- inherit existing (instantiated) locals
 compileFun' withSig def@(Defn {..}) = do
   reportSDoc "agda2hs.compile" 6 $ text "compiling function: " <+> prettyTCM defName

test/Fail/Fixities.agda

@@ -0,0 +1,9 @@
+module Fail.Fixities where
+
+open import Haskell.Prelude
+
+infixl 8.5 _<+>_
+_<+>_ : Int → Int → Int
+x <+> y = x
+
+{-# COMPILE AGDA2HS _<+>_ #-}

test/Fixities.agda

@@ -25,3 +25,15 @@ mixedAssoc m f = f =<< (((f =<< m) >>= f) >>= f)
 {-# COMPILE AGDA2HS rightAssoc #-}
 {-# COMPILE AGDA2HS nonAssoc   #-}
 {-# COMPILE AGDA2HS mixedAssoc #-}
+
+infixl 7 _<+>_
+_<+>_ : Int → Int → Int
+x <+> y = x + y
+
+{-# COMPILE AGDA2HS _<+>_ #-}
+
+infixr 8 _<->_
+_<->_ : Int → Int → Int
+x <-> y = x - y
+
+{-# COMPILE AGDA2HS _<->_ #-}

test/golden/Fixities.err

@@ -0,0 +1,2 @@
+test/Fail/Fixities.agda:6,1-6
+Invalid fixity 8.5 for operator _<+>_

test/golden/Fixities.hs

@@ -14,3 +14,11 @@ nonAssoc b = (b == b) == (b == b)
 mixedAssoc :: Maybe Int -> (Int -> Maybe Int) -> Maybe Int
 mixedAssoc m f = f =<< ((f =<< m) >>= f >>= f)
 
+infixl 7 <+>
+(<+>) :: Int -> Int -> Int
+x <+> y = x + y
+
+infixr 8 <->
+(<->) :: Int -> Int -> Int
+x <-> y = x - y
+