X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=c3e90a43763c820af3ea4c561b465986d05a73ad;hp=9de00e34564e51ba250c606753782c3290a32942;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=a9bbdf55d01ad494d42018c0eaa252da1d7b5d97;ds=sidebyside diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 9de00e3..c3e90a4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -7,71 +7,99 @@ Require Import Preamble. Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. +Require Import HaskKinds. Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. Require Import HaskWeakVars. +Require Import HaskWeakTypes. Require Import HaskWeak. +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 unsafeCoerce : CoreCoercion. - Extract Inlined Constant unsafeCoerce => "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)". - -(* a dummy variable which is never referenced but needed for a binder *) -Variable dummyVariable : CoreVar. - -Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := -match wv with -| WExprVar (weakExprVar v _ ) => v -| WTypeVar (weakTypeVar v _ ) => v -| WCoerVar (weakCoerVar v _ _ ) => v -end. - -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 _ => unsafeCoerce. +Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := + CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). - Fixpoint weakExprToCoreExpr (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 e1) (weakExprToCoreExpr e2) - | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType t) - | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) - (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) + | 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 ) + | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e ) | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co) - | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType t) - | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t) + | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp + ((CoreEType (TyVarTy ec)):: + (CoreEType (weakTypeToCoreType t)):: + (weakExprToCoreExpr e):: + nil) + (CoreEVar v) + | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp + ((CoreEType (TyVarTy ec)):: + (CoreEType (weakTypeToCoreType t)):: + (weakExprToCoreExpr e):: + nil) + (CoreEVar v) + | 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 e tbranches n tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches + | WECase vscrut escrut tbranches tc types alts => + CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches) (sortAlts (( - fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) := + fix mkCaseBranches (alts:Tree + ??(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,lwv,e)) => - (mkTriple ac (map weakVarToCoreVar lwv) (weakExprToCoreExpr e))::nil + | T_Leaf (Some (ac,tvars,cvars,evars,e)) => + (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 e))::nil end ) alts)) | WELetRec mlr e => CoreELet (CoreRec @@ -84,4 +112,10 @@ Section HaskWeakToCore. (weakExprToCoreExpr e) end. -End HaskWeakToCore. \ No newline at end of file +Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := + coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)). + +Instance weakExprToString : ToString WeakExpr := + { toString := fun we => toString (weakExprToCoreExpr we) }. + +