From: Adam Megacz Date: Mon, 28 Mar 2011 00:20:22 +0000 (-0700) Subject: Merge branch 'master' of http://git.megacz.com/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=ddac2a6a7301788326cd9107965e59fc0804daad;hp=-c Merge branch 'master' of git.megacz.com/coq-hetmet Conflicts: src/Extraction-prefix.hs --- ddac2a6a7301788326cd9107965e59fc0804daad diff --combined src/Extraction-prefix.hs index ea7cabf,56322c9..fbe22cb --- a/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)