-{-# 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
-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
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
module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
where
import qualified Unique
+import qualified Kind
import qualified UniqSupply
import qualified MkCore
import qualified TysWiredIn
import qualified Coercion
import qualified Var
import qualified Id
+import qualified Pair
import qualified FastString
import qualified BasicTypes
import qualified DataCon
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))
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.
-- 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
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
--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)
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".
(* 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 :=
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.
| 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.
"CoreSyn.Case"
"CoreSyn.Cast"
"CoreSyn.Note"
- "CoreSyn.Type" ].
+ "CoreSyn.Type"
+ "CoreSyn.Coercion"
+ ].
Extract Inductive CoreBind =>
"CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
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".
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')
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
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
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.
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.
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.
| _ => 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!"
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 <tyvar> e) where e!=EType"
end
- | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
+ | 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 =>
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"
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 =>
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)
OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
end
end.
-
-
-
-
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".
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".
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.
[ Γ > Δ > 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.
[ Γ > Δ > 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.
[ Γ > Δ > Σ |- [@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.
[ Γ > Δ > Σ |- [@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.
[Γ > Δ > Σ,,[@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.
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'.
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 ].
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.
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.
| 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 _
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.
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.
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.
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.
| 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]
[Γ > Δ > (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) *)
| 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).
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.
| 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"
match r with
| RArrange _ _ _ _ _ _ r => nd_hideURule r
| RVoid _ _ _ => true
- | RJoin _ _ _ _ _ _ _ => true
+ | RLeft _ _ _ _ _ _ => true
+ | RRight _ _ _ _ _ _ => true
| _ => false
end.
| 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 _
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_.
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.
| 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 _
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.
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 ].
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 ].
Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
+Require Import HaskCoreToWeak.
Require Import HaskCoreVars.
Section HaskStrong.
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))),
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,
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.
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 =>
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
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
| 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 )
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
+Require Import HaskCoreToWeak.
Require Import HaskCoreTypes.
Open Scope string_scope.
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.
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".
projects / coq-hetmet.git / commitdiff