-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
- let (t1,t2) := coreCoercionKind cc
- in coreTypeToWeakType t1 >>= fun t1' =>
- coreTypeToWeakType t2 >>= fun t2' =>
- OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
+Definition isKappa (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3))
+ => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
+Definition isKappaApp (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3)) _)
+ => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
+ match coreVarToWeakVar' ec with
+ | OK (WTypeVar tv) => match coreVarToWeakVar' v with
+ | OK (WExprVar v') => Some (v',tv,tbody)
+ | _ => None
+ end
+ | _ => None
+ end else None
+ | _ => None
+end.
+
+(* 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: " +++ toString wt)
+ | _ => Error ("expectTyConApp encountered " +++ toString wt)
+ end.
+
+(* expects to see an EType with a coercion payload *)
+Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion :=
+ match ce with
+ | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2)
+ | _ => Error ("coreExprToWeakCoercion got a " +++ toString ce)
+ end.
+
+(* expects to see an EType *)
+Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType :=
+ match ce with
+ | CoreEType t => coreTypeToWeakType t
+ | _ => Error ("coreExprToWeakType got a " +++ toString ce)
+ end.