coqc := coqc -noglob -opt
coqfiles := $(shell find src -name \*.v | grep -v \\\#)
allfiles := $(coqfiles) $(shell find src -name \*.hs | grep -v \\\#)
-coq_version := 8.3pl2-tracer
+coq_version := $(shell coqc -v | head -n1 | sed 's_.*version __' | sed 's_ .*__')
+coq_version_wanted := 8.3pl2-tracer
default: all
cd build; $(MAKE) -f Makefile.coq OPT="-opt -dont-load-proofs" All.vo
build/CoqPass.hs: $(allfiles)
- $(coqc) -v | grep 'version $(coq_version)' || (echo;echo "You need Coq version $(coq_version) to proceed";echo; false)
+ifeq ($(coq_version),$(coq_version_wanted))
make build/Makefile.coq
cd build; $(MAKE) -f Makefile.coq OPT="-opt -dont-load-proofs" ExtractionMain.vo
cd build; $(MAKE) -f Makefile.coq Extraction.vo
cat src/Extraction-prefix.hs > build/CoqPass.hs
cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs
+else
+ @echo
+ @echo ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ @echo ++ YOU DO NOT HAVE COQ VERSION $(coq_version_wanted) INSTALLED ++
+ @echo ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ @echo
+ @echo Therefore, I am going to "git pull -f" from the coq-extraction-baked-in
+ @echo branch of the repository.
+ @echo
+ git pull -f http://git.megacz.com/coq-hetmet.git coq-extraction-baked-in:master
+endif
+
build/Makefile.coq: $(coqfiles) src/categories/src
mkdir -p build
-{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint #-}
+{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables #-}
module Demo (demo) where
---demo con mer = <[ ~~mer ~~(con (2::Int)) ~~(con (12::Int)) ]>
+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' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
+
+
+{-
demo const mult =
- <[ let four = ~~mult four ~~(const 4)
+ <[ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) ]>
+-}
+
+{-
+demo const mult =
+ <[ \(y::Int) ->
+ let four = ~~mult four ~~(const 4)
-- twelve = {- {- ~~mult four -} ~~(const 12) -} four
in four
]>
-
+-}
demo ::
- forall a c .
- (Int -> <[a]>@c) ->
- <[a -> a -> a]>@c ->
- <[a]>@c
+ forall c .
+ (Int -> <[Int]>@c) ->
+ <[Int -> Int -> Int]>@c ->
+ <[Int -> Int]>@c
{-
demo const mult =
import GHC.HetMet.GArrow
import Demo
-{-
-demo' ::
- (Int -> PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) ) ->
- ( PGArrow g (GArrowTensor g (GArrowTensor g Int Int) (GArrowUnit g)) Int) ->
- (PGArrow g (GArrowUnit g) (GArrowTensor g (GArrowUnit g) Int) )
-demo' = demo
--}
-
-main = tikz $ \const merge -> demo const merge
+main = tikz demo
| PortTensor (PortShape a) (PortShape a)
| PortFree a
+instance Show a => Show (PortShape a) where
+ show PortUnit = "U"
+ show (PortTensor p1 p2) = "("++show p1++"*"++show p2++")"
+ show (PortFree x) = show x
+
data GArrowPortShape m s a b =
GASPortPassthrough
(PortShape s)
unify' (PortTensor x1 y1) (PortTensor x2 y2) = mergeU (unify x1 x2) (unify y1 y2)
unify' PortUnit PortUnit = emptyUnifier
unify' s1 s2 = error $ "Unifiable UPort got impossible unification case: "
--- ++ show s1 ++ " and " ++ show s2
+
+ replace uv prep PortUnit = PortUnit
+ replace uv prep (PortTensor p1 p2) = PortTensor (replace uv prep p1) (replace uv prep p2)
+ replace uv prep (PortFree x) = if x==uv then prep else PortFree x
+
inject = PortFree
project (PortFree v) = Just v
project _ = Nothing
}
detect (GAS_const i) = do { x <- freshM; return $ GASPortShapeWrapper PortUnit (PortFree x) (GAS_const i) }
--- FIXME: I need to fix the occurs check before I can make these different again
detect GAS_merge = do { x <- freshM
- ; y <- freshM
- ; return $ GASPortShapeWrapper (PortTensor (PortFree x) (PortFree y)) (PortFree x) GAS_merge }
+ ; return $ GASPortShapeWrapper (PortTensor (PortFree x) (PortFree x)) (PortFree x) GAS_merge }
+
detect (GAS_loopl f) = do { x <- freshM
; y <- freshM
; z <- freshM
- ; z' <- freshM -- remove once I fix the occurs check
; f' <- detect f
; unifyM (fst $ shapes f') (PortTensor (PortFree z) (PortFree x))
- ; unifyM (snd $ shapes f') (PortTensor (PortFree z') (PortFree y))
+ ; unifyM (snd $ shapes f') (PortTensor (PortFree z) (PortFree y))
; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopl (GAS_misc f'))
}
detect (GAS_loopr f) = do { x <- freshM
; y <- freshM
; z <- freshM
- ; z' <- freshM -- remove once I fix the occurs check
; f' <- detect f
; unifyM (fst $ shapes f') (PortTensor (PortFree x) (PortFree z))
- ; unifyM (snd $ shapes f') (PortTensor (PortFree y) (PortFree z'))
+ ; unifyM (snd $ shapes f') (PortTensor (PortFree y) (PortFree z))
; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopr (GAS_misc f'))
}
-- diagram which ks *equivalent to* the term, rather than structurally
-- exactly equal to it.
--
-module GArrowSkeleton (GArrowSkeleton(..), optimize)
+module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify)
where
-import Prelude hiding ( id, (.), lookup )
+import Prelude hiding ( id, (.), lookup, repeat )
import Control.Category
import GHC.HetMet.GArrow
import Unify
-- laws, but no guarantees about which optimizations actually happen.
--
optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
+optimize = repeat (gasl2gas . optimizel . gas2gasl)
+
+{-
optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
where
optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
-- Some optimizations fail due to misparenthesization; we default to
-- left-associativity and hope for the best
- optimize' (GAS_comp f (GAS_comp g h)) = GAS_comp (GAS_comp f g) h
+ optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
-
optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
g' = optimize' g
optimize' (GAS_first GAS_id ) = GAS_id
optimize' (GAS_second GAS_id ) = GAS_id
+-- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
+-- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
optimize' (GAS_first f ) = GAS_first $ optimize' f
optimize' (GAS_second f ) = GAS_second $ optimize' f
- optimize' (GAS_loopl GAS_id) = GAS_id
- optimize' (GAS_loopr GAS_id) = GAS_id
- optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
- optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
- optimize' x = x
+ optimize' (GAS_loopl GAS_id ) = GAS_id
+ optimize' (GAS_loopr GAS_id ) = GAS_id
+ optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
+ optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
+ optimize' x = x
optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
- optimize_pair (GAS_first f) (GAS_first g) = Just $ GAS_first (GAS_comp f g)
- optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g)
-
optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
optimize_pair _ _ = Nothing
+-}
+
+repeat :: Eq a => (a -> a) -> a -> a
+repeat f x = let x' = f x in
+ if x == x'
+ then x
+ else repeat f 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')
+ 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 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 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')
+ (f' , g' ) -> GAS_comp f' g'
+ beautify' (GAS_first f) = GAS_first $ beautify' f
+ beautify' (GAS_second f) = GAS_second $ beautify' f
+ beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
+ beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
+ beautify' q = q
+
+
+
+
+gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
+gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k
+gas2gasl (GAS_id ) = GASL_id
+gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
+gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
+gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
+gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
+gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
+gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
+gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
+gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
+gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
+gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
+gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
+gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
+gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge
+gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
+gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
+gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
+
+-- apply "first" to a GASL
+gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
+gasl_firstify (GASL_id ) = GASL_id
+gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
+gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
+
+-- apply "second" to a GASL
+gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
+gasl_secondify (GASL_id ) = GASL_id
+gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
+gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
+
+-- concatenates two GASL's
+gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
+gaslcat (GASL_id ) g' = g'
+gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
+gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
+
+data GArrowSkeletonL m :: * -> * -> *
+ where
+ GASL_id :: GArrowSkeletonL m x x
+ GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
+ GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
+
+data GArrowSkeletonY m :: * -> * -> *
+ where
+ 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)
+
+data GArrowSkeletonX m :: * -> * -> *
+ where
+ GASX_const :: Int -> GArrowSkeletonX m () Int
+ GASX_cancell :: GArrowSkeletonX m ((),x) x
+ GASX_cancelr :: GArrowSkeletonX m (x,()) x
+ GASX_uncancell :: GArrowSkeletonX m x ((),x)
+ GASX_uncancelr :: GArrowSkeletonX m x (x,())
+ GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
+ GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
+ GASX_drop :: GArrowSkeletonX m x ()
+ GASX_copy :: GArrowSkeletonX m x (x,x)
+ GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
+ GASX_merge :: GArrowSkeletonX m (x,y) z
+ GASX_misc :: m x y -> GArrowSkeletonX m x y
+ GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
+ GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
+
+-- TO DO: gather "maximal chunks" of ga_first/ga_second
+gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
+gasl2gas GASL_id = GAS_id
+gasl2gas (GASL_Y gy ) = gasy2gas gy
+gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
+
+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)
+
+gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
+gasx2gas (GASX_const k) = GAS_const k
+gasx2gas (GASX_cancell) = GAS_cancell
+gasx2gas (GASX_cancelr) = GAS_cancelr
+gasx2gas (GASX_uncancell) = GAS_uncancell
+gasx2gas (GASX_uncancelr) = GAS_uncancelr
+gasx2gas (GASX_assoc) = GAS_assoc
+gasx2gas (GASX_unassoc) = GAS_unassoc
+gasx2gas (GASX_drop) = GAS_drop
+gasx2gas (GASX_copy) = GAS_copy
+gasx2gas (GASX_swap) = GAS_swap
+gasx2gas (GASX_merge) = GAS_merge
+gasx2gas (GASX_misc m) = GAS_misc m
+gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
+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 gl) = GASL_comp (optimizey gy) (optimizel gl)
+
+--optimize' (GAS_loopl GAS_id ) = GAS_id
+--optimize' (GAS_loopr GAS_id ) = GAS_id
+--optimize_pair f GAS_drop = Just $ GAS_drop
+{-
+ optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
+ optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
+ optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
+ optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
+ optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
+ optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
+ optimize_pair GAS_swap GAS_swap = Just $ GAS_id
+ optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
+ optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
+ optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
+ optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
+ optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
+ optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
+-}
+
+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_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
+
+-- 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_X GASX_uncancell) = True
+pushright (GASY_X GASX_uncancelr) = True
+pushright (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)
+optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
+optimizex (GASX_const k) = GASX_const k
+optimizex (GASX_cancell) = GASX_cancell
+optimizex (GASX_cancelr) = GASX_cancelr
+optimizex (GASX_uncancell) = GASX_uncancell
+optimizex (GASX_uncancelr) = GASX_uncancelr
+optimizex (GASX_assoc) = GASX_assoc
+optimizex (GASX_unassoc) = GASX_unassoc
+optimizex (GASX_drop) = GASX_drop
+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 gl) = GASX_loopl $ optimizel gl
+optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
getOut (DiagramBox 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 "mismatch" }
-getOut (DiagramLoopBot d t) = case getOut d of { TT y z -> y ; _ -> error "mismatch" }
+getOut (DiagramLoopTop t d) = case getOut d of { TT z y -> y ; _ -> error "DiagramLoopTop: mismatch" }
+getOut (DiagramLoopBot d t) = case getOut d of { TT y z -> y ; _ -> error "DiagramLoopBot: mismatch" }
-- | get the input tracks of a diagram
getIn :: Diagram -> Tracks
getIn (DiagramBox 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 "mismatch" }
-getIn (DiagramLoopBot d t) = case getIn d of { TT x z -> x ; _ -> error "mismatch" }
+getIn (DiagramLoopTop t d) = case getIn d of { TT z x -> x ; _ -> error "DiagramLoopTop: mismatch" }
+getIn (DiagramLoopBot d t) = case getIn d of { TT x z -> x ; _ -> error "DiagramLoopBot: mismatch" }
-- | A BoxRenderer is just a routine that, given the dimensions of a
-- boxes-and-wires box element, knows how to spit out a bunch of TikZ
; return (T t)
}
-
mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram
mkdiag (GASPortPassthrough inp outp m) = error "not supported"
mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x
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) "black" "dashed"
+ drawLine x1 (tp!lowermost x) ((x1+x2)/2) (tp!uppermost y) "gray!50" "dashed"
; return $ DiagramBox 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) "black" "dashed"
+ drawLine x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "gray!50" "dashed"
; return $ DiagramBox 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) "black" "dashed"
+ drawLine ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "gray!50" "dashed"
; return $ DiagramBox 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) "black" "dashed"
+ drawLine ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "dashed"
; return $ DiagramBox 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
drawWires tp x1 z x2 z "black"
; return $ DiagramBox top (TT x (TT y z)) r (TT (TT x y) z) bot
}
- mkdiag' (GAS_loopr f) = do { (top,(TT _ x),bot) <- alloc inp; f' <- mkdiag' f ; constrainBot f' 1 (uppermost x)
- ; return $ DiagramLoopBot f' x }
- mkdiag' (GAS_loopl f) = do { (top,(TT x _),bot) <- alloc inp; f' <- mkdiag' f ; constrainTop (lowermost x) 1 f'
- ; return $ DiagramLoopTop x f' }
+ mkdiag' (GAS_loopl f) = do { f' <- mkdiag' f
+ ; l <- allocLoop (case (getIn f') of (TT z _) -> z ; _ -> error "GAS_loopl: mismatch")
+ ; constrainTop (lowermost l) loopgap f'
+ ; return $ DiagramLoopTop l f' }
+ mkdiag' (GAS_loopr f) = do { f' <- mkdiag' f
+ ; l <- allocLoop (case (getIn f') of (TT _ z) -> z ; _ -> error "GAS_loopr: mismatch")
+ ; constrainBot f' loopgap (uppermost l)
+ ; return $ DiagramLoopBot f' l }
mkdiag' (GAS_misc f ) = mkdiag f
diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram
constrainBot (DiagramLoopBot d p) i v = constrain v GT (lowermost p) 2
-- | The width of a box is easy to calculate
-width :: Diagram -> Float
-width (DiagramComp d1 d2) = (width d1) + 1 + (width d2)
-width (DiagramBox ptop pin x pout pbot) = 2
-width (DiagramBypassTop p d) = (width d) + 2
-width (DiagramBypassBot d p) = (width d) + 2
-width (DiagramLoopTop p d) = (width d) + 2
-width (DiagramLoopBot d p) = (width d) + 2
+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 (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))
drawWires :: TrackPositions -> Float -> Tracks -> Float -> Tracks -> String -> String
drawWires tp x1 (TT a b) x2 (TT a' b') color = drawWires tp x1 a x2 a' color ++ drawWires tp x1 b x2 b' color
-drawWires tp x1 (T a) x2 (T a') color = drawLine x1 (tp!a) x2 (tp!a') color "-"
-drawWires tp x1 (TU a) x2 (TU a') color = drawLine x1 (tp!a) x2 (tp!a') color "dashed"
+drawWires tp x1 (T a) x2 (T a') color = drawLine x1 (tp!a) x2 (tp!a') color "-"
+drawWires tp x1 (TU a) x2 (TU a') color = drawLine x1 (tp!a) x2 (tp!a') "gray!50" "dashed"
drawWires tp _ _ _ _ _ = error "drawwires fail"
+wirecos :: TrackPositions -> Tracks -> [(Float,Bool)]
+wirecos tp (TT a b) = wirecos tp a ++ wirecos tp b
+wirecos tp (T a) = [(tp!a,True)]
+wirecos tp (TU a) = [(tp!a,False)]
+
+wire90 :: Float -> Float -> (Float,Float,Bool) -> String
+wire90 x y (y1,y2,b) = drawLine' [(x,y1),(x',y1),(x',y2),(x,y2)] color (style++",rounded corners")
+ where
+ color = if b then "black" else "gray!50"
+ style = if b then "-" else "dashed"
+ x' = x - (y - y1) - loopgap
+
+wire90' x y (y1,y2,b) = drawLine' [(x,y1),(x',y1),(x',y2),(x,y2)] color (style++",rounded corners")
+ where
+ color = if b then "black" else "gray!50"
+ style = if b then "-" else "dashed"
+ x' = x + (y - y1) + loopgap
+
tikZ :: TrackPositions ->
Diagram ->
Float -> -- horizontal position
tikZ m = tikZ'
where
tikZ' d@(DiagramComp d1 d2) x = tikZ' d1 x
- ++ wires' (x+width d1) (getOut d1) (x+width d1+0.5) "black" "->"
- ++ wires' (x+width d1+0.5) (getOut d1) (x+width d1+1) "black" "-"
- ++ tikZ' d2 (x + width d1 + 1)
+ ++ 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
let bot = getBot d' in
- drawBox x top (x+width d') bot "gray!50" "second"
+ 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 d) (getOut d) (x+1+width d+1) (getOut d) "black"
- ++ drawWires m x p (x+1+width d+1) p "black"
+ ++ 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
let bot = getBot d' in
- drawBox x top (x+width d') bot "gray!50" "first"
+ drawBox x top (x+width m d') bot "gray!50" "first"
++ drawWires m x (getIn d) (x+1) (getIn d) "black"
++ tikZ' d (x+1)
- ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
- ++ drawWires m x p (x+1+width d+1) p "black"
+ ++ 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'@(DiagramLoopTop p d) x = let top = getTop d' in
let bot = getBot d' in
- drawBox x top (x+width d') bot "gray!50" "loopl"
- ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
- ++ tikZ' d (x+1)
- ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
- ++ drawWires m x p (x+1+width d+1) p "black"
- tikZ' d'@(DiagramLoopBot d p) x = let top = getTop d' in
- let bot = getBot d' in
- drawBox x top (x+width d') bot "gray!50" "loopr"
- ++ drawWires m x (getIn d) (x+1) (getIn d) "black"
- ++ tikZ' d (x+1)
- ++ drawWires m (x+1+width d) (getOut d) (x+1+width d+1) (getOut d) "black"
- ++ drawWires m x p (x+1+width d+1) p "black"
- tikZ' d@(DiagramBox ptop pin r pout pbot) x = r m x (m ! ptop) (x + width d) (m ! pbot)
+ let gap = loopgap + (m ! lowermost p) - (m ! uppermost p) in
+ drawBox x top (x+width m d') bot "gray!50" "loopl"
+ ++ tikZ' d (x+1+gap)
+ ++ drawWires m (x+1+gap) p (x+1+gap+width m d) p "black"
+ ++ let p' = case getIn d of TT z _ -> z ; _ -> error "DiagramLoopTop: mismatch"
+ pzip = map (\((y,b),(y',_)) -> (y,y',b)) $ zip (wirecos m p) (reverse $ wirecos m p')
+ in concatMap (wire90 (x+1+gap) (m ! lowermost p)) pzip
+ ++ let p' = case getOut d of TT z _ -> z ; _ -> error "DiagramLoopTop: mismatch"
+ pzip = map (\((y,b),(y',_)) -> (y,y',b)) $ zip (wirecos m p) (reverse $ wirecos m p')
+ in concatMap (wire90' (x+1+gap+width m d) (m ! lowermost p)) pzip
+ ++ let rest = case getIn d of TT _ z -> z ; _ -> error "DiagramLoopTop: mismatch"
+ in drawWires m x rest (x+1+gap) rest "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)
wires x1 t x2 c = wires' x1 t x2 c "-"
wires' :: Float -> Tracks -> Float -> String -> String -> String
wires' x1 (TT x y) x2 color st = wires' x1 x x2 color st ++ wires' x1 y x2 color st
wires' x1 (T v) x2 color st = drawLine x1 (m ! v) x2 (m ! v) color st -- ++ textc ((x1+x2) / 2) (m!v) (show v) "purple"
- wires' x1 (TU v) x2 color st = drawLine x1 (m ! v) x2 (m ! v) color "dashed"
+ wires' x1 (TU v) x2 color st = drawLine x1 (m ! v) x2 (m ! v) "gray!50" "dashed"
getTop :: Diagram -> Float
getTop (DiagramComp d1 d2) = min (getTop d1) (getTop d2)
; return (TT x1 x2)
}
+-- allocates a second set of tracks identical to the first one but constrained only relative to each other (one unit apart)
+-- and upside-down
+allocLoop :: Tracks -> ConstraintM Tracks
+allocLoop (TU _) = do { T x <- alloc1 ; return (TU x) }
+allocLoop (T _) = do { x <- alloc1 ; return x }
+allocLoop (TT t1 t2) = do { x1 <- allocLoop t2
+ ; x2 <- allocLoop t1
+ ; constrain (lowermost x1) LT (uppermost x2) (-1)
+ ; return (TT x1 x2)
+ }
+
do_lp_solve :: [Constraint] -> IO String
do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n"
; putStrLn stdin
}
in do { let (_,constraints) = execState cm (0,[])
; lps <- do_lp_solve $ constraints
- ; let trackpos = lp_solve_to_trackpos lps
- ; return $ tikZ trackpos (evalState cm (0,[])) 0
+ ; let m = lp_solve_to_trackpos lps
+ ; let d = evalState cm (0,[])
+ ; let t = tikZ m d 1
+ ; return (t ++ drawWires m 0 (getIn d) 1 (getIn d) "black"
+ ++ drawWires m (width m d+1) (getOut d) (width m d+2) (getOut d) "black")
}
+
-tikz :: (forall g a .
- (Int -> PGArrow g (GArrowUnit g) a) ->
- (
- forall b . PGArrow g (GArrowTensor g b b) b) ->
- PGArrow g (GArrowUnit g) a) -> IO ()
-
-tikz x = tikz' $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }) )
+tikz :: forall c .
+ (forall g .
+ (Int -> PGArrow g (GArrowUnit g) Int) ->
+ (PGArrow g (GArrowTensor g c c) c) ->
+ PGArrow g c c)
+ -> IO ()
+tikz x = tikz' $ beautify $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge }))
tikz' example
= do putStrLn "\\documentclass{article}"
"("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
"("++show (x2*xscale)++","++show (y2*yscale)++");\n"
+drawLine' [] color style = ""
+drawLine' (xy1:xy) color style =
+ "\\path[draw,color="++color++","++style++"] "++
+ foldl (\x y -> x ++ " -- " ++ y) (f xy1) (map f xy)
+ ++ ";\n"
+ where
+ f = (\(x,y) -> "("++show (x*xscale)++","++show (y*yscale)++")")
+
-- | x scaling factor for the entire diagram, since TikZ doesn't scale font sizes
xscale = 1
-- | y scaling factor for the entire diagram, since TikZ doesn't scale font sizes
yscale = 1
+
+-- | extra gap placed between loopback wires and the contents of the loop module
+loopgap = 1
\ No newline at end of file
--- | A very simple unification engine; used by GArrowTikZ
-module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve, occurs)
+-- | A very simple finite-sized-term unification engine; used by GArrowTikZ
+module Unify(UVar, Unifier, Unifiable(..), mergeU, emptyUnifier, getU, uvarSupply, unify, resolve)
+--
+-- | Terminology: a value of type @t@ (for which an instance
+-- @Unifiable t@ exists) is "fully resolved" with respect to some
+-- value of type @Unifier t@ if no @UVar@ which occurs in the
+-- @t@-value is a key in the unifier map.
+--
where
import Prelude hiding (lookup)
import Data.Map hiding (map)
import Data.List (nub)
import Control.Monad.Error
--- TO DO: propagate occurs-check errors through the Unifier instead of using Prelude.error
-
-- | a unification variable
newtype UVar = UVar Int
deriving (Ord, Eq)
instance Show UVar where
show (UVar v) = "u" ++ show v
--- | A unifier is a map from unification /variables/ to unification /values/ of type @t@.
+-- | A unifier is a map from unification /variables/ to unification
+-- /values/ of type @t@. Invariant: values of the map are always
+-- fully resolved with respect to the map.
data Unifier t = Unifier (Map UVar t)
+ | UnifierError String
--- | Resolves a unification variable according to a Unifier (not recursively).
+-- | Resolves a unification variable according to a Unifier.
getU :: Unifier t -> UVar -> Maybe t
-getU (Unifier u) v = lookup v u
+getU (Unifier u) v = lookup v u
+getU (UnifierError e) v = error e
-- | An infinite supply of distinct unification variables.
uvarSupply :: [UVar]
emptyUnifier = Unifier empty
-- | Types for which we know how to do unification.
-class Unifiable t where
+class Show t => Unifiable t where
-- | Turns a @UVar@ into a @t@
inject :: UVar -> t
-- | Instances must implement this; it is called by @(unify x y)@
-- only when both @(project x)@ and @(project y)@ are @Nothing@
- unify' :: t -> t -> Unifier t
+ unify' :: t -> t -> Unifier t
- -- | Returns a list of all @UVars@ occurring in @t@; duplicates are okay and resolution should not be performed.
+ -- | Returns a list of all @UVars@ occurring in @t@
occurrences :: t -> [UVar]
--- | Returns a list of all UVars occurring anywhere in t and any UVars which
--- occur in values unified therewith.
-resolve :: Unifiable t => Unifier t -> UVar -> [UVar]
-resolve (Unifier u) v | member v u = v:(concatMap (resolve (Unifier u)) $ occurrences $ u ! v)
- | otherwise = [v]
+ -- | @(replace vrep trep t)@ returns a copy of @t@ in which all occurrences of @vrep@ have been replaced by @trep@
+ replace :: UVar -> t -> t -> t
--- | The occurs check.
-occurs :: Unifiable t => Unifier t -> UVar -> t -> Bool
-occurs u v x = elem v $ concatMap (resolve u) (occurrences x)
+-- | Returns a copy of the @t@ argument in which all @UVar@
+-- occurrences have been replaced by fully-resolved @t@ values.
+resolve :: Unifiable t => Unifier t -> t -> t
+resolve (UnifierError e) _ = error e
+resolve (Unifier m) t = resolve' (toList m) t
+ where
+ resolve' [] t = t
+ resolve' ((uv,v):rest) t | Just uvt <- project t = if uvt == uv
+ then v -- we got this out of the unifier, so it must be fully resolved
+ else resolve' rest t
+ | otherwise = resolve' rest (replace uv v t)
-- | Given two unifiables, find their most general unifier.
unify :: Unifiable t => t -> t -> Unifier t
-unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2' = emptyUnifier
-unify v1 v2 | (Just v1') <- project v1 = if occurs emptyUnifier v1' v2
- then error "occurs check failed"
- else Unifier $ insert v1' v2 empty
-unify v1 v2 | (Just v2') <- project v2 = unify v2 v1
-unify v1 v2 | _ <- project v1, _ <- project v2 = unify' v1 v2
+unify v1 v2 | (Just v1') <- project v1, (Just v2') <- project v2, v1'==v2' = emptyUnifier
+unify v1 v2 | (Just v1') <- project v1 = if elem v1' (occurrences v2)
+ then UnifierError "occurs check failed in Unify.unify"
+ else Unifier $ insert v1' v2 empty
+unify v1 v2 | (Just v2') <- project v2 = unify v2 v1
+unify v1 v2 | _ <- project v1, _ <- project v2 = unify' v1 v2
-- | Merge two unifiers into a single unifier.
mergeU :: Unifiable t => Unifier t -> Unifier t -> Unifier t
-mergeU (Unifier u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k v) u' (toList u)
+mergeU ue@(UnifierError _) _ = ue
+mergeU (Unifier u) u' = foldr (\(k,v) -> \uacc -> mergeU' uacc k (resolve uacc v)) u' (toList u)
where
- mergeU' u@(Unifier m) v1 v2 | member v1 m = mergeU u $ unify (m ! v1) v2
- | occurs u v1 v2 = error "occurs check failed"
- | otherwise = Unifier $ insert v1 v2 m
+ mergeU' ue@(UnifierError _) _ _ = ue
+ mergeU' u@(Unifier m) v1 v2 | member v1 m = mergeU u $ unify (m ! v1) v2
+ | Just v2' <- project (resolve u v2), v2' == v1 = u
+ | elem v1 (occurrences v2) = UnifierError "occurs check failed in Unify.mergeU"
+ | otherwise = Unifier $ insert v1 v2 m
-- | Enumerates the unification variables, sorted by occurs-check.
sortU :: (Unifiable t, Eq t) => Unifier t -> [UVar]
-sortU u@(Unifier um) = reverse $ nub $ concatMap (resolve u) (keys um)
-
-
+sortU u@(Unifier um) = reverse $ nub $ concatMap (\k -> occurrences (um!k)) (keys um)
+sortU (UnifierError ue) = error ue
import qualified Type
import qualified TypeRep
import qualified DataCon
+import qualified DsMonad
+import qualified IOEnv
+import qualified TcRnTypes
import qualified TyCon
import qualified Coercion
import qualified Var
import Data.Bits ((.&.), shiftL, (.|.))
import Prelude ( (++), (+), (==), Show, show, (.), ($) )
import qualified Prelude
+import qualified HscTypes
import qualified GHC.Base
+import qualified CoreMonad
import qualified System.IO.Unsafe
getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
Variable mkExVar : Name -> CoreType -> CoreVar.
Extract Inlined Constant mkExVar => "Id.mkLocalId".
+Variable CoreM : Type -> Type.
+ Extract Constant CoreM "a" => "CoreMonad.CoreM".
+ Extraction Inline CoreM.
+Variable CoreMreturn : forall a, a -> CoreM a.
+ Extraction Implicit CoreMreturn [a].
+ Implicit Arguments CoreMreturn [[a]].
+ Extract Inlined Constant CoreMreturn => "Prelude.return".
+Variable CoreMbind : forall a b, CoreM a -> (a -> CoreM b) -> CoreM b.
+ Extraction Implicit CoreMbind [a b].
+ Implicit Arguments CoreMbind [[a] [b]].
+ Extract Inlined Constant CoreMbind => "(Prelude.>>=)".
+
Section core2proof.
Context (ce:@CoreExpr CoreVar).
Context (hetmet_brak : WeakExprVar).
Context (hetmet_esc : WeakExprVar).
- Context (hetmet_flatten : WeakExprVar).
- Context (hetmet_unflatten : WeakExprVar).
- Context (hetmet_flattened_id : WeakExprVar).
Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
(do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
- (hetmet_flatten : CoreVar)
- (hetmet_unflatten : CoreVar)
- (hetmet_flattened_id : CoreVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
- Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
- Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
- Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString cex)
(addErrorMessage ("HaskStrong...")
(if do_skolemize
then
- (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
+ (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun q => OK (weakExprToCoreExpr q))
else (if do_flatten
then
- (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
+ (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
End coqPassCoreToCore.
+ Notation "a >>= b" := (@CoreMbind _ _ a b).
+
Definition coqPassCoreToCore
- (do_flatten : bool)
- (do_skolemize : bool)
- (hetmet_brak : CoreVar)
- (hetmet_esc : CoreVar)
- (hetmet_flatten : CoreVar)
- (hetmet_unflatten : CoreVar)
- (hetmet_flattened_id : CoreVar)
+ (do_flatten : bool)
+ (do_skolemize : bool)
+ (dsLookupVar : string -> string -> CoreM CoreVar)
+ (dsLookupTyc : string -> string -> CoreM TyFun)
(uniqueSupply : UniqSupply)
- (lbinds:list (@CoreBind CoreVar))
- (hetmet_PGArrowTyCon : TyFun)
- (hetmet_PGArrow_unit_TyCon : TyFun)
- (hetmet_PGArrow_tensor_TyCon : TyFun)
- (hetmet_PGArrow_exponent_TyCon : TyFun)
- (hetmet_pga_id : CoreVar)
- (hetmet_pga_comp : CoreVar)
- (hetmet_pga_first : CoreVar)
- (hetmet_pga_second : CoreVar)
- (hetmet_pga_cancell : CoreVar)
- (hetmet_pga_cancelr : CoreVar)
- (hetmet_pga_uncancell : CoreVar)
- (hetmet_pga_uncancelr : CoreVar)
- (hetmet_pga_assoc : CoreVar)
- (hetmet_pga_unassoc : CoreVar)
- (hetmet_pga_copy : CoreVar)
- (hetmet_pga_drop : CoreVar)
- (hetmet_pga_swap : CoreVar)
- (hetmet_pga_applyl : CoreVar)
- (hetmet_pga_applyr : CoreVar)
- (hetmet_pga_curryl : CoreVar)
- (hetmet_pga_curryr : CoreVar)
- (hetmet_pga_loopl : CoreVar)
- (hetmet_pga_loopr : CoreVar)
- : list (@CoreBind CoreVar) :=
- coqPassCoreToCore'
+ (lbinds : list (@CoreBind CoreVar))
+ : CoreM (list (@CoreBind CoreVar)) :=
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+ dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
+ dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
+ dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
+ dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
+ dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
+ dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
+ dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
+ dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
+ dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
+ dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
+ dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
+ dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
+ dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
+ dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
+ 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 =>
+
+ CoreMreturn
+ (coqPassCoreToCore'
do_flatten
do_skolemize
hetmet_brak
hetmet_esc
- hetmet_flatten
- hetmet_unflatten
- hetmet_flattened_id
uniqueSupply
- hetmet_PGArrowTyCon
- hetmet_PGArrow_unit_TyCon
- hetmet_PGArrow_tensor_TyCon
+ hetmet_PGArrow
+ hetmet_PGArrow_unit
+ hetmet_PGArrow_tensor
(* hetmet_PGArrow_exponent_TyCon*)
hetmet_pga_id
hetmet_pga_comp
hetmet_pga_applyr
hetmet_pga_curryl
*)
-
+ )
.
End core2proof.
(*******************************************************************************)
- Context (hetmet_flatten : WeakExprVar).
- Context (hetmet_unflatten : WeakExprVar).
- Context (hetmet_id : WeakExprVar).
Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
(fun TV : Kind → Type => take_arg_types ○ t TV))))).
reflexivity.
unfold flatten_type.
- clear hetmet_flatten.
- clear hetmet_unflatten.
- clear hetmet_id.
clear gar.
set (t tv ite) as x.
admit.
rename l into g.
rename σ into l.
destruct l as [|ec lev]; simpl.
+ (*
destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
set (flatten_type (g wev)) as t.
set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
apply nd_rule.
apply q.
apply INil.
+ *)
unfold flatten_leveled_type. simpl.
apply nd_rule; rewrite globals_do_not_have_code_types.
apply RGlobal.
projects / coq-hetmet.git / commitdiff