Merge branch 'master' of http://git.megacz.com/coq-hetmet

Conflicts:
	src/Extraction-prefix.hs

diff --combined src/Extraction-prefix.hs
index ea7cabf,56322c9..fbe22cb
--- 1/src/Extraction-prefix.hs
--- 2/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@@ -35,6 -35,13 +35,6 @@@ import qualified GHC.Bas
  import qualified System.IO
  import qualified System.IO.Unsafe
  
 -{-  -- used for extracting strings WITHOUT the patch for Coq
 -bin2ascii =
 -  (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
 -     let f b i = if b then 1 `shiftL` i else 0
 -     in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
 --}
 -
  getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  getTyConTyVars tc =
    if TyCon.isFunTyCon tc
@@@ -51,17 -58,18 +51,17 @@@ cmpAlts (a1,_,_) (a2,_,_)         = Dat
  sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  
 --- 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
@@@ -77,6 -85,7 +77,6 @@@ nat2int (S x) = 1 + (nat2int x
  natToString :: Nat -> Prelude.String
  natToString n = show (nat2int n)
  
 --- only needs to sanitize characters which might appear in Haskell identifiers
  sanitizeForLatex :: Prelude.String -> Prelude.String
  sanitizeForLatex []      = []
  sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
@@@ -99,15 -108,10 +99,15 @@@ coreKindToKind k 
                   else if (Coercion.isArgTypeKind k)      then KindStar
                   else if (Coercion.isUbxTupleKind k)     then KindStar
                   else if (Coercion.isOpenTypeKind k)     then KindStar
 +--
 +-- The "subkinding" in GHC is not dealt with in System FC, and dealing
 +-- with it is not actually as simple as you'd think.
 +--
  --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
  --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
  --                 else if (Coercion.isArgTypeKind k)      then KindArgType
  --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
 +--
                   else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
                   else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
                   else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
@@@ -115,6 -119,10 +115,6 @@@
  outputableToString :: Outputable.Outputable a => a -> Prelude.String
  outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
  
 --- I'm leaving this here (commented out) in case I ever need it again)
 ---checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 ---checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
 -
  coreViewDeep :: Type.Type -> Type.Type
  coreViewDeep t =
      case t of
@@@ -130,30 -138,36 +130,36 @@@
                                 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)
@@@ -183,14 -197,3 +189,14 @@@ trace msg x = System.IO.Unsafe.unsafePe
  trace msg x = System.IO.Unsafe.unsafePerformIO $
                  (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
  -}
 +
 +{-  -- used for extracting strings WITHOUT the patch for Coq
 +bin2ascii =
 +  (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
 +     let f b i = if b then 1 `shiftL` i else 0
 +     in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
 +-}
 +
 +-- I'm leaving this here (commented out) in case I ever need it again)
 +--checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 +--checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)