3 files changed, 82 insertions, 106 deletions

diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index eb7f3681..35146c86 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -246,8 +246,10 @@ pattern LabelEnd x = LabelEnd_ LEPM x
 
 label LabelFix x y = FixLabel x y
 pmLabel :: FunName -> Int -> [Exp] -> Exp -> Exp
-pmLabel _ _ _ (unlabel -> LabelEnd y) = y
-pmLabel f i xs y = PMLabel f i xs y
+pmLabel _ _ _ (unlabel'' -> LabelEnd y) = y
+pmLabel f i xs y@Neut{} = PMLabel f i xs y
+pmLabel f i xs y@Lam{} = PMLabel f i xs y
+--pmLabel f i xs y = trace_ (ppShow y) $ PMLabel f i xs y
 
 pattern UL a <- (unlabel -> a) where UL = unlabel
 
@@ -659,7 +661,6 @@ app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++
 app_ (TyCon s xs) a = TyCon s (xs ++ [a])
 app_ (Label lk x e) a = label lk (app_ x a) $ app_ e a
 app_ (LabelEnd_ k x) a = LabelEnd_ k (app_ x a)   -- ???
---app_ (PMLabel x e) a = pmLabel (neutApp x a) $ app_ e a
 app_ (Neut f) a = neutApp f a
 
 neutApp (PMLabel_ f i xs e) a
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index dd61653c..1fc7ae79 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -1,4 +1,4 @@
--- contains Haskell source code copied from Text.Parsec.Token, see below
+-- contains modified Haskell source code copied from Text.Parsec.Token, see below
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE PatternSynonyms #-}
@@ -29,7 +29,7 @@ import Control.DeepSeq
 import Text.Parsec hiding (label, Empty, State, (<|>), many)
 import qualified Text.Parsec as Pa
 import qualified Text.Parsec.Token as Pa
-import Text.ParserCombinators.Parsec.Language (GenLanguageDef (..))
+import Text.ParserCombinators.Parsec.Language (GenLanguageDef)--hiding (identStart, identLetter, opStart, opLetter, reservedOpNames)
 import qualified Text.ParserCombinators.Parsec.Language as Pa
 import Text.Parsec.Indentation hiding (Any)
 import qualified Text.Parsec.Indentation as Pa
