{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XMultiParamTypeClasses -XTypeOperators #-}
module CircuitExample
where
-import GHC.HetMet.CodeTypes hiding ((-))
import GHC.HetMet.GArrow
+import GHC.HetMet.GuestLanguage hiding ((-))
import Control.Category
import Prelude hiding ( id, (.) )
-{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables #-}
+{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
module Demo (demo) where
+{-
+demo const mult =
+ <[ \y ->
+ ~~mult
+ (~~mult y y)
+ (~~mult y y)
+ ]>
+-}
+
+
+
+
+
-demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
{-
-demo const mult = <[ \y -> ~~(demo' 0) ]>
- where
- demo' 0 = const 4
- demo' n = const 4
+demo const mult =
+ <[ \y ->
+ ~~mult
+ (~~mult (~~mult y y) (~~mult y y))
+ (~~mult (~~mult y y) (~~mult y y))
+ ]>
-}
--- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
{-
demo const mult =
+ <[ \y -> ~~(foo 4) ]>
+ where
+ foo 0 = const (12::Int)
+ foo n = <[ let bar = ~~(foo (n-1))
+ in ~~mult bar bar
+ ]>
+
+-}
+
+
+
+{-
+demo const mult =
+ <[ \y -> ~~(foo 3) ]>
+ where
+ foo 0 = const (12::Int)
+ foo n = <[ let recurs = ~~(foo (n-1))
+ in ~~mult recurs recurs
+ ]>
+
+-}
+
+
+
+
+
+demo const mult =
+ <[ \y ->
+ let foo = ~~mult (~~mult foo (~~mult y foo)) y
+ in foo ]>
+
+
+
+
+
+
+
+
+
+
+
+
+{-
+demo const mult =
+ <[ \y -> ~~(foo 2 <[y]>) ]>
+ where
+ foo 0 y = const (12::Int)
+ foo n y = <[ let recurs = ~~(foo (n-1) y)
+ in ~~mult recurs recurs
+ ]>
+-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+-- demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
+-- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
+-- golden
+{-
+demo const mult =
+ <[ \y ->
+ let twelve = ~~mult twelve y
+ in twelve ]>
+-}
+
+{-
+demo const mult =
<[ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) ]>
-}
in let four = ~~(const (4::Int))
in ~~mult four twelve ]>
-}
-{-
-demo const mult =
- <[ let twelve = ~~(const (12::Int))
- in let twelvea = twelve
- four = ~~(const (4::Int))
- twelveb = twelve
- in ~~mult (~~mult twelvea four) (~~mult twelveb twelveb) ]>
--}
{-
demo const mult = demo' 3
demo' 0 = const 12
demo' 1 = const 12
demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) ]>
--}
\ No newline at end of file
+-}
+
+-- BUG
+--demo const mult = <[ \y -> ~~(demo' 0) ]>
+-- where
+-- demo' 0 = const 4
+-- demo' n = const 4
{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XFlexibleContexts #-}
module DotProduct
where
-import GHC.HetMet.CodeTypes hiding ((-))
+import GHC.HetMet.GuestLanguage hiding ((-))
import Prelude hiding ( id, (.) )
--------------------------------------------------------------------------------
-- laws, but no guarantees about which optimizations actually happen.
--
optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
-optimize = repeat (gasl2gas . optimizel . gas2gasl)
+optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
{-
optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
-- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
--
beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
-beautify = optimize . (repeat beautify')
+beautify = repeat beautify'
where
beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
- beautify' (GAS_comp (GAS_comp f g) h) = GAS_comp f $ GAS_comp g h
- beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = GAS_comp f $ GAS_comp g $ GAS_comp h k
+ beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
+ beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
(GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
(GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
(f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
+ beautify' (GAS_comp f GAS_id) = f
+ beautify' (GAS_comp GAS_id f) = f
beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
(GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
(GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
+ GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
+ GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
data GArrowSkeletonX m :: * -> * -> *
where
gasy2gas (GASY_X gx) = gasx2gas gx
gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
+gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
+gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
gasx2gas (GASX_const k) = GAS_const k
optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
optimizel (GASL_id ) = GASL_id
optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
-optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = optimizel $ gaslcat x gl
-optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
-optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
+optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
+optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
+optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
--optimize' (GAS_loopl GAS_id ) = GAS_id
-}
optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
-optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
-optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
+
+optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
+optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
+
optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
-optpair _ _ = Nothing
-
-pushpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
-pushpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ pushpair gy1 gy2
-pushpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ pushpair gy1 gy2
-pushpair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
-pushpair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
-pushpair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
-pushpair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
-pushpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
-pushpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
-pushpair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
-pushpair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
-pushpair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
-pushpair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
-pushpair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
-pushpair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
-pushpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
-pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
-pushpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
-pushpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
-pushpair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
-pushpair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
-pushpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
-pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
-pushpair _ _ = Nothing
+optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
+optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
+optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
+optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
+optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
+optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
+optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
+optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
+optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
+optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
+optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
+optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
+optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
+optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
+
+-- swap with an {un}cancel{l,r} before/after it
+optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
+optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
+optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
+optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
+
+{-
+optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
+ Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
+optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
+ Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
+optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
+ Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
+optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
+ Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
+-}
+optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
+optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
+
+optpair a@(GASY_X GASX_uncancell) (GASY_first b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b
+optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b
+
+optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
+ = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
+optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
+ = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
+
+optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
+optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
+optpair _ _ = Nothing
+
+swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
+
+swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
+swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
+
+swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
+swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
+swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
+swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
+swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
+swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
+swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
+swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
+swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
+swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
+swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
+swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
+swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
+swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
+
+swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
+swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
+swappair _ _ = Nothing
-- pushright can only return True for central morphisms
pushright :: GArrowSkeletonY m x y -> Bool
pushright (GASY_first gy) = pushright gy
pushright (GASY_second gy) = pushright gy
+pushright (GASY_atomicl _) = False
+pushright (GASY_atomicr _) = False
pushright (GASY_X GASX_uncancell) = True
pushright (GASY_X GASX_uncancelr) = True
pushright (GASY_X _ ) = False
+-- says if we should push it into a loopl/r
+pushin :: GArrowSkeletonY m x y -> Bool
+pushin gy = pushright gy || pushin' gy
+ where
+ pushin' :: GArrowSkeletonY m a b -> Bool
+ pushin' (GASY_first gy) = pushin' gy
+ pushin' (GASY_second gy) = pushin' gy
+ pushin' (GASY_atomicl _) = False
+ pushin' (GASY_atomicr _) = False
+
+ -- not sure if these are a good idea
+ pushin' (GASY_X GASX_copy) = True
+ pushin' (GASY_X GASX_swap) = True
+
+ pushin' (GASY_X _ ) = False
+
optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
optimizey (GASY_X gx) = GASY_X $ optimizex gx
optimizey (GASY_first gy) = GASY_first (optimizey gy)
optimizey (GASY_second gy) = GASY_second (optimizey gy)
+optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
+optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
optimizex (GASX_const k) = GASX_const k
optimizex (GASX_swap) = GASX_swap
optimizex (GASX_merge) = GASX_merge
optimizex (GASX_misc m) = GASX_misc m
+optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
+optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
+
+pushleft :: GArrowSkeletonY m x y -> Bool
+pushleft (GASY_first gy) = pushleft gy
+pushleft (GASY_second gy) = pushleft gy
+pushleft (GASY_atomicl _) = False
+pushleft (GASY_atomicr _) = False
+pushleft (GASY_X GASX_cancell) = True
+pushleft (GASY_X GASX_cancelr) = True
+pushleft (GASY_X _ ) = False
-- | A Diagram is the visual representation of a GArrowSkeleton
data Diagram
= DiagramComp Diagram Diagram
- | DiagramBox TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
+ | DiagramBox Float TrackIdentifier Tracks BoxRenderer Tracks TrackIdentifier
| DiagramBypassTop Tracks Diagram
| DiagramBypassBot Diagram Tracks
| DiagramLoopTop Tracks Diagram
-- | get the output tracks of a diagram
getOut :: Diagram -> Tracks
getOut (DiagramComp f g) = getOut g
-getOut (DiagramBox ptop pin q pout pbot) = pout
+getOut (DiagramBox wid ptop pin q pout pbot) = pout
getOut (DiagramBypassTop p f) = TT p (getOut f)
getOut (DiagramBypassBot f p) = TT (getOut f) p
getOut (DiagramLoopTop t d) = case getOut d of { TT z y -> y ; _ -> error "DiagramLoopTop: mismatch" }
-- | get the input tracks of a diagram
getIn :: Diagram -> Tracks
getIn (DiagramComp f g) = getIn f
-getIn (DiagramBox ptop pin q pout pbot) = pin
+getIn (DiagramBox wid ptop pin q pout pbot) = pin
getIn (DiagramBypassTop p f) = TT p (getIn f)
getIn (DiagramBypassBot f p) = TT (getIn f) p
getIn (DiagramLoopTop t d) = case getIn d of { TT z x -> x ; _ -> error "DiagramLoopTop: mismatch" }
Float -> -- x2
Float -> -- y2
String -- TikZ code
-
-
+noRender :: BoxRenderer
+noRender _ _ _ _ _ = ""
; return $ DiagramBypassBot f' x }
mkdiag' (GAS_second f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
; return $ DiagramBypassTop x f' }
- mkdiag' (GAS_id ) = do { (top, x ,bot) <- alloc inp ; simpleDiag "id" top x x bot [(x,x)] }
+ mkdiag' (GAS_id ) = do { (top, x ,bot) <- alloc inp ; simpleDiag' "id" top x x bot [(x,x)] "gray!50" }
mkdiag' GAS_cancell = do { (top,(TT x y),bot) <- alloc inp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancell" ++
drawWires tp x1 y x2 y "black" ++
drawLine x1 (tp!lowermost x) ((x1+x2)/2) (tp!uppermost y) "gray!50" "dashed"
- ; return $ DiagramBox top (TT x y) r y bot }
+ ; return $ DiagramBox 2 top (TT x y) r y bot }
mkdiag' GAS_cancelr = do { (top,(TT x y),bot) <- alloc inp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancelr" ++
drawWires tp x1 x x2 x "black" ++
drawLine x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "gray!50" "dashed"
- ; return $ DiagramBox top (TT x y) r x bot }
+ ; return $ DiagramBox 2 top (TT x y) r x bot }
mkdiag' GAS_uncancell = do { (top,(TT x y),bot) <- alloc outp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancell" ++
drawWires tp x1 y x2 y "black" ++
drawLine ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "gray!50" "dashed"
- ; return $ DiagramBox top y r (TT x y) bot }
+ ; return $ DiagramBox 2 top y r (TT x y) bot }
mkdiag' GAS_uncancelr = do { (top,(TT x y),bot) <- alloc outp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancelr" ++
drawWires tp x1 x x2 x "black" ++
drawLine ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "dashed"
- ; return $ DiagramBox top x r (TT x y) bot }
+ ; return $ DiagramBox 2 top x r (TT x y) bot }
mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp ; simpleDiag "drop" top x x bot [] }
mkdiag' (GAS_const i) = do { (top, x ,bot) <- alloc inp
; (_, y ,_) <- alloc outp
drawWires tp x1 x ((x1+x2)/2) x "black" ++
drawWires tp ((x1+x2)/2) x x2 y "black" ++
drawWires tp ((x1+x2)/2) x x2 z "black"
- ; return $ DiagramBox top x r (TT y z) bot
+ ; return $ DiagramBox 2 top x r (TT y z) bot
}
mkdiag' GAS_merge = do { (top,(TT x y),bot) <- alloc inp
; simpleDiag "times" top (TT x y) x bot [] }
drawWires tp x1 x x2 x "black" ++
drawWires tp x1 y x2 y "black" ++
drawWires tp x1 z x2 z "black"
- ; return $ DiagramBox top (TT (TT x y) z) r (TT x (TT y z)) bot
+ ; let pin = (TT (TT x y) z)
+ ; let pout = (TT x (TT y z))
+ ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
}
mkdiag' GAS_unassoc =
do { (top,(TT x (TT y z)),bot) <- alloc inp
drawWires tp x1 x x2 x "black" ++
drawWires tp x1 y x2 y "black" ++
drawWires tp x1 z x2 z "black"
- ; return $ DiagramBox top (TT x (TT y z)) r (TT (TT x y) z) bot
+ ; let pin = (TT x (TT y z))
+ ; let pout = (TT (TT x y) z)
+ ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
}
mkdiag' (GAS_loopl f) = do { f' <- mkdiag' f
; l <- allocLoop (case (getIn f') of (TT z _) -> z ; _ -> error "GAS_loopl: mismatch")
; constrain ptop LT (uppermost pout) (-1)
; constrain pbot GT (lowermost pout) 1
; constrain ptop LT pbot (-1)
- ; return $ DiagramBox ptop pin r pout pbot
+ ; return $ DiagramBox 2 ptop pin r pout pbot
}
simpleDiag text ptop pin pout pbot conn = simpleDiag' text ptop pin pout pbot conn "black"
simpleDiag' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot
-- ++ wires (x-1) p1 x "green"
-- ++ wires (x+w) p2 (x+w+1) "red"
+--draw_assoc = False
+--draw_first_second = False
+draw_assoc = True
+draw_first_second = True
+
-- constrain that Ports is at least Int units above the topmost portion of Diagram
constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM ()
constrainTop v i (DiagramComp d1 d2) = do { constrainTop v i d1 ; constrainTop v i d2 ; return () }
constrainTop v i (DiagramBypassTop p d) = constrain v LT (uppermost p) (-1 * i)
constrainTop v i (DiagramBypassBot d p) = constrainTop v (i+1) d
-constrainTop v i (DiagramBox ptop pin r pout pbot) = constrain v LT ptop (-1 * i)
+constrainTop v i (DiagramBox wid ptop pin r pout pbot) = constrain v LT ptop (-1 * i)
constrainTop v i (DiagramLoopTop p d) = constrain v LT (uppermost p) (-1 * i)
constrainTop v i (DiagramLoopBot d p) = constrainTop v (i+1) d
constrainBot (DiagramComp d1 d2) i v = do { constrainBot d1 i v ; constrainBot d2 i v ; return () }
constrainBot (DiagramBypassTop p d) i v = constrainBot d (i+1) v
constrainBot (DiagramBypassBot d p) i v = constrain v GT (lowermost p) 2
-constrainBot (DiagramBox ptop pin r pout pbot) i v = constrain v GT pbot i
+constrainBot (DiagramBox wid ptop pin r pout pbot) i v = constrain v GT pbot i
constrainBot (DiagramLoopTop p d) i v = constrainBot d (i+1) v
constrainBot (DiagramLoopBot d p) i v = constrain v GT (lowermost p) 2
-- | The width of a box is easy to calculate
width :: TrackPositions -> Diagram -> Float
width m (DiagramComp d1 d2) = (width m d1) + 1 + (width m d2)
-width m (DiagramBox ptop pin x pout pbot) = 2
-width m (DiagramBypassTop p d) = (width m d) + 2
-width m (DiagramBypassBot d p) = (width m d) + 2
+width m (DiagramBox wid ptop pin x pout pbot) = wid
+width m (DiagramBypassTop p d) = (width m d) + (if draw_first_second then 2 else 0)
+width m (DiagramBypassBot d p) = (width m d) + (if draw_first_second then 2 else 0)
width m (DiagramLoopTop p d) = (width m d) + 2 + 2 * (loopgap + (m ! lowermost p) - (m ! uppermost p))
width m (DiagramLoopBot d p) = (width m d) + 2 + 2 * (loopgap + (m ! lowermost p) - (m ! uppermost p))
++ wires' (x+width m d1) (getOut d1) (x+width m d1+0.5) "black" "->"
++ wires' (x+width m d1+0.5) (getOut d1) (x+width m d1+1) "black" "-"
++ tikZ' d2 (x + width m d1 + 1)
- tikZ' d'@(DiagramBypassTop p d) x = let top = getTop d' in
+ tikZ' d'@(DiagramBypassTop p d) x = if not draw_first_second
+ then drawWires m x p (x+width m d) p "black" ++ tikZ' d x
+ else
+ let top = getTop d' in
let bot = getBot d' in
drawBox x top (x+width m d') bot "gray!50" "second"
++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
++ drawWires m (x+1+width m d) (getOut d) (x+1+width m d+1) (getOut d) "black"
++ drawWires m x p (x+1+width m d+1) p "black"
- tikZ' d'@(DiagramBypassBot d p) x = let top = getTop d' in
+ tikZ' d'@(DiagramBypassBot d p) x = if not draw_first_second
+ then drawWires m x p (x+width m d) p "black" ++ tikZ' d x
+ else
+ let top = getTop d' in
let bot = getBot d' in
drawBox x top (x+width m d') bot "gray!50" "first"
++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ let rest = case getOut d of TT _ z -> z ; _ -> error "DiagramLoopTop: mismatch"
in drawWires m (x+1+gap+width m d) rest (x+width m d') rest "black"
tikZ' d'@(DiagramLoopBot d p) x_ = error "not implemented"
- tikZ' d@(DiagramBox ptop pin r pout pbot) x = r m x (m ! ptop) (x + width m d) (m ! pbot)
+ tikZ' d@(DiagramBox wid ptop pin r pout pbot) x = r m x (m ! ptop) (x + width m d) (m ! pbot)
wires x1 t x2 c = wires' x1 t x2 c "-"
getTop :: Diagram -> Float
getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
- getTop (DiagramBox ptop _ _ _ _) = m ! ptop
+ getTop (DiagramBox wid ptop _ _ _ _) = m ! ptop
getTop (DiagramBypassTop p d) = (m ! uppermost p) - 1
getTop (DiagramBypassBot d p) = getTop d - 1
getTop (DiagramLoopTop p d) = (m ! uppermost p) - 1
getBot :: Diagram -> Float
getBot (DiagramComp d1 d2) = max (getBot d1) (getBot d2)
- getBot (DiagramBox _ _ _ _ pbot) = m ! pbot
+ getBot (DiagramBox wid _ _ _ _ pbot) = m ! pbot
getBot (DiagramBypassTop p d) = getBot d + 1
getBot (DiagramBypassBot d p) = (m ! lowermost p) + 1
getBot (DiagramLoopTop p d) = getBot d + 1
where
import Data.Bits
import Data.Bool (not)
-import GHC.HetMet.CodeTypes hiding ((-))
import GHC.HetMet.GArrow
+import GHC.HetMet.GuestLanguage hiding ( (-) )
import Control.Category
import Control.Arrow
import Prelude hiding ( id, (.) )
apply curry.
Defined.
+ Definition fToC1' {Γ}{Δ}{a}{s}{lev} :
+ ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
+ ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
+ intro pf.
+ eapply nd_comp.
+ apply pf.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
+ apply curry.
+ Defined.
+
Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
apply curry.
Defined.
+ Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ :
+ ND Rule [] [ Γ > Δ > [] |- [(a1 ---> a2) ---> a3 ]@l ] ->
+ ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ]
+ [Γ > Δ > Σ |- [a3]@l ].
+ intro pf.
+ eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ].
+ set (fToC1 pf) as pf'.
+ apply boost.
+ apply pf'.
+ Defined.
+
Section coqPassCoreToCore.
Context
(do_flatten : bool)
(hetmet_pga_curryr : CoreVar)
(hetmet_pga_loopl : CoreVar)
(hetmet_pga_loopr : CoreVar)
+ (hetmet_pga_kappa : CoreVar)
.
; 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))*)
-(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
; ga_loopl := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
; ga_loopr := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+
+ ; ga_curry := fun Γ Δ ec l a => Prelude_error "ga_curry"
+
+ ; ga_apply := fun Γ Δ ec l a => Prelude_error "ga_apply"
; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
- ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
- ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
- ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
+(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
+ ; ga_kappa := fun Γ Δ ec l a b c Σ =>
+ fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
}.
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa =>
CoreMreturn
(coqPassCoreToCore'
hetmet_pga_swap
hetmet_pga_loopl
hetmet_pga_loopr
+ hetmet_pga_kappa
lbinds
(*
hetmet_pga_applyl
| (a::al) => f a /\ mapProp f al
end.
+
+(* delete the n^th element of a list *)
+Definition list_del : forall {T:Type} (l:list T) (n:nat)(pf:lt n (length l)), list T.
+ refine (fix list_del {T:Type} (l:list T) (n:nat) : lt n (length l) -> list T :=
+ match l as L return lt n (length L) -> list T with
+ | nil => _
+ | a::b => match n with
+ | O => fun _ => b
+ | S n' => fun pf => (fun list_del' => _) (list_del _ b n')
+ end
+ end).
+ intro pf.
+ simpl in pf.
+ assert False.
+ inversion pf.
+ inversion H.
+
+ simpl in *.
+ apply list_del'.
+ omega.
+ Defined.
+
+Definition list_get : forall {T:Type} (l:list T) (n:nat), lt n (length l) -> T.
+ refine (fix list_get {T:Type} (l:list T) (n:nat) : lt n (length l) -> T :=
+ match l as L return lt n (length L) -> T with
+ | nil => _
+ | a::b => match n with
+ | O => fun _ => a
+ | S n' => fun pf => (fun list_get' => _) (list_get _ b n')
+ end
+ end).
+ intro pf.
+ assert False.
+ inversion pf.
+ inversion H.
+
+ simpl in *.
+ apply list_get'.
+ omega.
+ Defined.
+
+Fixpoint list_ins (n:nat) {T:Type} (t:T) (l:list T) : list T :=
+ match n with
+ | O => t::l
+ | S n' => match l with
+ | nil => t::nil
+ | a::b => a::(list_ins n' t b)
+ end
+ end.
+
+Lemma list_ins_nil : forall T n x, @list_ins n T x nil = x::nil.
+ intros.
+ destruct n; auto.
+ Qed.
+
+Fixpoint list_take {T:Type}(l:list T)(n:nat) :=
+ match n with
+ | O => nil
+ | S n' => match l with
+ | nil => nil
+ | a::b => a::(list_take b n')
+ end
+ end.
+
+Fixpoint list_drop {T:Type}(l:list T)(n:nat) :=
+ match n with
+ | O => l
+ | S n' => match l with
+ | nil => nil
+ | a::b => list_drop b n'
+ end
+ end.
+
+Lemma list_ins_app T n κ : forall Γ, @list_ins n T κ Γ = app (list_take Γ n) (κ::(list_drop Γ n)).
+ induction n.
+ simpl.
+ intros.
+ destruct Γ; auto.
+ intro Γ.
+ destruct Γ.
+ reflexivity.
+ simpl.
+ rewrite <- IHn.
+ reflexivity.
+ Qed.
+
+Lemma list_take_drop T l : forall n, app (@list_take T l n) (list_drop l n) = l.
+ induction l; auto.
+ simpl.
+ destruct n; auto.
+ simpl.
+ destruct n.
+ reflexivity.
+ simpl.
+ rewrite IHl.
+ reflexivity.
+ Qed.
+
Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
induction l.
auto.
inversion v; subst; auto.
Defined.
+Lemma ilist_app {T}{F}{l1:list T}(v1:IList T F l1) : forall {l2:list T}(v2:IList T F l2), IList T F (app l1 l2).
+ induction l1; auto.
+ intros.
+ inversion v1.
+ subst.
+ simpl.
+ apply ICons.
+ apply X.
+ apply IHl1; auto.
+ Defined.
+
+Definition ilist_ins {T}{F}{l:list T} z (fz:F z) : forall n (il:IList T F l), IList T F (list_ins n z l).
+ induction l; simpl.
+ intros.
+ destruct n; simpl.
+ apply ICons; [ apply fz | apply INil ].
+ apply ICons; [ apply fz | apply INil ].
+ intros.
+ destruct n; simpl.
+ apply ICons; auto.
+ inversion il; subst.
+ apply ICons; auto.
+ Defined.
+
Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
match il with
| INil => nil
Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
Definition addErrorMessage s {T} (x:OrError T) :=
- x >>=[ s ] (fun y => OK y).
+ x >>=[ eol +++ eol +++ s ] (fun y => OK y).
Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
| Indexed_Error : forall error_message:string, Indexed f (Error error_message)
*)
Section HaskFlattener.
-
Ltac eqd_dec_refl' :=
match goal with
| [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
Axiom flatten_commutes_with_HaskTApp :
- forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
- flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
- HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
+ forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+ flatten_type (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) =
+ HaskTApp (weakF_ (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ).
- Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
- flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
+ Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t,
+ flatten_leveled_type (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
flatten_type (g v) = g v.
; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ]
; ga_apply : ∀ Γ Δ ec l a a' b c,
ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
- ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
- [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
- [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
+ ; ga_kappa : ∀ Γ Δ ec l a b c Σ, ND Rule
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec b c ]@l ]
+ [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,b) c ]@l ]
}.
Context `(gar:garrow).
apply precompose.
Defined.
+
+
+
(* useful for cutting down on the pretty-printed noise
Notation "` x" := (take_lev _ x) (at level 20).
clear y q.
set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
- destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
- destruct s.
+ destruct (decide_tree_empty q).
- simpl.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
- set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
- eapply nd_comp; [ idtac | apply RLet ].
- clear q''.
- eapply nd_comp; [ apply nd_rlecnac | idtac ].
- apply nd_prod.
- apply nd_rule.
- apply RArrange.
- eapply AComp; [ idtac | apply ACanR ].
- apply ALeft.
- apply (@arrangeCancelEmptyTree _ _ _ _ e).
-
- eapply nd_comp.
- eapply nd_rule.
- eapply (@RVar Γ Δ t nil).
- apply nd_rule.
+ destruct s.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
+ set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
+ eapply nd_comp; [ idtac | apply RLet ].
+ clear q''.
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_rule.
apply RArrange.
- eapply AComp.
- apply AuCanR.
+ eapply AComp; [ idtac | apply ACanR ].
apply ALeft.
- apply AWeak.
-(*
- eapply decide_tree_empty.
-
- simpl.
- set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
- destruct (decide_tree_empty escapified).
+ apply (@arrangeCancelEmptyTree _ _ _ _ e).
+
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply (@RVar Γ Δ t nil).
+ apply nd_rule.
+ apply RArrange.
+ eapply AComp.
+ apply AuCanR.
+ apply ALeft.
+ apply AWeak.
- induction succ.
- destruct a.
- unfold drop_lev.
- destruct l.
simpl.
- unfold mkDropFlags; simpl.
+ clear q.
+ unfold q'.
+ clear q'.
+ apply nd_rule.
+ apply RArrange.
+ induction succ.
+ destruct a.
+ destruct l as [t' l'].
+ simpl.
+ Transparent drop_lev.
+ simpl.
unfold take_lev.
unfold mkTakeFlags.
simpl.
- destruct (General.list_eq_dec h0 (ec :: nil)).
- simpl.
- rewrite e.
- apply nd_id.
- simpl.
- apply nd_rule.
- apply RArrange.
- apply ALeft.
- apply AWeak.
+ unfold drop_lev.
simpl.
- apply nd_rule.
- unfold take_lev.
- simpl.
- apply RArrange.
- apply ALeft.
- apply AWeak.
- apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
-*)
- Defined.
+ unfold mkDropFlags.
+ simpl.
+ unfold flatten_leveled_type.
+ destruct (General.list_eq_dec l' (ec :: nil)); simpl.
+ rewrite e.
+ unfold levels_to_tcode.
+ eapply AComp.
+ apply ACanL.
+ apply AuCanR.
+ eapply AComp.
+ apply ACanR.
+ eapply AComp.
+ apply AuCanL.
+ apply ARight.
+ apply AWeak.
+
+ simpl.
+ apply ARight.
+ apply AWeak.
+
+ drop_simplify.
+ simpl.
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ2)) as d2 in *.
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ1)) as d1 in *.
+ set (mapOptionTree flatten_leveled_type (dropT (mkFlags
+ (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ1))) as s1 in *.
+ set (mapOptionTree flatten_leveled_type (dropT (mkFlags
+ (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ2))) as s2 in *.
+ set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
+ (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
+ set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
+ (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
+
+ eapply AComp.
+ apply arrangeSwapMiddle.
+
+ eapply AComp.
+ eapply ALeft.
+ apply IHsucc2.
+
+ eapply AComp.
+ eapply ARight.
+ apply IHsucc1.
+
+ eapply AComp.
+ apply arrangeSwapMiddle.
+ apply ARight.
+ unfold take_lev.
+ unfold mkTakeFlags.
+
+ unfold s1'.
+ unfold s2'.
+ clear s1' s2'.
+ set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
+ (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
+ set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
+ (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
+
+ apply (Prelude_error "almost there!").
+ Defined.
Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
intros.
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
rewrite flatten_commutes_with_HaskTApp.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
simpl.
- set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
- set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
+ set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a.
+ set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
assert (a=q').
unfold a.
unfold q'.
reflexivity.
destruct case_RCase.
- simpl.
- apply (Prelude_error "Case not supported (BIG FIXME)").
+ destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
+ apply nd_rule.
+ rewrite <- mapOptionTree_compose.
+ replace (mapOptionTree
+ (fun x => flatten_judgment (pcb_judg (snd x)))
+ alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil])
+ with
+ (mapOptionTree
+ (fun x => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x))
+ alts,,
+ [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]).
+ replace (mapOptionTree flatten_leveled_type
+ (mapOptionTreeAndFlatten
+ (fun x => (snd x)) alts))
+ with (mapOptionTreeAndFlatten
+ (fun x =>
+ (snd x)) alts).
+ apply RCase.
+ admit.
+ admit.
destruct case_SBrak.
simpl.
apply secondify.
apply IHx2.
- (* environment has non-empty leaves *)
- apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
+
+ replace (mapOptionTree (fun ht => levels_to_tcode (unlev ht) (getlev ht) @@ nil) (drop_lev (ec :: nil) succ))
+ with (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)).
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply AExch | idtac ].
+ apply ga_kappa.
+ induction succ.
+ destruct a.
+ destruct l.
+ Transparent drop_lev.
+ simpl.
+ unfold drop_lev.
+ Opaque drop_lev.
+ unfold mkDropFlags.
+ simpl.
+ destruct (General.list_eq_dec h1 (ec :: nil)).
+ simpl.
+ auto.
+ simpl.
+ unfold flatten_leveled_type.
+ simpl.
+ auto.
+ simpl.
+ auto.
+ simpl.
+ drop_simplify.
+ simpl.
+ rewrite IHsucc1.
+ rewrite IHsucc2.
+ reflexivity.
(* nesting too deep *)
apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50).
(* information needed to define a case branch in a HaskProof *)
-Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
-{ pcb_freevars : Tree ??(LeveledHaskType Γ ★)
-; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
+Definition pcb_judg
+ {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc}
+ (pcb_freevars : Tree ??(LeveledHaskType Γ ★)) :=
+ sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
> (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
(vec2list (sac_types sac Γ avars))))
- |- [weakT' branchtype ] @ weakL' lev
-}.
-Implicit Arguments ProofCaseBranch [ ].
+ |- [weakT' branchtype ] @ weakL' lev.
(* Figure 3, production $\vdash_E$, all rules *)
Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
-| RAbsT : ∀ Γ Δ Σ κ σ l,
- Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
+| RAbsT : ∀ Γ Δ Σ κ σ l n,
+ Rule [(list_ins n κ Γ)> (weakCE_ Δ) > mapOptionTree weakLT_ Σ |- [ HaskTApp (weakF_ σ) (FreshHaskTyVar_ _) ]@(weakL_ l)]
[Γ>Δ > Σ |- [HaskTAll κ σ ]@l]
| RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
| RCase : forall Γ Δ lev tc Σ avars tbranches
- (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
+ (alts:Tree ??( (@StrongAltCon tc) * (Tree ??(LeveledHaskType Γ ★)) )),
Rule
- ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
+ ((mapOptionTree (fun x => @pcb_judg tc Γ Δ lev tbranches avars (fst x) (snd x)) alts),,
[Γ > Δ > Σ |- [ caseType tc avars ] @lev])
- [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
+ [Γ > Δ > (mapOptionTreeAndFlatten (fun x => (snd x)) alts),,Σ |- [ tbranches ] @ lev]
.
Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
| Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
| Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
-| Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
+| Flat_RAbsT : ∀ Γ Σ κ σ a q n , Rule_Flat (RAbsT Γ Σ κ σ a q n)
| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
| Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
| RGlobal _ _ _ _ _ => "Global"
| RLam _ _ _ _ _ _ => "Abs"
| RCast _ _ _ _ _ _ _ => "Cast"
- | RAbsT _ _ _ _ _ _ => "AbsT"
+ | RAbsT _ _ _ _ _ _ _ => "AbsT"
| RAppT _ _ _ _ _ _ _ => "AppT"
| RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
exists x; auto.
Defined.
- Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
- : ITree { x:X & F x } (fun x => J (projT1 x)) t
- -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
+ Definition fix_indexing X Y (J:X->Type)(t:Tree ??(X*Y))
+ : ITree (X * Y) (fun x => J (fst x)) t
+ -> ITree X (fun x:X => J x) (mapOptionTree (@fst _ _) t).
intro it.
induction it; simpl in *.
apply INone.
Defined.
Definition case_helper tc Γ Δ lev tbranches avars ξ :
- forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
- prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
+ forall pcb:(StrongAltCon * Tree ??(LeveledHaskType Γ ★)),
+ prod (judg2exprType (@pcb_judg tc Γ Δ lev tbranches avars (fst pcb) (snd pcb)))
+ {vars' : Tree ??VV & (snd pcb) = mapOptionTree ξ vars'} ->
((fun sac => FreshM
{ scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
& Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
- (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
+ (weakT' tbranches) (weakL' lev) }) (fst pcb)).
intro pcb.
intro X.
simpl in X.
destruct s as [vars vars_pf].
refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
- (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
+ (mapOptionTree weakLT' pcb) (weakLT' ○ ξ) (weakL' lev) _ ; _).
apply FreshMon.
rewrite vars_pf.
rewrite <- mapOptionTree_compose.
Defined.
Definition gather_branch_variables
- Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
- ProofCaseBranch tc Γ Δ lev tbranches avars sac})
+ Γ Δ
+ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev
+ (alts:Tree ??(@StrongAltCon tc * Tree ??(LeveledHaskType Γ ★)))
:
forall vars,
- mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
- -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
- -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
- { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+ mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars
+ -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts)
+ -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q)))
+ { vars' : _ & (snd q) = mapOptionTree ξ vars' })
alts.
induction alts;
intro vars;
simpl in *.
apply ileaf in source.
apply ILeaf.
- destruct s as [sac pcb].
+ destruct p as [sac pcb].
simpl in *.
split.
intros.
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te x => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ a n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
apply (ileaf X).
destruct case_RAbsT.
- apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+ apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
rewrite mapOptionTree_compose.
rewrite <- H.
reflexivity.
apply ileaf in X. simpl in *.
- apply ETyLam.
+ apply (ETyLam _ _ _ _ _ _ n).
apply X.
destruct case_RAppCo.
| RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
| RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
| RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
- | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
| RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
| RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
destruct case_RAbsT.
simpl.
- destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+ destruct lev; simpl.
+ apply nd_rule.
+ apply SFlat.
+ apply (@RAbsT Γ Δ Σ κ σ nil n).
apply (Prelude_error "RAbsT at depth>0").
destruct case_RAppCo.
eapply RLetRec.
destruct case_RCase.
- simpl.
- apply (Prelude_error "CASE: BIG FIXME").
+ destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
+ apply nd_rule.
+ apply SFlat.
+ rewrite <- mapOptionTree_compose.
+ assert
+ ((mapOptionTree (fun x => skolemize_judgment (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts) =
+ (mapOptionTree (fun x => (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts)).
+ admit.
+ rewrite H.
+ set (@RCase Γ Δ nil tc Σ avars tbranches alts) as q.
+ apply q.
Defined.
Transparent take_arg_types_as_tree.
| ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
| ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
| ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l
- | ETyLam : ∀ Γ Δ ξ κ σ l,
- Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
+ | ETyLam : ∀ Γ Δ ξ κ σ l n,
+ Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
| ECase : forall Γ Δ ξ l tc tbranches atypes,
Expr Γ Δ ξ (caseType tc atypes) l ->
Tree ??{ sac : _
| ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")"
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)"
| ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2"
- | ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e
+ | ETyLam _ _ _ k _ _ _ e => "\@_ ->"+++ exprToString e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => "\~_ ->"+++ exprToString e
| ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
| ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
| EBrak Γ Δ ξ ec t lev e => expr2antecedent e
| ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
| ENote Γ Δ ξ t l n e => expr2antecedent e
- | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
+ | ETyLam Γ Δ ξ κ σ l n e => expr2antecedent e
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
| ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
| ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
| ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
end.
-Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
-(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
- & Expr (sac_gamma sac Γ)
- (sac_delta sac Γ atypes (weakCK'' Δ))
- (scbwv_xi scb ξ l)
- (weakT' tbranches) (weakL' l) } })
- : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
- destruct alt.
- exists x.
- exact
- {| pcb_freevars := mapOptionTree ξ
- (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
- (expr2antecedent (projT2 s)))
- |}.
- Defined.
-
-
Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
match elrb with
| ELR_nil Γ Δ ξ lev => []
Qed.
+Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
+(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+ & Expr (sac_gamma sac Γ)
+ (sac_delta sac Γ atypes (weakCK'' Δ))
+ (scbwv_xi scb ξ l)
+ (weakT' tbranches) (weakL' l) } })
+ : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★).
+ destruct alt.
+ split.
+ apply x.
+ apply (mapOptionTree ξ
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
+ (expr2antecedent (projT2 s)))).
+ Defined.
+
Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
(alts':Tree
??{sac : StrongAltCon &
Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
- (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+ (mapOptionTreeAndFlatten (fun x => snd x)
(mapOptionTree mkProofCaseBranch alts'))
,,
mapOptionTree ξ (expr2antecedent e) =
| EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
- | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+ | ETyLam Γ Δ ξ κ σ l n e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
| ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
(sac_delta sac Γ atypes (weakCK'' Δ))
(scbwv_xi scb ξ l)
(weakT' tbranches) (weakL' l) } })
- : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
+ : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) :=
match alts as ALTS return ND Rule []
- (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
+ (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) ALTS) with
| T_Leaf None => let case_nil := tt in _
| T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
| T_Leaf (Some x) =>
- match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
+ match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes
+ (fst (mkProofCaseBranch X))
+ (snd (mkProofCaseBranch X))] with
existT sac (existT scbx ex) =>
(fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
end
destruct case_leaf.
clear o x alts alts' e.
- eapply nd_comp; [ apply e' | idtac ].
+ simpl.
+ apply (fun x => nd_comp e' x).
clear e'.
- apply nd_rule.
- apply RArrange.
+ unfold pcb_judg.
simpl.
rewrite mapleaves'.
simpl.
rewrite <- mapleaves'.
rewrite vec2list_map_list2vec.
unfold sac_gamma.
- rewrite <- (scbwv_coherent scbx l ξ).
rewrite <- vec2list_map_list2vec.
rewrite mapleaves'.
- set (@factorContextRightAndWeaken'') as q.
- unfold scbwv_xi.
set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
unfold scbwv_varstypes in z.
rewrite vec2list_map_list2vec in z.
rewrite fst_zip in z.
rewrite <- z.
clear z.
+ unfold sac_gamma in *.
+ simpl in *.
+ Unset Printing Implicit.
+ idtac.
+ apply nd_rule.
+ apply RArrange.
+ set (scbwv_exprvars_distinct scbx) as q'.
+ rewrite <- leaves_unleaves in q'.
+ apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')).
+ clear q'.
- replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
- (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
- apply q.
- apply (sac_delta sac Γ atypes (weakCK'' Δ)).
- rewrite leaves_unleaves.
- apply (scbwv_exprvars_distinct scbx).
+ set (scbwv_coherent scbx l ξ) as H.
rewrite leaves_unleaves.
- reflexivity.
+ unfold scbwv_varstypes.
+ apply ALeft.
+ rewrite <- mapleaves'.
+ rewrite <- mapleaves'.
+ rewrite mapleaves'.
+ rewrite vec2list_map_list2vec.
+ rewrite <- H.
+ clear H.
+ rewrite <- mapleaves'.
+ rewrite vec2list_map_list2vec.
+ unfold scbwv_xi.
+ unfold scbwv_varstypes.
+ apply AId.
destruct case_nil.
apply nd_id0.
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
+ Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+ : InstantiatedTypeEnv TV (list_ins n κ Γ).
+ rewrite list_ins_app.
+ rewrite <- (list_take_drop _ Γ n) in ite.
+ apply ilist_app.
+ apply ilist_chop in ite; auto.
+ apply ICons.
+ apply tv.
+ apply ilist_chop' in ite.
+ apply ite.
+ Defined.
+
Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
: UniqM WeakCoercion
:= bind t1' = @typeToWeakType Γ κ t1 ite
| ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
; return WECast e' c'
- | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k
- ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
+ | ETyLam _ _ _ k _ _ n e => fun ite => bind tv = mkWeakTypeVar k
+ ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
; return WETyLam tv e'
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
; bind t2' = typeToWeakType σ₂ ite
Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
+
Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
:= fun TV env => TAll κ (σ TV env).
Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
unfold InstantiatedCoercionEnv; simpl.
apply vec_cons; auto.
Defined.
+
(* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
-Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
- := ilist_tail ite.
+Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite.
+Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
+Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)).
+Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite).
+Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
+Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end.
+Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
+ : InstantiatedCoercionEnv TV CV Γ Δ.
+ intros.
+ unfold InstantiatedCoercionEnv; intros.
+ unfold InstantiatedCoercionEnv in ice.
+ unfold weakCE in ice.
+ simpl in ice.
+ rewrite <- map_preserves_length in ice.
+ apply ice.
+ Defined.
+Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
+ unfold HaskCoercionKind in *.
+ intros.
+ apply hck; clear hck.
+ inversion X; subst; auto.
+ Defined.
+Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
+ fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
+Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
+ forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
+ := fun TV ite tv => (f TV (weakITE ite) tv).
+
+
Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
-Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
- := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
-Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
- := fun TV ite => (cv' TV (weakITE ite)).
Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
induction κ; auto. apply weakV; auto. Defined.
-Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
- := fun TV ite => lt TV (weakITE ite).
-Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
- := map weakV lt.
Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
induction κ; auto. apply weakT; auto. Defined.
Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
apply lt.
apply X.
Defined.
-Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
- rewrite <- ass_app in lt.
- exact lt.
- Defined.
Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
induction κ; auto. apply weakL; auto. Defined.
-Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
- := match lt with t @@ l => weakT t @@ weakL l end.
Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
:= match lt with t @@ l => weakT' t @@ weakL' l end.
Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
induction κ; auto. apply weakCE; auto. Defined.
-Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
- : InstantiatedCoercionEnv TV CV Γ Δ.
- intros.
- unfold InstantiatedCoercionEnv; intros.
- unfold InstantiatedCoercionEnv in ice.
- unfold weakCE in ice.
- simpl in ice.
- rewrite <- map_preserves_length in ice.
- apply ice.
- Defined.
-Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
- unfold HaskCoercionKind in *.
- intros.
- apply hck; clear hck.
- inversion X; subst; auto.
- Defined.
Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
induction κ; auto.
apply weakCK.
Defined.
Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
map weakCK' hck.
-Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
- fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
-Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
- forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
- := fun TV ite tv => (f TV (weakITE ite) tv).
+
+Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
+ rewrite list_ins_app in ite.
+ set (weakITE' ite) as ite'.
+ set (ilist_chop ite) as a.
+ rewrite <- (list_take_drop _ Γ n).
+ apply ilist_app; auto.
+ inversion ite'; auto.
+ Defined.
+
+Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
+ unfold HaskTyVar; intros.
+ unfold HaskTyVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ Defined.
+
+Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
+ unfold HaskType; intros.
+ apply lt.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
+ unfold HaskLevel; intros.
+ unfold HaskLevel in lev.
+ eapply map.
+ apply weakV_.
+ apply lev.
+ Defined.
+Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
+ match lt with t@@l => weakT_ t @@ weakL_ l end.
+Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
+ unfold HaskCoercionKind; intros.
+ unfold HaskCoercionKind in hck.
+ apply hck.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
+Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
+ forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
+ intros.
+ apply f.
+ apply weakITE_ in env.
+ apply env.
+ apply X.
+ Defined.
+Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
+ unfold HaskCoVar; intros.
+ unfold HaskCoVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ unfold InstantiatedCoercionEnv.
+ unfold InstantiatedCoercionEnv in cenv.
+ replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
+ apply cenv.
+ unfold weakCE_.
+ rewrite <- map_preserves_length.
+ reflexivity.
+ Defined.
+
+Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
+ intros.
+ unfold HaskTyVar.
+ intros.
+ rewrite list_ins_app in env.
+ apply weakITE' in env.
+ inversion env; subst; auto.
+ Defined.
+
+
Fixpoint caseType0 {Γ}(lk:list Kind) :
IList _ (HaskType Γ) lk ->
Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
{ toString := typeToString }.
+
+Definition TBool {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp BoolTyCon _ _ TyFunApp_nil.
+Definition TInt {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp IntTyCon _ _ TyFunApp_nil.
Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
Variable PairTyCon : TyFun. Extract Inlined Constant PairTyCon => "TysWiredIn.pairTyCon".
Variable UnitTyCon : TyFun. Extract Inlined Constant UnitTyCon => "TysWiredIn.unitTyCon".
+Variable IntTyCon : TyFun. Extract Inlined Constant IntTyCon => "TysWiredIn.intTyCon".
+Variable BoolTyCon : TyFun. Extract Inlined Constant BoolTyCon => "TysWiredIn.boolTyCon".
Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
+ rewrite <- ass_app in lt.
+ exact lt.
+ Defined.
+
Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
unfold TyVarResolver.
refine (fun tv' =>
| WETyLam tv e => let φ2 := upPhi tv φ in
weakTypeOfWeakExpr e >>= fun te =>
weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
- weakExprToStrongExpr _ (weakCE Δ) φ2
- (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
- >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+ weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+ (fun x => (ψ x) >>= fun y =>
+ OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+ >>= fun e' => castExpr we "WETyLam2" _ _
+ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')
| WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
match te with
Defined.
+ Lemma arrangePullback' {T Q}{f:T->Q}
+ : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??Q), Arrange Σ₁ Σ₂ ->
+ forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ .
+
+ refine ((fix arrangePullback Σ₁ Σ₂ (arr:Arrange Σ₁ Σ₂) {struct arr} :
+ forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ :=
+ match arr as R in Arrange A B return
+ forall Σ₂', B = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (A = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ with
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in (fun rec => _) (arrangePullback _ _ r')
+ | ARight a b c r' => let case_ARight := tt in (fun rec => _) (arrangePullback _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in (fun rec1 rec2 => _) (arrangePullback _ _ r1) (arrangePullback _ _ r2)
+ end)); clear arrangePullback; intros.
+
+ destruct case_AId.
+ exists Σ₂'; split.
+ subst.
+ reflexivity.
+ apply AId.
+
+ destruct case_ACanL.
+ exists ([],,Σ₂'); split.
+ subst.
+ simpl.
+ reflexivity.
+ apply ACanL.
+
+ destruct case_ACanR.
+ exists (Σ₂',,[]); split.
+ subst.
+ simpl.
+ reflexivity.
+ apply ACanR.
+
+ destruct case_AuCanL.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ eexists; split.
+ reflexivity.
+ simpl in H.
+ inversion H.
+ destruct Σ₂'1; try destruct o; inversion H2.
+ apply AuCanL.
+
+ destruct case_AuCanR.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ eexists; split.
+ reflexivity.
+ simpl in H.
+ inversion H.
+ destruct Σ₂'2; try destruct o; inversion H2.
+ apply AuCanR.
+
+ destruct case_AAssoc.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct Σ₂'1; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AAssoc.
+
+ destruct case_AuAssoc.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct Σ₂'2; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AuAssoc.
+
+ destruct case_AExch.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AExch.
+
+ destruct case_AWeak.
+ exists []; split.
+ reflexivity.
+ apply AWeak.
+
+ destruct case_ACont.
+ exists (Σ₂',,Σ₂').
+ subst; split.
+ reflexivity.
+ apply ACont.
+
+ destruct case_ALeft.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct (rec _ (refl_equal _)).
+ destruct p.
+ rewrite e.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply ALeft.
+ apply a0.
+
+ destruct case_ARight.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct (rec _ (refl_equal _)).
+ destruct p.
+ rewrite e.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply ARight.
+ apply a0.
+
+ destruct case_AComp.
+ destruct (rec2 _ H).
+ destruct p.
+ destruct (rec1 _ e).
+ destruct p.
+ rewrite e0.
+ eexists; split.
+ reflexivity.
+ eapply AComp.
+ apply a1.
+ apply a0.
+ Defined.
+
+ Lemma arrangePullback {T Q}{f:T->Q}
+ : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??T), Arrange Σ₁ (mapOptionTree f Σ₂) ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂) }.
+ intros.
+ eapply arrangePullback'.
+ apply X.
+ reflexivity.
+ Defined.
+
(* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
(*
- Lemma arrangeTake {T} pred
+ Lemma arrangePullback {T} pred
: forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
unfold takeT'.
*)
+ (* like Arrange, but without weakening or contraction *)
+ Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type :=
+ | PId : forall a , Permutation a a
+ | PCanL : forall a , Permutation ( [],,a ) ( a )
+ | PCanR : forall a , Permutation ( a,,[] ) ( a )
+ | PuCanL : forall a , Permutation ( a ) ( [],,a )
+ | PuCanR : forall a , Permutation ( a ) ( a,,[] )
+ | PAssoc : forall a b c , Permutation (a,,(b,,c) ) ((a,,b),,c )
+ | PuAssoc : forall a b c , Permutation ((a,,b),,c ) ( a,,(b,,c) )
+ | PExch : forall a b , Permutation ( (b,,a) ) ( (a,,b) )
+ | PLeft : forall {h}{c} x , Permutation h c -> Permutation ( x,,h ) ( x,,c)
+ | PRight : forall {h}{c} x , Permutation h c -> Permutation ( h,,x ) ( c,,x)
+ | PComp : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c
+ .
+ Notation "a ≈ b" := (@Permutation _ a b) (at level 30).
+ Notation "a ⊆ b" := (@Arrange _ a b) (at level 30).
+
+ Definition permuteSwapMiddle {T} (a b c d:Tree ??T) :
+ ((a,,b),,(c,,d)) ≈ ((a,,c),,(b,,d)).
+ eapply PComp.
+ apply PuAssoc.
+ eapply PComp.
+ eapply PLeft.
+ eapply PComp.
+ eapply PAssoc.
+ eapply PRight.
+ apply PExch.
+ eapply PComp.
+ eapply PLeft.
+ eapply PuAssoc.
+ eapply PAssoc.
+ Defined.
+
+ Definition permuteMap :
+ forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
+ Σ₁ ≈ Σ₂ ->
+ (mapOptionTree f Σ₁) ≈ (mapOptionTree f Σ₂).
+ intros.
+ induction X; simpl.
+ apply PId.
+ apply PCanL.
+ apply PCanR.
+ apply PuCanL.
+ apply PuCanR.
+ apply PAssoc.
+ apply PuAssoc.
+ apply PExch.
+ apply PLeft; auto.
+ apply PRight; auto.
+ eapply PComp; [ apply IHX1 | apply IHX2 ].
+ Defined.
+
+ (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
+ Definition partitionPermutation :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Σ ≈ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply PuCanL.
+ apply PuCanR.
+ simpl.
+ apply PuCanL.
+ simpl in *.
+ eapply PComp; [ idtac | apply permuteSwapMiddle ].
+ eapply PComp.
+ eapply PLeft.
+ apply IHΣ2.
+ eapply PRight.
+ apply IHΣ1.
+ Defined.
+
+ Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b.
+ intro arr.
+ induction arr.
+ apply AId.
+ apply ACanL.
+ apply ACanR.
+ apply AuCanL.
+ apply AuCanR.
+ apply AAssoc.
+ apply AuAssoc.
+ apply AExch.
+ apply ALeft; apply IHarr.
+ apply ARight; apply IHarr.
+ eapply AComp.
+ apply IHarr1.
+ apply IHarr2.
+ Defined.
+
+ Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a.
+ intro perm.
+ induction perm.
+ apply PId.
+ apply PuCanL.
+ apply PuCanR.
+ apply PCanL.
+ apply PCanR.
+ apply PuAssoc.
+ apply PAssoc.
+ apply PExch.
+ eapply PLeft; apply IHperm.
+ eapply PRight; apply IHperm.
+ eapply PComp.
+ apply IHperm2.
+ apply IHperm1.
+ Defined.
+
+ (*
+ Definition factorArrangementAsPermutation {T} : forall (a b:Tree ??T), a ⊆ b -> { c : _ & (c,,a) ≈ b }.
+
+ refine ((fix factor a b (arr:Arrange a b) :=
+ match arr as R in Arrange A B return
+ { c : _ & (c,,A) ≈ B }
+ with
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in (fun r'' => _) (factor _ _ r')
+ | ARight a b c r' => let case_ARight := tt in (fun r'' => _) (factor _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (factor _ _ r1) (factor _ _ r2)
+ end)); clear factor; intros.
+
+ destruct case_AId.
+ exists []. apply PCanL.
+
+ destruct case_ACanL.
+ exists [].
+ eapply PComp.
+ apply PCanL.
+ apply PCanL.
+
+ destruct case_ACanR.
+ exists [].
+ eapply PComp.
+ apply PCanL.
+ apply PCanR.
+
+ destruct case_AuCanL.
+ exists [].
+ apply PRight.
+ apply PId.
+
+ destruct case_AuCanR.
+ exists [].
+ apply PExch.
+
+ destruct case_AAssoc.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PAssoc.
+
+ destruct case_AuAssoc.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PuAssoc.
+
+ destruct case_AExch.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PExch.
+
+ destruct case_AWeak.
+ exists a0.
+ eapply PCanR.
+
+ destruct case_ACont.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ eapply PComp.
+ eapply PLeft.
+ eapply
+
+ Defined.
+ *)
+
End NaturalDeductionContext.
projects / coq-hetmet.git / commitdiff