From d2ee0de25b0330c1ed53e2e0ae68e5ddda042aca Mon Sep 17 00:00:00 2001 From: Natalie Perna Date: Fri, 2 Jun 2017 12:39:40 -0400 Subject: [PATCH] Complete float Pullback diffs. Yet to be trimmed and put in figures. --- Figures/Pullback_abstract.diff | 171 ++++++++++++++++++++++++++++++++ Figures/Pullback_crosscall.diff | 127 ++++++++++++++++++++++++ Figures/Pullback_float.diff | 88 ++++++++++++++++ 3 files changed, 386 insertions(+) create mode 100644 Figures/Pullback_abstract.diff create mode 100644 Figures/Pullback_crosscall.diff create mode 100644 Figures/Pullback_float.diff diff --git a/Figures/Pullback_abstract.diff b/Figures/Pullback_abstract.diff new file mode 100644 index 0000000..d28a4d0 --- /dev/null +++ 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 new file mode 100644 index 0000000..295056c --- /dev/null +++ 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 new file mode 100644 index 0000000..b7504e7 --- /dev/null +++ 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