-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 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
+ | WExprVar _ => None
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
+ | WCoerVar _ => 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.