(\ 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
-- 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"))
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
-- 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 =
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: "
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 =
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)
| 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)) :=
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 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".
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 }.
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.
| 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".
-(* 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
- | 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
- | 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
- | 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.
-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 }.