fallback plan: turn all CoreSyn coercions into unsafeCoerce

diff --git a/examples/tutorial.hs b/examples/tutorial.hs
index 6ef4cbd..7668eab 100644 (file)
--- a/examples/tutorial.hs
+++ b/examples/tutorial.hs
@@ -441,7 +441,12 @@ staged_accept (Const c) k        =
 --------------------------------------------------------------------------------
 -- Unflattening
 
-{-
+-- The current implementation has problems with literals at level>0;
+-- there are special-purpose hacks for Int and Char, but none for
+-- unit.  So I use this instead as a placeholder for <[ () ]>
+
+<[ u ]> = Prelude.error "FIXME"
+
 -- This more or less "undoes" the flatten function.  People often ask
 -- me how you "translate generalized arrows back into multi-level
 -- terms".. I'm not sure why you'd want to do that, but this is how:
@@ -457,11 +462,10 @@ instance GArrow Code (,) () where
   ga_cancell     = Code <[ \(_,x) -> x ]>
 
   ga_cancelr     = Code <[ \(x,_) -> x ]>
-  ga_uncancell   = Code <[ \x -> (%%(),x) ]>
-  ga_uncancelr   = Code <[ \x -> (x,%%()) ]>
+  ga_uncancell   = Code <[ \x -> (u,x) ]>
+  ga_uncancelr   = Code <[ \x -> (x,u) ]>
   ga_assoc       = Code <[ \((x,y),z) -> (x,(y,z)) ]>
   ga_unassoc     = Code <[ \(x,(y,z)) -> ((x,y),z) ]>
--}
 
 
 
@@ -496,14 +500,10 @@ instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
   ga_unassoc     = GArrowInversePair { forward = ga_unassoc           , backward = ga_assoc     }
 instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
   ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
-{-
-instance (GArrowDrop g (**) u, GArrowCopy g (**) u) => GArrowCopy (GArrowInversePair g (**) u) (**) u where
-  ga_copy = GArrowInversePair { forward = ga_copy , backward = ga_second ga_drop >>> ga_cancelr }
--}
 -- but notice that we can't (in general) get
 -- instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
 
-{-
+
 -- For that, we need PreLenses, which "log the history" where necessary.
 -- I call this a "PreLens" because it consists of the data required
 -- for a Lens (as in BCPierce's Lenses) but does not necessarily
@@ -515,7 +515,7 @@ instance Category PreLens where
   id    = PreLens { preLens = \x -> (x, (\x -> x)) }
   f . g = PreLens { preLens = \x -> let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q -> g' (f' q)) }
 
-instance GArrow PreLens (,) where
+instance GArrow PreLens (,) () where
   ga_first     f = PreLens { preLens = \(x,z) -> let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) -> (f' q1,q2))) }
   ga_second    f = PreLens { preLens = \(z,x) -> let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) -> (q1,f' q2))) }
   ga_cancell     = PreLens { preLens = \(_,x) -> (x,            (\x -> ((),x))) }
@@ -525,25 +525,25 @@ instance GArrow PreLens (,) where
   ga_assoc       = PreLens { preLens = \((x,y),z) -> ( (x,(y,z)) , (\(x,(y,z)) -> ((x,y),z)) ) }
   ga_unassoc     = PreLens { preLens = \(x,(y,z)) -> ( ((x,y),z) , (\((x,y),z) -> (x,(y,z))) ) }
 
-instance GArrowDrop PreLens (,) where
+instance GArrowDrop PreLens (,) () where
   ga_drop        = PreLens { preLens = \x     -> (()    , (\() -> x)) }
-instance GArrowCopy PreLens (,) where
+instance GArrowCopy PreLens (,) () where
   ga_copy        = PreLens { preLens = \x     -> ((x,x) , fst) }
-instance GArrowSwap PreLens (,) where
+instance GArrowSwap PreLens (,) () where
   ga_swap        = PreLens { preLens = \(x,y) -> ((y,x) , (\(z,q) -> (q,z))) }
 
 
 
 data Lens x y where
   Lens :: forall x y c1 c2 . ((x,c1)->(y,c2)) -> ((y,c2)->(x,c1)) -> Lens x y
-
+{-
 -- can we make lenses out of GArrows other than (->)?
 instance Category Lens where
   id                          = Lens (\x -> x) (\x -> x)
   (Lens g1 g2) . (Lens f1 f2) = Lens (\(x,(c1,c2)) -> let (y,fc) = f1 (x,c1) in  let (z,gc) = g1 (y,c2) in  (z,(fc,gc)))
                                      (\(z,(c1,c2)) -> let (y,gc) = g2 (z,c2) in  let (x,fc) = f2 (y,c1) in  (x,(fc,gc)))
 
-instance GArrow Lens (,) where
+instance GArrow Lens (,) () where
   ga_first     (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x1,c) in ((y,x2),c'))
                                    (\((x1,x2),c) -> let (y,c') = f2 (x1,c) in ((y,x2),c'))
   ga_second    (Lens f1 f2) = Lens (\((x1,x2),c) -> let (y,c') = f1 (x2,c) in ((x1,y),c'))
@@ -561,20 +561,19 @@ instance GArrow Lens (,) where
   ga_unassoc                = Lens (\((x,(y,z)),()) -> (((x,y),z),()))
                                    (\(((x,y),z),()) -> ((x,(y,z)),()))
 
-instance GArrowDrop Lens (,) where
+instance GArrowDrop Lens (,) () where
   ga_drop        = Lens (\(x,()) -> ((),x)) (\((),x) -> (x,()))
-instance GArrowCopy Lens (,) where
+instance GArrowCopy Lens (,) () where
   ga_copy        = Lens (\(x,()) -> ((x,x),())) (\((x,_),()) -> (x,()))
-instance GArrowSwap Lens (,) where
+instance GArrowSwap Lens (,) () where
   ga_swap        = Lens (\((x,y),()) -> ((y,x),())) (\((x,y),()) -> ((y,x),()))
 
-instance BiGArrow Lens (,) where
+instance BiGArrow Lens (,) () where
   biga_arr f f'  = Lens (\(x,()) -> ((f x),())) (\(x,()) -> ((f' x),()))
   biga_inv (Lens f1 f2) = Lens f2 f1
 -}
 
 
-
 --------------------------------------------------------------------------------
 -- An example generalized arrow
 

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 3179cdb..56322c9 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -61,15 +61,15 @@ sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT e
 -- to do: this could be moved into Coq
 coreVarToWeakVar :: Var.Var -> WeakVar
 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
- where
-  errOrFail (OK x)    = x
-  errOrFail (Error s) = Prelude.error s
 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") 
                                                              (Prelude.error "FIXME") (Prelude.error "FIXME"))
 coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 
+errOrFail (OK x)    = x
+errOrFail (Error s) = Prelude.error s
+
 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
 tyConOrTyFun n =
    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
@@ -138,30 +138,36 @@ coreViewDeep t =
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 
--- FIXME: cotycon applications may be oversaturated
 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 coreCoercionToWeakCoercion c =
+ WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
+   where
+    (t1,t2) = Coercion.coercionKind c
+{-
+-- REMEMBER: cotycon applications may be oversaturated
  case c of
   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
   TypeRep.TyConApp tc t  ->
       case TyCon.isCoercionTyCon_maybe tc of
-        Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+        Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
         Prelude.Just (_, ctcd) ->
             case (ctcd,t) of
               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
--- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
+--            (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
---              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+              (TyCon.CoAxiom _ _ _ , _   ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+              ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+-}
 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)