Require Import HaskWeakTypes.
Require Import HaskWeak.
-Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon).
-Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
+ Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
+
+(* extracts the Name from a CoreVar *)
+Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
+
+(* the magic wired-in name for the modal type introduction/elimination forms *)
+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".
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
match ct with
| 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
| PredTy (EqPred _ _) => Error "hit a bare EqPred"
end.
-Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
+Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
end else None
| _ => None
end.
+
Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
| _ => None
end.
-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) : ??(CoreVar * 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 => Some (v,tv,tbody)
+ | 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: " +++ wt)
+ | _ => Error ("expectTyConApp encountered " +++ wt)
+ end.
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)
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
OK (WEEsc 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
+ | None => match isCSP e1 with
+ | Some (v,tv,t) =>
+ 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
end
| 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' =>
- (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
- >>= fun tca =>
+ coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
+ coreExprToWeakExpr e >>= fun e' =>
+ 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)) :=
projects / coq-hetmet.git / blobdiff