Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Coq.Lists.List.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import General.
+Require Import HaskKinds.
+Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskWeakVars.
+Require Import HaskWeakTypes.
Require Import HaskWeak.
-Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
+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
+ | TyVarTy cv => match coreVarToWeakVar cv with
+ | WExprVar _ => Error "encountered expression variable in a type"
+ | WTypeVar tv => OK (WTyVarTy tv)
+ | WCoerVar _ => Error "encountered coercion variable in a type"
+ end
+
+ | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
+
+ | 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')
+ end) lct)
+ 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: " +++ toString 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' =>
+ 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')
+ | 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' =>
+ 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 (EqPred _ _) => Error "hit a bare EqPred"
+ end.
+
+Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (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) : ??(WeakExprVar * 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)
| WCoerVar _ => None
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
end else None
| _ => None
end.
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * 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 => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
+ | WCoerVar _ => None
+ end else None
+ | _ => None
+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
| WExprVar _ => None
- | WTypeVar tv => Some (tv,tbody)
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
| WCoerVar _ => None
end else None
| _ => None
end.
-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
- let (t1,t2) := coreCoercionKind cc
- in weakCoercion t1 t2 cc.
+(* 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.
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' =>
- OK (WECast e' (coreCoercionToWeakCoercion 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) => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e' t)
+ | Some (v,tv,t) =>
+ coreExprToWeakExpr e2 >>= fun e' =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WEBrak v tv e' t')
| None => match isEsc e1 with
- | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e' t)
- | None => coreExprToWeakExpr e1 >>= fun e1' =>
- match e2 with
- | CoreEType t => OK (WETyApp e1' t)
- | _ => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
- end
+ | Some (v,tv,t) =>
+ coreExprToWeakExpr e2 >>= fun e' =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WEEsc v tv e' t')
+ | 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' => coreTypeOfWeakExpr e' >>= fun te' =>
- match te' with
- | TyConApp _ tc lt =>
- ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
- : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+ coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
+ expectTyConApp te' nil >>= fun tca =>
+ let (tc,lt) := tca:(TyCon * list WeakType) in
+ ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
+ : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match branches with
| nil => OK nil
| (mkTriple alt vars e)::rest =>
mkBranches rest >>= fun rest' =>
coreExprToWeakExpr e >>= fun e' =>
match alt with
- | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest')
- | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest')
- | DataAlt _ _ _ _ tc' dc => let vars := map coreVarToWeakVar vars in
- OK (((DataAlt _ dc),
- (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+ | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
+ | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
+ | DataAlt dc => let vars := map coreVarToWeakVar vars in
+ OK (((WeakDataAlt dc),
+ (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
e')::rest')
end
end) alts)
- >>= fun branches => coreExprToWeakExpr e
- >>= fun scrutinee =>
- list2vecOrError lt _ >>= fun lt' =>
- OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches)))
- | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
- end
+ >>= fun branches =>
+ coreExprToWeakExpr e >>= fun scrutinee =>
+ coreTypeToWeakType tbranches >>= fun tbranches' =>
+ OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
end
end.
+
+
+
projects / coq-hetmet.git / blobdiff