Require Import HaskWeakTypes.
Require Import HaskWeak.
-(* this distinguishes SystemFC "type functions" (true) which are always fully applied from "type constructors" which aren't *)
-Variable isFamilyTyCon : TyCon -> bool. Extract Inlined Constant isFamilyTyCon => "TyCon.isFamilyTyCon".
-
-
Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon).
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
-Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
-
-Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType :=
+Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
match ct with
| TyVarTy cv => match coreVarToWeakVar cv with
| WExprVar _ => Error "encountered expression variable in a type"
| WCoerVar _ => Error "encountered coercion variable in a type"
end
- | AppTy t1 t2 => coreTypeToWeakType t2 >>= fun t2' => coreTypeToWeakType t1 >>= fun t1' => OK (WAppTy t1' t2')
+ | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
- | TyConApp tc lct =>
+ | TyConApp tc_ lct =>
let recurse := ((fix rec tl := match tl with
| nil => OK nil
- | a::b => coreTypeToWeakType a >>= fun a' => rec b >>= fun b' => OK (a'::b')
+ | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
end) lct)
- in if (isFamilyTyCon tc)
- then recurse >>= fun recurse' => OK (WTyFunApp tc recurse')
- else if eqd_dec tc ModalBoxTyCon
- then match lct with
- | ((TyVarTy ec)::tbody::nil) =>
- match coreVarToWeakVar ec with
- | WTypeVar ec' => coreTypeToWeakType tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
- | 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"
- end
- else let tc' := if eqd_dec tc ArrowTyCon
- then WFunTyCon
- else WTyCon tc
- in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
- | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType t1 >>= fun t1' =>
- coreTypeToWeakType t2 >>= fun t2' =>
- coreTypeToWeakType t3 >>= fun t3' =>
+ in match tyConOrTyFun tc_ with
+ | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
+ | inl tc => if eqd_dec tc ModalBoxTyCon
+ then match lct with
+ | ((TyVarTy ec)::tbody::nil) =>
+ match coreVarToWeakVar ec with
+ | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
+ | 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: " +++ ct)
+ end
+ else let tc' := if eqd_dec tc ArrowTyCon
+ then WFunTyCon
+ else WTyCon tc
+ in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
+ end
+ | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
+ coreTypeToWeakType' t2 >>= fun t2' =>
+ coreTypeToWeakType' t3 >>= fun t3' =>
OK (WCoFunTy t1' t2' t3')
- | FunTy t1 t2 => coreTypeToWeakType t1 >>= fun t1' =>
- coreTypeToWeakType t2 >>= fun t2' =>
+ | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
+ coreTypeToWeakType' t2 >>= fun t2' =>
OK (WAppTy (WAppTy WFunTyCon t1') t2')
| ForAllTy cv t => match coreVarToWeakVar cv with
| WExprVar _ => Error "encountered expression variable in a type"
- | WTypeVar tv => coreTypeToWeakType t >>= fun t' => OK (WForAllTy tv t')
+ | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
| WCoerVar _ => Error "encountered coercion variable in a type"
end
| PredTy (ClassP cl lct) => ((fix rec tl := match tl with
| nil => OK nil
- | a::b => coreTypeToWeakType a >>= fun a' =>
+ | a::b => coreTypeToWeakType' a >>= fun a' =>
rec b >>= fun b' => OK (a'::b')
end) lct) >>= fun lct' => OK (WClassP cl lct')
- | PredTy (IParam ipn ct) => coreTypeToWeakType ct >>= fun ct' => OK (WIParam ipn ct')
+ | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
| PredTy (EqPred _ _) => Error "hit a bare EqPred"
end.
+Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
+
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_brak_name (coreVarCoreName v) then
- match coreVarToWeakVar v with
+ match coreVarToWeakVar ec with
| WExprVar _ => None
- | WTypeVar tv => Some (tv,tbody)
+ | WTypeVar tv => Some (v,tv,tbody)
| WCoerVar _ => None
end else None
| _ => None
end.
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_esc_name (coreVarCoreName v) then
- match coreVarToWeakVar v with
+ match coreVarToWeakVar ec with
| WExprVar _ => None
- | WTypeVar tv => Some (tv,tbody)
+ | WTypeVar tv => Some (v,tv,tbody)
| WCoerVar _ => None
end else None
| _ => 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 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)
end
| CoreEApp e1 e2 => match isBrak e1 with
- | Some (tv,t) =>
+ | Some (v,tv,t) =>
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
- OK (WEBrak tv e' t')
+ OK (WEBrak v tv e' t')
| None => match isEsc e1 with
- | Some (tv,t) =>
+ | Some (v,tv,t) =>
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
- OK (WEEsc tv e' t')
+ OK (WEEsc v tv e' t')
| None => coreExprToWeakExpr e1 >>= fun e1' =>
match e2 with
| CoreEType t =>
| 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
>>= fun branches =>
coreExprToWeakExpr e >>= fun scrutinee =>
coreTypeToWeakType tbranches >>= fun tbranches' =>
- OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
+ OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
end
end.
+
+
+