X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=4abbf69a35de08723f9ef1a679d07dc8e7f8c1be;hp=68c40e5ddde382f8d29722708a3caabc20918be3;hb=6232ffa2805211654c6ff40a9852d7fc312382d2;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 68c40e5..4abbf69 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,18 +1,7 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
-module Extraction ( coqCoreToStringPass )
+module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
---import HsSyn
---import TcType
---import CoreFVs
---import CoreUtils
---import MkCore
---import Var
---import BasicTypes
---import Bag
---import VarSet
---import SrcLoc
---import Data.List
-
+import qualified MkCore
 import qualified TysWiredIn
 import qualified TysPrim
 import qualified Outputable
@@ -32,17 +21,51 @@ import qualified DataCon
 import qualified CoreSyn
 import qualified Class
 import qualified Data.Char 
-
 import Data.Bits ((.&.), shiftL, (.|.))
 import Prelude ( (++), (+), (==), Show, show, Char )
+import qualified Prelude
+import qualified GHC.Base
+
+-- used for extracting strings
+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
+
+-- 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)))
+coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME"))
+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)
 
-{-
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 nat2int (S x) = 1 + (nat2int x)
 
-nat2string :: Nat -> Prelude.String
-nat2string n = show (nat2int n)
+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
@@ -66,12 +89,27 @@ coreKindToKind k =
                  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: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))
-coreVarSort :: Var.Var -> CoreVarSort
-coreVarSort v | Id.isId     v = CoreExprVar (Var.varType{-AsType-} v)
-coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v))
-coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v)
-coreVarSort v | otherwise     = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
-
-outputableToString :: Outputable -> String
+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)
+
+coreViewDeep :: Type.Type -> Type.Type
+coreViewDeep t =
+    case t of
+      TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
+      TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
+      TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
+      TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
+      TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
+                        in case Type.coreView t' of
+                               Prelude.Nothing     -> t'
+                               Prelude.Just    t'' -> t''
+      TypeRep.PredTy p         -> case Type.coreView t of
+                               Prelude.Nothing     -> TypeRep.PredTy p
+                               Prelude.Just    t'  -> t'