X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=c3e90a43763c820af3ea4c561b465986d05a73ad;hp=959133d8f89de99646add568de1912fd5afcd8e6;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=02af384ece10c5aa927c7d7c1379e9d202926cc8 diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 959133d..c3e90a4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -7,73 +7,94 @@ 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. -Coercion weakVarToCoreVar : WeakVar >-> CoreVar. - -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 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 + (mkTriple (weakAltConToCoreAltCon ac) (app (app (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) @@ -91,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) }. + +