Update the 7.10 testsuite. Finally fixes #136.

goldfirere · Apr 26, 2016 · 889bd7a · 889bd7a
1 parent 373ab17
commit 889bd7a
Show file tree

Hide file tree

Showing 32 changed files with 587 additions and 345 deletions.
diff --git a/tests/compile-and-dump/GradingClient/Database.ghc710.template b/tests/compile-and-dump/GradingClient/Database.ghc710.template
@@ -97,7 +97,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
         = let
             lambda ::
               (t0 ~ ZeroSym0, t1 ~ ZeroSym0) =>
-              Sing (Apply (Apply CompareSym0 ZeroSym0) ZeroSym0 :: Ordering)
+              Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
             lambda
               = applySing
                   (applySing
@@ -115,7 +115,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                     t1 ~ Apply SuccSym0 b_0123456789) =>
               Sing a_0123456789
               -> Sing b_0123456789
-                 -> Sing (Apply (Apply CompareSym0 (Apply SuccSym0 a_0123456789)) (Apply SuccSym0 b_0123456789) :: Ordering)
+                 -> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
             lambda a_0123456789 b_0123456789
               = applySing
                   (applySing
@@ -138,7 +138,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
               forall _z_0123456789. (t0 ~ ZeroSym0,
                                      t1 ~ Apply SuccSym0 _z_0123456789) =>
               Sing _z_0123456789
-              -> Sing (Apply (Apply CompareSym0 ZeroSym0) (Apply SuccSym0 _z_0123456789) :: Ordering)
+              -> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
             lambda _z_0123456789 = SLT
           in lambda _s_z_0123456789
       sCompare (SSucc _s_z_0123456789) SZero
@@ -147,7 +147,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
               forall _z_0123456789. (t0 ~ Apply SuccSym0 _z_0123456789,
                                      t1 ~ ZeroSym0) =>
               Sing _z_0123456789
-              -> Sing (Apply (Apply CompareSym0 (Apply SuccSym0 _z_0123456789)) ZeroSym0 :: Ordering)
+              -> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
             lambda _z_0123456789 = SGT
           in lambda _s_z_0123456789
     instance SingI Zero where
@@ -519,8 +519,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall _z_0123456789. (t ~ _z_0123456789, t ~ Apply SchSym0 '[]) =>
-            Sing _z_0123456789
-            -> Sing (Apply (Apply LookupSym0 _z_0123456789) (Apply SchSym0 '[]) :: U)
+            Sing _z_0123456789 -> Sing (Apply (Apply LookupSym0 t) t :: U)
           lambda _z_0123456789 = undefined
         in lambda _s_z_0123456789
     sLookup sName (SSch (SCons (SAttr sName' sU) sAttrs))
@@ -530,9 +529,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                                         t ~ Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') u)) attrs)) =>
             Sing name
             -> Sing name'
-               -> Sing u
-                  -> Sing attrs
-                     -> Sing (Apply (Apply LookupSym0 name) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') u)) attrs)) :: U)
+               -> Sing u -> Sing attrs -> Sing (Apply (Apply LookupSym0 t) t :: U)
           lambda name name' u attrs
             = let
                 sScrutinee_0123456789 ::
@@ -545,27 +542,26 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                       -> let
                            lambda ::
                              TrueSym0 ~ Let0123456789Scrutinee_0123456789Sym4 name name' u attrs =>
-                             Sing (Case_0123456789 name name' u attrs TrueSym0)
+                             Sing (Case_0123456789 name name' u attrs TrueSym0 :: U)
                            lambda = u
                          in lambda
                     SFalse
                       -> let
                            lambda ::
                              FalseSym0 ~ Let0123456789Scrutinee_0123456789Sym4 name name' u attrs =>
-                             Sing (Case_0123456789 name name' u attrs FalseSym0)
+                             Sing (Case_0123456789 name name' u attrs FalseSym0 :: U)
                            lambda
                              = applySing
                                  (applySing (singFun2 (Proxy :: Proxy LookupSym0) sLookup) name)
                                  (applySing (singFun1 (Proxy :: Proxy SchSym0) SSch) attrs)
                          in lambda } ::
-                    Sing (Case_0123456789 name name' u attrs (Let0123456789Scrutinee_0123456789Sym4 name name' u attrs))
+                    Sing (Case_0123456789 name name' u attrs (Let0123456789Scrutinee_0123456789Sym4 name name' u attrs) :: U)
         in lambda sName sName' sU sAttrs
     sOccurs _s_z_0123456789 (SSch SNil)
       = let
           lambda ::
             forall _z_0123456789. (t ~ _z_0123456789, t ~ Apply SchSym0 '[]) =>
-            Sing _z_0123456789
-            -> Sing (Apply (Apply OccursSym0 _z_0123456789) (Apply SchSym0 '[]) :: Bool)
+            Sing _z_0123456789 -> Sing (Apply (Apply OccursSym0 t) t :: Bool)
           lambda _z_0123456789 = SFalse
         in lambda _s_z_0123456789
     sOccurs sName (SSch (SCons (SAttr sName' _s_z_0123456789) sAttrs))
@@ -576,8 +572,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
             Sing name
             -> Sing name'
                -> Sing _z_0123456789
-                  -> Sing attrs
-                     -> Sing (Apply (Apply OccursSym0 name) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') _z_0123456789)) attrs)) :: Bool)
+                  -> Sing attrs -> Sing (Apply (Apply OccursSym0 t) t :: Bool)
           lambda name name' _z_0123456789 attrs
             = applySing
                 (applySing
@@ -593,7 +588,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
           lambda ::
             forall _z_0123456789. (t ~ _z_0123456789, t ~ Apply SchSym0 '[]) =>
             Sing _z_0123456789
-            -> Sing (Apply (Apply AttrNotInSym0 _z_0123456789) (Apply SchSym0 '[]) :: Bool)
+            -> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool)
           lambda _z_0123456789 = STrue
         in lambda _s_z_0123456789
     sAttrNotIn
@@ -611,8 +606,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
             -> Sing u
                -> Sing name'
                   -> Sing _z_0123456789
-                     -> Sing t
-                        -> Sing (Apply (Apply AttrNotInSym0 (Apply (Apply AttrSym0 name) u)) (Apply SchSym0 (Apply (Apply (:$) (Apply (Apply AttrSym0 name') _z_0123456789)) t)) :: Bool)
+                     -> Sing t -> Sing (Apply (Apply AttrNotInSym0 t) t :: Bool)
           lambda name u name' _z_0123456789 t
             = applySing
                 (applySing
@@ -630,8 +624,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall _z_0123456789. (t ~ Apply SchSym0 '[], t ~ _z_0123456789) =>
-            Sing _z_0123456789
-            -> Sing (Apply (Apply DisjointSym0 (Apply SchSym0 '[])) _z_0123456789 :: Bool)
+            Sing _z_0123456789 -> Sing (Apply (Apply DisjointSym0 t) t :: Bool)
           lambda _z_0123456789 = STrue
         in lambda _s_z_0123456789
     sDisjoint (SSch (SCons sH sT)) sS
@@ -641,8 +634,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                            t ~ s) =>
             Sing h
             -> Sing t
-               -> Sing s
-                  -> Sing (Apply (Apply DisjointSym0 (Apply SchSym0 (Apply (Apply (:$) h) t))) s :: Bool)
+               -> Sing s -> Sing (Apply (Apply DisjointSym0 t) t :: Bool)
           lambda h t s
             = applySing
                 (applySing
@@ -660,9 +652,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall s1 s2. (t ~ Apply SchSym0 s1, t ~ Apply SchSym0 s2) =>
-            Sing s1
-            -> Sing s2
-               -> Sing (Apply (Apply AppendSym0 (Apply SchSym0 s1)) (Apply SchSym0 s2) :: Schema)
+            Sing s1 -> Sing s2 -> Sing (Apply (Apply AppendSym0 t) t :: Schema)
           lambda s1 s2
             = applySing
                 (singFun1 (Proxy :: Proxy SchSym0) SSch)

diff --git a/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc710.template b/tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc710.template
@@ -150,26 +150,22 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall _z_0123456789. (t ~ ZeroSym0, t ~ _z_0123456789) =>
-            Sing _z_0123456789
-            -> Sing (Apply (Apply LeqSym0 ZeroSym0) _z_0123456789 :: Bool)
+            Sing _z_0123456789 -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
           lambda _z_0123456789 = STrue
         in lambda _s_z_0123456789
     sLeq (SSucc _s_z_0123456789) SZero
       = let
           lambda ::
             forall _z_0123456789. (t ~ Apply SuccSym0 _z_0123456789,
                                    t ~ ZeroSym0) =>
-            Sing _z_0123456789
-            -> Sing (Apply (Apply LeqSym0 (Apply SuccSym0 _z_0123456789)) ZeroSym0 :: Bool)
+            Sing _z_0123456789 -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
           lambda _z_0123456789 = SFalse
         in lambda _s_z_0123456789
     sLeq (SSucc sA) (SSucc sB)
       = let
           lambda ::
             forall a b. (t ~ Apply SuccSym0 a, t ~ Apply SuccSym0 b) =>
-            Sing a
-            -> Sing b
-               -> Sing (Apply (Apply LeqSym0 (Apply SuccSym0 a)) (Apply SuccSym0 b) :: Bool)
+            Sing a -> Sing b -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
           lambda a b
             = applySing
                 (applySing (singFun2 (Proxy :: Proxy LeqSym0) sLeq) a) b
@@ -178,7 +174,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall n. (t ~ n, t ~ '[]) =>
-            Sing n -> Sing (Apply (Apply InsertSym0 n) '[] :: [Nat])
+            Sing n -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
           lambda n
             = applySing
                 (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) n) SNil
@@ -188,9 +184,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
           lambda ::
             forall n h t. (t ~ n, t ~ Apply (Apply (:$) h) t) =>
             Sing n
-            -> Sing h
-               -> Sing t
-                  -> Sing (Apply (Apply InsertSym0 n) (Apply (Apply (:$) h) t) :: [Nat])
+            -> Sing h -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
           lambda n h t
             = let
                 sScrutinee_0123456789 ::
@@ -203,7 +197,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                       -> let
                            lambda ::
                              TrueSym0 ~ Let0123456789Scrutinee_0123456789Sym3 n h t =>
-                             Sing (Case_0123456789 n h t TrueSym0)
+                             Sing (Case_0123456789 n h t TrueSym0 :: [Nat])
                            lambda
                              = applySing
                                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) n)
@@ -213,27 +207,25 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                       -> let
                            lambda ::
                              FalseSym0 ~ Let0123456789Scrutinee_0123456789Sym3 n h t =>
-                             Sing (Case_0123456789 n h t FalseSym0)
+                             Sing (Case_0123456789 n h t FalseSym0 :: [Nat])
                            lambda
                              = applySing
                                  (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) h)
                                  (applySing
                                     (applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) n) t)
                          in lambda } ::
-                    Sing (Case_0123456789 n h t (Let0123456789Scrutinee_0123456789Sym3 n h t))
+                    Sing (Case_0123456789 n h t (Let0123456789Scrutinee_0123456789Sym3 n h t) :: [Nat])
         in lambda sN sH sT
     sInsertionSort SNil
       = let
-          lambda :: t ~ '[] => Sing (Apply InsertionSortSym0 '[] :: [Nat])
+          lambda :: t ~ '[] => Sing (Apply InsertionSortSym0 t :: [Nat])
           lambda = SNil
         in lambda
     sInsertionSort (SCons sH sT)
       = let
           lambda ::
             forall h t. t ~ Apply (Apply (:$) h) t =>
-            Sing h
-            -> Sing t
-               -> Sing (Apply InsertionSortSym0 (Apply (Apply (:$) h) t) :: [Nat])
+            Sing h -> Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat])
           lambda h t
             = applySing
                 (applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) h)

diff --git a/tests/compile-and-dump/Singletons/AsPattern.ghc710.template b/tests/compile-and-dump/Singletons/AsPattern.ghc710.template
@@ -226,7 +226,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
       Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat)
     sFoo SNil
       = let
-          lambda :: t ~ '[] => Sing (Apply FooSym0 '[] :: [Nat])
+          lambda :: t ~ '[] => Sing (Apply FooSym0 t :: [Nat])
           lambda
             = let
                 sP :: Sing Let0123456789PSym0
@@ -237,8 +237,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall wild_0123456789. t ~ Apply (Apply (:$) wild_0123456789) '[] =>
-            Sing wild_0123456789
-            -> Sing (Apply FooSym0 (Apply (Apply (:$) wild_0123456789) '[]) :: [Nat])
+            Sing wild_0123456789 -> Sing (Apply FooSym0 t :: [Nat])
           lambda wild_0123456789
             = let
                 sP :: Sing (Let0123456789PSym1 wild_0123456789)
@@ -257,8 +256,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
                    wild_0123456789. t ~ Apply (Apply (:$) wild_0123456789) (Apply (Apply (:$) wild_0123456789) wild_0123456789) =>
             Sing wild_0123456789
             -> Sing wild_0123456789
-               -> Sing wild_0123456789
-                  -> Sing (Apply FooSym0 (Apply (Apply (:$) wild_0123456789) (Apply (Apply (:$) wild_0123456789) wild_0123456789)) :: [Nat])
+               -> Sing wild_0123456789 -> Sing (Apply FooSym0 t :: [Nat])
           lambda wild_0123456789 wild_0123456789 wild_0123456789
             = let
                 sP ::
@@ -277,9 +275,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
             forall wild_0123456789
                    wild_0123456789. t ~ Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789 =>
             Sing wild_0123456789
-            -> Sing wild_0123456789
-               -> Sing (Apply TupSym0 (Apply (Apply Tuple2Sym0 wild_0123456789) wild_0123456789) :: (Nat,
-                                                                                                     Nat))
+            -> Sing wild_0123456789 -> Sing (Apply TupSym0 t :: (Nat, Nat))
           lambda wild_0123456789 wild_0123456789
             = let
                 sP :: Sing (Let0123456789PSym2 wild_0123456789 wild_0123456789)
@@ -292,8 +288,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         in lambda sWild_0123456789 sWild_0123456789
     sBaz_ SNothing
       = let
-          lambda ::
-            t ~ NothingSym0 => Sing (Apply Baz_Sym0 NothingSym0 :: Maybe Baz)
+          lambda :: t ~ NothingSym0 => Sing (Apply Baz_Sym0 t :: Maybe Baz)
           lambda
             = let
                 sP :: Sing Let0123456789PSym0
@@ -309,8 +304,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
                    wild_0123456789. t ~ Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789) =>
             Sing wild_0123456789
             -> Sing wild_0123456789
-               -> Sing wild_0123456789
-                  -> Sing (Apply Baz_Sym0 (Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789) wild_0123456789) wild_0123456789)) :: Maybe Baz)
+               -> Sing wild_0123456789 -> Sing (Apply Baz_Sym0 t :: Maybe Baz)
           lambda wild_0123456789 wild_0123456789 wild_0123456789
             = let
                 sP ::
@@ -330,8 +324,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall wild_0123456789. t ~ Apply JustSym0 wild_0123456789 =>
-            Sing wild_0123456789
-            -> Sing (Apply BarSym0 (Apply JustSym0 wild_0123456789) :: Maybe Nat)
+            Sing wild_0123456789 -> Sing (Apply BarSym0 t :: Maybe Nat)
           lambda wild_0123456789
             = let
                 sX :: Sing (Let0123456789XSym1 wild_0123456789)
@@ -342,16 +335,14 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         in lambda sWild_0123456789
     sBar SNothing
       = let
-          lambda ::
-            t ~ NothingSym0 => Sing (Apply BarSym0 NothingSym0 :: Maybe Nat)
+          lambda :: t ~ NothingSym0 => Sing (Apply BarSym0 t :: Maybe Nat)
           lambda = SNothing
         in lambda
     sMaybePlus (SJust sN)
       = let
           lambda ::
             forall n. t ~ Apply JustSym0 n =>
-            Sing n
-            -> Sing (Apply MaybePlusSym0 (Apply JustSym0 n) :: Maybe Nat)
+            Sing n -> Sing (Apply MaybePlusSym0 t :: Maybe Nat)
           lambda n
             = applySing
                 (singFun1 (Proxy :: Proxy JustSym0) SJust)
@@ -364,8 +355,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
     sMaybePlus SNothing
       = let
           lambda ::
-            t ~ NothingSym0 =>
-            Sing (Apply MaybePlusSym0 NothingSym0 :: Maybe Nat)
+            t ~ NothingSym0 => Sing (Apply MaybePlusSym0 t :: Maybe Nat)
           lambda
             = let
                 sP :: Sing Let0123456789PSym0

diff --git a/tests/compile-and-dump/Singletons/BoxUnBox.ghc710.template b/tests/compile-and-dump/Singletons/BoxUnBox.ghc710.template
@@ -32,7 +32,7 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
       = let
           lambda ::
             forall a. t ~ Apply FBoxSym0 a =>
-            Sing a -> Sing (Apply UnBoxSym0 (Apply FBoxSym0 a) :: a)
+            Sing a -> Sing (Apply UnBoxSym0 t :: a)
           lambda a = a
         in lambda sA
     data instance Sing (z :: Box a)