From: Adam Megacz Date: Tue, 31 May 2011 14:14:25 +0000 (-0700) Subject: Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=edb0c8776c642011e4e3c56d3db10bf2161ac972;hp=58275f561112bb1660eda14d535b2601188c3842 Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet --- diff --git a/examples/BiGArrow.hs b/examples/BiGArrow.hs index 466fbc2..40ff343 100644 --- a/examples/BiGArrow.hs +++ b/examples/BiGArrow.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances #-} +{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances -XDatatypeContexts #-} module BiGArrow where import GHC.HetMet.GArrow diff --git a/examples/Makefile b/examples/Makefile index b9fa6a7..7926143 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -1,11 +1,11 @@ -ghc_opt := -fwarn-incomplete-patterns -Werror +ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build open: make demo open .build/test.pdf #sanity += BiGArrow.hs -#sanity += CircuitExample.hs +sanity += CircuitExample.hs sanity += CommandSyntaxExample.hs sanity += DotProduct.hs sanity += GArrowTutorial.hs @@ -14,18 +14,20 @@ sanity += ImmutableHeap.hs sanity += IsomorphismForCodeTypes.hs sanity += LambdaCalculusInterpreter.hs sanity += TypeSafeRun.hs -sanity += Unflattening.hs +#sanity += Unflattening.hs + +sanity_opts = -dcore-lint -fforce-recomp -fcoqpass -ddump-coqpass -ddump-to-file +sanity_opts += -fsimpleopt-before-flatten +sanity_opts += -odir .build -hidir .build sanity: - ../../../inplace/bin/ghc-stage2 -dcore-lint -fforce-recomp -fcoqpass -ddump-coqpass -ddump-to-file \ - $(sanity) \ - +RTS -K500M + for A in $(sanity); do echo; echo; ../../../inplace/bin/ghc-stage2 $(sanity_opts) $$A +RTS -K500M || exit -1; done demo: mkdir -p .build - ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build -c Demo.hs -fforce-recomp - ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build --show-iface .build/Demo.hi - ../../../inplace/bin/ghc-stage2 $(ghc_opt) -odir .build -hidir .build GArrowTikZ.hs Demo.hs DemoMain.hs Unify.hs -o .build/demo + ../../../inplace/bin/ghc-stage2 $(ghc_opt) -c Demo.hs -fforce-recomp + ../../../inplace/bin/ghc-stage2 $(ghc_opt) --show-iface .build/Demo.hi + ../../../inplace/bin/ghc-stage2 $(ghc_opt) GArrowTikZ.hs Demo.hs DemoMain.hs Unify.hs -o .build/demo ./.build/demo > .build/test.tex cd .build; pdflatex test.tex diff --git a/examples/Unify.dump-coqpass b/examples/Unify.dump-coqpass deleted file mode 100644 index e69de29..0000000 diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index f11e63b..09f4b34 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -2,6 +2,7 @@ module CoqPass ( coqPassCoreToString, coqPassCoreToCore ) where import qualified Unique +import qualified Kind import qualified UniqSupply import qualified MkCore import qualified TysWiredIn @@ -18,6 +19,7 @@ import qualified TyCon import qualified Coercion import qualified Var import qualified Id +import qualified Pair import qualified FastString import qualified BasicTypes import qualified DataCon @@ -50,19 +52,11 @@ cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x -coreVarToWeakVar :: Var.Var -> WeakVar -coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) -coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) -coreVarToWeakVar v | Var.isCoVar v - = WCoerVar (WeakCoerVar v - (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v))))) - (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v)))))) -coreVarToWeakVar _ = - Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" - -errOrFail :: OrError t -> t -errOrFail (OK x) = x -errOrFail (Error s) = Prelude.error s +coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult +coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v) +coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v)) +coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v)) +coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!" rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind ) rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk)) @@ -95,21 +89,21 @@ sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x) sanitizeForLatex (c:x) = c:(sanitizeForLatex x) kindToCoreKind :: Kind -> TypeRep.Kind -kindToCoreKind KindStar = TypeRep.liftedTypeKind -kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) +kindToCoreKind KindStar = Kind.liftedTypeKind +kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) kindToCoreKind k = Prelude.error ((Prelude.++) "kindToCoreKind does not know how to handle kind " (kindToString k)) coreKindToKind :: TypeRep.Kind -> Kind coreKindToKind k = - case Coercion.splitKindFunTy_maybe k of + case Kind.splitKindFunTy_maybe k of Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2) Prelude.Nothing -> - if (Coercion.isLiftedTypeKind k) then KindStar - else if (Coercion.isUnliftedTypeKind k) then KindStar - else if (Coercion.isArgTypeKind k) then KindStar - else if (Coercion.isUbxTupleKind k) then KindStar - else if (Coercion.isOpenTypeKind k) then KindStar + if (Kind.isLiftedTypeKind k) then KindStar + else if (Kind.isUnliftedTypeKind k) then KindStar + else if (Kind.isArgTypeKind k) then KindStar + else if (Kind.isUbxTupleKind k) then KindStar + else if (Kind.isOpenTypeKind k) then KindStar -- -- The "subkinding" in GHC is not dealt with in System FC, and dealing -- with it is not actually as simple as you'd think. @@ -119,8 +113,7 @@ coreKindToKind k = -- else if (Coercion.isArgTypeKind k) then KindArgType -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple -- - else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" - else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" + else if (Kind.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " (Outputable.showSDoc (Outputable.ppr k))) outputableToString :: Outputable.Outputable a => a -> Prelude.String @@ -141,54 +134,6 @@ coreViewDeep t = Prelude.Nothing -> TypeRep.PredTy p Prelude.Just t' -> t' -coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion -coreCoercionToWeakCoercion c = - WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2)) - where - (t1,t2) = Coercion.coercionKind c -{- --- REMEMBER: cotycon applications may be oversaturated - case c of - TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME")) - TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2) - TypeRep.TyConApp tc t -> - case TyCon.isCoercionTyCon_maybe tc of - Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c)) - Prelude.Just (_, ctcd) -> - case (ctcd,t) of - (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y) - (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x) - (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x) - (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x) --- (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2) - (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1" - (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1" - (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1" - (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1" - (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1" - (TyCon.CoAxiom _ _ _ , _ ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)" - ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2)) - _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c)) - _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c)) --} --- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t) --- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y) --- CoreSyn.Type t -> WCoType (coreTypeToWeakType t) - -{- -weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type -| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2) -| WCoType t => Prelude_error "FIXME WCoType" -| WCoApp c1 c2 => Prelude_error "FIXME WCoApp" -| WCoAppT c t => Prelude_error "FIXME WCoAppT" -| WCoAll k f => Prelude_error "FIXME WCoAll" -| WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2) -| WCoComp c1 c2 => Prelude_error "FIXME WCoComp" -| WCoLeft c => Prelude_error "FIXME WCoLeft" -| WCoRight c => Prelude_error "FIXME WCoRight" -| WCoUnsafe t1 t2 => (t1,t2) --} - {-# NOINLINE trace #-} trace :: Prelude.String -> a -> a trace msg x = x @@ -202,14 +147,6 @@ trace msg x = x --trace msg x = System.IO.Unsafe.unsafePerformIO $ -- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x) - -{- -- used for extracting strings WITHOUT the patch for Coq -bin2ascii = - (\ b0 b1 b2 b3 b4 b5 b6 b7 -> - let f b i = if b then 1 `shiftL` i else 0 - in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) --} - -- I'm leaving this here (commented out) in case I ever need it again) --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 4926bff..d70cd58 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -71,7 +71,7 @@ Variable mkSystemName : Unique -> string -> nat -> Name. Variable mkTyVar : Name -> Kind -> CoreVar. Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))". Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. - Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))". + Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))". Variable mkExVar : Name -> CoreType -> CoreVar. Extract Inlined Constant mkExVar => "Id.mkLocalId". @@ -92,14 +92,15 @@ Section core2proof. (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no * free tyvars in them *) Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ := - match coreVarToWeakVar cv with - | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with + match coreVarToWeakVar' cv with + | OK (WExprVar wev) => match weakTypeToTypeOfKind φ wev ★ with | Error s => Prelude_error ("Error converting weakType of top-level variable "+++ toString cv+++": " +++ s) | OK t => t @@ nil end - | WTypeVar _ => Prelude_error "top-level xi got a type variable" - | WCoerVar _ => Prelude_error "top-level xi got a coercion variable" + | OK (WTypeVar _) => Prelude_error "top-level xi got a type variable" + | OK (WCoerVar _) => Prelude_error "top-level xi got a coercion variable" + | Error s => Prelude_error s end. Definition header : string := @@ -228,8 +229,9 @@ Section core2proof. End CoreToCore. Definition coreVarToWeakExprVarOrError cv := - match coreVarToWeakVar cv with - | WExprVar wv => wv + match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with + | OK (WExprVar wv) => wv + | Error s => Prelude_error s | _ => Prelude_error "IMPOSSIBLE" end. diff --git a/src/HaskCore.v b/src/HaskCore.v index b05c34f..13a263e 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -23,6 +23,7 @@ Inductive CoreExpr {b:Type} := | CoreECast : CoreExpr -> CoreCoercion -> CoreExpr | CoreENote : Note -> CoreExpr -> CoreExpr | CoreEType : CoreType -> CoreExpr +| CoreECoercion : CoreCoercion -> CoreExpr with CoreBind {b:Type} := | CoreNonRec : b -> CoreExpr -> CoreBind | CoreRec : list (b * CoreExpr ) -> CoreBind. @@ -36,7 +37,9 @@ Extract Inductive CoreExpr => "CoreSyn.Case" "CoreSyn.Cast" "CoreSyn.Note" - "CoreSyn.Type" ]. + "CoreSyn.Type" + "CoreSyn.Coercion" + ]. Extract Inductive CoreBind => "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ]. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index ccd4973..7669e5d 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -16,10 +16,10 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -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". +Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". +Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". +Variable coercionKind : CoreCoercion -> (CoreType * CoreType). + Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))". (* extracts the Name from a CoreVar *) Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". @@ -35,12 +35,16 @@ Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType := let (args,rest) := argsrest in OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)). +(* a hack to evade the guardedness check of Fixpoint *) +Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType. +Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'". + Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with | TyVarTy cv => match coreVarToWeakVar cv with - | WExprVar _ => Error "encountered expression variable in a type" - | WTypeVar tv => OK (WTyVarTy tv) - | WCoerVar _ => Error "encountered coercion variable in a type" + | CVTWVR_EVar ct => Error "encountered expression variable in a type" + | CVTWVR_TyVar k => OK (WTyVarTy (weakTypeVar cv k)) + | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type" end | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2') @@ -56,11 +60,12 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := 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" + | CVTWVR_EVar ct => Error "encountered expression variable in a modal box type" + | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type" + | CVTWVR_TyVar k => coreTypeToWeakType' tbody >>= fun tbody' => + OK (WCodeTy (weakTypeVar ec k) tbody') end - | _ => Error ("mis-applied modal box tycon: " +++ toString ct) + | _ => Error ("mis-applied modal box tycon: " +++ toString ct) end else let tc' := if eqd_dec tc ArrowTyCon then WFunTyCon @@ -75,11 +80,12 @@ 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 abstraction" - | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t') - | WCoerVar (weakCoerVar v t1' t2') => - coreTypeToWeakType' t >>= fun t3' => - OK (WCoFunTy t1' t2' t3') + | CVTWVR_EVar ct => Error "encountered expression variable in a type abstraction" + | CVTWVR_TyVar k => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t') + | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' => + coreTypeToWeakTypeCheat' t2 >>= fun t2' => + coreTypeToWeakType' t >>= fun t3' => + OK (WCoFunTy t1' t2' t3') end | PredTy (ClassP cl lct) => ((fix rec tl := match tl with | nil => OK nil @@ -93,18 +99,35 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := Definition coreTypeToWeakType t := addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)). +Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar := + addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol) + match coreVarToWeakVar cv with + | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t')) + | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k)) + | CVTWVR_CoVar t1 t2 => + (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *) + addErrorMessage ("with t2=" +++ toString t2 +++ eol) + ((coreTypeToWeakType t2) >>= fun t2' => + addErrorMessage ("with t1=" +++ toString t1 +++ eol) + (coreTypeToWeakType t1) >>= fun t1' => + OK (WCoerVar (weakCoerVar cv t1' t2'))) + end. +Definition tyConTyVars (tc:CoreTyCon) := + filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)). + Opaque tyConTyVars. +Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). + (* detects our crude Core-encoding of modal type introduction/elimination forms *) 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 - | WCoerVar _ => None - | WTypeVar tv => match coreVarToWeakVar v with - | WExprVar v' => Some (v',tv,tbody) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end + | _ => None end else None | _ => None end. @@ -113,13 +136,12 @@ Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreTyp 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 => match coreVarToWeakVar v with - | WExprVar v' => Some (v',tv,tbody) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end - | WCoerVar _ => None + | _ => None end else None | _ => None end. @@ -128,13 +150,12 @@ Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreTyp 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) + match coreVarToWeakVar' ec with + | OK (WTypeVar tv) => match coreVarToWeakVar' v with + | OK (WExprVar v') => Some (v',tv,tbody) | _ => None end - | WCoerVar _ => None + | _ => None end else None | _ => None end. @@ -148,15 +169,33 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak | _ => Error ("expectTyConApp encountered " +++ toString wt) end. +(* expects to see an EType with a coercion payload *) +Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion := + match ce with + | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2) + | _ => Error ("coreExprToWeakCoercion got a " +++ toString ce) + end. + +(* expects to see an EType *) +Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType := + match ce with + | CoreEType t => coreTypeToWeakType t + | _ => Error ("coreExprToWeakType got a " +++ toString ce) + end. + Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with | CoreELit lit => OK (WELit lit) | 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" + | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been" | CoreECast e co => coreExprToWeakExpr e >>= fun e' => - OK (WECast e' (coreCoercionToWeakCoercion co)) + let (ct1,ct2) := coercionKind co + in coreTypeToWeakType ct1 >>= fun t1 => + coreTypeToWeakType ct2 >>= fun t2 => + OK (WECast e' (WCoUnsafe t1 t2)) - | CoreEVar v => match coreVarToWeakVar v with + | CoreEVar v => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => OK (WEVar ev) | WTypeVar _ => Error "found a type variable inside an EVar!" | WCoerVar _ => Error "found a coercion variable inside an EVar!" @@ -189,20 +228,25 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := end end - | CoreELam v e => match coreVarToWeakVar v with + | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e') | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e') | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e') end - | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with + | CoreELet (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' => coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e') - | WTypeVar _ => match e with - | CoreEType t => Error "saw a type-let" + | WTypeVar tv => match e with + | CoreEType t => coreExprToWeakExpr e >>= fun e' => + coreExprToWeakType ve >>= fun ty' => + OK (WETyApp (WETyLam tv e') ty') | _ => Error "saw (ELet e) where e!=EType" end - | WCoerVar _ => Error "saw an (ELet )" + | WCoerVar (weakCoerVar cv t1 t2) => + coreExprToWeakExpr e >>= fun e' => + coreExprToWeakCoercion t1 t2 ve >>= fun co' => + OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co') end | CoreELet (CoreRec rb) e => @@ -210,7 +254,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match cel with | nil => OK nil | (v',e')::t => coreExprToWeakExprList t >>= fun t' => - match coreVarToWeakVar v' with + coreVarToWeakVar' v' >>= fun v'' => match v'' with | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t') | WTypeVar _ => Error "found a type variable in a recursive let" | WCoerVar _ => Error "found a coercion variable in a recursive let" @@ -220,7 +264,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := OK (WELetRec (unleaves' rb') e') | CoreECase e v tbranches alts => - match coreVarToWeakVar v with + coreVarToWeakVar' v >>= fun v' => match v' with | WTypeVar _ => Error "found a type variable in a case" | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => @@ -237,11 +281,11 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match alt with | 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 + | DataAlt dc => let vars := map coreVarToWeakVar' vars in 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)), + (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)), + (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)), + (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)), e')::rest') end end) alts) @@ -251,7 +295,3 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := OK (WECase ev scrutinee tbranches' tc lt (unleaves branches)) end end. - - - - diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 4babf36..79ab342 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -12,7 +12,9 @@ Require Import HaskCoreVars. Require Import HaskLiterals. Require Import HaskTyCons. -Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". +Variable CoreCoercionCoAxiom : Type. Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom". +Variable Int : Type. Extract Inlined Constant Int => "Prelude.Int". + Variable classTyCon : Class_ -> CoreTyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". Variable coreTyConToString : CoreTyCon -> string. Extract Inlined Constant coreTyConToString => "outputableToString". Variable coreDataConToString : CoreDataCon -> string. Extract Inlined Constant coreDataConToString => "outputableToString". @@ -34,11 +36,38 @@ Extract Inductive CoreType => Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. +Inductive CoreCoercion : Type := + CoreCoercionRefl : CoreType -> CoreCoercion + | CoreCoercionTyConAppCo : CoreTyCon -> list CoreCoercion -> CoreCoercion + | CoreCoercionAppCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionForAllCo : CoreVar -> CoreCoercion -> CoreCoercion + | CoreCoercionCoVarCo : CoreVar -> CoreCoercion + | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion + | CoreCoercionUnsafeCo : CoreType -> CoreType -> CoreCoercion + | CoreCoercionSymCo : CoreCoercion -> CoreCoercion + | CoreCoercionTransCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionNthCo : Int -> CoreCoercion -> CoreCoercion + | CoreCoercionInstCo : CoreCoercion -> CoreType -> CoreCoercion. + +Extract Inductive CoreCoercion => + "Coercion.Coercion" [ + "Coercion.Refl" + "Coercion.TyConAppCo" + "Coercion.AppCo" + "Coercion.ForAllCo" + "Coercion.CoVarCo" + "Coercion.AxiomInstCo" + "Coercion.UnsafeCo" + "Coercion.SymCo" + "Coercion.TransCo" + "Coercion.NthCo" + "Coercion.InstCo" ]. + Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". Variable coreCoercionKind : Kind -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)". -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Kind.typeKind)". Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)". Variable setVarType : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType => "Var.setVarType". diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index d805de4..1731aad 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -288,7 +288,7 @@ Section HaskFlattener. ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -304,7 +304,7 @@ Section HaskFlattener. [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ] [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -327,7 +327,7 @@ Section HaskFlattener. [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ] [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -348,7 +348,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -371,7 +371,7 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -394,12 +394,12 @@ Section HaskFlattener. [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ]. intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply ga_first. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply postcompose. @@ -450,14 +450,14 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply + eapply nd_comp; [ idtac | apply (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply r2'. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. @@ -537,13 +537,13 @@ Section HaskFlattener. intro pfb. apply secondify with (c:=a) in pfb. apply firstify with (c:=[]) in pfa. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ eapply nd_llecnac | idtac ]. apply nd_prod. apply pfa. clear pfa. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. @@ -576,7 +576,7 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. apply nd_prod. Focus 2. apply nd_id. @@ -643,7 +643,7 @@ Section HaskFlattener. simpl. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ]. set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ idtac | apply RLet ]. clear q''. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -830,12 +830,9 @@ Section HaskFlattener. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ - | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ - | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ - | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ - | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ @@ -931,12 +928,6 @@ Section HaskFlattener. apply flatten_coercion; auto. apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported"). - destruct case_RJoin. - simpl. - destruct l; - [ apply nd_rule; apply RJoin | idtac ]; - apply (Prelude_error "RJoin at depth >0"). - destruct case_RApp. simpl. @@ -965,59 +956,6 @@ Section HaskFlattener. Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1). *) - destruct case_RLet. - simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. - repeat drop_simplify. - repeat take_simplify. - simpl. - - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. - - eapply nd_comp. - eapply nd_prod; [ idtac | apply nd_id ]. - eapply boost. - apply (ga_first _ _ _ _ _ _ Σ₂'). - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - apply nd_prod. - apply nd_id. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)]. - apply precompose. - - destruct case_RWhere. - simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ]. - repeat take_simplify. - repeat drop_simplify. - simpl. - - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. - set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. - set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''. - - eapply nd_comp. - eapply nd_prod; [ eapply nd_id | idtac ]. - eapply (first_nd _ _ _ _ _ _ Σ₃'). - eapply nd_comp. - eapply nd_prod; [ eapply nd_id | idtac ]. - eapply (second_nd _ _ _ _ _ _ Σ₁'). - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ]. - apply nd_prod; [ idtac | apply nd_id ]. - eapply nd_comp; [ idtac | eapply precompose' ]. - apply nd_rule. - apply RArrange. - apply ALeft. - apply ACanL. - destruct case_RCut. simpl. destruct l as [|ec lev]; simpl. @@ -1029,41 +967,46 @@ Section HaskFlattener. rewrite <- IHΣ₁₂1. rewrite <- IHΣ₁₂2. reflexivity. - simpl. - repeat drop_simplify. - simpl. - repeat take_simplify. + simpl; repeat drop_simplify. + simpl; repeat take_simplify. simpl. set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1. rewrite take_lemma'. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. rewrite unlev_relev. rewrite <- mapOptionTree_compose. rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. apply nd_prod. apply nd_id. eapply nd_comp. eapply nd_rule. eapply RArrange. + eapply ALeft. eapply ARight. unfold x1. rewrite drop_to_nothing. apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)). admit. (* OK *) - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ]. set (mapOptionTree flatten_type Σ₁₂) as a. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. simpl. - eapply ga_first. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. + eapply secondify. + apply ga_first. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. simpl. apply precompose. @@ -1279,7 +1222,7 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | eapply boost ]. induction x. diff --git a/src/HaskProof.v b/src/HaskProof.v index 46009f8..5e6fac4 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -65,15 +65,10 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l] -| RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ] - (* order is important here; we want to be able to skolemize without introducing new AExch'es *) | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l] -| RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l] -| RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l] - -| RCut : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l] +| RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l] | RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l] | RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l] @@ -99,6 +94,34 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev] . +Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l, + ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + apply nd_prod. + apply nd_id. + apply nd_rule. + apply RArrange. + apply AuCanL. + Defined. + +Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, + ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + apply nd_prod. + apply nd_id. + eapply nd_rule; eapply RArrange; eapply AuCanL. + Defined. + +Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, + ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]. + intros. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply RCut. + Defined. (* A rule is considered "flat" if it is neither RBrak nor REsc *) (* TODO: change this to (if RBrak/REsc -> False) *) @@ -114,8 +137,6 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l) | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 ) | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) -| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) -| Flat_RJoin : ∀ q a b c d e l, Rule_Flat (RJoin q a b c d e l) | Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l) | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). @@ -151,9 +172,6 @@ Lemma no_rules_with_multiple_conclusions : forall c h, destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. - destruct X0; destruct s; inversion e. - destruct X0; destruct s; inversion e. - destruct X0; destruct s; inversion e. Qed. Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index dedc152..716a983 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -189,12 +189,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo" | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" | RApp _ _ _ _ _ _ _ => "App" - | RLet _ _ _ _ _ _ _ => "Let" - | RCut _ _ _ _ _ _ _ => "Cut" + | RCut _ _ _ _ _ _ _ _ => "Cut" | RLeft _ _ _ _ _ _ => "Left" | RRight _ _ _ _ _ _ => "Right" - | RWhere _ _ _ _ _ _ _ _ => "Where" - | RJoin _ _ _ _ _ _ _ => "RJoin" | RLetRec _ _ _ _ _ _ => "LetRec" | RCase _ _ _ _ _ _ _ _ => "Case" | RBrak _ _ _ _ _ _ => "Brak" @@ -223,7 +220,8 @@ Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with | RArrange _ _ _ _ _ _ r => nd_hideURule r | RVoid _ _ _ => true - | RJoin _ _ _ _ _ _ _ => true + | RLeft _ _ _ _ _ _ => true + | RRight _ _ _ _ _ _ => true | _ => false end. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index b16d4a8..0d90d4c 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -763,12 +763,9 @@ Section HaskProofToStrong. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ - | RJoin Γ p lri m x q l => let case_RJoin := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ @@ -849,19 +846,6 @@ Section HaskProofToStrong. apply ileaf in X. simpl in X. apply X. - destruct case_RJoin. - apply ILeaf; simpl; intros. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - destruct vars; inversion H. - destruct o; inversion H3. - refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _). - apply FreshMon. - apply FreshMon. - apply IBranch; auto. - destruct case_RApp. apply ILeaf. inversion X_. @@ -883,54 +867,19 @@ Section HaskProofToStrong. simpl in *. apply (EApp _ _ _ _ _ _ q1' q2'). - destruct case_RLet. - eapply rlet. - apply X_. - - destruct case_RWhere. - apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - destruct vars2; try destruct o; inversion H2. - clear H2. - - assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. - refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)). - apply FreshMon. - - destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - - refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _). - apply FreshMon. - simpl. - inversion pf1. - rewrite H3. - rewrite H4. - rewrite pf2. - reflexivity. - - refine (X0 ξ vars2_1 _ >>>= fun X1' => _). - apply FreshMon. - reflexivity. - apply FreshMon. - - apply ILeaf. - apply ileaf in X0'. - apply ileaf in X1'. - simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X1'. - apply X0'. - destruct case_RCut. + apply rassoc. + apply swapr. + apply rassoc'. + inversion X_. subst. clear X_. + + apply rassoc' in X0. + apply swapr in X0. + apply rassoc in X0. + induction Σ₃. destruct a. subst. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 6b6c756..435b687 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -231,12 +231,9 @@ Section HaskSkolemizer. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ - | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ - | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ - | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ - | RJoin Γ p lri m x q l => let case_RJoin := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ @@ -351,14 +348,6 @@ Section HaskSkolemizer. apply γ. apply (Prelude_error "found RCast at level >0"). - destruct case_RJoin. - simpl. - destruct l. - apply nd_rule. - apply SFlat. - apply RJoin. - apply (Prelude_error "found RJoin at level >0"). - destruct case_RApp. simpl. destruct lev. @@ -381,56 +370,8 @@ Section HaskSkolemizer. eapply take_unarrange. eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. - eapply nd_rule; eapply SFlat; apply RWhere. - - destruct case_RLet. - simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RLet. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - - eapply nd_comp. - eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ]. - - set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ]. - apply nd_prod. - apply nd_id. - apply nd_rule. - eapply SFlat. - eapply RArrange. - eapply AuAssoc. - - destruct case_RWhere. - simpl. - destruct lev. - apply nd_rule. - apply SFlat. - apply RWhere. - set (check_hof σ₁) as hof_tx. - destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ]. - destruct a. - rewrite H. - rewrite H0. - - eapply nd_comp. - eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ]. - apply nd_prod; [ idtac | eapply nd_id ]. - eapply nd_rule; apply SFlat; eapply RArrange. - eapply AComp. - eapply AuAssoc. - apply ALeft. - eapply AuAssoc. + eapply nd_comp; [ apply nd_exch | idtac ]. + eapply nd_rule; eapply SFlat; eapply RCut. destruct case_RCut. simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ]. @@ -438,24 +379,38 @@ Section HaskSkolemizer. set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''. set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''. set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''. - destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l))); + [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. rewrite <- e. + clear e. + destruct s. eapply nd_comp. - eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + eapply nd_prod. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply ALeft. + eapply arrangeCancelEmptyTree with (q:=x). + apply e. + apply ACanR. + apply nd_id. eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ]. apply nd_prod. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. - apply nd_rule. - apply SFlat. - apply RArrange. - apply ALeft. - destruct s. - eapply arrangeCancelEmptyTree with (q:=x). - rewrite e0. - admit. (* FIXME, but not serious *) apply nd_id. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AId. destruct case_RLeft. simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ]. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index bf51e1a..874b368 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -13,6 +13,7 @@ Require Import HaskLiterals. Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskWeakVars. +Require Import HaskCoreToWeak. Require Import HaskCoreVars. Section HaskStrong. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 1b9f6af..1f1229d 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -961,10 +961,13 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : destruct q. simpl in *. apply n. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; auto. - Defined. + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply IHX1. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply IHX2. + Defined. Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), @@ -1015,10 +1018,14 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. - eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ]. - eapply nd_comp; [ apply nd_rlecnac | idtac ]. - apply nd_prod; auto. - Defined. + + eapply nd_comp; [ idtac | eapply RCut' ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ]. + apply pf. + Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, @@ -1182,7 +1189,7 @@ Definition expr2proof : inversion H. destruct case_ELet; intros; simpl in *. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply pf_let. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 24f349b..e5a10ba 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -19,11 +19,11 @@ Require Import HaskCoreToWeak. Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars". -Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". +Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta". Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". Definition dataConExTyVars cdc := - filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). + filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)). Opaque dataConExTyVars. Definition dataConCoerKinds cdc := filter (map (fun x => match x with EqPred t1 t2 => diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 8ceb0b7..c3e90a4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -25,13 +25,6 @@ Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@trip Extract Inlined Constant sortAlts => "sortAlts". Implicit Arguments sortAlts [[a][b]]. -Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion. - Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion". - -(* 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)". - Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon := match wa with | WeakDataAlt cdc => DataAlt cdc @@ -59,7 +52,7 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := end. Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := - mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). + CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with @@ -67,8 +60,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := | WELit lit => CoreELit lit | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) - | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) - (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) + | 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 ) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 156c2ce..d8dcf42 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,6 +19,7 @@ Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreVars. +Require Import HaskCoreToWeak. Require Import HaskCoreTypes. Open Scope string_scope. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 3fb7a4b..e7ab943 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -14,6 +14,11 @@ Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskWeakTypes. +Inductive CoreVarToWeakVarResult : Type := +| CVTWVR_EVar : CoreType -> CoreVarToWeakVarResult +| CVTWVR_TyVar : Kind -> CoreVarToWeakVarResult +| CVTWVR_CoVar : CoreType -> CoreType -> CoreVarToWeakVarResult. + (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *) Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar. @@ -42,12 +47,8 @@ Definition haskLiteralToWeakType lit : WeakType := WTyCon (haskLiteralToTyCon lit). Coercion haskLiteralToWeakType : HaskLiteral >-> WeakType. -Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". -Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars". -Definition tyConTyVars (tc:CoreTyCon) := - filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). - Opaque tyConTyVars. -Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc). +Variable coreVarToWeakVar : CoreVar -> CoreVarToWeakVarResult. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". +Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars". Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".