update for new GHC coercion representation

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 7fb0160..09f4b34 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -2,6 +2,7 @@
 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
 import qualified Unique
+import qualified Kind
 import qualified UniqSupply
 import qualified MkCore
 import qualified TysWiredIn
@@ -18,6 +19,7 @@ import qualified TyCon
 import qualified Coercion
 import qualified Var
 import qualified Id
+import qualified Pair
 import qualified FastString
 import qualified BasicTypes
 import qualified DataCon
@@ -53,8 +55,7 @@ sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT e
 coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
 coreVarToWeakVar v | Id.isId     v = CVTWVR_EVar  (Var.varType v)
 coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
-coreVarToWeakVar v | Var.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coercionKind (Var.varType v)))
-                                                  (Prelude.snd (Coercion.coercionKind (Var.varType v)))
+coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
 coreVarToWeakVar _                 = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
 
 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
@@ -88,21 +89,21 @@ sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
 
 kindToCoreKind :: Kind -> TypeRep.Kind
-kindToCoreKind KindStar          = TypeRep.liftedTypeKind
-kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
+kindToCoreKind KindStar          = Kind.liftedTypeKind
+kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
 kindToCoreKind k                 = Prelude.error ((Prelude.++)
                                                     "kindToCoreKind does not know how to handle kind "
                                                                                (kindToString k))
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
-  case Coercion.splitKindFunTy_maybe k of
+  case Kind.splitKindFunTy_maybe k of
       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
       Prelude.Nothing -> 
