X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=5a657bc26ffce107a3a7b7f209b8e09dfe86f6b1;hp=558d0aba3ac00f35ac7c02d63eb45e32e3d7c4ac;hb=635ee434c9edbad1bc6c9bf5ba2b91cb8c51be8e;hpb=f49db0fc38c6c430585e4e48304510212c3f1a0f

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 558d0ab..5a657bc 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -35,18 +35,14 @@ 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))
---bin2ascii' =
---  (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
---shiftAscii =
---  \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
-
--- crude way of casting Coq "error monad" into Haskell exceptions
-errOrFail :: OrError a -> a
-errOrFail (OK x)    = x
-errOrFail (Error s) = Prelude.error s
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
-getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
+getTyConTyVars tc =
+  if TyCon.isFunTyCon tc
+  then []
+  else if TyCon.isPrimTyCon tc
+       then []
+       else TyCon.tyConTyVars tc
 
 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
 sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x
@@ -54,6 +50,9 @@ sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2)
 -- 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"))
@@ -61,12 +60,12 @@ coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 
 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
---FIXME: go back to this
---tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
-tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
-
-tyFunResultKind :: TyCon.TyCon -> Kind
-tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
+tyConOrTyFun n =
+   if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
+   then Prelude.Right n
+   else if TyCon.isFamInstTyCon n
+        then Prelude.Right n
+        else Prelude.Left n
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
@@ -77,11 +76,11 @@ natToString n = show (nat2int n)
 
 -- only needs to sanitize characters which might appear in Haskell identifiers
 sanitizeForLatex :: Prelude.String -> Prelude.String
-sanitizeForLatex []    = []
+sanitizeForLatex []      = []
 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
-sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
+sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
 
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
@@ -89,10 +88,14 @@ coreKindToKind k =
       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
       Prelude.Nothing -> 
                       if (Coercion.isLiftedTypeKind k)   then KindType
-                 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.isUnliftedTypeKind k) then KindType
+                 else if (Coercion.isArgTypeKind k)      then KindType
+                 else if (Coercion.isUbxTupleKind k)     then KindType
+                 else if (Coercion.isOpenTypeKind k)     then KindType
+--                 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: "
@@ -100,12 +103,9 @@ coreKindToKind k =
 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 
--- TO DO: I think we can remove this now
-checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
-checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
-
---showType t = outputableToString (Type.expandTypeSynonyms t)
-showType t = outputableToString (coreViewDeep t)
+-- 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 =