Complete float Pullback diffs. Yet to be trimmed and put in figures.

sudonatalie · Jun 2, 2017 · d2ee0de · d2ee0de
1 parent ae2b95d
commit d2ee0de
Show file tree

Hide file tree

Showing 3 changed files with 386 additions and 0 deletions.
diff --git a/Figures/Pullback_abstract.diff b/Figures/Pullback_abstract.diff
@@ -0,0 +1,171 @@
+--- compile/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
++++ compile-abstract/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
+@@ -44,14 +44,22 @@
+ d26 v0 v1 v2 v3 v4 = du26 v1 v2 v3 v4
+ du26 v0 v1 v2 v3
+   = coe
+-      MAlonzo.Code.Data.Vec.du192 MAlonzo.Code.Data.Product.d26
++      MAlonzo.Code.Data.Vec.du192
++      (\ v4 ->
++         case coe v4 of
++           MAlonzo.Code.Data.Product.C30 v5 v6 -> coe v5
++           _ -> MAlonzo.RTE.mazUnreachableError)
+       (coe du24 v0 v1 v2 v3)
+ name28 = "Data.Fin.VecCat.PullbackB.FinPB\8320.p"
+ d28 v0 v1 v2 v3 v4 = du28 v1 v2 v3 v4
+ du28 v0 v1 v2 v3
+   = coe
+       MAlonzo.Code.Data.Fin.VecCat.PullbackVecUtils.du120
+-      MAlonzo.Code.Data.Product.d26 (coe du24 v0 v1 v2 v3)
++      (\ v4 ->
++         case coe v4 of
++           MAlonzo.Code.Data.Product.C30 v5 v6 -> coe v5
++           _ -> MAlonzo.RTE.mazUnreachableError)
++      (coe du24 v0 v1 v2 v3)
+ name30 = "Data.Fin.VecCat.PullbackB.FinPB\8320.\960"
+ d30 v0 v1 v2 v3 v4
+   = coe
+@@ -90,19 +98,30 @@
+ name60 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.s"
+ d60 v0 v1 v2 v3 v4 v5 v6 v7 = du60 v1 v2 v3 v4 v5
+ du60 v0 v1 v2 v3 v4
+-  = coe MAlonzo.Code.Data.Product.d26 (coe du58 v0 v1 v2 v3 v4)
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in
++    case coe v5 of
++      MAlonzo.Code.Data.Product.C30 v6 v7 -> coe v6
++      _ -> coe MAlonzo.RTE.mazUnreachableError
+ name62 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.n\8320"
+ d62 v0 v1 v2 v3 v4 v5 v6 v7 = du62 v1 v2 v3 v4 v5
+ du62 v0 v1 v2 v3 v4
+-  = let v5
+-          = coe MAlonzo.Code.Data.Product.d28 (coe du58 v0 v1 v2 v3 v4) in
+-    coe MAlonzo.Code.Data.Product.d26 v5
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in
++    case coe v5 of
++      MAlonzo.Code.Data.Product.C30 v6 v7
++        -> case coe v7 of
++             MAlonzo.Code.Data.Product.C30 v8 v9 -> coe v8
++             _ -> coe MAlonzo.RTE.mazUnreachableError
++      _ -> coe MAlonzo.RTE.mazUnreachableError
+ name70 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.v"
+ d70 v0 v1 v2 v3 v4 v5 v6 v7 = du70 v1 v2 v3 v4 v5
+ du70 v0 v1 v2 v3 v4
+-  = let v5
+-          = coe MAlonzo.Code.Data.Product.d28 (coe du58 v0 v1 v2 v3 v4) in
+-    coe MAlonzo.Code.Data.Product.d28 v5
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in
++    case coe v5 of
++      MAlonzo.Code.Data.Product.C30 v6 v7
++        -> case coe v7 of
++             MAlonzo.Code.Data.Product.C30 v8 v9 -> coe v9
++             _ -> coe MAlonzo.RTE.mazUnreachableError
++      _ -> coe MAlonzo.RTE.mazUnreachableError
+ name78 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.r\8320"
+ d78 v0 v1 v2 v3 v4 v5 v6 v7 = du78 v1 v2 v3 v4 v5 v6
+ du78 v0 v1 v2 v3 v4 v5
+@@ -162,25 +181,39 @@
+ name856
+   = "Data.Fin.VecCat.PullbackB._.\9417-HasPullbacks-HasProducts"
+ d856
+-  = let v0
+-          = coe
+-              MAlonzo.Code.Categoric.Category.d26
+-              MAlonzo.Code.Data.Fin.VecCat.d32 in
++  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+     coe
+       MAlonzo.Code.Categoric.FinLimits.du3924
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d522 v0)
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d524 v0)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
+ name858
+   = "Data.Fin.VecCat.PullbackB._.\9417-HasPullbacks-mkProduct"
+ d858
+-  = let v0
+-          = coe
+-              MAlonzo.Code.Categoric.Category.d26
+-              MAlonzo.Code.Data.Fin.VecCat.d32 in
++  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+     coe
+       MAlonzo.Code.Categoric.FinLimits.du3872
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d522 v0)
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d524 v0)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
+ name2950 = "Data.Fin.VecCat.PullbackB.FinPB._.f\10814g\728"
+ d2950 v0 v1 v2 v3 v4 = du2950 v1 v2 v3 v4
+ du2950 v0 v1 v2 v3 = coe du24 v0 v1 v2 v3
+@@ -242,23 +275,37 @@
+ d2992 v0 v1 v2 = coe d2990 v1 v2 v0
+ name3004 = "Data.Fin.VecCat.PullbackB.mkProduct\8242"
+ d3004
+-  = let v0
+-          = coe
+-              MAlonzo.Code.Categoric.Category.d26
+-              MAlonzo.Code.Data.Fin.VecCat.d32 in
++  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+     coe
+       MAlonzo.Code.Categoric.FinLimits.du3872
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d522 v0)
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d524 v0) (1 :: Integer)
+-      MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (1 :: Integer) MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
+ name3006 = "Data.Fin.VecCat.PullbackB.hasProducts\8242"
+ d3006
+-  = let v0
+-          = coe
+-              MAlonzo.Code.Categoric.Category.d26
+-              MAlonzo.Code.Data.Fin.VecCat.d32 in
++  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+     coe
+       MAlonzo.Code.Categoric.FinLimits.du3924
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d522 v0)
+-      (coe MAlonzo.Code.Categoric.Semigroupoid.d524 v0) (1 :: Integer)
+-      MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
+\ No newline at end of file
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (case coe v0 of
++         MAlonzo.Code.Categoric.Category.C1 v1 v2
++           -> case coe v1 of
++                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
++                _ -> coe MAlonzo.RTE.mazUnreachableError
++         _ -> MAlonzo.RTE.mazUnreachableError)
++      (1 :: Integer) MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
+\ No newline at end of file
diff --git a/Figures/Pullback_crosscall.diff b/Figures/Pullback_crosscall.diff
@@ -0,0 +1,127 @@
+--- compile-float/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
++++ compile-crosscall/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
+@@ -88,9 +88,10 @@
+ name46 = "Data.Fin.VecCat.PullbackB.FinPB\8320.mkPair"
+ d46 v0 v1 v2 v3 v4 v5 v6 v7 = du46 v1 v2 v3 v4 v5 v6
+ du46 v0 v1 v2 v3 v4 v5
+-  = coe
+-      MAlonzo.Code.Data.Nat.DivMod.du76 (coe du78 v0 v1 v2 v3 v4 v5)
+-      (coe du28 v0 v1 v2 v3)
++  = let v6 = coe du28 v0 v1 v2 v3 in
++    let v7 = coe du78 v0 v1 v2 v3 v4 v5 in dv46 v0 v1 v2 v3 v4 v5 v6 v7
++dv46 v0 v1 v2 v3 v4 v5 v6 v7
++  = coe MAlonzo.Code.Data.Nat.DivMod.du76 v7 v6
+ name58 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.lk"
+ d58 v0 v1 v2 v3 v4 v5 v6 v7 = du58 v1 v2 v3 v4 v5
+ du58 v0 v1 v2 v3 v4
+@@ -128,13 +129,21 @@
+ name78 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.r\8320"
+ d78 v0 v1 v2 v3 v4 v5 v6 v7 = du78 v1 v2 v3 v4 v5 v6
+ du78 v0 v1 v2 v3 v4 v5
+-  = coe
+-      addInt (coe du60 v0 v1 v2 v3 v4)
++  = let v6 = coe du58 v0 v1 v2 v3 v4 in dv78 v0 v1 v2 v3 v4 v5 v6
++dv78 v0 v1 v2 v3 v4 v5 v6
++  = case coe v6 of
++      MAlonzo.Code.Data.Product.C30 v7 v8
++        -> case coe v8 of
++             MAlonzo.Code.Data.Product.C30 v9 v10
++               -> coe
++                    addInt (coe dv60 v0 v1 v2 v3 v4 v6 v7 v8)
+       (coe
+          MAlonzo.Code.Data.Fin.du18
+          (coe
+             MAlonzo.Code.Data.Fin.VecCat.PullbackVecUtils.du302
+-            (coe du70 v0 v1 v2 v3 v4) v5))
++                          (coe dv70 v0 v1 v2 v3 v4 v6 v7 v8 v9 v10) v5))
++             _ -> coe MAlonzo.RTE.mazUnreachableError
++      _ -> coe MAlonzo.RTE.mazUnreachableError
+ name80 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.j\8712v"
+ d80
+   = error
+@@ -204,19 +213,22 @@
+ d858 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv858 v0
+ dv858 v0
+   = coe
+-      MAlonzo.Code.Categoric.FinLimits.du3872
+-      (case coe v0 of
+-         MAlonzo.Code.Categoric.Category.C1 v1 v2
+-           -> case coe v1 of
+-                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
++      (\ v1 ->
++         let v2
++               = case coe v0 of
++                   MAlonzo.Code.Categoric.Category.C1 v2 v3
++                     -> case coe v2 of
++                          MAlonzo.Code.Categoric.Semigroupoid.C5311 v4 v5 -> coe v5
++                          _ -> coe MAlonzo.RTE.mazUnreachableError
++                   _ -> coe MAlonzo.RTE.mazUnreachableError in
++         let v3
++               = case coe v0 of
++                   MAlonzo.Code.Categoric.Category.C1 v3 v4
++                     -> case coe v3 of
++                          MAlonzo.Code.Categoric.Semigroupoid.C5311 v5 v6 -> coe v5
+                 _ -> coe MAlonzo.RTE.mazUnreachableError
+-         _ -> MAlonzo.RTE.mazUnreachableError)
+-      (case coe v0 of
+-         MAlonzo.Code.Categoric.Category.C1 v1 v2
+-           -> case coe v1 of
+-                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
+-                _ -> coe MAlonzo.RTE.mazUnreachableError
+-         _ -> MAlonzo.RTE.mazUnreachableError)
++                   _ -> coe MAlonzo.RTE.mazUnreachableError in
++         \ v4 -> coe MAlonzo.Code.Categoric.FinLimits.du3872 v3 v2)
+ name2950 = "Data.Fin.VecCat.PullbackB.FinPB._.f\10814g\728"
+ d2950 v0 v1 v2 v3 v4 = du2950 v1 v2 v3 v4
+ du2950 v0 v1 v2 v3 = coe du24 v0 v1 v2 v3
+@@ -231,7 +243,7 @@
+ d2956 v0 v1 v2 v3 v4 = du2956 v1 v2 v4
+ du2956 v0 v1 v2 = coe du22 v0 v1 v2
+ name2958 = "Data.Fin.VecCat.PullbackB.FinPB._.mkPair"
+-d2958 v0 v1 v2 v3 v4 = du2958 v1 v2 v3 v4
++d2958 v0 v1 v2 v3 v4 v5 = du2958 v1 v2 v3 v4
+ du2958 v0 v1 v2 v3 v4 v5 v6 = coe du46 v0 v1 v2 v3 v4 v5
+ name2960 = "Data.Fin.VecCat.PullbackB.FinPB._.p"
+ d2960 v0 v1 v2 v3 v4 = du2960 v1 v2 v3 v4
+@@ -277,23 +289,28 @@
+ name2992 = "Data.Fin.VecCat.PullbackB.hasPullbacks\8242"
+ d2992 v0 v1 v2 = coe d2990 v1 v2 v0
+ name3004 = "Data.Fin.VecCat.PullbackB.mkProduct\8242"
+-d3004 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv3004 v0
+-dv3004 v0
+-  = coe
+-      MAlonzo.Code.Categoric.FinLimits.du3872
+-      (case coe v0 of
+-         MAlonzo.Code.Categoric.Category.C1 v1 v2
+-           -> case coe v1 of
+-                MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v3
+-                _ -> coe MAlonzo.RTE.mazUnreachableError
+-         _ -> MAlonzo.RTE.mazUnreachableError)
+-      (case coe v0 of
++d3004
++  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
++    let v1
++          = case coe v0 of
+          MAlonzo.Code.Categoric.Category.C1 v1 v2
+            -> case coe v1 of
+                 MAlonzo.Code.Categoric.Semigroupoid.C5311 v3 v4 -> coe v4
+                 _ -> coe MAlonzo.RTE.mazUnreachableError
+-         _ -> MAlonzo.RTE.mazUnreachableError)
+-      (1 :: Integer) MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
++              _ -> coe MAlonzo.RTE.mazUnreachableError in
++    let v2
++          = case coe v0 of
++              MAlonzo.Code.Categoric.Category.C1 v2 v3
++                -> case coe v2 of
++                     MAlonzo.Code.Categoric.Semigroupoid.C5311 v4 v5 -> coe v4
++                     _ -> coe MAlonzo.RTE.mazUnreachableError
++              _ -> coe MAlonzo.RTE.mazUnreachableError in
++    dv3004 v0 v1 v2
++dv3004 v0 v1 v2
++  = coe
++      (\ v3 ->
++         let v4 = coe d2992 in
++         coe MAlonzo.Code.Categoric.FinLimits.du3872 v2 v1 d2992)
+ name3006 = "Data.Fin.VecCat.PullbackB.hasProducts\8242"
+ d3006 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv3006 v0
+ dv3006 v0
diff --git a/Figures/Pullback_float.diff b/Figures/Pullback_float.diff
@@ -0,0 +1,88 @@
+--- compile-abstract/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
++++ compile-float/MAlonzo/Code/Data/Fin/VecCat/PullbackB.hs
+@@ -98,15 +98,17 @@
+ name60 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.s"
+ d60 v0 v1 v2 v3 v4 v5 v6 v7 = du60 v1 v2 v3 v4 v5
+ du60 v0 v1 v2 v3 v4
+-  = let v5 = coe du58 v0 v1 v2 v3 v4 in
+-    case coe v5 of
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in dv60 v0 v1 v2 v3 v4 v5
++dv60 v0 v1 v2 v3 v4 v5
++  = case coe v5 of
+       MAlonzo.Code.Data.Product.C30 v6 v7 -> coe v6
+       _ -> coe MAlonzo.RTE.mazUnreachableError
+ name62 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.n\8320"
+ d62 v0 v1 v2 v3 v4 v5 v6 v7 = du62 v1 v2 v3 v4 v5
+ du62 v0 v1 v2 v3 v4
+-  = let v5 = coe du58 v0 v1 v2 v3 v4 in
+-    case coe v5 of
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in dv62 v0 v1 v2 v3 v4 v5
++dv62 v0 v1 v2 v3 v4 v5
++  = case coe v5 of
+       MAlonzo.Code.Data.Product.C30 v6 v7
+         -> case coe v7 of
+              MAlonzo.Code.Data.Product.C30 v8 v9 -> coe v8
+@@ -115,8 +117,9 @@
+ name70 = "Data.Fin.VecCat.PullbackB.FinPB\8320._.v"
+ d70 v0 v1 v2 v3 v4 v5 v6 v7 = du70 v1 v2 v3 v4 v5
+ du70 v0 v1 v2 v3 v4
+-  = let v5 = coe du58 v0 v1 v2 v3 v4 in
+-    case coe v5 of
++  = let v5 = coe du58 v0 v1 v2 v3 v4 in dv70 v0 v1 v2 v3 v4 v5
++dv70 v0 v1 v2 v3 v4 v5
++  = case coe v5 of
+       MAlonzo.Code.Data.Product.C30 v6 v7
+         -> case coe v7 of
+              MAlonzo.Code.Data.Product.C30 v8 v9 -> coe v9
+@@ -180,9 +183,9 @@
+ d784 a0 a1 a2 a3 a4 = ()
+ name856
+   = "Data.Fin.VecCat.PullbackB._.\9417-HasPullbacks-HasProducts"
+-d856
+-  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+-    coe
++d856 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv856 v0
++dv856 v0
++  = coe
+       MAlonzo.Code.Categoric.FinLimits.du3924
+       (case coe v0 of
+          MAlonzo.Code.Categoric.Category.C1 v1 v2
+@@ -198,9 +201,9 @@
+          _ -> MAlonzo.RTE.mazUnreachableError)
+ name858
+   = "Data.Fin.VecCat.PullbackB._.\9417-HasPullbacks-mkProduct"
+-d858
+-  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+-    coe
++d858 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv858 v0
++dv858 v0
++  = coe
+       MAlonzo.Code.Categoric.FinLimits.du3872
+       (case coe v0 of
+          MAlonzo.Code.Categoric.Category.C1 v1 v2
+@@ -274,9 +277,9 @@
+ name2992 = "Data.Fin.VecCat.PullbackB.hasPullbacks\8242"
+ d2992 v0 v1 v2 = coe d2990 v1 v2 v0
+ name3004 = "Data.Fin.VecCat.PullbackB.mkProduct\8242"
+-d3004
+-  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+-    coe
++d3004 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv3004 v0
++dv3004 v0
++  = coe
+       MAlonzo.Code.Categoric.FinLimits.du3872
+       (case coe v0 of
+          MAlonzo.Code.Categoric.Category.C1 v1 v2
+@@ -292,9 +295,9 @@
+          _ -> MAlonzo.RTE.mazUnreachableError)
+       (1 :: Integer) MAlonzo.Code.Data.Fin.VecCat.d3916 d2992
+ name3006 = "Data.Fin.VecCat.PullbackB.hasProducts\8242"
+-d3006
+-  = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in
+-    coe
++d3006 = let v0 = coe MAlonzo.Code.Data.Fin.VecCat.d32 in dv3006 v0
++dv3006 v0
++  = coe
+       MAlonzo.Code.Categoric.FinLimits.du3924
+       (case coe v0 of
+          MAlonzo.Code.Categoric.Category.C1 v1 v2