7 files changed, 10 insertions, 11 deletions

diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 7e4a938e..c8c0dcaa 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -226,7 +226,7 @@ compFrameBuffer = \case
 
 compSemantics = map compSemantic . compList
 
-compList (A2 "Cons" a x) = a : compList x
+compList (A2 ":" a x) = a : compList x
 compList (A0 "Nil") = []
 compList x = error $ "compList: " ++ ppShow x
 
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index c17717f3..5d3a70f3 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -242,6 +242,9 @@ infixl 2 `SAppV`, `SAppH`
 pattern SBuiltin s <- SGlobal (SIName _ s)
   where SBuiltin s =  SGlobal (SIName (debugSI $ "builtin " ++ s) s)
 
+pattern ConsName <- SIName _ ":"
+  where ConsName =  SIName_ mempty (Just $ InfixR 5) ":"
+
 pattern SRHS a      = SBuiltin "_rhs"     `SAppV` a
 pattern Section e   = SBuiltin "^section" `SAppV` e
 pattern SType       = SBuiltin "'Type"
@@ -256,7 +259,7 @@ pattern HNil      = SBuiltin "HNil"
 
 -- builtin list
 pattern BList a   = SBuiltin "'List" `SAppV` a
-pattern BCons a b = SBuiltin "Cons" `SAppV` a `SAppV` b
+pattern BCons a b = SGlobal ConsName `SAppV` a `SAppV` b
 pattern BNil      = SBuiltin "Nil"
 
 getTTuple (HList (getList -> Just xs)) = xs
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 1b747e69..986a564d 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -192,7 +192,7 @@ fntable =
     , (,) "EQ"  FEQ
     , (,) "TT"  FTT
     , (,) "Nil"  FNil
-    , (,) "Cons"  FCons
+    , (,) ":"  FCons
     , (,) "'Split"  FSplit
     ]
 
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index e10ac817..9f5e1c7d 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -233,10 +233,7 @@ expect msg p i = i >>= \n -> if p n then unexpected (msg ++ " " ++ show n) else
 
 identifier name = lexemeName $ try $ expect "reserved word" (`Set.member` theReservedNames) name
 
-operator name = lexemeName $ try $ trCons <$> expect "reserved operator" (`Set.member` theReservedOpNames) name
-  where
-    trCons ":" = "Cons"
-    trCons x = x
+operator name = lexemeName $ try $ expect "reserved operator" (`Set.member` theReservedOpNames) name
 
 theReservedOpNames = Set.fromList ["::","..","=","\\","|","<-","->","@","~","=>"]
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 70525cba..8f457e49 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -404,7 +404,7 @@ parseDef =
             (af, cs) <- option (True, []) $
                  (,) True . map (second $ (,) Nothing) . concat <$ reserved "where" <*> identation True (typedIds id npsd Nothing)
              <|> (,) False <$ reservedOp "=" <*>
-                      sepBy1 ((,) <$> addFixity' upperCase
+                      sepBy1 ((,) <$> (addFixity' upperCase <|> parens (addFixity colonSymbols))
                                   <*> (mkConTy True <$> braces telescopeDataFields <|> mkConTy False <$> telescope Nothing)
                              )
                              (reservedOp "|")
diff --git a/src/LambdaCube/Compiler/Patterns.hs b/src/LambdaCube/Compiler/Patterns.hs
index a6b96d58..856de00d 100644
--- a/src/LambdaCube/Compiler/Patterns.hs
+++ b/src/LambdaCube/Compiler/Patterns.hs
@@ -92,12 +92,12 @@ pBuiltin n = pBuiltin_ (SIName (debugSI $ "Constructor_" ++ n) n)
 
 cTrue = pBuiltin "True" (Left ((CaseName "'Bool", 0), [("False", 0), ("True", 0)])) []
 cZero = pBuiltin "Zero" (Left ((CaseName "'Nat", 0), [("Zero", 0), ("Succ", 1)])) []
-cNil  = pBuiltin "Nil"  (Left ((CaseName "'List", 0), [("Nil", 0), ("Cons", 2)])) []
+cNil  = pBuiltin "Nil"  (Left ((CaseName "'List", 0), [("Nil", 0), (":", 2)])) []
 cHNil = pBuiltin "HNil" (Left (("hlistNilCase", -1), [("HNil", 0)])) []
 cList  a = pBuiltin "'List" (Right 1) [a]
 cHList a = pBuiltin "'HList" (Right 1) [a]
 cSucc  a = pBuiltin "Succ" (Left ((CaseName "'Nat", 0), [("Zero", 0), ("Succ", 1)])) [a]
-cCons  a b = pBuiltin_ (SIName_ mempty (Just $ InfixR 5) "Cons") (Left ((CaseName "'List", 0), [("Nil", 0), ("Cons", 2)])) [a, b]
+cCons  a b = pBuiltin_ ConsName (Left ((CaseName "'List", 0), [("Nil", 0), (":", 2)])) [a, b]
 cHCons a b = pBuiltin "HCons" (Left (("hlistConsCase", -1), [("HCons", 2)])) [a, b]
 
 pattern PParens p = ViewPatSimp (SBuiltin "parens") p
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index 204a9547..e7047a7e 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -175,7 +175,6 @@ renderDoc
         addParA (ComplexAtom s i d a) = ComplexAtom s i (addPar tn (Infix i) d) $ addParA a
 
         addBackquotes "'EqCTt" = "~"
-        addBackquotes "Cons" = ":"
         addBackquotes s@(c:_) | isAlpha c || c == '_' || c == '\'' = '`': s ++ "`"
         addBackquotes s = s