refactoring

3 files changed, 28 insertions, 32 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index eb7c59cf..4f04a2ae 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -73,8 +73,8 @@ data Exp
     = ELit   Lit
     | TType_ Freq
     | Lam_   FreeVars Exp
-    | Con_   FreeVars ConName !Int{-number of ereased arguments applied-} [Exp]
-    | TyCon_ FreeVars TyConName [Exp]
+    | Con_   FreeVars ConName !Int{-number of ereased arguments applied-} [Exp]{-args reversed-}
+    | TyCon_ FreeVars TyConName [Exp]{-args reversed-}
     | Pi_    FreeVars Visibility Exp Exp
     | Neut   Neutral
     | RHS    Exp{-always in hnf-}
@@ -160,8 +160,7 @@ pattern DFunN_ a t xs <- Fun (FunName' a t) xs _
   where DFunN_ a t xs =  Fun (FunName' a t) xs delta
 
 conParams (conTypeName -> TyConName _ _ _ _ (CaseFunName _ _ pars)) = pars
-mkConPars n (snd . getParams . hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) xs
---mkConPars 0 TType = []  -- ?
+mkConPars n (snd . getParams . hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) $ reverse xs
 mkConPars n x@Neut{} = error $ "mkConPars!: " ++ ppShow x
 mkConPars n x = error $ "mkConPars: " ++ ppShow (n, x)
 
@@ -169,11 +168,8 @@ pattern ConN s a   <- Con (ConName (FTag s) _ _) _ a
 tCon s i t a        = Con (ConName (FTag s) i t) 0 a
 tCon_ k s i t a     = Con (ConName (FTag s) i t) k a
 pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a
-pattern TTyCon s t a <- TyCon (TyConName s _ t _ _) a
 
 pattern TTyCon0 s  <- TyCon (TyConName (FTag s) _ _ _ _) []
-
-tTyCon s t a cs = TyCon (TyConName s (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a
 tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
 
 pattern a :~> b = Pi Visible a b
@@ -189,9 +185,9 @@ pattern TFloat      <- TTyCon0 F'Float     where TFloat      = tTyCon0 F'Float $
 pattern TString     <- TTyCon0 F'String    where TString     = tTyCon0 F'String $ error "cs 6"
 pattern TChar       <- TTyCon0 F'Char      where TChar       = tTyCon0 F'Char $ error "cs 7"
 pattern TOrdering   <- TTyCon0 F'Ordering  where TOrdering   = tTyCon0 F'Ordering $ error "cs 8"
-pattern TVec a b    <- TyConN (FTag F'VecS) [b, a]
+pattern TVec a b    <- TyConN (FTag F'VecS) [a, b]
 
-pattern Empty s    <- TyCon (TyConName (FTag F'Empty) _ _ _ _) [HString{-hnf?-} s]
+pattern Empty s    <- TyCon (TyConName (FTag F'Empty) _ _ _ _) (HString{-hnf?-} s: _)
   where Empty s     = TyCon (TyConName (FTag F'Empty) (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s]
 
 pattern TT          <- Con _ _ _
@@ -232,7 +228,7 @@ pattern ENat n <- (fromNatE -> Just n)
 
 fromNatE :: Exp -> Maybe Int
 fromNatE (hnf -> ConN FZero _) = Just 0
-fromNatE (hnf -> ConN FSucc (n:_)) = succ <$> fromNatE n
+fromNatE (hnf -> ConN FSucc (n: _)) = succ <$> fromNatE n
 fromNatE _ = Nothing
 
 mkOrdering x = case x of
@@ -404,12 +400,12 @@ instance MkDoc Exp where
         Pi h TType b    -> shLam_ (usedVar 0 b) (BPi h) Nothing (mkDoc pr b)
         Pi h a b        -> shLam (usedVar 0 b) (BPi h) (mkDoc pr a) (mkDoc pr b)
         ENat n          -> pShow n
-        Con s@(ConName _ i _) _ xs | body -> text $ "<<" ++ showNth i ++ " constructor of " ++ show (conTypeName s) ++ ">>"
-        ConN FHCons [_, _, x, xs] -> foldl DApp (text "HCons") (mkDoc pr <$> [x, xs])
-        Con s _ xs      -> foldl DApp (pShow s) (mkDoc pr <$> xs)
-        TyCon s@(TyConName _ i _ cs _) xs | body
+        Con s@(ConName _ i _) _ _ | body -> text $ "<<" ++ showNth i ++ " constructor of " ++ show (conTypeName s) ++ ">>"
+        ConN FHCons (xs: x: _{-2-}) -> foldl DApp (text "HCons") (mkDoc pr <$> [x, xs])
+        Con s _ xs      -> foldlrev DApp (pShow s) (mkDoc pr <$> xs)
+        TyCon s@(TyConName _ i _ cs _) _ | body
             -> text $ "<<type constructor with " ++ show i ++ " indices; constructors: " ++ intercalate ", " (show . fst <$> cs) ++ ">>"
-        TyConN s xs     -> foldl DApp (pShow s) (mkDoc pr <$> xs)
+        TyConN s xs     -> foldlrev DApp (pShow s) (mkDoc pr <$> xs)
         TType           -> text "Type"
         ELit l          -> pShow l
         Neut x          -> mkDoc pr x
@@ -446,7 +442,7 @@ instance MkDoc Neutral where
           where (_h, v) = splitAt loc $ mkDoc pr <$> reverse xs
         Var_ k              -> shVar k
         App_ a b            -> mkDoc pr a `DApp` mkDoc pr b
-        CaseFun_ s@(CaseFunName _ _ p) xs n | body -> text $ "<<case function of a type with " ++ show p ++ " parameters>>"
+        CaseFun_ s@(CaseFunName _ _ p) _ n | body -> text $ "<<case function of a type with " ++ show p ++ " parameters>>"
         CaseFun_ s xs n     -> foldl DApp (pShow s) (map (mkDoc pr) $ xs ++ [Neut n])
         TyCaseFun_ _ _ _ | body -> text "<<type case function>>"
         TyCaseFun_ s [m, t, f] n  -> foldl DApp (pShow s) (mkDoc pr <$> [m, t, Neut n, f])
@@ -494,8 +490,8 @@ getFunDef t s f = case show s of
 
     "unsafeCoerce"      -> Just $ \case xs@(x@(hnf -> NonNeut): _{-2-}) -> x; xs -> f xs
     "reflCstr"          -> Just $ \case _ -> TT
-    "hlistNilCase"      -> Just $ \case ((hnf -> Con n@(ConName _ 0 _) _ _): x: _{-1-}) -> x; xs -> f xs
-    "hlistConsCase"     -> Just $ \case ((hnf -> Con n@(ConName _ 1 _) _ (_: _: a: b: _)): x: _{-3-}) -> x `app_` a `app_` b; xs -> f xs
+    "hlistNilCase"      -> Just $ \case ((hnf -> ConN FHCons _): x: _{-1-}) -> x; xs -> f xs
+    "hlistConsCase"     -> Just $ \case ((hnf -> ConN FHNil (b: a: _{-2-})): x: _{-3-}) -> x `app_` a `app_` b; xs -> f xs
 
     -- general compiler primitives
     "primAddInt"        -> Just $ \case (HInt j: HInt i: _)    -> HInt (i + j); xs -> f xs
@@ -564,7 +560,7 @@ getFunDef t s f = case show s of
     modF x y = x - fromIntegral (floor (x / y)) * y
 
 evalCaseFun _ a ps (Con n@(ConName _ i _) _ vs)
-    | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs
+    | i /= (-1) = foldlrev app_ (ps !!! (i + 1)) vs
     | otherwise = error "evcf"
   where
     xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps
@@ -580,7 +576,7 @@ evalTyCaseFun a b c = evalTyCaseFun_ (foldMap getFreeVars b <> getFreeVars c) a
 evalTyCaseFun_ s a b (Reduced c) = evalTyCaseFun_ s a b c
 evalTyCaseFun_ s a b (Neut c) = Neut $ TyCaseFun__ s a b c
 evalTyCaseFun_ _ (TyCaseFunName (FTag F'Type) ty) (_: t: f: _) TType = t
-evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldl app_ t vs
+evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) (TyCon (TyConName n' _ _ _ _) vs) | n == n' = foldlrev app_ t vs
 --evalTyCaseFun (TyCaseFunName n ty) [_, t, f] (DFun (FunName n' _) vs) | n == n' = foldl app_ t vs  -- hack
 evalTyCaseFun_ _ (TyCaseFunName n ty) (_: t: f: _) _ = f
 
@@ -597,9 +593,9 @@ cstr = f []
     f_ _ _ a a' | a == a' = CUnit
     f_ ns typ (RHS a) (RHS a') = f ns typ a a'
     f_ ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = 
-        ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs'
+        ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ reverse $ zip xs xs'
     f_ ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = 
-        ff ns (nType a) $ zip xs xs'
+        ff ns (nType a) $ reverse $ zip xs xs'
     f_ (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a'
     f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b')
 
@@ -640,8 +636,8 @@ app_ :: Exp -> Exp -> Exp
 app_ a b = app__ (getFreeVars a <> getFreeVars b) a b
 
 app__ _ (Lam x) a = subst 0 a x
-app__ _ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a])
-app__ _ (TyCon s xs) a = TyCon s (xs ++ [a])
+app__ _ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (a: xs)
+app__ _ (TyCon s xs) a = TyCon s (a: xs)
 app__ _ (SubstLet f) a = app_ f a
 app__ s (Neut f) a = neutApp f a
   where
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 6dd39a93..892eda2e 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -862,8 +862,8 @@ mkPi _ = Nothing
 mkLam (ExpTV (I.Lam y) (I.Pi b x yt) vs) = Just (b, x .@ vs, ExpTV y yt $ addToEnv x vs)
 mkLam _ = Nothing
 
-mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs)
-mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (I.Con s n (reverse -> xs)) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs)
+mkCon (ExpTV (I.TyCon s (reverse -> xs)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
 mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ loc _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, drop loc $ chain vs (nType s) xs)
 mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n])
 mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f])
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index f726f30b..6d26cedd 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -201,11 +201,11 @@ neutType' te = \case
     Fun s a _      -> foldlrev appTy (nType s) a
 
 makeCaseFunPars te n = case neutType te n of
-    (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars xs
+    (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars $ reverse xs
     x -> error $ "makeCaseFunPars: " ++ ppShow x
 
 makeCaseFunPars' te n = case neutType' te n of
-    (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars xs
+    (hnf -> TyCon (TyConName _ _ _ _ (CaseFunName _ _ pars)) xs) -> take pars $ reverse xs
 
 -------------------------------------------------------------------------------- inference
 
@@ -261,7 +261,7 @@ inferN_ tellTrace = infer  where
             = infer te $ x `SAppV` SLamV (STyped (ET (substTo (v+1) (Var 0) $ up 1 t) TType)) `SAppV` a `SAppV` b `SAppV` SVar siv v
             -- temporal hack
         | x@(SGlobal (sName -> CaseName "'VecS")) `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v <- e
-        , TyConN (FTag F'VecS) [_, Var n'] <- snd $ varType "xx" v te
+        , TyConN (FTag F'VecS) [Var n', _] <- snd $ varType "xx" v te
             = infer te $ x `SAppV` SLamV (SLamV (STyped (ET (substTo (n'+2) (Var 1) $ up 2 t) TType))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v
 
 {-
@@ -471,8 +471,8 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt
         ET (Neut (App__ md a b)) zt
             | ET (Neut a') at <- recheck'' "app1" te $ ET (Neut a) (neutType te a)
             -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b]
-        ET (Con_ md s n as) zt      -> checkApps (ppShow s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as
-        ET (TyCon_ md s as) zt      -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as
+        ET (Con_ md s n as) zt      -> checkApps (ppShow s) [] zt (Con_ md s n . reverse . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ reverse as
+        ET (TyCon_ md s as) zt      -> checkApps (ppShow s) [] zt (TyCon_ md s . reverse) te (nType s) $ reverse as
         ET (Neut (CaseFun__ fs s@(CaseFunName _ t pars) as n)) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun fs s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
         ET (Neut (TyCaseFun__ fs s [m, t, f] n)) zt  -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun_ fs s [m, t, f] n) te (nType s) [m, t, Neut n, f]
         ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
@@ -564,7 +564,7 @@ handleStmt = \case
     e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun' cfn (init $ drop (length ps) xs) (last xs)) ct
     let ps' = fst $ getParams vty
         t =   (TType :~> TType)
-          :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps'))
+          :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo' 0 $ length ps'))
           :~>  TType
           :~> Var 2 `app_` Var 0
           :~> Var 3 `app_` Var 1