import qualified BasicTypes
import qualified DataCon
import qualified CoreSyn
+import qualified CoreUtils
import qualified Class
import qualified Data.Char
+import qualified Data.Typeable
import Data.Bits ((.&.), shiftL, (.|.))
-import Prelude ( (++), (+), (==), Show, show, Char )
+import Prelude ( (++), (+), (==), Show, show, Char, (.) )
import qualified Prelude
import qualified GHC.Base
getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
+sortAlts :: [(CoreSyn.AltCon,a,b)] -> [(CoreSyn.AltCon,a,b)]
+sortAlts x = x -- FIXME
+
-- 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 v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
+ (Prelude.error "FIXME") (Prelude.error "FIXME"))
coreVarToWeakVar _ =
Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
case Coercion.splitKindFunTy_maybe k of
Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
Prelude.Nothing ->
- if (Coercion.isLiftedTypeKind k) then KindType
+ 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
TypeRep.PredTy p -> case Type.coreView t of
Prelude.Nothing -> TypeRep.PredTy p
Prelude.Just t' -> t'
+
+-- FIXME: cotycon applications may be oversaturated
+coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
+coreCoercionToWeakCoercion c =
+ 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 " (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)
+-- FIXME (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)"
+ _ -> 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)
+-}
\ No newline at end of file
Require Import HaskWeakVars.
Require Import HaskWeakTypes.
Require Import HaskWeak.
-Require Import HaskWeakToCore.
Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon).
Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
- | _ => Error "mis-applied modal box tycon"
+ | _ => Error ("mis-applied modal box tycon: " +++ ct)
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
-Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
- coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
-
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
match ce with
| _ => None
end.
-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
+Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
+ Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
+(*
let (t1,t2) := coreCoercionKind cc
in coreTypeToWeakType t1 >>= fun t1' =>
- coreTypeToWeakType t2 >>= fun t2' =>
- OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
+ coreTypeToWeakType t2 >>= fun t2' =>
+ OK (WCoUnsafe t1' t2').
+*)
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
match ce with
| 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"
| CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
- coreCoercionToWeakCoercion co >>= fun co' =>
- OK (WECast e' co')
+ OK (WECast e' (coreCoercionToWeakCoercion co))
| CoreEVar v => match coreVarToWeakVar v with
| WExprVar ev => OK (WEVar ev)
| WTypeVar _ => Error "found a type variable in a case"
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
- coreExprToWeakExpr e >>= fun e' =>
- weakTypeOfWeakExpr e' >>= fun te' =>
+ 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 =>
let (tc,lt) := tca in
Require Import HaskCoreVars.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
+Require Import HaskWeak.
Require Import HaskCoreToWeak.
Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Require Import HaskWeakVars.
Require Import HaskWeakTypes.
Require Import HaskWeak.
+Require Import HaskCoreToWeak.
Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
Extract Inlined Constant sortAlts => "sortAlts".
Implicit Arguments sortAlts [[a][b]].
-Variable trustMeCoercion : CoreCoercion.
- Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
+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 weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
- fun _ => trustMeCoercion.
-
+ Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+ mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
match me with
(weakExprToCoreExpr e)
end.
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+ coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
Instance weakExprToString : ToString WeakExpr :=
{ toString := fun we => toString (weakExprToCoreExpr we) }.
-
Require Import HaskStrong.
Require Import HaskCoreTypes.
Require Import HaskCoreVars.
-Require Import HaskCoreToWeak.
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
- | WECast e co => let (_,t1,t2,_) := co in
+ | WECast e co => let (t1,t2) := weakCoercionTypes co in
weakTypeToType'' φ t1 ★ >>= fun t1' =>
weakTypeToType'' φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
right; intro; apply n; inversion H; subst; auto.
Defined.
+(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
+
+Inductive WeakCoercion : Type :=
+| WCoVar : WeakCoerVar -> WeakCoercion (* g *)
+| WCoType : WeakType -> WeakCoercion (* τ *)
+| WCoApp : WeakCoercion -> WeakCoercion -> WeakCoercion (* γ γ *)
+| WCoAppT : WeakCoercion -> WeakType -> WeakCoercion (* γ@v *)
+| WCoAll : Kind -> (WeakTypeVar -> WeakCoercion) -> WeakCoercion (* ∀a:κ.γ *)
+| WCoSym : WeakCoercion -> WeakCoercion (* sym *)
+| WCoComp : WeakCoercion -> WeakCoercion -> WeakCoercion (* ◯ *)
+| WCoLeft : WeakCoercion -> WeakCoercion (* left *)
+| WCoRight : WeakCoercion -> WeakCoercion (* right *)
+| WCoUnsafe : WeakType -> WeakType -> WeakCoercion (* unsafe *)
+(*| WCoCFApp : ∀ n, CoFunConst n -> vec WeakCoercion n -> WeakCoercion (* C γⁿ *)*)
+(*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*)
+.
+
+Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
+Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
+match wc with
+| 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)
+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".
Require Import HaskCoreTypes.
Require Import HaskWeakTypes.
-(* TO DO: finish this *)
-Inductive WeakCoercion : Type := weakCoercion : Kind -> WeakType -> WeakType -> CoreCoercion -> WeakCoercion.
-
-(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
-Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
-
(* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.
projects / coq-hetmet.git / commitdiff