refactoring

4 files changed, 153 insertions, 139 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index bacf769b..15a37c0f 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -206,7 +206,7 @@ data Neutral
     | App__       !MaxDB Neutral Exp
     | CaseFun__   !MaxDB CaseFunName   [Exp] Neutral
     | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral
-    | Fun_        !MaxDB FunName [Exp]{-local vars-} !Int{-number of missing parameters-} [Exp]{-given parameters, reversed-} Neutral{-unfolded expression-}{-not neut?-}
+    | Fun_        !MaxDB FunName [Exp]{-local vars-} [Exp]{-given parameters, reversed-} Exp{-unfolded expression-}
     | RHS_ Exp                 -- not neut?
     | Delta (SData ([Exp] -> Exp))  -- not neut?
 
@@ -225,16 +225,19 @@ infixr 1 :~>
 
 pattern NoLE <- (isNoRHS -> True)
 
-isNoRHS (RHS_ _) = False
+isNoRHS (Neut (RHS_ _)) = False
 isNoRHS _ = True
 
-pattern Fun' f vs i xs n <- Fun_ _ f vs i xs n where Fun' f vs i xs n = Fun_ (foldMap maxDB_ vs <> foldMap maxDB_ xs {- <> iterateN i lowerDB (maxDB_ n)-}) f vs i xs n
-pattern Fun f i xs n = Fun' f [] i xs n
-pattern UTFun a t b <- (unfixlabel -> Neut (Fun (FunName a _ t) _ (reverse -> b) NoLE))
+getLams' (Lam e) = first (+1) $ getLams' e
+getLams' e = (0, e)
+
+pattern Fun' f vs xs n <- Fun_ _ f vs xs n where Fun' f vs xs n = Fun_ (foldMap maxDB_ vs <> foldMap maxDB_ xs {- <> iterateN i lowerDB (maxDB_ n)-}) f vs xs n
+pattern Fun f xs n = Fun' f [] xs n
+pattern UTFun a t b <- (unfixlabel -> Neut (Fun (FunName a _ t) (reverse -> b) NoLE))
 pattern UFunN a b <- UTFun a _ b
-pattern DFun_ fn xs <- Fun fn 0 (reverse -> xs) (Delta _) where
-    DFun_ fn@(FunName n _ _) xs = Fun fn 0 (reverse xs) d where
-        d = Delta $ SData $ getFunDef n $ \xs -> Neut $ Fun fn 0 (reverse xs) d
+pattern DFun_ fn xs <- Fun fn (reverse -> xs) (Neut (Delta _)) where
+    DFun_ fn@(FunName n _ _) xs = Fun fn (reverse xs) d where
+        d = Neut $ Delta $ SData $ getFunDef n $ \xs -> Neut $ Fun fn (reverse xs) d
 pattern TFun' a t b = DFun_ (FunName a Nothing t) b
 pattern TFun a t b = Neut (TFun' a t b)
 
@@ -337,12 +340,11 @@ trueExp = EBool True
 pattern RHS x = Neut (RHS_ x)
 
 --pmLabel' :: FunName -> [Exp] -> Int -> [Exp] -> Exp -> Exp
-pmLabel' _ (FunName _ _ _) _ 0 as (Neut (Delta (SData f))) = f $ reverse as
-pmLabel' md f vs i xs (unfixlabel -> Neut y) = Neut $ Fun_ md f vs i xs y
-pmLabel' _ f _ i xs (unfixlabel -> y) = error $ "pmLabel:\n" ++ ppShow (f, i, length xs) ++ "\n" ++ ppShow y --show (f, i, length xs, y)
+pmLabel' _ (FunName _ _ _) _ as (Neut (Delta (SData f))) = f $ reverse as
+pmLabel' md f vs xs (unfixlabel -> y) = Neut $ Fun_ md f vs xs y
 
-pmLabel :: FunName -> [Exp] -> Int -> [Exp] -> Exp -> Exp
-pmLabel f vs i xs e = pmLabel' (foldMap maxDB_ vs <> foldMap maxDB_ xs) f vs (i + numLams e) xs (Neut $ dropLams e)
+pmLabel :: FunName -> [Exp] -> [Exp] -> Exp -> Exp
+pmLabel f vs xs e = pmLabel' (foldMap maxDB_ vs <> foldMap maxDB_ xs) f vs xs e
 
 dropLams (unfixlabel -> Lam x) = dropLams x
 dropLams (unfixlabel -> Neut x) = x
@@ -350,12 +352,12 @@ dropLams (unfixlabel -> Neut x) = x
 numLams (unfixlabel -> Lam x) = 1 + numLams x
 numLams x = 0
 
-pattern FL' y <- Fun' f _ 0 xs (RHS_ y)
+pattern FL' y <- Fun' f _ xs (Neut (RHS_ y))
 pattern FL y <- Neut (FL' y)
 
 pattern Func n def ty xs <- (mkFunc -> Just (n, def, ty, xs))
 
-mkFunc (Neut (Fun (FunName n (Just def) ty) 0 xs RHS_{})) | Just def' <- removeLams (length xs) def = Just (n, def', ty, xs)
+mkFunc (Neut (Fun (FunName n (Just def) ty) xs (Neut RHS_{}))) | Just def' <- removeLams (length xs) def = Just (n, def', ty, xs)
 mkFunc _ = Nothing
 
 removeLams 0 (RHS x) = Just x
