From: Adam Megacz Date: Tue, 30 Aug 2011 13:59:54 +0000 (-0700) Subject: Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=08b41911dfc33a7dcd24aa26a83ac174aa67a826;hp=6ba2c98f5e7f9c00651d6050a98d1d7aab758958 Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet --- diff --git a/examples/CircuitExample.hs b/examples/CircuitExample.hs index f4f5151..b8ca60b 100644 --- a/examples/CircuitExample.hs +++ b/examples/CircuitExample.hs @@ -1,8 +1,8 @@ {-# 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, (.) ) diff --git a/examples/Demo.hs b/examples/Demo.hs index 0a5e4e4..bb3bf17 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,20 +1,137 @@ -{-# 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) ]> -} @@ -38,14 +155,6 @@ demo const mult = 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 @@ -53,4 +162,10 @@ 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 diff --git a/examples/DotProduct.hs b/examples/DotProduct.hs index 6de0c01..4b36019 100644 --- a/examples/DotProduct.hs +++ b/examples/DotProduct.hs @@ -1,7 +1,7 @@ {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XFlexibleContexts #-} module DotProduct where -import GHC.HetMet.CodeTypes hiding ((-)) +import GHC.HetMet.GuestLanguage hiding ((-)) import Prelude hiding ( id, (.) ) -------------------------------------------------------------------------------- diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index 8775d4a..dd7937b 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -119,7 +119,7 @@ instance Eq ((GArrowSkeleton m) a b) -- 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' @@ -206,15 +206,17 @@ repeat f x = let x' = f x in -- | 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') @@ -277,6 +279,8 @@ data GArrowSkeletonY m :: * -> * -> * 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 @@ -305,6 +309,8 @@ gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y 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 @@ -327,10 +333,10 @@ gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl 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 @@ -353,53 +359,118 @@ optimizel (GASL_comp gy gl) -} 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 @@ -414,5 +485,16 @@ optimizex (GASX_copy) = GASX_copy 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 diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index f3ad728..d3ae2e0 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -78,7 +78,7 @@ lowermost (TT x y) = lowermost y -- | 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 @@ -87,7 +87,7 @@ data 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" } @@ -96,7 +96,7 @@ getOut (DiagramLoopBot d t) = case getOut d of { TT y z -> y ; -- | 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" } @@ -112,8 +112,8 @@ type BoxRenderer = Float -> -- x2 Float -> -- y2 String -- TikZ code - - +noRender :: BoxRenderer +noRender _ _ _ _ _ = "" @@ -183,27 +183,27 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x ; 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 @@ -216,7 +216,7 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x 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 [] } @@ -244,7 +244,9 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x 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 @@ -265,7 +267,9 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x 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") @@ -283,7 +287,7 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x ; 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 @@ -293,12 +297,17 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x -- ++ 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 @@ -307,16 +316,16 @@ constrainBot :: Diagram -> Float -> TrackIdentifier -> ConstraintM () 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)) @@ -354,14 +363,20 @@ tikZ m = tikZ' ++ 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" @@ -385,7 +400,7 @@ tikZ m = tikZ' ++ 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 "-" @@ -396,7 +411,7 @@ tikZ m = tikZ' 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 @@ -404,7 +419,7 @@ tikZ m = tikZ' 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 diff --git a/examples/GArrowTutorial.hs b/examples/GArrowTutorial.hs index c614d0d..a993582 100644 --- a/examples/GArrowTutorial.hs +++ b/examples/GArrowTutorial.hs @@ -3,8 +3,8 @@ module GArrowTutorial 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, (.) ) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 05e9c0b..88714c7 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -267,6 +267,16 @@ Section core2proof. 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 ]. @@ -284,6 +294,17 @@ Section core2proof. 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) @@ -315,6 +336,7 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) (hetmet_pga_loopl : CoreVar) (hetmet_pga_loopr : CoreVar) + (hetmet_pga_kappa : CoreVar) . @@ -415,16 +437,16 @@ Section core2proof. ; 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. @@ -539,6 +561,7 @@ Section core2proof. 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' @@ -566,6 +589,7 @@ Section core2proof. hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr + hetmet_pga_kappa lbinds (* hetmet_pga_applyl diff --git a/src/General.v b/src/General.v index ee5cb16..541dc6f 100644 --- a/src/General.v +++ b/src/General.v @@ -218,6 +218,104 @@ Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop := | (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. @@ -803,6 +901,30 @@ Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2. 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 @@ -915,7 +1037,7 @@ Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrErr 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) diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 59636bf..c7625b8 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -46,7 +46,6 @@ Set Printing Width 130. *) Section HaskFlattener. - Ltac eqd_dec_refl' := match goal with | [ |- context[@eqd_dec ?T ?V ?X ?X] ] => @@ -232,12 +231,12 @@ Section HaskFlattener. 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. @@ -274,9 +273,9 @@ Section HaskFlattener. ; 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). @@ -407,6 +406,9 @@ Section HaskFlattener. apply precompose. Defined. + + + (* useful for cutting down on the pretty-printed noise Notation "` x" := (take_lev _ x) (at level 20). @@ -636,66 +638,109 @@ Section HaskFlattener. 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. @@ -821,7 +866,7 @@ Section HaskFlattener. | 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 _ @@ -1118,8 +1163,8 @@ Section HaskFlattener. 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'. @@ -1196,8 +1241,26 @@ Section HaskFlattener. 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. @@ -1288,8 +1351,37 @@ Section HaskFlattener. 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"). diff --git a/src/HaskProof.v b/src/HaskProof.v index f98800d..7f15825 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -36,14 +36,13 @@ Inductive Judg := 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 := @@ -75,8 +74,8 @@ 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, @@ -87,11 +86,11 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | 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, @@ -132,7 +131,7 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | 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 ) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 716a983..e85bb39 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -184,7 +184,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RGlobal _ _ _ _ _ => "Global" | RLam _ _ _ _ _ _ => "Abs" | RCast _ _ _ _ _ _ _ => "Cast" - | RAbsT _ _ _ _ _ _ => "AbsT" + | RAbsT _ _ _ _ _ _ _ => "AbsT" | RAppT _ _ _ _ _ _ _ => "AppT" | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo" | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 3dbc81f..ab10fd8 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -393,9 +393,9 @@ Section HaskProofToStrong. 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. @@ -418,12 +418,13 @@ Section HaskProofToStrong. 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. @@ -435,7 +436,7 @@ Section HaskProofToStrong. 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. @@ -470,14 +471,15 @@ Section HaskProofToStrong. 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; @@ -487,7 +489,7 @@ Section HaskProofToStrong. simpl in *. apply ileaf in source. apply ILeaf. - destruct s as [sac pcb]. + destruct p as [sac pcb]. simpl in *. split. intros. @@ -758,7 +760,7 @@ Section HaskProofToStrong. | 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 _ @@ -938,12 +940,12 @@ Section HaskProofToStrong. 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. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 8764102..0d1cecb 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -226,7 +226,7 @@ Section HaskSkolemizer. | 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 _ @@ -472,7 +472,10 @@ Section HaskSkolemizer. 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. @@ -518,8 +521,17 @@ Section HaskSkolemizer. 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. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 874b368..6629511 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -47,8 +47,8 @@ Section HaskStrong. | 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 : _ @@ -90,7 +90,7 @@ Section HaskStrong. | 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 diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 114f2d9..e93ddd9 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -520,7 +520,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : | 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 @@ -549,23 +549,6 @@ match elrb with | 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 => [] @@ -1057,6 +1040,21 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : 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 & @@ -1064,7 +1062,7 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e 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) = @@ -1119,7 +1117,7 @@ Definition expr2proof : | 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) @@ -1131,13 +1129,15 @@ Definition expr2proof : (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 @@ -1250,10 +1250,10 @@ Definition expr2proof : 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. @@ -1262,26 +1262,40 @@ Definition expr2proof : 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. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index deb7adc..8bb52e1 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -79,6 +79,18 @@ Section HaskStrongToWeak. 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 @@ -144,8 +156,8 @@ Section HaskStrongToWeak. | 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 diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index e5a10ba..4740acb 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -155,6 +155,7 @@ Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@Ins 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 ★) @@ -350,21 +351,41 @@ Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:Instanti 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 Γ κ) κ₂. @@ -375,34 +396,12 @@ 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. @@ -410,11 +409,80 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ 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 -> @@ -687,3 +755,6 @@ Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string := 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. diff --git a/src/HaskTyCons.v b/src/HaskTyCons.v index 617cd59..1eb479a 100644 --- a/src/HaskTyCons.v +++ b/src/HaskTyCons.v @@ -29,4 +29,6 @@ Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toS 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". diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index d8dcf42..0acc0af 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -26,6 +26,11 @@ Open Scope string_scope. 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' => @@ -604,9 +609,11 @@ Definition weakExprToStrongExpr : forall | 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 diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v index 57dfdb8..4da8922 100644 --- a/src/NaturalDeductionContext.v +++ b/src/NaturalDeductionContext.v @@ -245,11 +245,348 @@ Section NaturalDeductionContext. 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.