X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=fbe22cb074eb5d340efd28a5d282c999f991d858;hp=56322c94441954b9e48329125ea5fdcaf25f314d;hb=ddac2a6a7301788326cd9107965e59fc0804daad;hpb=e2be3300379a5c0e1397c33f7b983a5259c5f51b

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 56322c9..fbe22cb 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -35,13 +35,6 @@ import qualified GHC.Base
 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
@@ -58,7 +51,6 @@ cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
 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))))
 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
@@ -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)
@@ -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: "
@@ -119,10 +115,6 @@ coreKindToKind k =
 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
@@ -197,3 +189,14 @@ trace msg x = System.IO.Unsafe.unsafePerformIO $
 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)