Require Import HaskWeakTypes.
Require Import HaskWeak.
-Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
-Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Variable getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType).
- Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
+ Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
(* extracts the Name from a CoreVar *)
Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+Variable hetmet_kappa_name : CoreName. Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name".
+Variable hetmet_kappa_app_name: CoreName.
+Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name".
Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
split_list lwt (length (fst (tyFunKind tf))) >>=
| _ => None
end.
+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))
| CoreELit lit => OK (WELit lit)
| 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"
+ | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
| CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
- let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co
+ let (ct1,ct2) := coercionKind co
in coreTypeToWeakType ct1 >>= fun t1 =>
coreTypeToWeakType ct2 >>= fun t2 =>
OK (WECast e' (WCoUnsafe t1 t2))
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
OK (WECSP v tv e' t')
- | None => coreExprToWeakExpr e1 >>= fun e1' =>
- match e2 with
- | CoreEType t =>
- coreTypeToWeakType t >>= fun t' =>
- OK (WETyApp e1' t')
- | _ => coreExprToWeakExpr e2
- >>= fun e2' => OK (WEApp e1' e2')
- end
- end
- end
+ | None =>
+ (*
+ if isKappa e1
+ then match e2 with
+ | CoreELam v e => match coreVarToWeakVar' v with
+ | OK (WExprVar ev) =>
+ coreExprToWeakExpr e >>= fun e' =>
+ OK (WEKappa ev e')
+ | _ => Error "bogus"
+ end
+ | _ => Error "bogus"
+ end
+ else if isKappaApp e1
+ then match e1 with
+ | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
+ coreExprToWeakExpr e1' >>= fun e1'' =>
+ coreExprToWeakExpr e2 >>= fun e2'' =>
+ OK (WEKappaApp e1'' e2'')
+ | _ => Error "bogus"
+ end
+ else
+ *)
+ coreExprToWeakExpr e1 >>= fun e1' =>
+ match e2 with
+ | CoreEType t =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WETyApp e1' t')
+ | _ => coreExprToWeakExpr e2
+ >>= fun e2' => OK (WEApp e1' e2')
+ end
+ end
+ end
end
| CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with