X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=abcd6b8babfe78affc8d08d5645e53d2532f1765;hp=d269cd10dd1c70be83cfdef3c4d6554b718df20f;hb=6c953e094065d487e85635df7fd5389271e4a279;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index d269cd1..abcd6b8 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -4,10 +4,10 @@ Generalizable All Variables. Require Import Preamble. -Require Import General. Require Import Coq.Lists.List. +Require Import General. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -15,15 +15,20 @@ Require Import HaskWeakVars. 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". - +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". -Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). +(* extracts the Name from a CoreVar *) +Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". -Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". +(* 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 := +Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with | TyVarTy cv => match coreVarToWeakVar cv with | WExprVar _ => Error "encountered expression variable in a type" @@ -31,79 +36,107 @@ Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType := | 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: " +++ 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' => + | 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. +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 => 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 coreTypeToWeakType t1 >>= fun t1' => - coreTypeToWeakType t2 >>= fun t2' => - OK (weakCoercion 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. Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with @@ -111,8 +144,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | 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) @@ -121,22 +153,29 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := 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') - | 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 + 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 @@ -175,33 +214,34 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | 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 => - let (tc,lt) := tca in - ((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') + | 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 (((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)), + 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 => 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. + + +