@@ -364,10 +366,10 @@ removeLams _ _ = Nothing
 
 pattern UFL y <- (unFunc -> Just y)
 
-unFunc (Neut (Fun' (FunName _ (Just def) _) _ n xs y)) = Just $ iterateN n Lam $ Neut y
+unFunc (Neut (Fun' (FunName _ (Just def) _) _ xs y)) = Just y
 unFunc _ = Nothing
 
-unFunc_ (Neut (Fun' _ _ n xs y)) = Just $ iterateN n Lam $ Neut y
+unFunc_ (Neut (Fun' _ _ xs y)) = Just y
 unFunc_ _ = Nothing
 
 unfixlabel (FL y) = unfixlabel y
@@ -406,7 +408,7 @@ instance Eq Exp where
     _ == _ = False
 
 instance Eq Neutral where
-    Fun' f vs i a _ == Fun' f' vs' i' a' _ = (f, vs, i, a) == (f', vs', i', a')
+    Fun' f vs a _ == Fun' f' vs' a' _ = (f, vs, a) == (f', vs', a')
     FL' a == a' = a == Neut a'
     a == FL' a' = Neut a == a'
     RHS_ a == RHS_ a' = a == a'
@@ -455,7 +457,7 @@ instance Subst Exp Exp where
                 CaseFun_ s as n -> evalCaseFun s (f i <$> as) (substNeut n)
                 TyCaseFun_ s as n -> evalTyCaseFun s (f i <$> as) (substNeut n)
                 App_ a b  -> app_ (substNeut a) (f i b)
-                Fun_ md fn vs c xs v -> pmLabel' (md <> upDB i dx) fn (f i <$> vs) c (f i <$> xs) $ f (i + c) $ Neut v
+                Fun_ md fn vs xs v -> pmLabel' (md <> upDB i dx) fn (f i <$> vs) (f i <$> xs) $ f i v
                 RHS_ a -> RHS $ f i a
                 d@Delta{} -> Neut d
         f i e | cmpDB i e = e
@@ -483,7 +485,7 @@ instance Rearrange Neutral where
             CaseFun__ md s as ne -> CaseFun__ (upDB_ g i md) s (rearrange i g <$> as) (rearrange i g ne)
             TyCaseFun__ md s as ne -> TyCaseFun__ (upDB_ g i md) s (rearrange i g <$> as) (rearrange i g ne)
             App__ md a b -> App__ (upDB_ g i md) (rearrange i g a) (rearrange i g b)
-            Fun_ md fn vs c x y -> Fun_ (upDB_ g i md) fn (rearrange i g <$> vs) c (rearrange i g <$> x) $ rearrange (i + c) g y
+            Fun_ md fn vs x y -> Fun_ (upDB_ g i md) fn (rearrange i g <$> vs) (rearrange i g <$> x) $ rearrange i g y
             RHS_ x -> RHS_ $ rearrange i g x
             d@Delta{} -> d
 
@@ -497,7 +499,7 @@ instance Up Neutral where
         CaseFun_ _ as n -> foldMap (foldVar f i) as <> foldVar f i n
         TyCaseFun_ _ as n -> foldMap (foldVar f i) as <> foldVar f i n
         App_ a b -> foldVar f i a <> foldVar f i b
-        Fun' _ vs j x d -> foldMap (foldVar f i) vs <> foldMap (foldVar f i) x -- <> foldVar f (i+j) d
+        Fun' _ vs x d -> foldMap (foldVar f i) vs <> foldMap (foldVar f i) x -- <> foldVar f i d
         RHS_ x -> foldVar f i x
         Delta{} -> mempty
 
@@ -507,7 +509,7 @@ instance HasMaxDB Neutral where
         CaseFun__ c _ _ _ -> c
         TyCaseFun__ c _ _ _ -> c
         App__ c a b -> c
-        Fun_ c _ _ _ _ _ -> c
+        Fun_ c _ _ _ _ -> c
         RHS_ x -> maxDB_ x
         Delta{} -> mempty
 
@@ -543,7 +545,7 @@ instance ClosedExp Neutral where
         CaseFun__ _ a as n -> CaseFun__ mempty a (closedExp <$> as) (closedExp n)
         TyCaseFun__ _ a as n -> TyCaseFun__ mempty a (closedExp <$> as) (closedExp n)
         App__ _ a b -> App__ mempty (closedExp a) (closedExp b)
-        Fun_ _ f l i x y -> Fun_ mempty f l i (closedExp <$> x) y
+        Fun_ _ f l x y -> Fun_ mempty f l (closedExp <$> x) y
         RHS_ a -> RHS_ (closedExp a)
         d@Delta{} -> d
 
@@ -584,7 +586,7 @@ instance MkDoc Neutral where
         f = \case
             CstrT' t a b     -> shCstr (g (a, t)) (g (b, t))
             FL' a | pr -> g a
-            Fun' s vs i (mkExpTypes (nType s) . reverse -> xs) _ -> foldl (shApp Visible) (pShow s) (g <$> xs)
+            Fun' s vs (mkExpTypes (nType s) . reverse -> xs) _ -> foldl (shApp Visible) (pShow s) (g <$> xs)
             Var_ k           -> shVar k
             App_ a b         -> shApp Visible (g a) (g b)
             CaseFun_ s xs n  -> foldl (shApp Visible) (pShow s) (map g $ {-mkExpTypes (nType s) $ makeCaseFunPars te n ++ -} xs ++ [Neut n])
@@ -769,7 +771,7 @@ app_ (TyCon s xs) a = TyCon s (xs ++ [a])
 app_ (Neut f) a = neutApp f a
   where
     neutApp (FL' x) a = app_ x a    -- ???
-    neutApp (Fun' f vs i xs e) a | i > 0 = pmLabel f vs (i-1) (a: xs) (subst (i-1) (up (i-1) a) $ Neut e)
+    neutApp (Fun' f vs xs (Lam e)) a = pmLabel f vs (a: xs) (subst 0 a e)
     neutApp f a = Neut $ App_ f a
 
 
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index bcdd0968..c5497a98 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -864,7 +864,7 @@ mkLam _ = Nothing
 
 mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (conType et s) $ mkConPars n et ++ xs)
 mkCon (ExpTV (TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
-mkCon (ExpTV (Neut (I.Fun s i (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (Neut (I.Fun s (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
 mkCon (ExpTV (CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [Neut n])
 mkCon (ExpTV (TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, Neut n, f])
 mkCon _ = Nothing
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index ec66c801..6e351410 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -210,14 +210,14 @@ neutType te = \case
     Var_ i          -> snd $ varType "C" i te
     CaseFun_ s ts n -> appTy (foldl appTy (nType s) $ makeCaseFunPars te n ++ ts) (Neut n)
     TyCaseFun_ s [m, t, f] n -> foldl appTy (nType s) [m, t, Neut n, f]
-    Fun' s _ _ a _ -> foldlrev appTy (nType s) a
+    Fun' s _ a _ -> foldlrev appTy (nType s) a
 
 neutType' te = \case
     App_ f x        -> appTy (neutType' te f) x
     Var_ i          -> varType' i te
     CaseFun_ s ts n -> appTy (foldl appTy (nType s) $ makeCaseFunPars' te n ++ ts) (Neut n)
     TyCaseFun_ s [m, t, f] n -> foldl appTy (nType s) [m, t, Neut n, f]
-    Fun' s _ _ a _     -> foldlrev appTy (nType s) a
+    Fun' s _ a _     -> foldlrev appTy (nType s) a
 
 -------------------------------------------------------------------------------- error messages
 
@@ -522,9 +522,9 @@ recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
         (TyCon_ md s as, zt)      -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as
         (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
         (TyCaseFun s [m, t, f] n, zt)  -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f]
-        (Neut (Fun_ md f vs@[] i a x), zt) -> checkApps "lab" [] zt (\xs -> Neut $ Fun_ md f vs i (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
+        (Neut (Fun_ md f vs@[] a x), zt) -> checkApps "lab" [] zt (\xs -> Neut $ Fun_ md f vs (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
         -- TODO
-        (r@(Neut (Fun' f vs i a x)), zt) -> r
+        (r@(Neut (Fun' f vs a x)), zt) -> r
         (RHS x, zt) -> RHS $ recheck_ msg te (x, zt)
         (Neut d@Delta{}, zt) -> Neut d
       where
@@ -733,7 +733,7 @@ mkELet n x xt = {-(if null vs then id else trace_ $ "mkELet " ++ show (length vs
     vs = [Var i | i <- Set.toList $ free x <> free xt]
     fn = FunName (mkFName n) (Just x) xt
 
-    term = pmLabel fn vs 0 [] $ getFix x 0
+    term = pmLabel fn vs [] $ getFix x 0
 
     getFix (Lam z) i = Lam $ getFix z (i+1)
     getFix (TFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 08b066cd..09e9507b 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -87,17 +87,6 @@ trackSI p = do
     tell $ Right . TrackedCode <$> maybeToList (getRange $ sourceInfo x)
     return x
 
--- TODO: filter this in module imports
-data DesugarInfo = DesugarInfo
-    { fixityMap  :: Map.Map SName Fixity
-    , consMap    :: Map.Map SName ConsInfo
-    , definedSet :: DefinedSet
-    }
-
-instance Monoid DesugarInfo where
-    mempty = DesugarInfo mempty mempty mempty
-    DesugarInfo a b c `mappend` DesugarInfo a' b' c' = DesugarInfo (a <> a') (b <> b') (c <> c')
-
 addFixity :: BodyParser SIName -> BodyParser SIName
 addFixity p = f <$> asks (fixityMap . desugarInfo) <*> p
   where
@@ -125,6 +114,17 @@ addForalls_ s = addForalls . (Set.fromList (sName <$> s) <>) <$> asks (definedSe
 
 -------------------------------------------------------------------------------- desugar info
 
+-- TODO: filter this in module imports
+data DesugarInfo = DesugarInfo
+    { fixityMap  :: Map.Map SName Fixity
+    , consMap    :: Map.Map SName ConsInfo
+    , definedSet :: DefinedSet
+    }
+
+instance Monoid DesugarInfo where
+    mempty = DesugarInfo mempty mempty mempty
+    DesugarInfo a b c `mappend` DesugarInfo a' b' c' = DesugarInfo (a <> a') (b <> b') (c <> c')
+
 mkDesugarInfo :: [Stmt] -> DesugarInfo
 mkDesugarInfo ss = DesugarInfo
     { fixityMap = Map.fromList $ ("'EqCTt", Infix (-1)): [(sName s, f) | PrecDef s f <- ss]
@@ -145,10 +145,11 @@ mkDesugarInfo ss = DesugarInfo
 
 -------------------------------------------------------------------------------- expression parsing
 
+hiddenTerm p q = (,) Hidden <$ reservedOp "@" <*> typeNS p  <|>  (,) Visible <$> q
+
 parseType mb = maybe id option mb (reservedOp "::" *> typeNS (setR parseTermLam))
-typedIds f ds mb = (\ns t -> (,) <$> ns <*> pure t) <$> commaSep1 upperLower <*> (deBruijnify (ds :: [SIName]) <$> f (parseType mb))
 
-hiddenTerm p q = (,) Hidden <$ reservedOp "@" <*> typeNS p  <|>  (,) Visible <$> q
+typedIds f ds = (\ns t -> (,) <$> ns <*> pure t) <$> commaSep1 upperLower <*> (deBruijnify (ds :: [SIName]) <$> f (parseType Nothing))
 
 telescope mb = fmap mkTelescope $ many $ hiddenTerm
     (typedId <|> maybe empty (tvar . pure) mb)
@@ -183,22 +184,71 @@ parseTermLam =
                 identation False $ do
                     (fe, p) <- longPattern
                     (,) p . deBruijnify fe <$> parseRHS "->"
+  where
+    mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f
+
+    mkPi Hidden xs b = foldr (sNonDepPi Hidden) b $ getTTuple xs
+    mkPi h a b = sNonDepPi h a b
+
+    sNonDepPi h a b = SPi h a $ up1 b
+
 parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing
-parseTermOp = (notOp False <|> notExp) >>= calculatePrecs where
+
+parseTermOp = (notOp False <|> notExp) >>= calculatePrecs
+  where
     notExp = (++) <$> ope <*> notOp True
     notOp x = (++) <$> try_ "expression" ((++) <$> ex parseTermApp <*> option [] ope) <*> notOp True
          <|> if x then option [] (try_ "lambda" $ ex parseTermLam) else mzero
     ope = pure . Left <$> addFixity (rhsOperator <|> appRange (flip SIName "'EqCTt" <$ reservedOp "~"))
     ex pr = pure . Right <$> setR pr
+
+    calculatePrecs :: [Either SIName SExp] -> BodyParser SExp
+    calculatePrecs = go where
+
+        go (Right e: xs)         = waitOp False e [] xs
+        go xs@(Left (sName -> "-"): _) = waitOp False (mkLit $ LInt 0) [] xs
+        go (Left op: xs)         = Section . SLamV <$> waitExp True (sVar "leftSection" 0) [] op xs
+        go _                     = error "impossible @ Parser 479"
+
+        waitExp lsec e acc op (Right t: xs)  = waitOp lsec e ((op, if lsec then up 1 t else t): acc) xs
+        waitExp lsec e acc op [] | lsec      = fail "two-sided section is not allowed"
+                                 | otherwise = fmap (Section . SLamV) . calcPrec' e $ (op, sVar "rightSection" 0): map (second (up 1)) acc
+        waitExp _ _ _ _ _                    = fail "two operator is not allowed next to each-other"
+
+        waitOp lsec e acc (Left op: xs) = waitExp lsec e acc op xs
+        waitOp lsec e acc []            = calcPrec' e acc
+        waitOp lsec e acc _             = error "impossible @ Parser 488"
+
+        calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . getFixity) e . reverse
+
 parseTermApp =
         AppsS <$> try_ "record" (SGlobal <$> upperCase <* symbol "{")
               <*> commaSep ((,) Visible <$ lowerCase{-TODO-} <* reservedOp "=" <*> setR parseTermLam)
               <*  symbol "}"
      <|> AppsS <$> setR parseTermSwiz <*> many (hiddenTerm (setR parseTermSwiz) $ setR parseTermSwiz)
+
 parseTermSwiz = level parseTermProj $ \t ->
     mkSwizzling t <$> lexeme (try_ "swizzling" $ char '%' *> count' 1 4 (satisfy (`elem` ("xyzwrgba" :: String))))
+  where
+    mkSwizzling term = swizzcall . map (sc . synonym)
+      where
+        swizzcall []  = error "impossible: swizzling parsing returned empty pattern"
+        swizzcall [x] = SBuiltin "swizzscalar" `SAppV` term `SAppV` x
+        swizzcall xs  = SBuiltin "swizzvector" `SAppV` term `SAppV` foldl SAppV (SBuiltin $ "V" ++ show (length xs)) xs
+
+        sc c = SBuiltin ['S', c]
+
+        synonym 'r' = 'x'
+        synonym 'g' = 'y'
+        synonym 'b' = 'z'
+        synonym 'a' = 'w'
+        synonym c   = c
+
 parseTermProj = level parseTermAtom $ \t ->
     try_ "projection" $ mkProjection t <$ char '.' <*> sepBy1 lowerCase (char '.')
+  where
+    mkProjection = foldl $ \exp field -> SBuiltin "project" `SAppV` litString field `SAppV` exp
+
 parseTermAtom =
          mkLit <$> try_ "literal" parseLit
      <|> Wildcard (Wildcard SType) <$ reserved "_"
@@ -218,104 +268,73 @@ parseTermAtom =
      <|> parens (SGlobal <$> try_ "opname" (symbols <* lookAhead (symbol ")"))
              <|> mkTuple . tick <$> asks namespace <*> commaSep (setR parseTermLam))
 
-level pr f = pr >>= \t -> option t $ f t
+    mkTuple _      [Section e] = e
+    mkTuple ExpNS  [Parens e]  = HCons e HNil
+    mkTuple TypeNS [Parens e]  = HList $ BCons e BNil
+    mkTuple _      [x]         = Parens x
+    mkTuple ExpNS  xs          = foldr HCons HNil xs
+    mkTuple TypeNS xs          = HList $ foldr BCons BNil xs
 
+    mkList TypeNS [x] = BList x
+    mkList _      xs  = foldr BCons BNil xs
 
-mkSwizzling term = swizzcall . map (sc . synonym)
-  where
-    swizzcall []  = error "impossible: swizzling parsing returned empty pattern"
-    swizzcall [x] = SBuiltin "swizzscalar" `SAppV` term `SAppV` x
-    swizzcall xs  = SBuiltin "swizzvector" `SAppV` term `SAppV` foldl SAppV (SBuiltin $ "V" ++ show (length xs)) xs
+    -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, 2.0, 3.0)))
+    mkRecord (unzip -> (names, values))
+        = SBuiltin "RecordCons" `SAppH` foldr BCons BNil (mkRecItem <$> names) `SAppV` foldr HCons HNil values
 
-    sc c = SBuiltin ['S', c]
+    mkRecItem l = SBuiltin "RecItem" `SAppV` litString l `SAppV` Wildcard SType
 
-    synonym 'r' = 'x'
-    synonym 'g' = 'y'
-    synonym 'b' = 'z'
-    synonym 'a' = 'w'
-    synonym c   = c
+    mkDotDot e f = SBuiltin "fromTo" `SAppV` e `SAppV` f
 
-mkProjection = foldl $ \exp field -> SBuiltin "project" `SAppV` litString field `SAppV` exp
+    generator, letdecl, boolExpression :: BodyParser (SExp -> ErrorFinder SExp)
+    generator = do
+        (dbs, pat) <- try_ "generator" $ longPattern <* reservedOp "<-"
+        checkPattern dbs
+        exp <- setR parseTermLam
+        return $ \e -> do
+            cf <- runCheck $ compileGuardTree id id (Just $ SIName (sourceInfo pat) "") [(Visible, Wildcard SType)]
+                           $ compilePatts [pat] (noGuards $ deBruijnify dbs e) `mappend` noGuards BNil
+            return $ SBuiltin "concatMap" `SAppV` cf `SAppV` exp
 
--- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, 2.0, 3.0)))
-mkRecord (unzip -> (names, values))
-    = SBuiltin "RecordCons" `SAppH` foldr BCons BNil (mkRecItem <$> names) `SAppV` foldr HCons HNil values
+    letdecl = (return .) . mkLets <$ reserved "let" <*> (runCheck . compileStmt' =<< valueDef)
 
-mkRecItem l = SBuiltin "RecItem" `SAppV` litString l `SAppV` Wildcard SType
+    boolExpression = (\pred e -> return $ SBuiltin "primIfThenElse" `SAppV` pred `SAppV` e `SAppV` BNil) <$> setR parseTermLam
 
-litString (SIName si n) = SLit si $ LString n
 
-mkTuple _      [Section e] = e
-mkTuple ExpNS  [Parens e]  = HCons e HNil
-mkTuple TypeNS [Parens e]  = HList $ BCons e BNil
-mkTuple _      [x]         = Parens x
-mkTuple ExpNS  xs          = foldr HCons HNil xs
-mkTuple TypeNS xs          = HList $ foldr BCons BNil xs
+level pr f = pr >>= \t -> option t $ f t
 
-mkList TypeNS [x] = BList x
-mkList _      xs  = foldr BCons BNil xs
+litString (SIName si n) = SLit si $ LString n
 
 mkLit n@LInt{} = SBuiltin "fromInt" `SAppV` sLit n
 mkLit l = sLit l
 
-mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f
-
-mkDotDot e f = SBuiltin "fromTo" `SAppV` e `SAppV` f
-
-calculatePrecs :: [Either SIName SExp] -> BodyParser SExp
-calculatePrecs = go where
-
-    go (Right e: xs)         = waitOp False e [] xs
-    go xs@(Left (sName -> "-"): _) = waitOp False (mkLit $ LInt 0) [] xs
-    go (Left op: xs)         = Section . SLamV <$> waitExp True (sVar "leftSection" 0) [] op xs
-    go _                     = error "impossible @ Parser 479"
-
-    waitExp lsec e acc op (Right t: xs)  = waitOp lsec e ((op, if lsec then up 1 t else t): acc) xs
-    waitExp lsec e acc op [] | lsec      = fail "two-sided section is not allowed"
-                             | otherwise = fmap (Section . SLamV) . calcPrec' e $ (op, sVar "rightSection" 0): map (second (up 1)) acc
-    waitExp _ _ _ _ _                    = fail "two operator is not allowed next to each-other"
-
-    waitOp lsec e acc (Left op: xs) = waitExp lsec e acc op xs
-    waitOp lsec e acc []            = calcPrec' e acc
-    waitOp lsec e acc _             = error "impossible @ Parser 488"
-
-    calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . getFixity) e . reverse
-
-generator, letdecl, boolExpression :: BodyParser (SExp -> ErrorFinder SExp)
-generator = do
-    (dbs, pat) <- try_ "generator" $ longPattern <* reservedOp "<-"
-    checkPattern dbs
-    exp <- setR parseTermLam
-    return $ \e -> do
-        cf <- runCheck $ compileGuardTree id id (Just $ SIName (sourceInfo pat) "") [(Visible, Wildcard SType)] $ compilePatts [pat] (noGuards $ deBruijnify dbs e) `mappend` noGuards BNil
-        return $ SBuiltin "concatMap" `SAppV` cf `SAppV` exp
-
-letdecl = (return .) . mkLets <$ reserved "let" <*> (runCheck . compileStmt' =<< valueDef)
-
-boolExpression = (\pred e -> return $ SBuiltin "primIfThenElse" `SAppV` pred `SAppV` e `SAppV` BNil) <$> setR parseTermLam
-
-mkPi Hidden xs b = foldr (sNonDepPi Hidden) b $ getTTuple xs
-mkPi h a b = sNonDepPi h a b
-
-sNonDepPi h a b = SPi h a $ up1 b
-
 -------------------------------------------------------------------------------- pattern parsing
 
 setR p = appRange $ flip setSI <$> p
 
 --parsePat... :: BodyParser ParPat
-parsePatAnn = patType <$> setR parsePatArr <*> parseType (Just $ Wildcard SType)
-parsePatArr = parsePatOp
+parsePatAnn = patType <$> setR parsePatOp <*> parseType (Just $ Wildcard SType)
+  where
+    patType p (Wildcard SType) = p
+    patType p t = PatTypeSimp p t
+
 parsePatOp = join $ calculatePatPrecs <$> setR parsePatApp <*> option [] (oper >>= p)
   where
     oper = addConsInfo $ addFixity colonSymbols
     p op = do (exp, op') <- try_ "pattern" $ (,) <$> setR parsePatApp <*> oper
               ((op, exp):) <$> p op'
        <|> pure . (,) op <$> setR parsePatAnn
+
+    calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . getFixity . fst) e xs
+
 parsePatApp =
          PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt)
      <|> parsePatAt
+
 parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (reservedOp "@")
+  where
+    concatParPats ps = ParPat $ concat [p | ParPat p <- ps]
+
 parsePatAtom =
          mkLit <$> asks namespace <*> try_ "literal" parseLit
      <|> flip PConSimp [] <$> addConsInfo upperCase_
@@ -331,34 +350,27 @@ parsePatAtom =
          brackets (mkListPat . tick <$> asks namespace <*> patlist)
      <|> parens   (parseViewPat <|> mkTupPat  . tick <$> asks namespace <*> patlist)
 
-parseViewPat = ViewPatSimp <$> try_ "view pattern" (setR parseTermOp <* reservedOp "->") <*> setR parsePatAnn
-
-mkPVar (SIName si "") = PWildcard si
-mkPVar s = PVarSimp s
-
-concatParPats ps = ParPat $ concat [p | ParPat p <- ps]
-
-litP = flip ViewPatSimp cTrue . SAppV (SGlobal $ SIName_ mempty (Just $ Infix 4) "==")
+    mkListPat TypeNS [p] = cList p
+    mkListPat ns ps      = foldr cCons cNil ps
 
-patlist = commaSep $ setR parsePatAnn
+    --mkTupPat :: [Pat] -> Pat
+    mkTupPat TypeNS [PParens x] = mkTTup [x]
+    mkTupPat ns     [PParens x] = mkTup [x]
+    mkTupPat _      [x]         = PParens x
+    mkTupPat TypeNS ps          = mkTTup ps
+    mkTupPat ns     ps          = mkTup ps
 
-mkListPat TypeNS [p] = cList p
-mkListPat ns ps      = foldr cCons cNil ps
+    mkTTup = cHList . mkListPat ExpNS
+    mkTup ps = foldr cHCons cHNil ps
 
---mkTupPat :: [Pat] -> Pat
-mkTupPat TypeNS [PParens x] = mkTTup [x]
-mkTupPat ns     [PParens x] = mkTup [x]
-mkTupPat _      [x]         = PParens x
-mkTupPat TypeNS ps          = mkTTup ps
-mkTupPat ns     ps          = mkTup ps
+    parseViewPat = ViewPatSimp <$> try_ "view pattern" (setR parseTermOp <* reservedOp "->") <*> setR parsePatAnn
 
-mkTTup = cHList . mkListPat ExpNS
-mkTup ps = foldr cHCons cHNil ps
+    mkPVar (SIName si "") = PWildcard si
+    mkPVar s = PVarSimp s
 
-patType p (Wildcard SType) = p
-patType p t = PatTypeSimp p t
+    litP = flip ViewPatSimp cTrue . SAppV (SGlobal $ SIName_ mempty (Just $ Infix 4) "==")
 
-calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . getFixity . fst) e xs
+    patlist = commaSep $ setR parsePatAnn
 
 longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id)
 
@@ -397,7 +409,7 @@ parseDef =
                     , deBruijnify npsd $ foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ SGlobal <$> reverse npsd) ts'
                     )
             (af, cs) <- option (True, []) $
-                 (,) True . map (second $ (,) Nothing) . concat <$ reserved "where" <*> identation True (typedIds id npsd Nothing)
+                 (,) True . map (second $ (,) Nothing) . concat <$ reserved "where" <*> identation True (typedIds id npsd)
              <|> (,) False <$ reservedOp "=" <*>
                       sepBy1 ((,) <$> (addFixity' upperCase <|> parens (addFixity colonSymbols))
                                   <*> (mkConTy True <$> braces telescopeDataFields <|> mkConTy False <$> telescope Nothing)
@@ -407,7 +419,7 @@ parseDef =
  <|> do reserved "class" *> do
             x <- typeNS upperCase
             (nps, ts) <- telescope (Just SType)
-            cs <- option [] $ concat <$ reserved "where" <*> identation True (typedIds id nps Nothing)
+            cs <- option [] $ concat <$ reserved "where" <*> identation True (typedIds id nps)
             return $ pure $ Class x (map snd ts) cs
  <|> do reserved "instance" *> do
           typeNS $ do
@@ -433,7 +445,7 @@ parseDef =
                     runCheck $ fmap Stmt <$> compileStmt (compileGuardTrees id . const Nothing)
                         [{-TypeAnn x $ UncurryS ts $ SType-}{-todo-}]
                         [funAlt' x ts (map PVarSimp $ reverse nps) $ noGuards rhs]
- <|> do try_ "typed ident" $ map (uncurry TypeAnn) <$> typedIds addForalls' [] Nothing
+ <|> do try_ "typed ident" $ map (uncurry TypeAnn) <$> typedIds addForalls' []
  <|> fmap . (Stmt .) . flip PrecDef <$> parseFixity <*> commaSep1 rhsOperator
  <|> pure <$> funAltDef (Just lhsOperator) varId
  <|> valueDef