From: Adam Megacz Date: Tue, 10 May 2011 04:57:53 +0000 (-0700) Subject: start using type-family-based GArrow classes X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=14afe39e905be69eabd8944b97bb2b731bf44939 start using type-family-based GArrow classes --- diff --git a/examples/Demo.hs b/examples/Demo.hs index 74bbef0..fea2dc7 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -5,6 +5,5 @@ import GHC.HetMet.Private import GArrowTikZ foo x = <[ ~~x ]> -foo' = unG . pga_flatten . foo . pga_unflatten ---foo x z = <[ let y = ~~x in ~~z y y ]> -main = tikz (foo' (PGArrowD { unG = TikZ_const 12 })) + +main = tikz' $ pga_flatten . foo . pga_unflatten diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index f545937..db21658 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -1,5 +1,5 @@ -{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances #-} -module GArrowTikZ (tikz, GArrowTikZ(..)) +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances -XTypeFamilies #-} +module GArrowTikZ (tikz, tikz', GArrowTikZ(..)) where import Prelude hiding ( id, (.), lookup ) import Control.Category @@ -7,7 +7,7 @@ import GHC.HetMet.GArrow import Data.List hiding (lookup, insert) import Data.Map hiding (map, (!)) import Unify - +import GHC.HetMet.Private {- TO DO: @@ -128,7 +128,11 @@ instance GArrowLoop GArrowTikZ (**) () where ga_loopl = TikZ_loopl ga_loopr = TikZ_loopr -instance GArrowSTKC GArrowTikZ (,) () +type instance GArrowTensor GArrowTikZ = (,) +type instance GArrowUnit GArrowTikZ = () +type instance GArrowExponent GArrowTikZ = (->) + +instance GArrowSTKC GArrowTikZ name :: GArrowTikZ a b -> String @@ -420,6 +424,9 @@ toTikZ' g = foldr (\x y -> x++"\\\\\n"++y) [] (map foo s) s = sortit (strip k) m = valuatit empty s +tikz' :: (forall g a . PGArrow g (GArrowUnit g) a -> PGArrow g (GArrowUnit g) a) -> IO () +tikz' x = tikz $ unG (x (PGArrowD { unG = TikZ_const 12 })) +main = do putStrLn "hello" tikz example = do putStrLn "\\documentclass{article}" putStrLn "\\usepackage[landscape,paperheight=20in,textwidth=19in]{geometry}" diff --git a/examples/Makefile b/examples/Makefile index 7819837..e411f32 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -6,7 +6,7 @@ all: tikz: mkdir -p .build - ../../../inplace/bin/ghc-stage2 -odir .build -hidir .build GArrowTikZ.hs Unify.hs test.hs - ./test > .build/test.tex + ../../../inplace/bin/ghc-stage2 -odir .build -hidir .build GArrowTikZ.hs Unify.hs Demo.hs -o .build/demo + ./.build/demo > .build/test.tex cd .build; pdflatex test.tex open .build/test.pdf diff --git a/examples/Unify.dump-coqpass b/examples/Unify.dump-coqpass new file mode 100644 index 0000000..e69de29 diff --git a/examples/x b/examples/x new file mode 100644 index 0000000..48cdc1c --- /dev/null +++ b/examples/x @@ -0,0 +1,1184 @@ +[3 of 3] Compiling Main ( Demo.hs, .build/Main.o ) + +==================== Desugared, before opt ==================== +@ co_aLI::() ~ () +co_aLI = TYPE () + +@ co_aHe::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ () +co_aHe = TYPE trans GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ co_aLI + +Rec { +$dGArrowSTKC_aHd + :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ +[LclId] +$dGArrowSTKC_aHd = GArrowTikZ.$fGArrowSTKCGArrowTikZ + +Main.foo + :: forall (t_aD6 :: * -> * -> *) t_aD7. + <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6 +[LclId] +Main.foo = + \ (@ t_aD6::* -> * -> *) (@ t_aD7) -> + letrec { + foo_aD5 :: <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6 + [LclId] + foo_aD5 = + \ (x_aD4 :: <[t_aD7]>@t_aD6) -> + GHC.HetMet.CodeTypes.hetmet_brak + @ t_aD6 + @ t_aD7 + ((GHC.HetMet.CodeTypes.hetmet_esc @ t_aD6 @ t_aD7 x_aD4) + `cast` (t_aD7 :: t_aD7 ~ t_aD7)); } in + foo_aD5 + +Main.foo' + :: forall (g_aFo :: * -> * -> *) y_aFp. + (GHC.HetMet.GArrow.GArrowSTKC g_aFo, + GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) => + GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp +[LclId] +Main.foo' = + \ (@ g_aFo::* -> * -> *) + (@ y_aFp) + ($dGArrowSTKC_aFq :: GHC.HetMet.GArrow.GArrowSTKC g_aFo) + (@ co_aFr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) -> + let { + @ co_aMM::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMM = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aML::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aML = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMK::() ~ () + co_aMK = TYPE () } in + let { + @ co_aMJ::() ~ () + co_aMJ = TYPE () } in + let { + @ co_aMI::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMH::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMH = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMG::() ~ () + co_aMG = TYPE () } in + let { + @ co_aMF::() ~ () + co_aMF = TYPE () } in + let { + @ co_aME::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aME = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMD::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMD = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMC::() ~ () + co_aMC = TYPE () } in + let { + @ co_aMB::() ~ () + co_aMB = TYPE () } in + let { + @ co_aMz::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aMz = TYPE trans co_aFr (sym co_aMB) } in + let { + @ co_aMu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aMu = TYPE trans co_aFr (sym co_aMF) } in + let { + @ co_aMp::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aMp = TYPE trans co_aFr (sym co_aMJ) } in + let { + @ co_aM1::GHC.HetMet.GArrow.GArrowUnit g_aFo + ~ + GHC.HetMet.GArrow.GArrowUnit g_aFo + co_aM1 = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in + let { + @ co_aM4::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aM4 = TYPE trans (sym co_aM1) co_aFr } in + let { + @ co_aLZ::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aLZ = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aMn::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMn = TYPE trans co_aLZ (sym co_aML) } in + let { + @ co_aMs::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMs = TYPE trans co_aLZ (sym co_aMH) } in + let { + @ co_aMx::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aMx = TYPE trans co_aLZ (sym co_aMD) } in + let { + @ co_aLV::GHC.HetMet.GArrow.GArrowUnit g_aFo + ~ + GHC.HetMet.GArrow.GArrowUnit g_aFo + co_aLV = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in + let { + @ co_aM5::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aM5 = TYPE trans (sym co_aLV) co_aFr } in + let { + @ co_aLT::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aLT = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aM6::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aM6 = TYPE trans (sym co_aLT) co_aLZ } in + let { + @ co_aLP::GHC.HetMet.GArrow.GArrowUnit g_aFo + ~ + GHC.HetMet.GArrow.GArrowUnit g_aFo + co_aLP = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in + let { + @ co_aM7::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aM7 = TYPE trans (sym co_aLP) co_aFr } in + let { + @ co_aLN::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aLN = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aM8::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aM8 = TYPE trans (sym co_aLN) co_aLZ } in + let { + $dGArrowSwap_aLL + :: GHC.HetMet.GArrow.GArrowSwap + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrowSwap_aLL = + GHC.HetMet.GArrow.$p3GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in + let { + $dGArrow_aM2 + :: GHC.HetMet.GArrow.GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrow_aM2 = + GHC.HetMet.GArrow.$p1GArrowSwap + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrowSwap_aLL } in + let { + $dCategory_aM3 :: Control.Category.Category g_aFo + [LclId] + $dCategory_aM3 = + GHC.HetMet.GArrow.$p1GArrow + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrow_aM2 } in + let { + $dGArrow_aMa + :: GHC.HetMet.GArrow.GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrow_aMa = + $dGArrow_aM2 + `cast` (GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4 + :: GHC.HetMet.GArrow.T:GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrowSwap_aM9 + :: GHC.HetMet.GArrow.GArrowSwap + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrowSwap_aM9 = + $dGArrowSwap_aLL + `cast` (GHC.HetMet.GArrow.T:GArrowSwap + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4 + :: GHC.HetMet.GArrow.T:GArrowSwap + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrowSwap + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrowCopy_aLK + :: GHC.HetMet.GArrow.GArrowCopy + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrowCopy_aLK = + GHC.HetMet.GArrow.$p2GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in + let { + $dGArrow_aLW + :: GHC.HetMet.GArrow.GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrow_aLW = + GHC.HetMet.GArrow.$p1GArrowCopy + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrowCopy_aLK } in + let { + $dCategory_aLX :: Control.Category.Category g_aFo + [LclId] + $dCategory_aLX = + GHC.HetMet.GArrow.$p1GArrow + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrow_aLW } in + let { + $dGArrow_aMd + :: GHC.HetMet.GArrow.GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrow_aMd = + $dGArrow_aLW + `cast` (GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5 + :: GHC.HetMet.GArrow.T:GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrow_aMe + :: GHC.HetMet.GArrow.GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrow_aMe = + $dGArrow_aMd + `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM6 () + :: GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + ~ + GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrowCopy_aMb + :: GHC.HetMet.GArrow.GArrowCopy + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrowCopy_aMb = + $dGArrowCopy_aLK + `cast` (GHC.HetMet.GArrow.T:GArrowCopy + g_aFo co_aM6 (GHC.HetMet.GArrow.GArrowUnit g_aFo) + :: GHC.HetMet.GArrow.T:GArrowCopy + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrowCopy + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in + let { + $dGArrowCopy_aMc + :: GHC.HetMet.GArrow.GArrowCopy + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrowCopy_aMc = + $dGArrowCopy_aMb + `cast` (GHC.HetMet.GArrow.T:GArrowCopy + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5 + :: GHC.HetMet.GArrow.T:GArrowCopy + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrowCopy + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrowDrop_aLJ + :: GHC.HetMet.GArrow.GArrowDrop + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrowDrop_aLJ = + GHC.HetMet.GArrow.$p1GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in + let { + $dGArrow_aLQ + :: GHC.HetMet.GArrow.GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrow_aLQ = + GHC.HetMet.GArrow.$p1GArrowDrop + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrowDrop_aLJ } in + let { + $dCategory_aLR :: Control.Category.Category g_aFo + [LclId] + $dCategory_aLR = + GHC.HetMet.GArrow.$p1GArrow + @ g_aFo + @ (GHC.HetMet.GArrow.GArrowTensor g_aFo) + @ (GHC.HetMet.GArrow.GArrowUnit g_aFo) + $dGArrow_aLQ } in + let { + $dGArrow_aMh + :: GHC.HetMet.GArrow.GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrow_aMh = + $dGArrow_aLQ + `cast` (GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7 + :: GHC.HetMet.GArrow.T:GArrow + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrow_aMi + :: GHC.HetMet.GArrow.GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrow_aMi = + $dGArrow_aMh + `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM8 () + :: GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + ~ + GHC.HetMet.GArrow.T:GArrow + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + $dGArrowDrop_aMf + :: GHC.HetMet.GArrow.GArrowDrop + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + [LclId] + $dGArrowDrop_aMf = + $dGArrowDrop_aLJ + `cast` (GHC.HetMet.GArrow.T:GArrowDrop + g_aFo co_aM8 (GHC.HetMet.GArrow.GArrowUnit g_aFo) + :: GHC.HetMet.GArrow.T:GArrowDrop + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrowDrop + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in + let { + $dGArrowDrop_aMg + :: GHC.HetMet.GArrow.GArrowDrop + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) () + [LclId] + $dGArrowDrop_aMg = + $dGArrowDrop_aMf + `cast` (GHC.HetMet.GArrow.T:GArrowDrop + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7 + :: GHC.HetMet.GArrow.T:GArrowDrop + g_aFo + (GHC.HetMet.GArrow.GArrowTensor g_aFo) + (GHC.HetMet.GArrow.GArrowUnit g_aFo) + ~ + GHC.HetMet.GArrow.T:GArrowDrop + g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in + let { + @ co_aF3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aF3 = TYPE co_aFr } in + let { + @ co_aEX::() ~ () + co_aEX = TYPE () } in + let { + @ co_aEI::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aEG::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEG = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aEF::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEF = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aEE::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aEE = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aF3) + (sym co_aEX) } in + let { + @ co_aEz::() ~ () + co_aEz = TYPE () } in + let { + @ co_aF0::() ~ () + co_aF0 = TYPE trans co_aEz co_aEX } in + let { + @ co_aEy::() ~ () + co_aEy = TYPE () } in + let { + @ co_aEx::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEx = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEI) + (sym co_aEG) } in + let { + @ co_aEw::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEw = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aEH::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEH = TYPE trans co_aEw co_aEG } in + let { + @ co_aEv::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEv = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in + let { + @ co_aEu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aEu = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEE) + (sym co_aEz) } in + let { + @ co_aEq::() ~ () + co_aEq = TYPE () } in + let { + @ co_aEC::() ~ () + co_aEC = TYPE trans co_aEq co_aEz } in + let { + @ co_aEZ::() ~ () + co_aEZ = TYPE trans co_aEC co_aEX } in + let { + @ co_aEp::() ~ () + co_aEp = TYPE () } in + let { + @ co_aEo::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aEo = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEu) + (sym co_aEq) } in + let { + @ co_aEl::() ~ () + co_aEl = TYPE () } in + let { + @ co_aEs::() ~ () + co_aEs = TYPE trans co_aEl co_aEq } in + let { + @ co_aED::() ~ () + co_aED = TYPE trans co_aEs co_aEz } in + let { + @ co_aF1::() ~ () + co_aF1 = TYPE trans co_aED co_aEX } in + let { + @ co_aEk::() ~ () + co_aEk = TYPE () } in + let { + @ co_aEj::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aEj = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEo) + (sym co_aEl) } in + let { + @ co_aEh::() ~ () + co_aEh = TYPE () } in + let { + @ co_aEn::() ~ () + co_aEn = TYPE trans co_aEh co_aEl } in + let { + @ co_aEr::() ~ () + co_aEr = TYPE trans co_aEn co_aEq } in + let { + @ co_aEA::() ~ () + co_aEA = TYPE trans co_aEr co_aEz } in + let { + @ co_aEY::() ~ () + co_aEY = TYPE trans co_aEA co_aEX } in + let { + @ co_aEg::() ~ () + co_aEg = TYPE () } in + let { + @ co_aEf::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aEf = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in + let { + @ co_aEi::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aEi = + TYPE trans + co_aEf (GHC.HetMet.Private.PGArrow g_aFo co_aEh y_aFp) } in + let { + @ co_aEm::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aEm = + TYPE trans + co_aEi (GHC.HetMet.Private.PGArrow g_aFo co_aEl y_aFp) } in + let { + @ co_aEt::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aEt = + TYPE trans + co_aEm (GHC.HetMet.Private.PGArrow g_aFo co_aEq y_aFp) } in + let { + @ co_aEB::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aEB = + TYPE trans + co_aEt (GHC.HetMet.Private.PGArrow g_aFo co_aEz y_aFp) } in + let { + @ co_aF2::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aF2 = + TYPE trans + co_aEB (GHC.HetMet.Private.PGArrow g_aFo co_aEX y_aFp) } in + let { + @ co_aEd::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aEd = TYPE trans co_aEj (sym co_aEk) } in + let { + @ co_aEb::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aEb = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEx) + (sym co_aEw) } in + let { + @ co_aE8::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aE8 = TYPE trans co_aEo (sym co_aEp) } in + let { + @ co_aE6::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aE6 = TYPE trans co_aEb (sym co_aEv) } in + let { + @ co_aE3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aE3 = TYPE trans co_aEu (sym co_aEy) } in + let { + @ co_aE1::GHC.HetMet.GArrow.GArrowTensor g_aFo + ~ + GHC.HetMet.GArrow.GArrowTensor g_aFo + co_aE1 = TYPE trans co_aEx (sym co_aEF) } in + let { + @ co_aDD::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aDD = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in + let { + @ co_aDC::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aDC = + TYPE trans + (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEj) + (sym co_aEh) } in + let { + @ co_aDA::GHC.HetMet.Private.PGArrow g_aFo () y_aFp + ~ + GHC.HetMet.Private.PGArrow + g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp + co_aDA = + TYPE trans + co_aDD + (GHC.HetMet.Private.PGArrow + g_aFo + (trans (sym co_aDC) (GHC.HetMet.GArrow.GArrowUnit g_aFo)) + y_aFp) } in + let { + @ co_aDv::GHC.HetMet.Private.PGArrow + g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp + ~ + GHC.HetMet.Private.PGArrow g_aFo () y_aFp + co_aDv = TYPE sym co_aDA } in + let { + @ co_aDr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ () + co_aDr = TYPE trans co_aDC (sym co_aEg) } in + let { + $dGArrowSTKC_aDm :: GHC.HetMet.GArrow.GArrowSTKC g_aFo + [LclId] + $dGArrowSTKC_aDm = $dGArrowSTKC_aFq } in + letrec { + foo'_aDw + :: GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp + [LclId] + foo'_aDw = + GHC.Base.. + @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp) + @ (g_aFo () y_aFp) + @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp) + (GHC.HetMet.Private.unG @ g_aFo @ () @ y_aFp $dGArrowSTKC_aDm) + (GHC.Base.. + @ <[y_aFp]>@g_aFo + @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp) + @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp) + ((GHC.HetMet.CodeTypes.pga_flatten @ g_aFo @ GHC.Prim.Any @ y_aFp) + `cast` (<[y_aFp]>@g_aFo + -> GHC.HetMet.Private.PGArrow g_aFo co_aDr y_aFp + :: (<[y_aFp]>@g_aFo + -> GHC.HetMet.Private.PGArrow + g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp) + ~ + (<[y_aFp]>@g_aFo -> GHC.HetMet.Private.PGArrow g_aFo () y_aFp))) + (GHC.Base.. + @ <[y_aFp]>@g_aFo + @ <[y_aFp]>@g_aFo + @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp) + (Main.foo @ g_aFo @ y_aFp) + ((GHC.HetMet.CodeTypes.pga_unflatten + @ g_aFo @ GHC.Prim.Any @ y_aFp) + `cast` (co_aDv -> <[y_aFp]>@g_aFo + :: (GHC.HetMet.Private.PGArrow + g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp + -> <[y_aFp]>@g_aFo) + ~ + (GHC.HetMet.Private.PGArrow g_aFo () y_aFp + -> <[y_aFp]>@g_aFo))))); } in + foo'_aDw + +Main.main :: GHC.Types.IO () +[LclIdX] +Main.main = + let { + @ co_aLu::GHC.Types.Int ~ GHC.Types.Int + co_aLu = TYPE GHC.Types.Int } in + let { + @ co_aLt::GHC.Types.Int ~ GHC.Types.Int + co_aLt = TYPE GHC.Types.Int } in + letrec { + main_aHj :: GHC.Types.IO () + [LclId] + main_aHj = + GArrowTikZ.tikz + @ () + @ GHC.Types.Int + (Main.foo' + @ GArrowTikZ.GArrowTikZ + @ GHC.Types.Int + $dGArrowSTKC_aHd + @ co_aHe + (GHC.HetMet.Private.PGArrowD + @ GArrowTikZ.GArrowTikZ + @ () + @ GHC.Types.Int + (\ ($dGArrowSTKC_aHg + :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ) -> + let { + @ co_aHD::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + co_aHD = + TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in + let { + @ co_aHG::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ () + co_aHG = + TYPE trans (sym co_aHD) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in + let { + @ co_aHB::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + co_aHB = + TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in + let { + @ co_aHH::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + (,) + co_aHH = + TYPE trans + (sym co_aHB) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in + let { + @ co_aHx::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + co_aHx = + TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in + let { + @ co_aLd::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ () + co_aLd = + TYPE trans (sym co_aHx) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in + let { + @ co_aHv::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + co_aHv = + TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in + let { + @ co_aLe::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + (,) + co_aLe = + TYPE trans + (sym co_aHv) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in + let { + @ co_aHr::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ + co_aHr = + TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in + let { + @ co_aLf::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ () + co_aLf = + TYPE trans (sym co_aHr) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in + let { + @ co_aHp::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + co_aHp = + TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in + let { + @ co_aLg::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ + ~ + (,) + co_aLg = + TYPE trans + (sym co_aHp) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in + let { + $dGArrowSwap_aHn + :: GHC.HetMet.GArrow.GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrowSwap_aHn = + GHC.HetMet.GArrow.$p3GArrowSTKC + @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in + let { + $dGArrow_aHE + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrow_aHE = + GHC.HetMet.GArrow.$p1GArrowSwap + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrowSwap_aHn } in + let { + $dCategory_aHF :: Control.Category.Category GArrowTikZ.GArrowTikZ + [LclId] + $dCategory_aHF = + GHC.HetMet.GArrow.$p1GArrow + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrow_aHE } in + let { + $dGArrow_aLj + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrow_aLj = + $dGArrow_aHE + `cast` (GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + co_aHH + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in + let { + $dGArrow_aLk + :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrow_aLk = + $dGArrow_aLj + `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) co_aHG + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in + let { + $dGArrowSwap_aLh + :: GHC.HetMet.GArrow.GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + [LclId] + $dGArrowSwap_aLh = + $dGArrowSwap_aHn + `cast` (GHC.HetMet.GArrow.T:GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + co_aHG + :: GHC.HetMet.GArrow.T:GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + ()) } in + let { + $dGArrowSwap_aLi + :: GHC.HetMet.GArrow.GArrowSwap GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrowSwap_aLi = + $dGArrowSwap_aLh + `cast` (GHC.HetMet.GArrow.T:GArrowSwap + GArrowTikZ.GArrowTikZ co_aHH () + :: GHC.HetMet.GArrow.T:GArrowSwap + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + ~ + GHC.HetMet.GArrow.T:GArrowSwap GArrowTikZ.GArrowTikZ (,) ()) } in + let { + $dGArrowCopy_aHm + :: GHC.HetMet.GArrow.GArrowCopy + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrowCopy_aHm = + GHC.HetMet.GArrow.$p2GArrowSTKC + @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in + let { + $dGArrow_aHy + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrow_aHy = + GHC.HetMet.GArrow.$p1GArrowCopy + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrowCopy_aHm } in + let { + $dCategory_aHz :: Control.Category.Category GArrowTikZ.GArrowTikZ + [LclId] + $dCategory_aHz = + GHC.HetMet.GArrow.$p1GArrow + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrow_aHy } in + let { + $dGArrow_aLn + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + [LclId] + $dGArrow_aLn = + $dGArrow_aHy + `cast` (GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + co_aLd + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + ()) } in + let { + $dGArrow_aLo + :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrow_aLo = + $dGArrow_aLn + `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLe () + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + ~ + GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in + let { + $dGArrowCopy_aLl + :: GHC.HetMet.GArrow.GArrowCopy + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrowCopy_aLl = + $dGArrowCopy_aHm + `cast` (GHC.HetMet.GArrow.T:GArrowCopy + GArrowTikZ.GArrowTikZ + co_aLe + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + :: GHC.HetMet.GArrow.T:GArrowCopy + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrowCopy + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in + let { + $dGArrowCopy_aLm + :: GHC.HetMet.GArrow.GArrowCopy GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrowCopy_aLm = + $dGArrowCopy_aLl + `cast` (GHC.HetMet.GArrow.T:GArrowCopy + GArrowTikZ.GArrowTikZ (,) co_aLd + :: GHC.HetMet.GArrow.T:GArrowCopy + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrowCopy GArrowTikZ.GArrowTikZ (,) ()) } in + let { + $dGArrowDrop_aHl + :: GHC.HetMet.GArrow.GArrowDrop + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrowDrop_aHl = + GHC.HetMet.GArrow.$p1GArrowSTKC + @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in + let { + $dGArrow_aHs + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrow_aHs = + GHC.HetMet.GArrow.$p1GArrowDrop + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrowDrop_aHl } in + let { + $dCategory_aHt :: Control.Category.Category GArrowTikZ.GArrowTikZ + [LclId] + $dCategory_aHt = + GHC.HetMet.GArrow.$p1GArrow + @ GArrowTikZ.GArrowTikZ + @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + $dGArrow_aHs } in + let { + $dGArrow_aLr + :: GHC.HetMet.GArrow.GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + [LclId] + $dGArrow_aLr = + $dGArrow_aHs + `cast` (GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + co_aLf + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + ()) } in + let { + $dGArrow_aLs + :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrow_aLs = + $dGArrow_aLr + `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLg () + :: GHC.HetMet.GArrow.T:GArrow + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + () + ~ + GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in + let { + $dGArrowDrop_aLp + :: GHC.HetMet.GArrow.GArrowDrop + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + [LclId] + $dGArrowDrop_aLp = + $dGArrowDrop_aHl + `cast` (GHC.HetMet.GArrow.T:GArrowDrop + GArrowTikZ.GArrowTikZ + co_aLg + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + :: GHC.HetMet.GArrow.T:GArrowDrop + GArrowTikZ.GArrowTikZ + (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrowDrop + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in + let { + $dGArrowDrop_aLq + :: GHC.HetMet.GArrow.GArrowDrop GArrowTikZ.GArrowTikZ (,) () + [LclId] + $dGArrowDrop_aLq = + $dGArrowDrop_aLp + `cast` (GHC.HetMet.GArrow.T:GArrowDrop + GArrowTikZ.GArrowTikZ (,) co_aLf + :: GHC.HetMet.GArrow.T:GArrowDrop + GArrowTikZ.GArrowTikZ + (,) + (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ) + ~ + GHC.HetMet.GArrow.T:GArrowDrop GArrowTikZ.GArrowTikZ (,) ()) } in + let { + @ co_aHh::GHC.Types.Int ~ GHC.Types.Int + co_aHh = TYPE sym co_aLt } in + (GArrowTikZ.$WTikZ_const (GHC.Types.I# 12)) + `cast` (GArrowTikZ.GArrowTikZ () co_aHh + :: GArrowTikZ.GArrowTikZ () GHC.Types.Int + ~ + GArrowTikZ.GArrowTikZ () GHC.Types.Int)))); } in + main_aHj + +:Main.main :: GHC.Types.IO () +[LclIdX] +:Main.main = GHC.TopHandler.runMainIO @ () Main.main +end Rec } + + + + +==================== Desugar ==================== +Main.foo + :: forall (tv_~N6 :: * -> * -> *) tv_~N7. + GHC.HetMet.Private.PGArrow + tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7 + -> GHC.HetMet.Private.PGArrow + tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7 +[LclId] +Main.foo = + \ (@ tv_~N6::* -> * -> *) + (@ tv_~N7) + (ev_~N8 + :: GHC.HetMet.Private.PGArrow + tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7) -> + let { + ev_~N9 + :: GHC.HetMet.Private.PGArrow + tv_~N6 + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + [LclId] + ev_~N9 = + GHC.HetMet.Private.pga_id + @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in + let { + ev_~Na + :: GHC.HetMet.Private.PGArrow + tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7 + [LclId] + ev_~Na = + let { + ev_~Nh + :: GHC.HetMet.Private.PGArrow + tv_~N6 + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + [LclId] + ev_~Nh = + GHC.HetMet.Private.pga_id + @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in + let { + ev_~Ni + :: GHC.HetMet.Private.PGArrow + tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7 + [LclId] + ev_~Ni = ev_~N8 } in + let { + ev_~Nj + :: GHC.HetMet.Private.PGArrow + tv_~N6 + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + [LclId] + ev_~Nj = + GHC.HetMet.Private.pga_drop + @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in + GHC.HetMet.Private.pga_comp + @ tv_~N6 + @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + @ tv_~N7 + ev_~Nj + ev_~Ni } in + GHC.HetMet.Private.pga_comp + @ tv_~N6 + @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) + @ tv_~N7 + ev_~N9 + ev_~Na + +Main.maincoercionKind + base:GHC.HetMet.GArrow.GArrowUnit{tc 02y} + main:GArrowTikZ.GArrowTikZ{tc roV} + ~ + ghc-prim:GHC.Unit.(){(w) tc 40} +ghc-stage2: coreTypeToWeakType + hit a bare EqPred diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 7e68ba0..0775229 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -53,8 +53,10 @@ sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT e coreVarToWeakVar :: Var.Var -> WeakVar coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) -coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") - (Prelude.error "FIXME") (Prelude.error "FIXME")) +coreVarToWeakVar v | Var.isCoVar v + = WCoerVar (WeakCoerVar v + (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v))))) + (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v)))))) coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" @@ -87,8 +89,9 @@ sanitizeForLatex (c:x) = c:(sanitizeForLatex x) kindToCoreKind :: Kind -> TypeRep.Kind kindToCoreKind KindStar = TypeRep.liftedTypeKind kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) -kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that" - +kindToCoreKind k = Prelude.error ((Prelude.++) + "kindToCoreKind does not know how to handle kind " + (kindToString k)) coreKindToKind :: TypeRep.Kind -> Kind coreKindToKind k = case Coercion.splitKindFunTy_maybe k of diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index cae7174..3cd8ff6 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -161,7 +161,7 @@ Section core2proof. Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar := weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k. Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar := - weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2. + weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2. Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar := weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t. @@ -280,6 +280,9 @@ Section core2proof. (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) (hetmet_PGArrowTyCon : TyFun) + (hetmet_PGArrow_unit_TyCon : TyFun) + (hetmet_PGArrow_tensor_TyCon : TyFun) + (hetmet_PGArrow_exponent_TyCon : TyFun) (hetmet_pga_id : CoreVar) (hetmet_pga_comp : CoreVar) (hetmet_pga_first : CoreVar) @@ -299,9 +302,11 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) . - Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil. - Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ := - TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b. + + Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ := + @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil). + Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ := + TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b. Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ := TApp (TApp (TApp (@TyFunApp TV hetmet_PGArrowTyCon @@ -370,22 +375,22 @@ Section core2proof. |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))). Defined. - Definition gat {Γ}(x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ x. + Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x. Instance my_ga : garrow ga_unit ga_prod (@ga_type) := - { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat a) - ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat a) - ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat a) - ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a) - ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a) - ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c) - ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c) - ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b) - ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat a) - ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat a) - ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x)) - ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x)) - ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c)) + { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a) + ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a) + ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a) + ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a) + ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a) + ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c) + ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c) + ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b) + ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a) + ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a) + ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x)) + ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c)) (* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*) (* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*) (* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*) @@ -464,6 +469,9 @@ Section core2proof. (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) (hetmet_PGArrowTyCon : TyFun) + (hetmet_PGArrow_unit_TyCon : TyFun) + (hetmet_PGArrow_tensor_TyCon : TyFun) + (hetmet_PGArrow_exponent_TyCon : TyFun) (hetmet_pga_id : CoreVar) (hetmet_pga_comp : CoreVar) (hetmet_pga_first : CoreVar) @@ -489,6 +497,9 @@ Section core2proof. hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon + hetmet_PGArrow_unit_TyCon + hetmet_PGArrow_tensor_TyCon +(* hetmet_PGArrow_exponent_TyCon*) hetmet_pga_id hetmet_pga_comp hetmet_pga_first diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index ac2da8c..78223cf 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -69,9 +69,11 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := coreTypeToWeakType' t2 >>= fun t2' => OK (WAppTy (WAppTy WFunTyCon t1') t2') | ForAllTy cv t => match coreVarToWeakVar cv with - | WExprVar _ => Error "encountered expression variable in a type" + | WExprVar _ => Error "encountered expression variable in a type abstraction" | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t') - | WCoerVar _ => Error "encountered coercion variable in a type" + | WCoerVar (weakCoerVar v t1' t2') => + coreTypeToWeakType' t >>= fun t3' => + OK (WCoFunTy t1' t2' t3') end | PredTy (ClassP cl lct) => ((fix rec tl := match tl with | nil => OK nil @@ -82,7 +84,8 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | PredTy (EqPred _ _) => Error "hit a bare EqPred" end. -Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)). +Definition coreTypeToWeakType t := + addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)). (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) := diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 677287a..4babf36 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -36,7 +36,8 @@ Extract Inductive PredType => Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". -Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". +Variable coreCoercionKind : Kind -> CoreType*CoreType. + Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)". Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)". Variable setVarType : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType => "Var.setVarType". diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index b46f4d2..a23acfd 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -97,15 +97,15 @@ Section HaskFlattener. Context (hetmet_flatten : WeakExprVar). Context (hetmet_unflatten : WeakExprVar). Context (hetmet_id : WeakExprVar). - Context {unitTy : forall TV, RawHaskType TV ★ }. - Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. + Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }. + Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. - Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := - fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr). + Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (mapOptionTree (fun x => x TV ite) tr). Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := - fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite). + fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite). Class garrow := { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ] @@ -148,7 +148,7 @@ Section HaskFlattener. | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2) (garrowfy_raw_codetypes t) | TArrow => TArrow - | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e) + | TCode v e => gaTy TV v (unitTy TV v) (garrowfy_raw_codetypes e) | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt) end with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk := diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index f5a3f1a..8ceb0b7 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -72,7 +72,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := | WENote n e => CoreENote n (weakExprToCoreExpr e ) | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e ) | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e ) - | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr e ) + | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e ) | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co) | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp ((CoreEType (TyVarTy ec)):: diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 0055a17..d77d074 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,6 +19,7 @@ Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreVars. +Require Import HaskCoreTypes. Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). @@ -416,7 +417,7 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex Defined. Definition coVarKind (wcv:WeakCoerVar) : Kind := - match wcv with weakCoerVar _ κ _ _ => κ end. + match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end. Coercion coVarKind : WeakCoerVar >-> Kind. Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ). @@ -631,7 +632,7 @@ Definition weakExprToStrongExpr : forall | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te) end - | WECoLam cv e => let (_,_,t1,t2) := cv in + | WECoLam cv e => let (_,t1,t2) := cv in weakTypeOfWeakExpr e >>= fun te => weakTypeToTypeOfKind φ te ★ >>= fun te' => weakTypeToTypeOfKind φ t1 cv >>= fun t1' => diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 9b34188..9ec126e 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -47,7 +47,7 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar. Defined. (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) -Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar. +Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar. Inductive WeakCoercion : Type := | WCoVar : WeakCoerVar -> WeakCoercion (* g *) @@ -66,7 +66,7 @@ Inductive WeakCoercion : Type := Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType := match wc with -| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2) +| WCoVar (weakCoerVar _ t1 t2) => (WFunTyCon,WFunTyCon) (* FIXME!!! *) | WCoType t => (WFunTyCon,WFunTyCon) (* FIXME!!! *) | WCoApp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *) | WCoAppT c t => (WFunTyCon,WFunTyCon) (* FIXME!!! *) diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 8cb9da6..896aff4 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -32,9 +32,9 @@ Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind := Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := match wv with - | WExprVar (weakExprVar v _ ) => v - | WTypeVar (weakTypeVar v _ ) => v - | WCoerVar (weakCoerVar v _ _ _) => v + | WExprVar (weakExprVar v _ ) => v + | WTypeVar (weakTypeVar v _ ) => v + | WCoerVar (weakCoerVar v _ _) => v end. Coercion weakVarToCoreVar : WeakVar >-> CoreVar.