-                      if (Coercion.isLiftedTypeKind k)   then KindStar
-                 else if (Coercion.isUnliftedTypeKind k) then KindStar
-                 else if (Coercion.isArgTypeKind k)      then KindStar
-                 else if (Coercion.isUbxTupleKind k)     then KindStar
-                 else if (Coercion.isOpenTypeKind k)     then KindStar
+                      if (Kind.isLiftedTypeKind k)   then KindStar
+                 else if (Kind.isUnliftedTypeKind k) then KindStar
+                 else if (Kind.isArgTypeKind k)      then KindStar
+                 else if (Kind.isUbxTupleKind k)     then KindStar
+                 else if (Kind.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.
@@ -112,8 +113,7 @@ coreKindToKind k =
 --                 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 if (Kind.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 outputableToString :: Outputable.Outputable a => a -> Prelude.String
@@ -134,52 +134,6 @@ coreViewDeep t =
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 
-getSourceAndTargetTypesOfCoercion :: Type.Type -> (Type.Type,Type.Type)
-getSourceAndTargetTypesOfCoercion c = Coercion.coercionKind (Coercion.typeKind 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 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)
---            (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)"
-              ( _, [ 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)
-
-{-
-weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
-| WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
-| WCoType    t                       => Prelude_error "FIXME WCoType"
-| WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
-| WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
-| WCoAll     k f                     => Prelude_error "FIXME WCoAll"
-| WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
-| WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
-| WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
-| WCoRight   c                       => Prelude_error "FIXME WCoRight"
-| WCoUnsafe  t1 t2                   => (t1,t2)
--}
-
 {-# NOINLINE trace #-}
 trace :: Prelude.String -> a -> a
 trace msg x = x
@@ -193,14 +147,6 @@ trace msg x = x
 --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)

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2e51d0e..d70cd58 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -71,7 +71,7 @@ Variable mkSystemName : Unique -> string -> nat -> Name.
 Variable mkTyVar : Name -> Kind -> CoreVar.
   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
-  Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
+  Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))".
 Variable mkExVar : Name -> CoreType -> CoreVar.
   Extract Inlined Constant mkExVar => "Id.mkLocalId".
 

diff --git a/src/HaskCore.v b/src/HaskCore.v
index b05c34f..13a263e 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -23,6 +23,7 @@ Inductive CoreExpr {b:Type} :=
 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
 | CoreEType  : CoreType                         -> CoreExpr
+| CoreECoercion : CoreCoercion                  -> CoreExpr
 with      CoreBind {b:Type} :=
 | CoreNonRec : b -> CoreExpr         -> CoreBind  
 | CoreRec    : list (b * CoreExpr  ) -> CoreBind.
@@ -36,7 +37,9 @@ Extract Inductive CoreExpr =>
       "CoreSyn.Case"
       "CoreSyn.Cast"
       "CoreSyn.Note"
-      "CoreSyn.Type" ].
+      "CoreSyn.Type"
+      "CoreSyn.Coercion"
+   ].
 Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
 

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 673b999..7669e5d 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -16,10 +16,10 @@ Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 
-Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
-Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Variable getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType).
-  Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun.          Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType  -> CoreType.                 Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
+   Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
 
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
@@ -188,8 +188,9 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
     | CoreELit   lit   => OK (WELit lit)
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
+    | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
-                            let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co
+                            let (ct1,ct2) := coercionKind co
                              in coreTypeToWeakType ct1 >>= fun t1 =>
                                   coreTypeToWeakType ct2 >>= fun t2 =>
                                     OK (WECast e' (WCoUnsafe t1 t2))

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 4babf36..79ab342 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -12,7 +12,9 @@ Require Import HaskCoreVars.
 Require Import HaskLiterals.
 Require Import HaskTyCons.
 
-Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
+Variable CoreCoercionCoAxiom : Type.  Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom".
+Variable Int : Type.                  Extract Inlined Constant Int => "Prelude.Int".
+
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
 Variable coreTyConToString   : CoreTyCon   -> string.     Extract Inlined Constant coreTyConToString     => "outputableToString".
 Variable coreDataConToString : CoreDataCon -> string.     Extract Inlined Constant coreDataConToString   => "outputableToString".
@@ -34,11 +36,38 @@ Extract Inductive CoreType =>
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
+Inductive CoreCoercion : Type :=
+    CoreCoercionRefl        : CoreType                                 -> CoreCoercion
+  | CoreCoercionTyConAppCo  : CoreTyCon    -> list CoreCoercion        -> CoreCoercion
+  | CoreCoercionAppCo       : CoreCoercion -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionForAllCo    : CoreVar      -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionCoVarCo     : CoreVar                                  -> CoreCoercion
+  | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion
+  | CoreCoercionUnsafeCo    : CoreType -> CoreType                     -> CoreCoercion
+  | CoreCoercionSymCo       : CoreCoercion                             -> CoreCoercion
+  | CoreCoercionTransCo     : CoreCoercion -> CoreCoercion             -> CoreCoercion
+  | CoreCoercionNthCo       : Int -> CoreCoercion                      -> CoreCoercion
+  | CoreCoercionInstCo      : CoreCoercion -> CoreType                 -> CoreCoercion.
+
+Extract Inductive CoreCoercion =>
+  "Coercion.Coercion" [
+  "Coercion.Refl"
+  "Coercion.TyConAppCo"
+  "Coercion.AppCo"
+  "Coercion.ForAllCo"
+  "Coercion.CoVarCo"
+  "Coercion.AxiomInstCo"
+  "Coercion.UnsafeCo"
+  "Coercion.SymCo"
+  "Coercion.TransCo"
+  "Coercion.NthCo"
+  "Coercion.InstCo" ].
+
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 Variable coreCoercionKind : Kind -> CoreType*CoreType.
   Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
-Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
+Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Kind.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
 Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".
 

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 60e84b6..e5a10ba 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -19,7 +19,7 @@ Require Import HaskCoreToWeak.
 
 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
 Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Constant dataConExVars_    => "DataCon.dataConExTyVars".
-Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
+Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
 Definition dataConExTyVars cdc :=

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 8ceb0b7..c3e90a4 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -25,13 +25,6 @@ Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@trip
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
-Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
-    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
-
-(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
-Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
-  Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-
 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
   match wa with
   | WeakDataAlt cdc => DataAlt cdc
@@ -59,7 +52,7 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
   end.
 
 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
-  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+  CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
@@ -67,8 +60,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   | WELit   lit                          => CoreELit  lit
   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
-                                                           (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
+  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co))
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )