minor cleanups, deleted dead code, eliminated use of (==) on CoreType

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 558d0ab..5a657bc 100644 (file)
--- 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))
   (\ 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 :: 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
 
 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))))
 -- 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 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
    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
 
 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
 
 -- 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 ('_':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 =
 
 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
       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: "
                  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))
 
 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 =
 
 coreViewDeep :: Type.Type -> Type.Type
 coreViewDeep t =

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1cbaf22..63c7e95 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -107,6 +107,15 @@ Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
           OK (WCoUnsafe t1' t2').
 *)
 
           OK (WCoUnsafe t1' t2').
 *)
 

+(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
+Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
+  match wt with
+    | WTyCon tc        => OK (tc,acc)
+    | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
+    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
+    | _                => Error ("expectTyConApp encountered " +++ wt)
+  end.
+

 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)

@@ -178,8 +187,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
         coreExprToWeakExpr e >>= fun e' =>
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
         coreExprToWeakExpr e >>= fun e' =>

-          (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
-             >>= fun tca =>
+          expectTyConApp te' nil >>= fun tca =>

             let (tc,lt) := tca in
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
             let (tc,lt) := tca in
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index ea4a02a..5c4ce6e 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -40,11 +40,11 @@ Extract Inductive CoreType =>
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 

-Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "showType".

 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".

-Variable kindOfCoreType    : CoreType -> Kind.    Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
+Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
+Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".

 
 (* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
 Variable TyCon           : Type.                         Extract Inlined Constant TyCon             => "TyCon.TyCon".
 
 (* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
 Variable TyCon           : Type.                         Extract Inlined Constant TyCon             => "TyCon.TyCon".

@@ -56,8 +56,6 @@ Variable tyCon_eq            : EqDecider TyCon.           Extract Inlined Consta
 Variable tyFun_eq            : EqDecider TyFun.           Extract Inlined Constant tyFun_eq              => "(==)".
 Variable dataCon_eq          : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
 Variable coreName_eq         : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".
 Variable tyFun_eq            : EqDecider TyFun.           Extract Inlined Constant tyFun_eq              => "(==)".
 Variable dataCon_eq          : EqDecider CoreDataCon.     Extract Inlined Constant dataCon_eq            => "(==)".
 Variable coreName_eq         : EqDecider CoreName.        Extract Inlined Constant coreName_eq           => "(==)".

-Variable coretype_eq_dec     : EqDecider CoreType.        Extract Inlined Constant coretype_eq_dec       => "checkTypeEquality".
-Instance CoreTypeEqDecidable : EqDecidable CoreType    := { eqd_dec := coretype_eq_dec }.

 Instance CoreTyConEqDecidable: EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
 Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
 Instance TyFunEqDecidable    : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.
 Instance CoreTyConEqDecidable: EqDecidable CoreTyCon   := { eqd_dec := coreTyCon_eq }.
 Instance TyConEqDecidable    : EqDecidable TyCon       := { eqd_dec := tyCon_eq }.
 Instance TyFunEqDecidable    : EqDecidable TyFun       := { eqd_dec := tyFun_eq }.

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index cdbc9e7..8f55346 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -12,7 +12,6 @@ Require Import HaskCoreLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 

-(* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *)

 Variable tyConToCoreTyCon : TyCon -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
 Variable tyConToCoreTyCon : TyCon -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.

@@ -88,61 +87,28 @@ match wc with
 | WCoUnsafe  t1 t2                   => (t1,t2)
 end.
 
 | WCoUnsafe  t1 t2                   => (t1,t2)
 end.
 

-(* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)

 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
 
 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
 

-(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
-Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) :=
-  match wt with
-    | WTyCon tc    => Some (tc,acc)
-    | WAppTy t1 t2 => isTyConApp t1 (t2::acc)
-    | _            => None
-  end.
-
-(* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *)
-Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
-
-Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
+Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=

   match wt with
     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
   match wt with
     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v

-    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
-    | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
-                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
-                                           | t1'             => AppTy t1' (weakTypeToCoreType' t2)
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
+    | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
+                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
+                                           | t1'             => AppTy t1' (weakTypeToCoreType t2)

                                          end
     | WTyCon    tc                    => TyConApp tc nil
                                          end
     | WTyCon    tc                    => TyConApp tc nil

-    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType' lt)
-    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType' lt))
-    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType' ty))
-    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t)
+    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
+    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
+    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
+    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)

     | WFunTyCon                       => TyConApp ArrowTyCon nil
     | WFunTyCon                       => TyConApp ArrowTyCon nil

-    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil)
-    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)))
-                                            (weakTypeToCoreType' t3)
+    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
+    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
+                                            (weakTypeToCoreType t3)

   end.
 
   end.
 

-Definition weakTypeToCoreType (wt:WeakType) :=
-  weakTypeToCoreType' (normalizeWeakType wt).
-
-Definition compare_weakTypes (w1 w2:WeakType) :=
-  if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
-    then true
-    else false.
-
-(*
-Instance EqDecidableWeakType : EqDecidable WeakType.
-  apply Build_EqDecidable.
-  intros.
-  set (compare_weakTypes_axiom v1 v2) as x.
-  set (compare_weakTypes v1 v2) as y.
-  assert (y=compare_weakTypes v1 v2). reflexivity.
-  destruct y; rewrite <- H in x.
-  left; auto.
-  right; auto.
-  Defined.
-*)
-

 Instance WeakTypeToString : ToString WeakType :=
   { toString := coreTypeToString ○ weakTypeToCoreType }.
 
 Instance WeakTypeToString : ToString WeakType :=
   { toString := coreTypeToString ○ weakTypeToCoreType }.