X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=ccd497355f0be02006b2dc272f47ed958c6acd8f;hp=d47ab0ce3bbaf69c02e69e049824f6ca704ac93d;hb=6ae1b9b08da7c1d1f0de42afa1ccbf42acda3e62;hpb=53d4f1ce851b924cab5dc39419179a366001cbca diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index d47ab0c..ccd4973 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -4,10 +4,11 @@ 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 HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -23,11 +24,16 @@ Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. (* 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 form *) +(* 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". - -(* the magic wired-in name for the modal type elimination form *) 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". + +Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType := + split_list lwt (length (fst (tyFunKind tf))) >>= + fun argsrest => + let (args,rest) := argsrest in + OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)). Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with @@ -45,7 +51,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | 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') + | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse' | inl tc => if eqd_dec tc ModalBoxTyCon then match lct with | ((TyVarTy ec)::tbody::nil) => @@ -54,7 +60,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | 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) + | _ => Error ("mis-applied modal box tycon: " +++ toString ct) end else let tc' := if eqd_dec tc ArrowTyCon then WFunTyCon @@ -69,9 +75,11 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := 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" + | WExprVar _ => Error "encountered expression variable in a type abstraction" | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t') - | WCoerVar _ => Error "encountered coercion variable in a type" + | WCoerVar (weakCoerVar v t1' t2') => + coreTypeToWeakType' t >>= fun t3' => + OK (WCoFunTy t1' t2' t3') end | PredTy (ClassP cl lct) => ((fix rec tl := match tl with | nil => OK nil @@ -82,28 +90,50 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | PredTy (EqPred _ _) => Error "hit a bare EqPred" end. -Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)). +Definition coreTypeToWeakType t := + addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)). (* detects our crude Core-encoding of modal type introduction/elimination forms *) -Definition isBrak (ce:@CoreExpr CoreVar) : ??(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 ec with | WExprVar _ => None - | WTypeVar tv => Some (v,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) : ??(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 ec with | WExprVar _ => None - | WTypeVar tv => Some (v,tv,tbody) + | 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 => match coreVarToWeakVar v with + | WExprVar v' => Some (v',tv,tbody) + | _ => None + end | WCoerVar _ => None end else None | _ => None @@ -114,8 +144,8 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak 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) + | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt) + | _ => Error ("expectTyConApp encountered " +++ toString wt) end. Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := @@ -142,13 +172,20 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := 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 @@ -188,24 +225,23 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => 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)) := + 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)