X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=c3e90a43763c820af3ea4c561b465986d05a73ad;hp=24eedc6bbcd9bb2f3c36ccf6b0b8b37390100151;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=26733c04106397dc8a10396ce688e908e8d0cde7 diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 24eedc6..c3e90a4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -8,7 +8,8 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -20,79 +21,101 @@ Require Import HaskCoreToWeak. Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar. Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet". -Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b). - Extract Inlined Constant mkCoreLet => "sortAlts". +Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b). + Extract Inlined Constant sortAlts => "sortAlts". Implicit Arguments sortAlts [[a][b]]. -Variable trustMeCoercion : CoreCoercion. - Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce". - -(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *) -Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. - Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". - -Section HaskWeakToCore. +Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon := + match wa with + | WeakDataAlt cdc => DataAlt cdc + | WeakLitAlt lit => LitAlt lit + | WeakDEFAULT => DEFAULT + end. - (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *) - Context (hetmet_brak_var : CoreVar). - Context (hetmet_esc_var : CoreVar). +Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := + match wt with + | WTyVarTy (weakTypeVar v _) => TyVarTy v + | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2) + | WAppTy t1 t2 => match (weakTypeToCoreType t1) with + | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil)) + | t1' => AppTy t1' (weakTypeToCoreType t2) + end + | WTyCon tc => TyConApp tc nil + | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt) + | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt)) + | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty)) + | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t) + | WFunTyCon => TyConApp ArrowTyCon nil + | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil) + | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2))) + (weakTypeToCoreType t3) + end. - Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := - fun _ => trustMeCoercion. +Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := + CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). - Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar := +Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with | WEVar (weakExprVar v _) => CoreEVar v | WELit lit => CoreELit lit - | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2) - | WETyApp e t => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t)) - | WECoApp e co => CoreEApp (weakExprToCoreExpr f e ) - (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) - | WENote n e => CoreENote n (weakExprToCoreExpr f e ) - | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr f e ) - | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr f e ) - | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr f e ) - | WECast e co => CoreECast (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co) + | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) + | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) + | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co)) + | WENote n e => CoreENote n (weakExprToCoreExpr e ) + | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e ) + | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e ) + | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e ) + | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co) | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp ((CoreEType (TyVarTy ec)):: (CoreEType (weakTypeToCoreType t)):: - (weakExprToCoreExpr f e):: + (weakExprToCoreExpr e):: nil) (CoreEVar v) | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp ((CoreEType (TyVarTy ec)):: (CoreEType (weakTypeToCoreType t)):: - (weakExprToCoreExpr f e):: + (weakExprToCoreExpr e):: nil) (CoreEVar v) - | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr f ve)) (weakExprToCoreExpr f e) - | WECase e tbranches tc types alts => let (v,f') := next _ _ f tt in - CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches) + | WECSP v (weakTypeVar ec _) e t => fold_left CoreEApp + ((CoreEType (TyVarTy ec)):: + (CoreEType (weakTypeToCoreType t)):: + (weakExprToCoreExpr e):: + nil) + (CoreEVar v) + | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) + | WECase vscrut escrut tbranches tc types alts => + CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches) (sortAlts (( fix mkCaseBranches (alts:Tree - ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := + ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match alts with | T_Leaf None => nil | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2) | T_Leaf (Some (ac,tvars,cvars,evars,e)) => - (mkTriple (ac:AltCon) + (mkTriple (weakAltConToCoreAltCon ac) (app (app (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) (map (fun v:WeakExprVar => weakVarToCoreVar v) evars)) - (weakExprToCoreExpr f' e))::nil + (weakExprToCoreExpr e))::nil end ) alts)) | WELetRec mlr e => CoreELet (CoreRec ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) := match mlr with | T_Leaf None => nil - | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil + | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2) end) mlr)) - (weakExprToCoreExpr f e) + (weakExprToCoreExpr e) end. -End HaskWeakToCore. +Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := + coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)). + +Instance weakExprToString : ToString WeakExpr := + { toString := fun we => toString (weakExprToCoreExpr we) }.