@@ -73,12 +73,23 @@ namespace = asks snd
 {-# INLINE languageDef #-}
 languageDef :: GenLanguageDef (IndentStream (CharIndentStream String)) SourcePos InnerP
 languageDef = Pa.haskellDef
-        { Pa.identStart      = indentStreamParser $ charIndentStreamParser $ letter <|> char '_'  -- '_' is included also
-        , Pa.identLetter     = indentStreamParser $ charIndentStreamParser $ alphaNum <|> oneOf "_'#"
-        , Pa.opStart         = indentStreamParser $ charIndentStreamParser $ oneOf ":!#$%&*+./<=>?@\\^|-~"
-        , Pa.opLetter        = indentStreamParser $ charIndentStreamParser $ oneOf ":!#$%&*+./<=>?@\\^|-~"
+        { Pa.identStart      = undefined
+        , Pa.identLetter     = undefined
+        , Pa.opStart         = undefined
+        , Pa.opLetter        = undefined
         }
 
+reservedNames   = Pa.reservedNames languageDef
+reservedOpNames = Pa.reservedOpNames languageDef
+commentLine     = Pa.commentLine languageDef
+commentStart    = Pa.commentStart languageDef
+commentEnd      = Pa.commentEnd languageDef
+identStart      = letter <|> char '_'  -- '_' is included also
+identLetter     = alphaNum <|> oneOf "_'#"
+opStart         = oneOf ":!#$%&*+./<=>?@\\^|-~"
+opStart'        = oneOf "!#$%&*+./<=>?@\\^|-~"
+opLetter        = oneOf ":!#$%&*+./<=>?@\\^|-~"
+
 lexeme p = p <* (getPosition >>= setState >> whiteSpace)
 
 -------------------------------------------------------------------------------- names
@@ -202,25 +213,29 @@ switchNS = modifyLevel $ \case ExpLevel -> TypeLevel; TypeLevel -> ExpLevel
 
 -------------------------------------------------------------------------------- identifiers
 
-check msg p m = try_ msg $ mfilter p m
+maybeStartWith p i = i <|> (:) <$> satisfy p <*> i
+
+upperCase, lowerCase, symbols, colonSymbols, backquotedIdent :: P SName
+
+upperCase       = namespace >>= \ns -> tick ns <$> identifier_ (maybeStartWith (=='\'') $ if constructorNamespace ns then (:) <$> satisfy isUpper <*> many identLetter else ident) <?> "uppercase ident"
+lowerCase       = namespace >>= \ns -> identifier_ (if constructorNamespace ns then (:) <$> satisfy (\c -> isLower c || c == '_') <*> many identLetter else ident) <?> "lowercase ident"
+backquotedIdent = lexeme $ try_ "backquoted ident" $ expect "reserved word" isReservedName $ char '`' *> ident <* char '`'
+symbols         = operator_ ((:) <$> opStart' <*> many opLetter) <?> "symbols"
+colonSymbols    = trCons <$> operator_ ((:) <$> satisfy (== ':') <*> many opLetter) <?> "op symbols"
+  where
+    trCons ":" = "Cons"
+    trCons x = x
+
+expect msg p i = i >>= \n -> if (p n) then unexpected (msg ++ " " ++ show n) else return n
 
-firstCaseChar ('\'': c: _) = c
-firstCaseChar (c: _) = c
 
-upperCase, lowerCase, symbols, colonSymbols :: P SName
---upperCase NonTypeNamespace = mzero -- todo
-upperCase       = namespace >>= \ns -> (if constructorNamespace ns then check "uppercase ident" (isUpper . firstCaseChar) else id) $ tick ns <$> (identifier <|> try_ "tick ident" (('\'':) <$ char '\'' <*> identifier))
-lowerCase       = namespace >>= \ns -> (if constructorNamespace ns then check "lowercase ident" (isLower . firstCaseChar) else id) identifier
-              <|> try_ "underscore ident" (('_':) <$ char '_' <*> identifier)
-symbols         = check "symbols" ((/=':') . head) operator
-colonSymbols    = "Cons" <$ reservedOp ":" <|> check "symbols" ((==':') . head) operator
+-----------------
 
 moduleName      = {-qualified_ todo-} expNS upperCase
 patVar          = lowerCase <|> "" <$ reserved "_"
---qIdent          = {-qualified_ todo-} (lowerCase <|> upperCase)
-backquotedIdent = try_ "backquoted ident" $ lexeme $ char '`' *> ((:) <$> satisfy isAlpha <*> many (satisfy isAlphaNum)) <* char '`'
 operatorT       = symbols <|> colonSymbols <|> backquotedIdent
 varId           = lowerCase <|> parens operatorT
+--qIdent          = {-qualified_ todo-} (lowerCase <|> upperCase)
 
 {-
 qualified_ id = do
@@ -289,7 +304,7 @@ getFixity (fm, _) n = fromMaybe (InfixL, 9) $ Map.lookup n fm
 
 ----------------------------------------------------------------------
 ----------------------------------------------------------------------
--- copied from 
+-- modified version of
 --
 -- Module      :  Text.Parsec.Token
 -- Copyright   :  (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
@@ -497,10 +512,12 @@ number base baseDigit
 reservedOp name =
     lexeme $ try $
     do{ string name
-      ; notFollowedBy (opLetter languageDef) <?> ("end of " ++ show name)
+      ; notFollowedBy opLetter <?> ("end of " ++ show name)
       }
 
-operator =
+operator = operator_ oper
+
+operator_ oper =
     lexeme $ try $
     do{ name <- oper
       ; if (isReservedOp name)
@@ -509,39 +526,29 @@ operator =
       }
 
 oper =
-    do{ c <- (opStart languageDef)
-      ; cs <- many (opLetter languageDef)
+    do{ c <- opStart
+      ; cs <- many opLetter
       ; return (c:cs)
       }
     <?> "operator"
 
 isReservedOp name =
-    isReserved (sort (reservedOpNames languageDef)) name
+    isReserved theReservedOpNames name
 
+theReservedOpNames = sort reservedOpNames
 
 -----------------------------------------------------------
 -- Identifiers & Reserved words
 -----------------------------------------------------------
 reserved name =
     lexeme $ try $
-    do{ caseString name
-      ; notFollowedBy (identLetter languageDef) <?> ("end of " ++ show name)
+    do{ string name
+      ; notFollowedBy identLetter <?> ("end of " ++ show name)
       }
 
-caseString name
-    | caseSensitive languageDef  = string name
-    | otherwise               = do{ walk name; return name }
-    where
-      walk []     = return ()
-      walk (c:cs) = do{ caseChar c <?> msg; walk cs }
+identifier = identifier_ ident
 
-      caseChar c  | isAlpha c  = char (toLower c) <|> char (toUpper c)
-                  | otherwise  = char c
-
-      msg         = show name
-
-
-identifier =
+identifier_ ident =
     lexeme $ try $
     do{ name <- ident
       ; if (isReservedName name)
@@ -551,17 +558,14 @@ identifier =
 
 
 ident
-    = do{ c <- identStart languageDef
-        ; cs <- many (identLetter languageDef)
+    = do{ c <- identStart
+        ; cs <- many identLetter
         ; return (c:cs)
         }
     <?> "identifier"
 
 isReservedName name
-    = isReserved theReservedNames caseName
-    where
-      caseName      | caseSensitive languageDef  = name
-                    | otherwise               = map toLower name
+    = isReserved theReservedNames name
 
 
 isReserved names name
@@ -573,11 +577,7 @@ isReserved names name
                         EQ  -> True
                         GT  -> False
 
-theReservedNames
-    | caseSensitive languageDef  = sort reserved
-    | otherwise                  = sort . map (map toLower) $ reserved
-    where
-      reserved = reservedNames languageDef
+theReservedNames = sort reservedNames
 
 
 
@@ -588,46 +588,28 @@ symbol name
     = lexeme (string name)
 
 whiteSpace = ignoreAbsoluteIndentation (localTokenMode (const Pa.Any) whiteSpace')
-whiteSpace'
-    | noLine && noMulti  = skipMany (simpleSpace <?> "")
-    | noLine             = skipMany (simpleSpace <|> multiLineComment <?> "")
-    | noMulti            = skipMany (simpleSpace <|> oneLineComment <?> "")
-    | otherwise          = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
-    where
-      noLine  = null (commentLine languageDef)
-      noMulti = null (commentStart languageDef)
+whiteSpace' = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")
 
 simpleSpace =
     skipMany1 (satisfy isSpace)
 
 oneLineComment =
-    do{ try (string (commentLine languageDef))
+    do{ try (string commentLine)
       ; skipMany (satisfy (/= '\n'))
       ; return ()
       }
 
 multiLineComment =
-    do { try (string (commentStart languageDef))
-       ; inComment
+    do { try (string commentStart)
+       ; inCommentMulti
        }
 
-inComment
-    | nestedComments languageDef  = inCommentMulti
-    | otherwise                = inCommentSingle
-
 inCommentMulti
-    =   do{ try (string (commentEnd languageDef)) ; return () }
+    =   do{ try (string commentEnd) ; return () }
     <|> do{ multiLineComment                     ; inCommentMulti }
     <|> do{ skipMany1 (noneOf startEnd)          ; inCommentMulti }
     <|> do{ oneOf startEnd                       ; inCommentMulti }
     <?> "end of comment"
     where
-      startEnd   = nub (commentEnd languageDef ++ commentStart languageDef)
+      startEnd   = nub (commentEnd ++ commentStart)
 
-inCommentSingle
-    =   do{ try (string (commentEnd languageDef)); return () }
-    <|> do{ skipMany1 (noneOf startEnd)         ; inCommentSingle }
-    <|> do{ oneOf startEnd                      ; inCommentSingle }
-    <?> "end of comment"
-    where
-      startEnd   = nub (commentEnd languageDef ++ commentStart languageDef)
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 40739265..74f7d3d0 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -358,10 +358,8 @@ parseTerm prec = withRange setSI $ case prec of
             t' <- dbf' fe <$> parseTTerm PrecLam
             return $ foldr (uncurry f) t' ts
      <|> do expNS $ do
-                reservedOp "\\"
-                (fe, ts) <- telescopePat
+                (fe, ts) <- reservedOp "\\" *> telescopePat <* reservedOp "->"
                 checkPattern fe
-                reservedOp "->"
                 t' <- dbf' fe <$> parseTerm PrecLam
                 ge <- dsInfo
                 return $ foldr (uncurry (patLam_ id ge)) t' ts
@@ -372,30 +370,25 @@ parseTerm prec = withRange setSI $ case prec of
                         (fe, p) <- longPattern
                         (,) p <$> parseRHS (dbf' fe) "->"
      <|> compileGuardTree id id <$> dsInfo <*> (Alts <$> parseSomeGuards (const True))
-     <|> do t <- parseTerm PrecEq
-            option t $ mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam
-    PrecEq -> parseTerm PrecAnn >>= \t -> option t $ SAppV2 (SBuiltin "'EqCT" `SAppV` SType) t <$ reservedOp "~" <*> parseTTerm PrecAnn
-    PrecAnn -> parseTerm PrecOp >>= \t -> option t $ SAnn t <$> parseType Nothing
+     <|> do level PrecEq $ \t -> mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam
+    PrecEq -> level PrecAnn $ \t -> SAppV (SBuiltin "'EqCT" `SAppV` SType `SAppV` t) <$ reservedOp "~" <*> parseTTerm PrecAnn
+    PrecAnn -> level PrecOp $ \t -> SAnn t <$> parseType Nothing
     PrecOp -> join $ calculatePrecs <$> namespace <*> dsInfo <*> (notExp <|> notOp False)  where
-        notExp = (++) <$> ope <*> option [] (notOp True)
-        notOp x = (++) <$> try "expression" ((++) <$> ex PrecApp <*> option [] ope) <*> option [] (notOp True)
-             <|> if x then try "lambda" (ex PrecLam) else mzero
+        notExp = (++) <$> ope <*> notOp True
+        notOp x = (++) <$> try "expression" ((++) <$> ex PrecApp <*> option [] ope) <*> notOp True
+             <|> if x then option [] (try "lambda" $ ex PrecLam) else mzero
         ope = pure . Left <$> parseSIName operatorT
         ex pr = pure . Right <$> parseTerm pr
     PrecApp ->
         apps' <$> try "record" (sVar upperCase <* reservedOp "{") <*> (commaSep $ lowerCase *> reservedOp "=" *> ((,) Visible <$> parseTerm PrecLam)) <* reservedOp "}"
      <|> apps' <$> parseTerm PrecSwiz <*> many (hiddenTerm (parseTTerm PrecSwiz) $ parseTerm PrecSwiz)
-    PrecSwiz -> do
-        t <- parseTerm PrecProj
-        option t $ mkSwizzling t <$> try "swizzling" (lexeme $ char '%' *> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: String))))
-    PrecProj -> do
-        t <- parseTerm PrecAtom
-        option t $ try "projection" $ mkProjection t <$ char '.' <*> sepBy1 (sLit . LString <$> lowerCase) (char '.')
+    PrecSwiz -> level PrecProj $ \t -> try "swizzling" $ mkSwizzling t <$> lexeme (char '%' *> manyNM 1 4 (satisfy (`elem` ("xyzwrgba" :: String))))
+    PrecProj -> level PrecAtom $ \t -> try "projection" $ mkProjection t <$ char '.' <*> sepBy1 (sLit . LString <$> lowerCase) (char '.')
     PrecAtom ->
          sLit . LChar    <$> try "char literal" charLiteral
      <|> sLit . LString  <$> stringLiteral
      <|> sLit . LFloat   <$> try "float literal" float
-     <|> sLit . LInt . fromIntegral <$ char '#' <*> natural
+     <|> sLit . LInt . fromIntegral <$ char '#' <*> natural -- todo:  remove
      <|> mkNat <$> namespace <*> natural
      <|> Wildcard (Wildcard SType) <$ reserved "_"
      <|> char '\'' *> switchNS (parseTerm PrecAtom)
@@ -411,6 +404,8 @@ parseTerm prec = withRange setSI $ case prec of
             dcls <- localIndentation Ge $ localAbsoluteIndentation $ parseDefs xSLabelEnd
             mkLets True <$> dsInfo <*> pure dcls <* reserved "in" <*> parseTerm PrecLam
   where
+    level pr f = parseTerm pr >>= \t -> option t $ f t
+
     mkSwizzling term = swizzcall
       where
         sc c = SBuiltin ['S',c]
@@ -469,19 +464,17 @@ parseTerm prec = withRange setSI $ case prec of
 
     calculatePrecs :: Namespace -> DesugarInfo -> [Either SIName SExp] -> P SExp
     calculatePrecs ns dcls = either fail return . f where
-        f (Left op@(_, "-"): xs) = calcPrec' (mkNat ns 0) <$> h op xs
-        f (Left op: xs)      = h op xs <&> \((op, e): oe) -> LeftSection op $ calcPrec' e oe
-        f (Right t: xs)      = either (\(op, xs) -> RightSection (calcPrec' t xs) op) (calcPrec' t) <$> cont (Right []) g xs
-        f []                 = Left "TODO: better error message @461"
-        g op (Right t: xs)   = (second ((op, t):) +++ ((op, t):)) <$> cont (Right []) g xs
+        f []                 = error "impossible"
+        f (Right t: xs)      = either (\(op, xs) -> RightSection (calcPrec' t xs) op) (calcPrec' t) <$> cont xs
+        f xs@(Left op@(_, "-"): _) = f $ Right (mkNat ns 0): xs
+        f (Left op: xs)      = g op xs >>= either (const $ Left "TODO: better error message @476")
+                                                  (\((op, e): oe) -> return $ LeftSection op $ calcPrec' e oe)
+        g op (Right t: xs)   = (second ((op, t):) +++ ((op, t):)) <$> cont xs
         g op []              = return $ Left (op, [])
-        g op _               = Left "TODO: better error message @470"
-        h op (Right t: xs)   = ((op, t):) <$> cont [] h xs
-        h op _               = Left "TODO: better error message @472"
-        cont :: forall a . a -> (SIName -> [Either SIName SExp] -> Either String a) -> [Either SIName SExp] -> Either String a
-        cont _ f (Left op: xs) = f op xs
-        cont e _ []            = return e
-        cont _ _ _             = Left "TODO: better error message @477"
+        g op _               = Left "two operator is not allowed next to each-other"
+        cont (Left op: xs)   = g op xs
+        cont []              = return $ Right []
+        cont _               = error "impossible"
 
         calcPrec' = calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (getFixity dcls . snd)