From 8c26722a1ee110077968a8a166eb7130266b2035 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 12 Mar 2011 04:44:18 -0800 Subject: [PATCH] Make the HaskStrong type representation Kind-indexed, and many supporting changes (see long comment). This patch makes a whole lot of interlocking changes, with the ultimate (accomplished) goal of changing the HaskStrong type representation ("HaskType") so that it is indexed by the Haskell Kind of the type. As a result, the auxiliary well-kindedness judgment \vdash_{ty} is no longer necessary. Other changes in this patch: - Added Coq ToString class (similar to Haskell's Show class) - Massive reduction in volume of code extracted for string literals - Decidable equality on HaskStrong's - Much more reliable HaskWeakToStrong, although it has regressed a bit in terms of number of cases handled; this will be remediated shortly. --- src/Extraction-prefix.hs | 30 +- src/Extraction.v | 45 +-- src/General.v | 48 +++ src/HaskCoreLiterals.v | 15 +- src/HaskCoreToWeak.v | 67 ++-- src/HaskCoreTypes.v | 42 +-- src/HaskCoreVars.v | 5 +- src/HaskKinds.v | 32 +- src/HaskProof.v | 54 ++-- src/HaskProofToLatex.v | 193 ++++++------ src/HaskProofToStrong.v | 16 +- src/HaskStrong.v | 28 +- src/HaskStrongToProof.v | 67 ++-- src/HaskStrongToWeak.v | 74 ++--- src/HaskStrongTypes.v | 516 ++++++++++++++++++------------- src/HaskWeak.v | 6 +- src/HaskWeakToStrong.v | 759 ++++++++++++++++------------------------------ src/HaskWeakTypes.v | 15 +- src/HaskWeakVars.v | 16 + src/Preamble.v | 4 +- 20 files changed, 1018 insertions(+), 1014 deletions(-) diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index f9bdbe3..4abbf69 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -26,25 +26,46 @@ import Prelude ( (++), (+), (==), Show, show, Char ) import qualified Prelude import qualified GHC.Base +-- used for extracting strings +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)) +--bin2ascii' = +-- (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7)) +--shiftAscii = +-- \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0) + -- crude way of casting Coq "error monad" into Haskell exceptions errOrFail :: OrError a -> a errOrFail (OK x) = x errOrFail (Error s) = Prelude.error s +getTyConTyVars :: TyCon.TyCon -> [Var.TyVar] +getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc + -- to do: this could be moved into Coq 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 = Prelude.error "FIXME coerVarSort not fully implemented" +coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME")) coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" +tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon +--FIXME: go back to this +--tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n +tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n + +tyFunResultKind :: TyCon.TyCon -> Kind +tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc) + nat2int :: Nat -> Prelude.Int nat2int O = 0 nat2int (S x) = 1 + (nat2int x) -nat2string :: Nat -> Prelude.String -nat2string n = show (nat2int n) +natToString :: Nat -> Prelude.String +natToString n = show (nat2int n) -- only needs to sanitize characters which might appear in Haskell identifiers sanitizeForLatex :: Prelude.String -> Prelude.String @@ -71,9 +92,8 @@ coreKindToKind k = outputableToString :: Outputable.Outputable a => a -> Prelude.String outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) +-- TO DO: I think we can remove this now checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool --- checkTypeEquality t1 t2 = Type.coreEqType (coreViewDeep t1) (coreViewDeep t2) --- checkTypeEquality t1 t2 = Type.tcEqType (coreViewDeep t1) (coreViewDeep t2) checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) --showType t = outputableToString (Type.expandTypeSynonyms t) diff --git a/src/Extraction.v b/src/Extraction.v index 57e08a3..e2e3800 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -50,14 +50,10 @@ Extract Inlined Constant ascii_dec => "(==)". Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Prelude.Char" -[ -"{- If this appears, you're using Ascii internals. Please don't -} (\ 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))" -] -"{- If this appears, you're using Ascii internals. Please don't -} (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)". +Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'". +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => "shiftAscii". Unset Extraction Optimize. Unset Extraction AutoInline. @@ -72,7 +68,7 @@ Section core2proof. Definition Δ : CoercionEnv Γ := nil. - Definition φ : CoreVar->HaskTyVar Γ := + Definition φ : TyVarResolver Γ := fun cv => (fun TV env => fail "unbound tyvar"). (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*) @@ -81,8 +77,11 @@ 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 ξ : WeakExprVar -> WeakType * list WeakTypeVar - := fun (v:WeakExprVar) => ((v:WeakType),nil). + Definition ξ (wev:WeakExprVar) : LeveledHaskType Γ ★ := + match weakTypeToType' φ wev ★ with + | Error s => fail ("Error in top-level xi: " +++ s) + | OK t => t @@ nil + end. Definition header : string := "\documentclass[9pt]{article}"+++eol+++ @@ -105,17 +104,19 @@ Section core2proof. Definition handleExpr (ce:@CoreExpr CoreVar) : string := match coreExprToWeakExpr ce with | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s) - | OK me => - match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with - | Indexed_Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) - | Indexed_OK τ e => match e with - | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) - | OK e' => - eol+++"$$"+++ - nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++ - "$$"+++eol - end - end + | OK we => match weakTypeOfWeakExpr we >>= fun t => weakTypeToType φ t with + | Error s => fail ("unable to calculate HaskType of a HaskWeak expression because: " +++ s) + | OK τ => match τ with + | haskTypeOfSomeKind ★ τ' => + match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with + | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) + | OK e' => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol + end + | haskTypeOfSomeKind κ τ' => + fail ("encountered 'expression' of kind "+++κ+++" at top level (type "+++τ' + +++"); shouldn't happen") + end + end end. Definition handleBind (bind:@CoreBind CoreVar) : string := diff --git a/src/General.v b/src/General.v index b58bb96..f3e4379 100644 --- a/src/General.v +++ b/src/General.v @@ -21,6 +21,10 @@ Class EqDecidable (T:Type) := Coercion eqd_type : EqDecidable >-> Sortclass. +Class ToString (T:Type) := { toString : T -> string }. +Instance StringToString : ToString string := { toString := fun x => x }. +Notation "a +++ b" := (append (toString a) (toString b)) (at level 100). + (*******************************************************************************) (* Trees *) @@ -525,6 +529,50 @@ Inductive IList (I:Type)(F:I->Type) : list I -> Type := Implicit Arguments INil [ I F ]. Implicit Arguments ICons [ I F ]. +Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20). + +Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x. + intro il. + inversion il. + subst. + apply X. + Defined. + +Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y. + intro il. + inversion il. + subst. + apply X0. + Defined. + +Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il. + induction il; intros; auto. + apply INil. + inversion X; subst. + apply ICons; auto. + Defined. + +Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1. + induction l1; auto. + apply INil. + apply ICons. + inversion v; auto. + apply IHl1. + inversion v; auto. + Defined. + +Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2. + induction l1; auto. + apply IHl1. + inversion v; subst; auto. + Defined. + +Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z := + match il with + | INil => nil + | a::::b => a::(ilist_to_list b) + end. + (* a tree indexed by a (Tree (option X)) *) Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type := | INone : ITree I F [] diff --git a/src/HaskCoreLiterals.v b/src/HaskCoreLiterals.v index d332ccf..24432ee 100644 --- a/src/HaskCoreLiterals.v +++ b/src/HaskCoreLiterals.v @@ -45,6 +45,7 @@ Extract Inductive HaskFunctionOrData => "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ]. Variable haskLiteralToString : HaskLiteral -> string. Extract Inlined Constant haskLiteralToString => "outputableToString". +Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }. (* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *) Inductive triple {A B C:Type} := @@ -52,6 +53,13 @@ Inductive triple {A B C:Type} := Notation "a ** b ** c" := (mkTriple a b c) (at level 20). Extract Inductive triple => "(,,)" [ "(,,)" ]. +Inductive AltCon := +| DataAlt : CoreDataCon -> AltCon +| LitAlt : HaskLiteral -> AltCon +| DEFAULT : AltCon. +Extract Inductive AltCon => + "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. + (* the TyCons for each of the literals above *) Variable addrPrimTyCon : TyCon. Extract Inlined Constant addrPrimTyCon => "TysPrim.addrPrimTyCon". Variable intPrimTyCon : TyCon. Extract Inlined Constant intPrimTyCon => "TysPrim.intPrimTyCon". @@ -76,10 +84,3 @@ match lit with | HaskMachDouble _ => doublePrimTyCon | HaskMachLabel _ _ _ => addrPrimTyCon end. - -Inductive AltCon := -| DataAlt : CoreDataCon -> AltCon -| LitAlt : HaskLiteral -> AltCon -| DEFAULT : AltCon. -Extract Inductive AltCon => - "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ]. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index d269cd1..644d04d 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -15,15 +15,10 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -(* this distinguishes SystemFC "type functions" (true) which are always fully applied from "type constructors" which aren't *) -Variable isFamilyTyCon : TyCon -> bool. Extract Inlined Constant isFamilyTyCon => "TyCon.isFamilyTyCon". - - Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). +Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". -Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". - -Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType := +Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := match ct with | TyVarTy cv => match coreVarToWeakVar cv with | WExprVar _ => Error "encountered expression variable in a type" @@ -31,50 +26,54 @@ Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType := | WCoerVar _ => Error "encountered coercion variable in a type" end - | AppTy t1 t2 => coreTypeToWeakType t2 >>= fun t2' => coreTypeToWeakType t1 >>= fun t1' => OK (WAppTy t1' t2') + | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2') - | TyConApp tc lct => + | TyConApp tc_ lct => let recurse := ((fix rec tl := match tl with | nil => OK nil - | a::b => coreTypeToWeakType a >>= fun a' => rec b >>= fun b' => OK (a'::b') + | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b') end) lct) - in if (isFamilyTyCon tc) - then recurse >>= fun recurse' => OK (WTyFunApp tc recurse') - else if eqd_dec tc ModalBoxTyCon - 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" - end - | _ => Error "mis-applied modal box tycon" - end - else let tc' := if eqd_dec tc ArrowTyCon - then WFunTyCon - else WTyCon tc - in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc') - | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType t1 >>= fun t1' => - coreTypeToWeakType t2 >>= fun t2' => - coreTypeToWeakType t3 >>= fun t3' => + in match tyConOrTyFun tc_ with + | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse') + | inl tc => if eqd_dec tc ModalBoxTyCon + 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" + end + | _ => Error "mis-applied modal box tycon" + end + else let tc' := if eqd_dec tc ArrowTyCon + then WFunTyCon + else WTyCon tc + in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc') + end + | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' => + coreTypeToWeakType' t2 >>= fun t2' => + coreTypeToWeakType' t3 >>= fun t3' => OK (WCoFunTy t1' t2' t3') - | FunTy t1 t2 => coreTypeToWeakType t1 >>= fun t1' => - coreTypeToWeakType t2 >>= fun t2' => + | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' => + 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" - | WTypeVar tv => coreTypeToWeakType t >>= fun t' => OK (WForAllTy tv t') + | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t') | WCoerVar _ => Error "encountered coercion variable in a type" end | PredTy (ClassP cl lct) => ((fix rec tl := match tl with | nil => OK nil - | a::b => coreTypeToWeakType a >>= fun a' => + | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b') end) lct) >>= fun lct' => OK (WClassP cl lct') - | PredTy (IParam ipn ct) => coreTypeToWeakType ct >>= fun ct' => OK (WIParam ipn ct') + | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct') | PredTy (EqPred _ _) => Error "hit a bare EqPred" end. +Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". +Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t). + (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) := match ce with diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 4a7a056..ea4a02a 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -10,20 +10,16 @@ Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskCoreVars. -Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". +Variable CoreTyCon : Type. Extract Inlined Constant CoreTyCon => "TyCon.TyCon". Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon". Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name". Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". -Variable CoreCoFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". -Variable CoreTyFunConst : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class". -Variable classTyCon : Class_ -> TyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". -Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString". +Variable classTyCon : Class_ -> CoreTyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". +Variable tyConToString : CoreTyCon -> string. Extract Inlined Constant tyConToString => "outputableToString". Variable dataConToString : CoreDataCon-> string. Extract Inlined Constant dataConToString => "outputableToString". -Variable tyFunToString : CoreTyFunConst -> string. Extract Inlined Constant tyFunToString => "outputableToString". -Variable coFunToString : CoreCoFunConst -> string. Extract Inlined Constant coFunToString => "outputableToString". -Variable natTostring : nat->string. Extract Inlined Constant natTostring => "natTostring". Variable CoreIPName : Type -> Type. + Extract Constant CoreIPName "’a" => "BasicTypes.IPName". Extraction Inline CoreIPName. @@ -31,7 +27,7 @@ Variable CoreIPName : Type -> Type. Inductive CoreType := | TyVarTy : CoreVar -> CoreType | AppTy : CoreType -> CoreType -> CoreType (* first arg must be AppTy or TyVarTy*) -| TyConApp : TyCon -> list CoreType -> CoreType +| TyConApp : CoreTyCon -> list CoreType -> CoreType | FunTy : CoreType -> CoreType -> CoreType (* technically redundant since we have FunTyCon *) | ForAllTy : CoreVar -> CoreType -> CoreType | PredTy : PredType -> CoreType @@ -44,24 +40,34 @@ Extract Inductive CoreType => Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. +Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "showType". +Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". +Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". +Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". + +(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *) +Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". +Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon". + (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *) +Variable coreTyCon_eq : EqDecider CoreTyCon. Extract Inlined Constant coreTyCon_eq => "(==)". Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_eq => "(==)". +Variable tyFun_eq : EqDecider TyFun. Extract Inlined Constant tyFun_eq => "(==)". Variable dataCon_eq : EqDecider CoreDataCon. Extract Inlined Constant dataCon_eq => "(==)". Variable coreName_eq : EqDecider CoreName. Extract Inlined Constant coreName_eq => "(==)". Variable coretype_eq_dec : EqDecider CoreType. Extract Inlined Constant coretype_eq_dec => "checkTypeEquality". Instance CoreTypeEqDecidable : EqDecidable CoreType := { eqd_dec := coretype_eq_dec }. +Instance CoreTyConEqDecidable: EqDecidable CoreTyCon := { eqd_dec := coreTyCon_eq }. Instance TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_eq }. +Instance TyFunEqDecidable : EqDecidable TyFun := { eqd_dec := tyFun_eq }. Instance DataConEqDecidable : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }. Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName_eq }. -(* -Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString". -*) -Variable coreTypeToString : CoreType -> string. - Extract Inlined Constant coreTypeToString => "showType". -Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". -Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". -Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". +Instance CoreTypeToString : ToString CoreType := { toString := coreTypeToString }. +Instance CoreNameToString : ToString CoreName := { toString := coreNameToString }. +Instance CoreCoercionToString : ToString CoreCoercion := { toString := coreCoercionToString }. +Instance CoreDataConToString : ToString CoreDataCon := { toString := dataConToString }. +Instance CoreTyConToString : ToString CoreTyCon := { toString := tyConToString }. diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index 6e61128..954dfc5 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -5,10 +5,13 @@ Generalizable All Variables. Require Import Preamble. Require Import General. +Require Import Coq.Strings.String. (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *) Variable CoreVar : Type. Extract Inlined Constant CoreVar => "Var.Var". Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Extract Inlined Constant coreVar_eq => "(==)". +Variable coreVarToString : CoreVar -> string. Extract Inlined Constant coreVarToString => "outputableToString". Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq }. - +Instance CoreVarToString : ToString CoreVar := + { toString := coreVarToString }. diff --git a/src/HaskKinds.v b/src/HaskKinds.v index b063b56..583bb86 100644 --- a/src/HaskKinds.v +++ b/src/HaskKinds.v @@ -1,5 +1,5 @@ (*********************************************************************************************************************************) -(* HaskKinds: Definitions shared by all four representations (Core, Weak, Strong, Proof) *) +(* HaskKinds: Definitions shared by all four representations (Core, Weak, Strong, Proof) *) (*********************************************************************************************************************************) Generalizable All Variables. @@ -8,17 +8,31 @@ Require Import General. Require Import Coq.Strings.String. Open Scope nat_scope. -Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note". -Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string". +Variable Note : Type. Extract Inlined Constant Note => "CoreSyn.Note". +Variable natToString : nat -> string. Extract Inlined Constant natToString => "natToString". +Instance NatToStringInstance : ToString nat := { toString := natToString }. (* Figure 7: production κ, ι *) Inductive Kind : Type := - | KindType : Kind (* ★ - the kind of boxed types*) - | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ *) - | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *) - | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *) - | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *) - | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *). + | KindType : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *) + | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*) + | KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *) + | KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *) + | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *) + | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *). + +Open Scope string_scope. +Fixpoint kindToString (k:Kind) : string := + match k with + | KindType => "*" + | KindTypeFunction KindType k2 => "*=>"+++kindToString k2 + | KindTypeFunction k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2 + | KindUnliftedType => "#" + | KindUnboxedTuple => "(#)" + | KindArgType => "?" + | KindOpenType => "?" + end. +Instance KindToString : ToString Kind := { toString := kindToString }. Notation "'★'" := KindType. Notation "a ⇛ b" := (KindTypeFunction a b). diff --git a/src/HaskProof.v b/src/HaskProof.v index 8da87e8..7ae3462 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -26,8 +26,8 @@ Inductive Judg := mkJudg : forall Γ:TypeEnv, forall Δ:CoercionEnv Γ, - Tree ??(LeveledHaskType Γ) -> - Tree ??(LeveledHaskType Γ) -> + Tree ??(LeveledHaskType Γ ★) -> + Tree ??(LeveledHaskType Γ ★) -> Judg. Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). @@ -36,8 +36,8 @@ Inductive Judg := * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *) Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) := mkUJudg : - Tree ??(LeveledHaskType Γ) -> - Tree ??(LeveledHaskType Γ) -> + Tree ??(LeveledHaskType Γ ★) -> + Tree ??(LeveledHaskType Γ ★) -> UJudg Γ Δ. Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). Notation "'ext_tree_left'" := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t) s end). @@ -49,9 +49,9 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := Coercion UJudg2judg : UJudg >-> Judg. (* information needed to define a case branch in a HaskProof *) -Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ}{avars} := +Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars} := { pcb_scb : @StrongAltCon tc -; pcb_freevars : Tree ??(LeveledHaskType Γ) +; pcb_freevars : Tree ??(LeveledHaskType Γ ★) ; pcb_judg := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ) > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) (vec2list (sac_types pcb_scb Γ avars)))) @@ -90,21 +90,21 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := (* SystemFC rules *) | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]] -| RLam : ∀ Γ Δ Σ tx te l, Γ ⊢ᴛy tx : ★ -> Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] -| RCast : ∀ Γ Δ Σ σ τ γ l, Δ ⊢ᴄᴏ γ : σ ∼ τ -> Rule [Γ>Δ> Σ |- [σ@@l] ] [Γ>Δ> Σ |- [τ @@l]] +| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] +| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, +HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> + Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] | REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ] -| RAppT : ∀ Γ Δ Σ κ σ τ l, Γ ⊢ᴛy τ : κ -> Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] +| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]] | RAbsT : ∀ Γ Δ Σ κ σ l, Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]] [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]] -| RAppCo : forall Γ Δ Σ σ₁ σ₂ σ γ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> +| RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l, Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]] -| RAbsCo : ∀ Γ Δ Σ κ σ σ₁ σ₂ l, - Γ ⊢ᴛy σ₁:κ -> - Γ ⊢ᴛy σ₂:κ -> +| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l, Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] | RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ] @@ -123,16 +123,16 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r) | Flat_RNote : ∀ x y z , Rule_Flat (RNote x y z) | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l) -| Flat_RLam : ∀ Γ Δ Σ tx te q l, Rule_Flat (RLam Γ Δ Σ tx te q l) -| Flat_RCast : ∀ Γ Δ Σ σ τ γ q l, Rule_Flat (RCast Γ Δ Σ σ τ γ q l) +| Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q ) +| Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q ) | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q ) -| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q l, Rule_Flat (RAppT Γ Δ Σ κ σ τ q l) +| Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q ) | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l) -| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 q3 x ) +| 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_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e) -| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x ). +| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x). (* given a proof that uses only uniform rules, we can produce a general proof *) Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) @@ -159,12 +159,12 @@ Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h, intro. intro. induction 1; intros. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. apply IHX. destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *. @@ -178,9 +178,9 @@ Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h, inversion e. exists c1. exists c2. auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X; inversion X0; inversion H; inversion X1; destruct c; try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. + inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. Qed. Lemma no_rules_with_multiple_conclusions : forall c h, diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 493e6ce..f315603 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -10,6 +10,8 @@ Require Import NaturalDeductionToLatex. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. +Require Import HaskWeakVars. +Require Import HaskWeakTypes. Require Import HaskCoreLiterals. Require Import HaskStrongTypes. Require Import HaskStrong. @@ -29,7 +31,7 @@ Section ToLatex. | KindTypeFunction k1 k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2 | KindUnliftedType => "\text{\tt{\#}}" | KindUnboxedTuple => "\text{\tt{(\#)}}" - | KindArgType => "\text{\tt{?}}" + | KindArgType => "\text{\tt{??}}" | KindOpenType => "\text{\tt{?}}" end. @@ -47,7 +49,7 @@ Section ToLatex. | 8 => "f" | 9 => "g" | 10 => "h" - | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++(nat2string x)+++"}" + | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}" end. Close Scope nat_scope. @@ -56,51 +58,48 @@ Section ToLatex. | O => "\alpha" | S O => "\beta" | S (S O) => "\xi" - | S (S (S n)) => "\alpha_{"+++nat2string n+++"}" + | S (S (S n)) => "\alpha_{"+++n+++"}" end. Definition covar2greek (n:nat) := - "{\gamma_{"+++(nat2string n)+++"}}". + "{\gamma_{"+++n+++"}}". - Fixpoint count (n:nat) : vec nat n := - match n with - | O => vec_nil - | S n' => n':::(count n') - end. - - Fixpoint type2latex (needparens:bool)(n:nat)(t:RawHaskType nat) {struct t} : string := + (* TODO: now that PHOAS tyvar-representation-types are kind-indexed, we can do some clever stuff here *) + Fixpoint type2latex (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string := match t with - | TVar v => tyvar2greek v - | TCon tc => "\text{\tt{"+++sanitizeForLatex (tyConToString tc) +++"}}" - | TCoerc t1 t2 t => "{("+++type2latex false n t1+++"{\sim}" - +++type2latex false n t2+++")}\Rightarrow{" - +++type2latex needparens n t+++"}" - | (TApp (TApp TArrow t1) t2) => - (if needparens - then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")" - else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)) - | TArrow => "\text{\tt{(->)}}" - | TApp t1 t2 => + | TVar _ v => tyvar2greek v + | TCon tc => "\text{\tt{"+++sanitizeForLatex (toString tc) +++"}}" + | TCoerc _ t1 t2 t => "{("+++type2latex false n t1+++"{\sim}" + +++type2latex false n t2+++")}\Rightarrow{" + +++type2latex needparens n t+++"}" + | TApp _ _ t1 t2 => + match t1 with + | TApp _ _ TArrow t1 => + if needparens + then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")" + else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2) + | _ => if needparens then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")" else (type2latex true n t1)+++" "+++(type2latex false n t2) - | TFCApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (tyConToString tfc) +++"}}}"+++ - "_{"+++(nat2string n)+++"}"+++ - fold_left (fun x y => " \ "+++x+++y) - ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m) - : list string := - match lt with - | vec_nil => nil - | a:::b => (type2latex needparens n a)::(type2latex_vec needparens n _ b) - end ) - false n _ lt) "" - | TAll k f => let alpha := tyvar2greek n - in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++ - type2latex false (S n) (f n) - | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}" - end. + end + | TArrow => "\text{\tt{(->)}}" + | TAll k f => let alpha := tyvar2greek n + in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++ + type2latex false (S n) (f n) + | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}" + | TyFunApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (toString tfc) +++"}}}"+++ + "_{"+++n+++"}"+++ + fold_left (fun x y => " \ "+++x+++y) + (typeList2latex false n lt) "" + end + with typeList2latex (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string := + match t with + | TyFunApp_nil => nil + | TyFunApp_cons κ kl rhk rhkl => (type2latex needparens n rhk)::(typeList2latex needparens n rhkl) + end. - Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string := + Definition ltype2latex {Γ:TypeEnv}{κ}(t:RawHaskType (fun _ => nat) κ)(lev:list nat) : string := match lev with | nil => type2latex false O t | lv => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}" @@ -114,23 +113,37 @@ Section ToLatex. Definition enumerate {T:Type}(l:list T) := enumerate' O l. - Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ). - Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ). + Fixpoint count (n:nat) : vec nat n := + match n with + | O => vec_nil + | S n' => n':::(count n') + end. + + Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk := + match lk as LK return IList _ _ LK with + | nil => INil + | h::t => n::::(count' t (S n)) + end. + + Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv (fun _ => nat) Γ := count' Γ O. + Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ := count (length Δ). Definition judgment2latex (j:Judg) : string := match j with | mkJudg Γ Δ a b => let Γ' := InstantiatedTypeEnvString Γ in let Δ' := InstantiatedCoercionEnvString Γ Δ in - let lt2l := fun nt:nat*(LeveledHaskType Γ) => + let lt2l := fun nt:nat*(LeveledHaskType Γ ★) => let (n,lt) := nt in match lt with t @@ l => - (var2string n)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l)) + (var2string n)+++"{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ') + (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l)) end in - let lt2l' := fun lt:(LeveledHaskType Γ) => + let lt2l' := fun lt:(LeveledHaskType Γ ★) => match lt with t @@ l => - "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l)) + "e{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ') + (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l)) end in (list2latex "" lt2l "\ ,\ " (enumerate (leaves a))) +++" \ \vdash_e\ "(*+++"e{:}"*) @@ -142,63 +155,63 @@ Section ToLatex. Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string := match r with - | (RLeft _ _ c r ) => nd_urule2latex r - | (RRight _ _ c r ) => nd_urule2latex r - | (RCanL t a ) => "CanL" - | (RCanR t a ) => "CanR" - | (RuCanL t a ) => "uCanL" - | (RuCanR t a ) => "uCanR" - | (RAssoc t a b c ) => "Assoc" - | (RCossa t a b c ) => "Cossa" - | (RExch t a b ) => "Exch" - | (RWeak t a ) => "Weak" - | (RCont t a ) => "Cont" + | RLeft _ _ _ r => nd_urule2latex r + | RRight _ _ _ r => nd_urule2latex r + | RCanL _ _ => "CanL" + | RCanR _ _ => "CanR" + | RuCanL _ _ => "uCanL" + | RuCanR _ _ => "uCanR" + | RAssoc _ _ _ _ => "Assoc" + | RCossa _ _ _ _ => "Cossa" + | RExch _ _ _ => "Exch" + | RWeak _ _ => "Weak" + | RCont _ _ => "Cont" end. Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string := match r with - | RURule _ _ _ _ r => nd_urule2latex r - | RNote x n z => "Note" - | RLit Γ _ l _ => "Lit" - | RVar Γ _ σ p => "Var" - | RLam Γ _ Σ tx te p x => "Abs" - | RCast Γ _ Σ σ τ γ p x => "Cast" - | RAbsT Γ Σ κ σ a p => "AbsT" - | RAppT Γ _ Σ κ σ τ p y => "AppT" - | RAppCo Γ _ Σ _ σ₁ σ₂ σ γ p => "AppCo" - | RAbsCo Γ Σ κ σ cc σ₁ σ₂ p y q => "AbsCo" - | RApp Γ _ Σ₁ Σ₂ tx te p => "App" - | RLet Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let" - | REmptyGroup _ a => "REmptyGroup" - | RBindingGroup _ a b c d e => "RBindingGroup" - | RLetRec Γ _ p lri q => "LetRec" - | RCase Σ Γ T κlen κ ldcd τ _ => "Case" - | RBrak Σ _ a b c _ => "Brak" - | REsc Σ _ a b c _ => "Esc" + | RURule _ _ _ _ r => nd_urule2latex r + | RNote _ _ _ => "Note" + | RLit _ _ _ _ => "Lit" + | RVar _ _ _ _ => "Var" + | RLam _ _ _ _ _ _ => "Abs" + | RCast _ _ _ _ _ _ _ => "Cast" + | RAbsT _ _ _ _ _ _ => "AbsT" + | RAppT _ _ _ _ _ _ _ => "AppT" + | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo" + | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" + | RApp _ _ _ _ _ _ _ => "App" + | RLet _ _ _ _ _ _ _ => "Let" + | RBindingGroup _ _ _ _ _ _ => "RBindingGroup" + | RLetRec _ _ _ _ _ => "LetRec" + | RCase _ _ _ _ _ _ _ _ => "Case" + | RBrak _ _ _ _ _ _ => "Brak" + | REsc _ _ _ _ _ _ => "Esc" + | REmptyGroup _ _ => "REmptyGroup" end. Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool := match r with - | RLeft h c ctx r => nd_hideURule r - | RRight h c ctx r => nd_hideURule r - | RCanL t a => true - | RCanR t a => true - | RuCanL t a => true - | RuCanR t a => true - | RAssoc t a b c => true - | RCossa t a b c => true - | RExch t (T_Leaf None) b => true - | RExch t a (T_Leaf None) => true - | RWeak t (T_Leaf None) => true - | RCont t (T_Leaf None) => true - | _ => false + | RLeft _ _ _ r => nd_hideURule r + | RRight _ _ _ r => nd_hideURule r + | RCanL _ _ => true + | RCanR _ _ => true + | RuCanL _ _ => true + | RuCanR _ _ => true + | RAssoc _ _ _ _ => true + | RCossa _ _ _ _ => true + | RExch _ (T_Leaf None) b => true + | RExch _ a (T_Leaf None) => true + | RWeak _ (T_Leaf None) => true + | RCont _ (T_Leaf None) => true + | _ => false end. Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with - | RURule _ _ _ _ r => nd_hideURule r - | REmptyGroup a _ => true - | RBindingGroup _ _ _ _ _ _ => true - | _ => false + | RURule _ _ _ _ r => nd_hideURule r + | REmptyGroup _ _ => true + | RBindingGroup _ _ _ _ _ _ => true + | _ => false end. End ToLatex. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 5039004..89a0919 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -21,12 +21,12 @@ Section HaskProofToStrong. {eqdec_vv:EqDecidable VV} {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}. - Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ)(τ:Tree ??(LeveledHaskType Γ)) := + Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ ★)(τ:Tree ??(LeveledHaskType Γ ★)) := ITree _ (fun τ => Expr Γ Δ ξ τ) τ. Definition judg2exprType (j:Judg) : Type := match j with - (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ & Exprs Γ Δ ξ τ } + (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ ★ & Exprs Γ Δ ξ τ } end. (* reminder: need to pass around uniq-supplies *) @@ -43,12 +43,12 @@ Section HaskProofToStrong. | RNote x n z => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ p => let case_RVar := tt in _ - | RLam Γ Δ Σ tx te p x => let case_RLam := tt in _ - | RCast Γ Δ Σ σ τ γ p x => let case_RCast := tt in _ + | RLam Γ Δ Σ tx te x => let case_RLam := tt in _ + | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _ | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ - | RAppT Γ Δ Σ κ σ τ p y => let case_RAppT := tt in _ - | RAppCo Γ Δ Σ κ σ₁ σ₂ σ γ p => let case_RAppCo := tt in _ - | RAbsCo Γ Δ Σ κ σ cc σ₁ σ₂ p y => let case_RAbsCo := tt in _ + | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _ + | 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 _ | RLetRec Γ p lri x y => let case_RLetRec := tt in _ @@ -142,7 +142,7 @@ Section HaskProofToStrong. apply rest2. Defined. - Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ & Expr Γ Δ ξ τ }. + Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }. intro pf. set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd. apply closed2expr in cnd. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 50e7ab3..b7229d0 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -8,6 +8,7 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. +Require Import HaskWeakVars. Require Import HaskCoreTypes. Require Import HaskCoreLiterals. Require Import HaskStrongTypes. @@ -18,8 +19,9 @@ Section HaskStrong. Context `{EQD_VV:EqDecidable VV}. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:vec (HaskType Γ) tc} := - { scbwv_sac : @StrongAltCon tc + + Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{sac:@StrongAltCon tc}{atypes:IList _ (HaskType Γ) (tyConKind sac)} := + { scbwv_sac := sac ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac) ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes) ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list @@ -28,25 +30,27 @@ Section HaskStrong. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon. - Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type := + Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) - | ELam : ∀ Γ Δ ξ t1 t2 l ev, Γ ⊢ᴛy t1:★ ->Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) - | ECast : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 -> Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) + | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, + Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t - | ETyApp : ∀ Γ Δ κ σ τ ξ l, Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l) - | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l) - | ECoApp : ∀ Γ Δ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) + | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l) + | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, + Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l) + | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, + Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) | ETyLam : ∀ Γ Δ ξ κ σ l, Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) - - | ECase : forall Γ Δ ξ l tc atypes tbranches, + | ECase : forall Γ Δ ξ l tc tbranches sac atypes, Expr Γ Δ ξ (caseType tc atypes @@ l) -> - Tree ??{ scb : StrongCaseBranchWithVVs tc atypes + Tree ??{ scb : StrongCaseBranchWithVVs tc sac atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) @@ -59,7 +63,7 @@ Section HaskStrong. Expr Γ Δ ξ (τ@@l) (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *) - with ELetRecBindings : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ) -> Type := + with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type := | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l [] | ELR_leaf : ∀ Γ Δ ξ t l v, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)] | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index c0a0bb3..18e7825 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -21,9 +21,9 @@ Section HaskStrongToProof. (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform * expansion on an entire uniform proof *) -Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) +Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)). -Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ)) +Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)). Definition pivotContext {Γ}{Δ} a b c τ : @@ -75,27 +75,27 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) - | ELam Γ Δ ξ t1 t2 lev v pf e => stripOutVars (v::nil) (expr2antecedent e) + | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e) | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev)) | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e - | ECast Γ Δ ξ γ t1 t2 lev wfco e => expr2antecedent e + | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e | ENote Γ Δ ξ t n e => expr2antecedent e | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => expr2antecedent e - | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => expr2antecedent e - | ETyApp Γ Δ κ σ τ ξ l pf e => expr2antecedent e + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e + | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e + | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e | ELetRec Γ Δ ξ l τ vars branches body => let branch_context := eLetRecContext branches in let all_contexts := (expr2antecedent body),,branch_context in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts - | ECase Γ Δ ξ lev tc avars tbranches e' alts => + | ECase Γ Δ ξ l tc tbranches sac atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc avars + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) - (weakLT' (tbranches@@lev)) } + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) } ): Tree ??VV := match alts with | T_Leaf None => [] @@ -129,8 +129,8 @@ Definition judgFromEStrongAltCon Implicit Arguments caseBranchRuleInfoFromEStrongAltCon [ [Γ] [Δ] [ξ] [lev] [tc] [avars] [tbranches] ]. *) -Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. -Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ) := +Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ ★) : HaskType Γ ★ := match lht with t @@ l => t end. +Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev] @@ -144,7 +144,7 @@ Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) end. -Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ):= +Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):= match elrb with | ELR_nil Γ Δ ξ lev => [] | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)] @@ -154,7 +154,7 @@ Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ le Lemma stripping_nothing_is_inert {Γ:TypeEnv} - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) tree : stripOutVars nil tree = tree. induction tree. @@ -175,7 +175,7 @@ Definition arrangeContext v (* variable to be pivoted, if found *) ctx (* initial context *) τ (* type of succedent *) - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) : (* a proof concluding in a context where that variable does not appear *) @@ -352,10 +352,10 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, Definition update_ξ'' {Γ} ξ tree lev := (update_ξ ξ - (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) (leaves tree))). -Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree lev : +Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev : mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). induction tree; simpl in *; try reflexivity; auto. @@ -391,7 +391,7 @@ Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree Lemma updating_stripped_tree_is_inert' {Γ} lev - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) tree tree2 : mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2) = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2). @@ -400,7 +400,7 @@ admit. Lemma updating_stripped_tree_is_inert'' {Γ} - (ξ:VV -> LeveledHaskType Γ) + (ξ:VV -> LeveledHaskType Γ ★) v tree lev : mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree) = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree). @@ -467,7 +467,7 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches Defined. -Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ) tree z lev, +Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev, mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z. admit. Qed. @@ -487,7 +487,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : intro pf. intro lrsp. set ((update_ξ ξ - (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩) + (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩) (leaves tree)))) as ξ' in *. set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. set (mapOptionTree (@fst _ _) tree) as pctx. @@ -549,7 +549,7 @@ Definition expr2proof : | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in let e1' := expr2proof _ _ _ _ e1 in let e2' := expr2proof _ _ _ _ e2 in _ - | ELam Γ Δ ξ t1 t2 lev v pf e => let case_ELam := tt in + | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in let e' := expr2proof _ _ _ _ e in _ | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in let pf_let := (expr2proof _ _ _ _ ev) in @@ -557,7 +557,7 @@ Definition expr2proof : | ELetRec Γ Δ ξ lev t tree branches ebody => let e' := expr2proof _ _ _ _ ebody in let ξ' := update_ξ'' ξ tree lev in - let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'')) + let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' := match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with @@ -569,13 +569,13 @@ Definition expr2proof : let case_ELetRec := tt in _ | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _ | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _ - | ECast Γ Δ ξ γ t1 t2 lev wfco e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _ + | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _ | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _ | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ - | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ETyApp Γ Δ κ σ τ ξ l pf e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ - | ECase Γ Δ ξ lev tbranches tc avars e alts => + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _ + | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _ + | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _ + | ECase Γ Δ ξ l tc tbranches sac atypes e alts => (* let dcsp := ((fix mkdcsp (alts: @@ -629,7 +629,6 @@ Definition expr2proof : apply n. auto. inversion H. - apply pf. destruct case_ELet; intros. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -662,7 +661,7 @@ Definition expr2proof : apply e'. destruct case_ECast. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast with (γ:=γ)]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ]. apply e'. auto. @@ -679,11 +678,9 @@ Definition expr2proof : destruct case_ECoLam; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. apply e'. - auto. - auto. destruct case_ECoApp; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) σ₁ σ₂ σ γ l) ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index d5eeecf..759dcb9 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -22,35 +22,36 @@ CoInductive Fresh A T := ; split : Fresh A T * Fresh A T }. -Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))(rht:RawHaskType WeakTypeVar) {struct rht} : WeakType := +Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) + {struct rht} : WeakType := match rht with - | TVar v => WTyVarTy v + | TVar _ v => WTyVarTy v | TCon tc => WTyCon tc - | TCoerc t1 t2 t3 => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3) + | TCoerc _ t1 t2 t3 => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3) | TArrow => WFunTyCon - | TApp t1 t2 => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) + | TApp _ _ t1 t2 => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) | TAll k rht' => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv)) | TCode t1 t2 => match (rawHaskTypeToWeakType f t1) with | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2) | impossible => impossible (* TODO: find a way to convince Coq this can't happen *) end - | TFCApp tfc tls => WTyFunApp tfc ((fix rawHaskTypeToWeakTypeVec n v : list WeakType := - match v with - | vec_nil => nil - | a:::b => (rawHaskTypeToWeakType f a)::(rawHaskTypeToWeakTypeVec _ b) - end) _ tls) + | TyFunApp tfc tls => WTyFunApp tfc (rawHaskTypeListToWeakType f tls) +end +with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) := +match rht with + | TyFunApp_nil => nil + | TyFunApp_cons κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl') end. - Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)) - {Γ}(τ:HaskType Γ)(φ:InstantiatedTypeEnv WeakTypeVar Γ) : WeakType := + {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType := rawHaskTypeToWeakType f (τ _ φ). -Variable unsafeCoerce : WeakCoercion. - Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce". +Variable unsafeCoerce : WeakCoercion. Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce". -Definition strongCoercionToWeakCoercion {Γ}{Δ}(τ:HaskCoercion Γ Δ)(φ:InstantiatedTypeEnv WeakTypeVar Γ) : WeakCoercion. +Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) + : WeakCoercion. unfold HaskCoercion in τ. admit. Defined. @@ -63,41 +64,45 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH} Defined. *) -Definition updateITE {Γ:TypeEnv}{TV:Type}(tv:TV){κ}(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) - := tv:::ite. +Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) + := tv::::ite. Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) (exp:@Expr WeakExprVar _ Γ Δ ξ lev) - : InstantiatedTypeEnv WeakTypeVar Γ -> WeakExpr := -match exp as E in Expr G D X L return InstantiatedTypeEnv WeakTypeVar G -> WeakExpr with + : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr := +match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with | EVar _ _ _ ev => fun ite => WEVar ev | ELit _ _ _ lit _ => fun ite => WELit lit | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) -| ELam Γ' _ _ _ _ _ cv _ e => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite) +| ELam Γ' _ _ _ _ _ cv e => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite) | ELet Γ' _ _ _ _ _ ev e1 e2 => fun ite => WELet ev (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) | EEsc Γ' _ _ ec t _ e => fun ite => WEEsc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) | EBrak Γ' _ _ ec t _ e => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) -| ECast _ _ _ γ _ τ _ _ e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) +| ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) | ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite) -| ETyApp _ _ _ _ τ _ _ _ e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite) -| ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite) (strongExprToWeakExpr ftv fcv e ite) -| ECoApp _ _ γ _ _ _ _ _ _ e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) -| ECase Γ Δ ξ l tc atypes tbranches e alts => - fun ite => WECase (strongExprToWeakExpr ftv fcv e ite) - (@typeToWeakType ftv Γ tbranches ite) tc (map (fun t => typeToWeakType ftv t ite) (vec2list atypes)) +| ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite) +| ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite) +| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) +| ECase Γ Δ ξ l tc tbranches sac atypes e alts => + fun ite => WECase + (strongExprToWeakExpr ftv fcv e ite) + (@typeToWeakType ftv Γ _ tbranches ite) + tc + (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes)) ((fix caseBranches - (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes + (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) - (update_ξ (weakLT'○ξ) (vec2list (vec_map (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb)))) + (update_ξ (weakLT'○ξ) (vec2list (vec_map + (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb)))) (weakLT' (tbranches@@l)) }) : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) := match tree with | T_Leaf None => [] | T_Leaf (Some x) => let (scb,e) := x in -(* [(sac_altcon scb, + (*[(sac_altcon scb, nil, (* FIXME *) nil, (* FIXME *) (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *) @@ -107,17 +112,18 @@ match exp as E in Expr G D X L return InstantiatedTypeEnv WeakTypeVar G -> WeakE ) alts) | ETyLam _ _ _ k _ _ e => fun ite => let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite)) -| ECoLam _ _ k _ t1 t2 _ _ _ _ e => fun ite => - let t1' := typeToWeakType ftv t1 ite in - let t2' := typeToWeakType ftv t2 ite in +| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => + let t1' := typeToWeakType ftv σ₁ ite in + let t2' := typeToWeakType ftv σ₂ ite in let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite) end with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{lev}{vars} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars) - : InstantiatedTypeEnv WeakTypeVar Γ -> Tree ??(WeakExprVar * WeakExpr) := -match elrb as E in ELetRecBindings G D X L V return InstantiatedTypeEnv WeakTypeVar G -> Tree ??(WeakExprVar * WeakExpr) with + : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) := +match elrb as E in ELetRecBindings G D X L V + return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with | ELR_nil _ _ _ _ => fun ite => [] | ELR_leaf _ _ _ _ cv v e => fun ite => [(v,(strongExprToWeakExpr ftv fcv e ite))] | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite) diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 916afe1..87d02a1 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -15,20 +15,12 @@ Require Import HaskWeakTypes. Require Import HaskWeakVars. (* FIXME *) Require Import HaskCoreToWeak. (* FIXME *) -Variable CoFunConst : nat -> Type. (* FIXME *) -Variable TyFunConst : nat -> Type. (* FIXME *) - -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 dataConOrigArgTys_:CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_ =>"DataCon.dataConOrigArgTys". -Variable getTyConTyVars_ : TyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars". +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 dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". (* FIXME: might be a better idea to panic here than simply drop things that look wrong *) -Definition tyConTyVars (tc:TyCon) := - filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). - Opaque tyConTyVars. Definition dataConExTyVars cdc := filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). Opaque dataConExTyVars. @@ -81,33 +73,40 @@ Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc). right; auto. Defined. +Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc). + (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) Section Raw. (* TV is the PHOAS type which stands for type variables of System FC *) - Context {TV:Type}. + Context {TV:Kind -> Type}. (* Figure 7: ρ, σ, τ, ν *) - Inductive RawHaskType : Type := - | TVar : TV -> RawHaskType (* a *) - | TCon : TyCon -> RawHaskType (* T *) - | TArrow : RawHaskType (* (->) *) - | TCoerc : RawHaskType -> RawHaskType -> RawHaskType -> RawHaskType (* (+>) *) - | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) - | TFCApp : forall tc:TyCon, vec RawHaskType tc -> RawHaskType (* S_n *) - | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) - | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). + Inductive RawHaskType : Kind -> Type := + | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *) + | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *) + | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *) + | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *) + | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *) + | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *) + | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *) + | TyFunApp : ∀ tf, RawHaskTypeList (fst (tyFunKind tf)) -> RawHaskType (snd (tyFunKind tf)) (* S_n *) + with RawHaskTypeList : list Kind -> Type := + | TyFunApp_nil : RawHaskTypeList nil + | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl). (* the "kind" of a coercion is a pair of types *) - Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind. + Inductive RawCoercionKind : Type := + mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind. Section CV. (* the PHOAS type which stands for coercion variables of System FC *) - Context {CV:Type}. + (* Figure 7: γ, δ *) - Inductive RawHaskCoer : Prop := + Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *). +(* | CoVar : CV -> RawHaskCoer (* g *) | CoType : RawHaskType -> RawHaskCoer (* τ *) | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) @@ -119,21 +118,23 @@ Section Raw. | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) | CoRight : RawHaskCoer -> RawHaskCoer (* right *). - +*) End CV. End Raw. Implicit Arguments TCon [ [TV] ]. -Implicit Arguments TFCApp [ [TV] ]. +Implicit Arguments TyFunApp [ [TV] ]. Implicit Arguments RawHaskType [ ]. Implicit Arguments RawHaskCoer [ ]. Implicit Arguments RawCoercionKind [ ]. +Implicit Arguments TVar [ [TV] [κ] ]. +Implicit Arguments TCoerc [ [TV] [κ] ]. +Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ]. +Implicit Arguments TAll [ [TV] ]. Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))). Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)). - - (* Kind and Coercion Environments *) (* * In System FC, the environment consists of three components, each of @@ -145,56 +146,73 @@ Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV e *) Definition TypeEnv := list Kind. -Definition InstantiatedTypeEnv (TV:Type) (Γ:TypeEnv) := vec TV (length Γ). +Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ. Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV. -Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ). -Definition InstantiatedCoercionEnv (TV CV:Type)(Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ). - +Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ). +Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ). (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *) -Definition HaskTyVar (Γ:TypeEnv) := forall TV (env:@InstantiatedTypeEnv TV Γ), TV. -Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV. -Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ). -Definition HaskType (Γ:TypeEnv) := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV. -Definition HaskCoercion Γ Δ := ∀ TV CV, - @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> RawHaskCoer TV CV. -Inductive LeveledHaskType (Γ:TypeEnv) := mkLeveledHaskType : HaskType Γ -> HaskLevel Γ -> LeveledHaskType Γ. -Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) := fun TV env => vec_head env. -Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : HaskType Γ +Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ. +Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV. +Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★). +Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ. +Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite). + +Inductive HaskTypeOfSomeKind (Γ:TypeEnv) := + haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ. + Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ]. + Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) := + match htosk with + haskTypeOfSomeKind κ _ => κ + end. + Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind. + Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk := + match htosk as H return HaskType Γ H with + haskTypeOfSomeKind _ ht => ht + end. + Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType. + +Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ), + @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite). +Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ. +Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env. +Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★ := fun TV env => TAll κ (σ TV env). -Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ +Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) + (cv:HaskTyVar Γ κ) : HaskType Γ ★ := fun TV env => σ TV env (cv TV env). -Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env). -Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ := fun TV ite => TCon tc. -Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite). -Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ := - fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite). -Definition unMkHaskCoercionKind {Γ}(hck:HaskCoercionKind Γ) : (HaskType Γ * HaskType Γ) := - ((fun TV ite => match (hck TV ite) with mkRawCoercionKind t1 _ => t1 end), - (fun TV ite => match (hck TV ite) with mkRawCoercionKind _ t2 => t2 end)). - +Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:= + fun TV env => @TCode TV (TVar (v TV env)) (t TV env). +Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc)) + := fun TV ite => TCon tc. +Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ := + fun TV ite => TApp (t1 TV ite) (t2 TV ite). +Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ := + fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite). (* PHOAS substitution on types *) -Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(v:@HaskType Γ) : @HaskType Γ - := fun TV env => - (fix flattenT (exp: RawHaskType (RawHaskType TV)) : RawHaskType TV := +Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁) + : @HaskType Γ κ₂ := +fun TV env => + (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ := match exp with - | TVar x => x - | TAll k y => TAll k (fun v => flattenT (y (TVar v))) - | TApp x y => TApp (flattenT x) (flattenT y) + | TVar _ x => x + | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v))) + | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y) | TCon tc => TCon tc - | TCoerc t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t) + | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t) | TArrow => TArrow - | TCode v e => TCode (flattenT v) (flattenT e) - | TFCApp tfc lt => TFCApp tfc - ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n := - match expv in vec _ N return vec (RawHaskType TV) N with - | vec_nil => vec_nil - | x:::y => (flattenT x):::(flatten_vec _ y) - end) _ lt) - end) - (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)). -Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20). + | TCode v e => TCode (flattenT _ v) (flattenT _ e) + | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt) + end + with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk := + match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with + | TyFunApp_nil => TyFunApp_nil + | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest) + end + for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)). + +Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20). Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20). Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). @@ -204,22 +222,17 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). - - - - - - - (* yeah, things are kind of messy below this point *) -Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite. +Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) + := ilist_tail ite. Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) := map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ. -Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) - : InstantiatedTypeEnv TV (κ::Γ) := tv:::env. -Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:InstantiatedCoercionEnv TV CV Γ Δ)(tv:TV)(κ:Kind) +Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ) + : InstantiatedTypeEnv TV (κ::Γ) := tv::::env. +Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type} + (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ) : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ). simpl. unfold InstantiatedCoercionEnv. @@ -228,9 +241,7 @@ Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV CV:Type}(env:Ins rewrite <- map_preserves_length. apply env. Defined. -Definition typeEnvContainsType {Γ}{TV:Type}(env:InstantiatedTypeEnv TV Γ)(tv:TV)(κ:Kind) : Prop - := @vec_In _ _ (tv,κ) (vec_zip env (list2vec Γ)). -Definition coercionEnvContainsCoercion {Γ}{Δ}{TV CV:Type}(ite:InstantiatedTypeEnv TV Γ) +Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ) (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV) := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))). Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ := @@ -242,46 +253,40 @@ Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:Instanti unfold InstantiatedCoercionEnv; simpl. apply vec_cons; auto. Defined. -Notation "env ∋ tv : κ" := (@typeEnvContainsType _ _ env tv κ). -Notation "env '+' tv : κ" := (@addKindToInstantiatedTypeEnv _ _ env tv κ). - (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *) -Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := vec_tail ite. +Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ + := ilist_tail ite. Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ. induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined. -Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ. -Definition weakV {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (κ::Γ) := fun TV ite => (cv' TV (weakITE ite)). -Definition weakV' {Γ:TypeEnv}{κ}(cv':HaskTyVar Γ) : HaskTyVar (app κ Γ). +Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) + := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ. +Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv + := fun TV ite => (cv' TV (weakITE ite)). +Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv. induction κ; auto. apply weakV; auto. Defined. -Definition weakT {Γ:TypeEnv}{κ:Kind}(lt:HaskType Γ) : HaskType (κ::Γ) := fun TV ite => lt TV (weakITE ite). -Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt. -Definition weakT' {Γ}{κ}(lt:HaskType Γ) : HaskType (app κ Γ). +Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ + := fun TV ite => lt TV (weakITE ite). +Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) + := map weakV lt. +Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂. induction κ; auto. apply weakT; auto. Defined. -Definition weakT'' {Γ}{κ}(lt:HaskType Γ) : HaskType (app Γ κ). -unfold HaskType in *. -unfold InstantiatedTypeEnv in *. -intros. -apply vec_chop in X. -apply lt. -apply X. -Defined. -Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (app b c)). -rewrite <- ass_app in lt. -exact lt. -Defined. -Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ) := - let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT t1) (weakT t2). -Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ) := - let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT' t1) (weakT' t2). -Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := -match κ as K return list (HaskCoercionKind (app K Γ)) with - | nil => hck - | _ => map weakCK' hck -end. +Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂. + unfold HaskType in *. + unfold InstantiatedTypeEnv in *. + intros. + apply ilist_chop in X. + apply lt. + apply X. + Defined. +Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ. + rewrite <- ass_app in lt. + exact lt. + Defined. Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ). induction κ; auto. apply weakL; auto. Defined. -Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end. -Definition weakLT' {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (app κ Γ) +Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ + := match lt with t @@ l => weakT t @@ weakL l end. +Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂ := match lt with t @@ l => weakT' t @@ weakL' l end. Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ). induction κ; auto. apply weakCE; auto. Defined. @@ -295,108 +300,101 @@ Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:Instantiated rewrite <- map_preserves_length in ice. apply ice. Defined. -Definition weakICE' {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (app κ Γ) (weakCE' Δ)) - : InstantiatedCoercionEnv TV CV Γ Δ. - induction κ; auto. apply IHκ. eapply weakICE. apply ice. Defined. +Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ). + unfold HaskCoercionKind in *. + intros. + apply hck; clear hck. + inversion X; subst; auto. + Defined. +Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ). + induction κ; auto. + apply weakCK. + apply IHκ. + Defined. +Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := + match κ as K return list (HaskCoercionKind (app K Γ)) with + | nil => hck + | _ => map weakCK' hck + end. Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)). -Definition weakC {Γ}{κ}{Δ}(c:HaskCoercion Γ Δ) : HaskCoercion (κ::Γ) (weakCE Δ) := - fun TV CV ite ice => c TV CV (weakITE ite) (weakICE ice). -Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV) : - forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV +Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : + forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂ := fun TV ite tv => (f TV (weakITE ite) tv). +(* I keep mixing up left/right folds *) +(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *) +(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*) + +Fixpoint caseType0 {Γ}(lk:list Kind) : + IList _ (HaskType Γ) lk -> + HaskType Γ (fold_right KindTypeFunction ★ lk) -> + HaskType Γ ★ := + match lk as LK return + IList _ (HaskType Γ) LK -> + HaskType Γ (fold_right KindTypeFunction ★ LK) -> + HaskType Γ ★ + with + | nil => fun _ ht => ht + | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env)) + end. + +Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ := + caseType0 (tyConKind tc) atypes (fun TV env => TCon tc). + (* like a GHC DataCon, but using PHOAS representation for types and coercions *) Record StrongAltCon {tc:TyCon} := -{ sac_altcon : AltCon +{ sac_tc := tc +; sac_altcon : AltCon ; sac_numExTyVars : nat ; sac_numCoerVars : nat ; sac_numExprVars : nat -; sac_akinds : vec Kind tc ; sac_ekinds : vec Kind sac_numExTyVars -; sac_kinds := app (vec2list sac_akinds) (vec2list sac_ekinds) -; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ -; sac_coercions : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars -; sac_types : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskType (sac_Γ Γ)) sac_numExprVars -; sac_Δ := fun Γ (atypes:vec (HaskType Γ) tc) Δ => app (vec2list (sac_coercions Γ atypes)) Δ +; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds) +; sac_Γ := fun Γ => app (tyConKind tc) Γ +; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars +; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars +; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ }. +Coercion sac_tc : StrongAltCon >-> TyCon. Coercion sac_altcon : StrongAltCon >-> AltCon. + -Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) := - fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). - +Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ. -(***************************************************************************************************) -(* Well-Formedness of Types and Coercions *) -(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *) -Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type := - mkTFD : Kind -> TypeFunctionDecl tfc vk. +Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil. +Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★. + set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z. + unfold tyConKind' in z. + rewrite literal_tycons_are_of_ordinary_kind in z. + unfold HaskType. + apply z. + Defined. -(* Figure 8, upper half *) -Inductive WellKinded_RawHaskType (TV:Type) - : forall Γ:TypeEnv, InstantiatedTypeEnv TV Γ -> RawHaskType TV -> Kind -> Prop := - | WFTyVar : forall Γ env κ d, - env∋d:κ -> - WellKinded_RawHaskType TV Γ env (TVar d) κ - | WFTyApp : forall Γ env κ₁ κ₂ σ₁ σ₂, - WellKinded_RawHaskType TV Γ env σ₁ (κ₁ ⇛ κ₂) -> - WellKinded_RawHaskType TV Γ env σ₂ κ₂ -> - WellKinded_RawHaskType TV Γ env (TApp σ₁ σ₂) κ₂ - | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ , - (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) -> - WellKinded_RawHaskType TV _ env (TAll κ σ) ★ - | TySCon : forall Γ env tfc lt vk ι , - @TypeFunctionDecl tfc vk -> - ListWellKinded_RawHaskType TV Γ _ env lt vk -> - WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι -with ListWellKinded_RawHaskType (TV:Type) - : forall (Γ:TypeEnv) n, InstantiatedTypeEnv TV Γ -> vec (RawHaskType TV) n -> vec Kind n -> Prop := - | ListWFRawHaskTypenil : forall Γ env, - ListWellKinded_RawHaskType TV Γ 0 env vec_nil vec_nil - | ListWFRawHaskTypecons : forall Γ env n t k lt lk, - WellKinded_RawHaskType TV Γ env t k -> - ListWellKinded_RawHaskType TV Γ n env lt lk -> - ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk). - -Variable kindOfTyCon : forall (tc:TyCon), Kind. - Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")". - -Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind := -match rht with - | TVar k => OK k - | TCon tc => OK (kindOfTyCon tc) - | TCoerc t1 t2 t => OK (★ ⇛ ★ ) - | TArrow => OK (★ ⇛ ★ ⇛ ★ ) - | TApp ht1 ht2 => kindOfRawHaskType ht1 >>= fun k1 => - kindOfRawHaskType ht2 >>= fun k2 => - match k1 with - | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch" - | _ => Error "attempt to apply a non-functional kind" - end - | TFCApp tc rht' => Error "calculating kind of TFCApp is not yet implemented" - | TAll k t' => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k') - | TCode t1 t2 => OK ★ -end. +Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18). -Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ := - list2vec Γ. +Fixpoint update_ξ + `{EQD_VV:EqDecidable VV}{Γ} + (ξ:VV -> LeveledHaskType Γ ★) + (vt:list (VV * LeveledHaskType Γ ★)) + : VV -> LeveledHaskType Γ ★ := + match vt with + | nil => ξ + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' + end. -Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind := - kindOfRawHaskType (ht Kind (kindITE Γ)). -Definition WellKindedHaskType Γ (ht:HaskType Γ) κ := - forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ. - Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ). -(* "decl", production for "axiom" *) -Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type := -{ axd_τ : vec TV n -> RawHaskType TV -; axd_σ : vec TV n -> RawHaskType TV -}. +(***************************************************************************************************) +(* Well-Formedness of Types and Coercions *) +(* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *) +Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type := + mkTFD : Kind -> TypeFunctionDecl tfc vk. +(* Section WFCo. - Context {TV:Type}. + Context {TV:Kind->Type}. Context {CV:Type}. (* local notations *) @@ -420,7 +418,7 @@ Section WFCo. | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t (* | SComp :∀ Γ Δ t e γ n S σ τ κ, - ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t + ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV), ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) -> ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) -> @@ -453,14 +451,124 @@ Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:Hask forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ), @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)). Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b). +*) + + + + +(* Decidable equality on PHOAS types *) +Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool := +match t1 with +| TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end +| TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end +| TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end +| TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end +| TArrow => match t2 with TArrow => true | _ => false end +| TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end +| TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end +| TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end +end +with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool := +match t1 with +| TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end +| TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end +end. + +Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk := +match lk as LK return IList _ _ LK with + | nil => INil + | h::t => n::::(count' t (S n)) +end. -Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). +Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) := + compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)). + +(* This is not provable in Coq's logic because the Coq function space + * is "too big" - although its only definable inhabitants are Coq + * functions, it is not provable in Coq that all function space + * inhabitants are definable (i.e. there are no "exotic" inhabitants). + * This is actually an important feature of Coq: it lets us reason + * about properties of non-computable (non-recursive) functions since + * any property proven to hold for the entire function space will hold + * even for those functions. However when representing binding + * structure using functions we would actually prefer the smaller + * function-space of *definable* functions only. These two axioms + * assert that. *) +Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ), + if compareHT Γ κ ht1 ht2 + then ht1=ht2 + else ht1≠ht2. +Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ), + if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2) + then htv1=htv2 + else htv1≠htv2. + +(* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *) +Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ). + apply Build_EqDecidable. + intros. + set (compareHT_decides _ _ v1 v2) as z. + set (compareHT Γ κ v1 v2) as q. + destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *. + left; auto. + right; auto. + Defined. -Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). +Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ). + apply Build_EqDecidable. + intros. + set (compareVars _ _ v1 v2) as z. + set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q. + destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *. + left; auto. + right; auto. + Defined. -Fixpoint update_ξ - `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ := - match vt with - | nil => ξ - | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' +Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ). + apply Build_EqDecidable. + intros. + unfold HaskLevel in *. + apply (eqd_dec v1 v2). + Defined. + + + + + +(* ToString instance for PHOAS types *) +Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string := + match t with + | TVar _ v => "tv" +++ v + | TCon tc => toString tc + | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~" + +++typeToString' false n t2+++")=>" + +++typeToString' needparens n t + | TApp _ _ t1 t2 => + match t1 with + | TApp _ _ TArrow t1 => + if needparens + then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")" + else (typeToString' true n t1)+++"->"+++(typeToString' true n t2) + | _ => + if needparens + then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")" + else (typeToString' true n t1)+++" "+++(typeToString' false n t2) + end + | TArrow => "(->)" + | TAll k f => let alpha := "tv"+++n + in "(forall "+++ alpha +++ "{:}"+++ k +++")"+++ + typeToString' false (S n) (f n) + | TCode ec t => "<["+++(typeToString' true n ec)+++"]>@"+++(typeToString' false n t) + | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]" + end + with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string := + match t with + | TyFunApp_nil => nil + | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl) end. + +Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string := + typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)). + +Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) := + { toString := typeToString }. diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 31accd2..537bfbe 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -104,17 +104,17 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' => match t' with | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2 - | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp") + | _ => Error ("found non-function type "+++t'+++" in EApp") end | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with | WForAllTy v ct => OK (replaceWeakTypeVar ct v t) - | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp") + | _ => Error ("found non-forall type "+++te+++" in ETyApp") end | WECoApp e co => weakTypeOfWeakExpr e >>= fun te => match te with | WCoFunTy t1 t2 t => OK t - | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp") + | _ => Error ("found non-coercion type "+++te+++" in ETyApp") end | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t') | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t') diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 13fe7a5..e70e17d 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -17,17 +17,23 @@ Require Import HaskWeak. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreTypes. +Require Import HaskCoreVars. -Definition upφ {Γ}(tv:WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) : (WeakTypeVar -> HaskTyVar ((tv:Kind)::Γ)) := - fun tv' => - if eqd_dec tv tv' - then FreshHaskTyVar (tv:Kind) - else fun TV ite => φ tv' TV (weakITE ite). - +Open Scope string_scope. +Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt. +Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ. +Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). + unfold TyVarResolver. + refine (fun tv' => + if eqd_dec tv tv' + then let fresh := @FreshHaskTyVar Γ tv in _ + else fun TV ite => φ tv' TV (weakITE ite)). + rewrite <- _H; apply fresh. + Defined. -Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) - : (WeakTypeVar -> HaskTyVar (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). +Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) + : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). induction tvs. apply φ. simpl. @@ -35,56 +41,35 @@ Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) apply IHtvs. Defined. -Open Scope string_scope. - -Fixpoint weakTypeToType {Γ:TypeEnv}(φ:WeakTypeVar -> HaskTyVar Γ)(t:WeakType) : HaskType Γ := - match t with - | WTyVarTy v => fun TV env => @TVar TV (φ v TV env) - | WCoFunTy t1 t2 t3 => (weakTypeToType φ t1) ∼∼ (weakTypeToType φ t2) ⇒ (weakTypeToType φ t3) - | WFunTyCon => fun TV env => TArrow - | WTyCon tc => fun TV env => TCon tc - | WTyFunApp tc lt => fun TV env => fold_left TApp (map (fun t => weakTypeToType φ t TV env) lt) (TCon tc) (* FIXME *) - | WClassP c lt => fun TV env => fold_left TApp (map (fun t=> weakTypeToType φ t TV env) lt) (TCon (classTyCon c)) - | WIParam _ ty => weakTypeToType φ ty - | WForAllTy wtv t => (fun TV env => TAll (wtv:Kind) (fun tv => weakTypeToType (@upφ Γ wtv φ) t TV (tv:::env))) - | WAppTy t1 t2 => fun TV env => TApp (weakTypeToType φ t1 TV env) (weakTypeToType φ t2 TV env) - | WCodeTy ec tbody => fun TV env => TCode (TVar (φ ec TV env)) (weakTypeToType φ tbody TV env) - end. - - -Definition substPhi0 {Γ:TypeEnv}(κ:Kind)(θ:HaskType Γ) : HaskType (κ::Γ) -> HaskType Γ. +Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'. intro ht. refine (substT _ θ). clear θ. unfold HaskType in ht. intros. apply ht. - apply vec_cons; [ idtac | apply env ]. + apply ICons; [ idtac | apply env ]. apply X. Defined. -Definition substPhi {Γ:TypeEnv}(κ:list Kind)(θ:vec (HaskType Γ) (length κ)) : HaskType (app κ Γ) -> HaskType Γ. - induction κ. +Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. + induction lk. intro q; apply q. simpl. intro q. - apply IHκ. + apply IHlk. inversion θ; subst; auto. inversion θ; subst. - apply (substPhi0 _ (weakT' X) q). - Defined. - -Definition substφ {Γ}{n}(ltypes:vec (HaskType Γ) n)(Γ':vec _ n)(ht:HaskType (app (vec2list Γ') Γ)) : HaskType Γ. - apply (@substPhi Γ (vec2list Γ')). - rewrite vec2list_len. - apply ltypes. - apply ht. + eapply substPhi. + eapply weakT'. + apply X. + apply q. Defined. (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *) Record StrongAltConPlusJunk {tc:TyCon} := { sacpj_sac : @StrongAltCon tc -; sacpj_φ : forall Γ (φ:WeakTypeVar -> HaskTyVar Γ ), (WeakTypeVar -> HaskTyVar (sac_Γ sacpj_sac Γ)) +; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ)) ; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ), (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))) }. @@ -92,11 +77,11 @@ Implicit Arguments StrongAltConPlusJunk [ ]. Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. (* yes, I know, this is really clumsy *) -Variable emptyφ : WeakTypeVar -> HaskTyVar nil. +Variable emptyφ : TyVarResolver nil. Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")". Definition mkPhi (lv:list WeakTypeVar) - : (WeakTypeVar -> HaskTyVar (map (fun x:WeakTypeVar => x:Kind) lv)). + : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). set (upφ'(Γ:=nil) lv emptyφ) as φ'. rewrite <- app_nil_end in φ'. apply φ'. @@ -105,10 +90,134 @@ Definition mkPhi (lv:list WeakTypeVar) Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)). Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)). +Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ. +Notation " ` x " := (@fixkind _ x) (at level 100). + +Ltac matchThings T1 T2 S := + destruct (eqd_dec T1 T2) as [matchTypeVars_pf|]; + [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ]. + +Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★). + intros. + unfold InstantiatedTypeEnv in ite. + apply X. + apply (X0::::ite). + Defined. + +Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★. + intro. + unfold HaskType. + intros. + apply (TAll κ). + eapply mkTAll'. + apply X. + apply X0. + Defined. + +Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ). + refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) := + match t with + | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow)) + | WTyCon tc => let case_WTyCon := tt in _ + | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented" + | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented" + | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _ + | WTyVarTy v => let case_WTyVarTy := tt in _ + | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _ + | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => _ + | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in + weakTypeToType _ φ t1 >>= fun t1' => + weakTypeToType _ φ t2 >>= fun t2' => + weakTypeToType _ φ t3 >>= fun t3' => _ + | WTyFunApp tc lt => + ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType) + { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) := + match lt with + | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with + | nil => OK (fun TV _ => TyFunApp_nil) + | _ => Error "WTyFunApp not applied to enough types" + end + | tx::lt' => weakTypeToType Γ φ tx >>= fun t' => + match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with + | nil => Error "WTyFunApp applied to too many types" + | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' => + let case_weakTypeListToTypeList := tt in _ + end + end + ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _ + end ); clear weakTypeToType. + + destruct case_WTyVarTy. + apply OK. + exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))). + + destruct case_WAppTy. + destruct t1' as [k1' t1']. + destruct t2' as [k2' t2']. + destruct k1'; + try (matchThings k1'1 k2' "Kind mismatch in WAppTy: "; + subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env)))); + apply (Error "Kind mismatch in WAppTy:: "). + + destruct case_weakTypeListToTypeList. + destruct t' as [ k' t' ]. + matchThings k k' "Kind mismatch in weakTypeListToTypeList". + subst. + apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))). + + destruct case_WTyFunApp. + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply TyFunApp. + apply lt'. + apply X. + + destruct case_WTyCon. + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply (TCon tc). + + destruct case_WCodeTy. + destruct tbody'. + matchThings κ ★ "Kind mismatch in WCodeTy: ". + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply TCode. + apply (TVar (φ (@fixkind ★ ec) TV X)). + subst. + apply h. + apply X. + + destruct case_WCoFunTy. + destruct t1' as [ k1' t1' ]. + destruct t2' as [ k2' t2' ]. + destruct t3' as [ k3' t3' ]. + matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy". + subst. + matchThings k3' ★ "Kind mismatch in result of WCoFunTy". + subst. + apply OK. + apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')). + + destruct case_WForAllTy. + destruct t1. + matchThings ★ κ "Kind mismatch in WForAllTy: ". + subst. + apply OK. + apply (@haskTypeOfSomeKind _ ★). + apply (@mkTAll wtv). + apply h. + Defined. + + + (* information about a datacon/literal/default which is common to all instances of a branch with that tag *) Section StrongAltCon. Context (tc : TyCon)(dc:DataCon tc). - +(* Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ). intro avars. intro ct. @@ -186,15 +295,16 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. apply vec_chop' in cenv. apply cenv. Defined. +*) End StrongAltCon. - +(* Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc). destruct alt. set (c:DataCon _) as dc. set ((dataConTyCon c):TyCon) as tc' in *. set (eqd_dec tc tc') as eqpf; destruct eqpf; [ idtac - | apply (Error ("in a case of tycon "+++tyConToString tc+++", found a branch with datacon "+++dataConToString dc)) ]; subst. + | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst. apply OK. eapply mkStrongAltConPlusJunk. simpl in *. @@ -212,127 +322,20 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP intro; intro φ; apply φ. intro; intro; intro; intro ψ; apply ψ. Defined. - -Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) := +Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) := match mlr with - | T_Leaf None => [] + | T_Leaf None => [] | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)] - | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ)) + | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ)) end. +*) -Open Scope string_scope. -Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. - -Definition Indexed_Bind T f t (e:@Indexed T f t) : forall Q, (forall t, f t -> ???Q) -> ???Q. -intros. -destruct e; subst. -apply (Error error_message). -apply (X t f0). -Defined. -Notation "a >>>= b" := (@Indexed_Bind _ _ _ a _ b) (at level 20). - -Definition DoublyIndexed_Bind T f t (e:@Indexed T (fun z => ???(f z)) t) : forall Q, (forall t, f t -> ???Q) -> ???Q. - intros. - eapply Indexed_Bind. - apply e. - intros. - destruct X0. - apply (Error error_message). - apply (X t0 f0). - Defined. - -Notation "a >>>>= b" := (@DoublyIndexed_Bind _ _ _ a _ b) (at level 20). - -Ltac matchTypes T1 T2 S := - destruct (eqd_dec T1 T2) as [matchTypes_pf|]; - [ idtac | apply (Error ("type mismatch in "+++S+++": " +++ (weakTypeToString T1) +++ " and " +++ (weakTypeToString T2))) ]. -Ltac matchTypeVars T1 T2 S := - destruct (eqd_dec T1 T2) as [matchTypeVars_pf|]; - [ idtac | apply (Error ("type variable mismatch in"+++S)) ]. -Ltac matchLevs L1 L2 S := - destruct (eqd_dec L1 L2) as [matchLevs_pf|]; - [ idtac | apply (Error ("level mismatch in "+++S)) ]. - - -Definition cure {Γ}(ξ:WeakExprVar -> WeakType * list WeakTypeVar)(φ:WeakTypeVar->HaskTyVar Γ) - : WeakExprVar->LeveledHaskType Γ := - fun wtv => weakTypeToType φ (fst (ξ wtv)) @@ map φ (snd (ξ wtv)). Definition weakExprVarToWeakType : WeakExprVar -> WeakType := fun wev => match wev with weakExprVar _ t => t end. Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType. -Fixpoint upξ (ξ:WeakExprVar -> WeakType * list WeakTypeVar) - (evs:list WeakExprVar) - (lev:list WeakTypeVar) : - (WeakExprVar -> WeakType * list WeakTypeVar) := - fun wev => - match evs with - | nil => ξ wev - | a::b => if eqd_dec wev a then ((wev:WeakType),lev) else upξ ξ b lev wev - end. - -Variable weakCoercionToHaskCoercion : forall Γ Δ, WeakCoercion -> HaskCoercion Γ Δ. - -Notation "'checkit' ( Y ) X" := (match weakTypeOfWeakExpr Y as CTE return - CTE=weakTypeOfWeakExpr Y -> forall Γ Δ φ ψ ξ lev, Indexed _ CTE with - | Error s => fun _ _ _ _ _ _ _ => Indexed_Error _ s - | OK cte => fun cte_pf => (fun x Γ Δ φ ψ ξ lev => Indexed_OK _ _ (x Γ Δ φ ψ ξ lev)) X - end (refl_equal _)) (at level 10). - - -(* equality lemmas I have yet to prove *) - -Lemma upξ_lemma Γ ξ v lev φ - : cure(Γ:=Γ) (upξ ξ (v :: nil) lev) φ = update_ξ (cure ξ φ) ((v,weakTypeToType φ v @@ map φ lev)::nil). - admit. - Qed. - -(* this is tricky because of the test for ModalBoxTyCon is a type index for tc and because the fold is a left-fold *) - -Lemma letrec_lemma : forall Γ ξ φ rb lev, -let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in -(cure ξ' φ) = ( - update_ξ (cure ξ φ) - (map - (fun x : WeakExprVar * HaskType Γ => - ⟨fst x, snd x @@ map φ lev ⟩) (leaves (mLetRecTypesVars rb φ)))). -admit. -Qed. - -Lemma case_lemma1 tc Γ avars' (sac:StrongAltConPlusJunk tc) vars ξ φ lev : -(@scbwv_ξ WeakExprVar WeakExprVarEqDecidable tc Γ avars' - {| scbwv_sac := sac; scbwv_exprvars := vars |} - (@cure Γ ξ φ) (@map WeakTypeVar (HaskTyVar Γ) φ lev)) - = (cure ξ (sacpj_φ sac Γ φ)). - admit. - Qed. -Lemma case_lemma2 tc Γ (sac:@StrongAltConPlusJunk tc) φ lev : - (map (sacpj_φ sac Γ φ) lev) = weakL' (map φ lev). - admit. - Qed. -Lemma case_lemma3 Γ φ t tc (sac:@StrongAltConPlusJunk tc) : - (weakT' (weakTypeToType φ t) = weakTypeToType (sacpj_φ sac Γ φ) t). - admit. - Qed. -Lemma case_lemma4 Γ φ (tc:TyCon) avars0 : forall Q1 Q2, (@weakTypeToType Γ φ Q2)=Q1 -> - fold_left HaskAppT (map (weakTypeToType φ) avars0) Q1 = - weakTypeToType φ (fold_left WAppTy avars0 Q2). - induction avars0; intros. - simpl. - symmetry; auto. - simpl. - set (IHavars0 (HaskAppT Q1 (weakTypeToType φ a)) (WAppTy Q2 a)) as z. - rewrite z. - reflexivity. - rewrite <- H. - simpl. - auto. - Qed. - -(* for now... *) -Axiom assume_all_coercions_well_formed : forall Γ (Δ:CoercionEnv Γ) t1 t2 co, Δ ⊢ᴄᴏ co : t1 ∼ t2. -Axiom assume_all_types_well_formed : forall Γ t x, Γ ⊢ᴛy t : x. +(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*) Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) : WeakCoerVar -> HaskCoVar Γ (κ::Δ). @@ -343,353 +346,111 @@ Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ inversion cenv; auto. Defined. -Lemma substRaw {Γ}{κ} : HaskType (κ::Γ) -> (∀ TV, @InstantiatedTypeEnv TV Γ -> TV -> @RawHaskType TV). - intro ht. - intro TV. - intro env. - intro tv. - apply ht. - apply (tv:::env). +(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *) +Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ) + : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ'). + intros. + destruct τ as [τ l]. + destruct τ' as [τ' l']. + destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ]. + destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ]. + subst. + apply OK. + apply e. Defined. -Lemma substRaw_lemma : forall (Γ:TypeEnv) (φ:WeakTypeVar->HaskTyVar Γ) wt tsubst wtv, - substT (substRaw (weakTypeToType (upφ wtv φ) wt)) (weakTypeToType φ tsubst) = - weakTypeToType φ (replaceWeakTypeVar wt wtv tsubst). - admit. - Qed. +Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ). + intros. + set (weakTypeToType φ t) as wt. + destruct wt; try apply (Error error_message). + destruct h. + matchThings κ κ0 "Kind mismatch in weakTypeToType': ". + subst. + apply OK. + apply h. + Defined. Definition weakExprToStrongExpr : forall - (ce:WeakExpr) (Γ:TypeEnv) (Δ:CoercionEnv Γ) - (φ:WeakTypeVar->HaskTyVar Γ) - (ψ:WeakCoerVar->HaskCoVar Γ Δ) - (ξ:WeakExprVar->WeakType * list WeakTypeVar) - (lev:list WeakTypeVar) - , - Indexed (fun t' => ???(@Expr _ WeakExprVarEqDecidable Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) - (weakTypeOfWeakExpr ce). + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ), + WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ). refine (( - fix weakExprToStrongExpr (ce:WeakExpr) {struct ce} : forall Γ Δ φ ψ ξ lev, - Indexed (fun t' => ???(Expr Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) (weakTypeOfWeakExpr ce) := - (match ce as CE return (forall Γ Δ φ ψ ξ lev, Indexed _ (weakTypeOfWeakExpr CE)) - with - | WEVar v => let case_WEVar := tt in checkit (WEVar v) (fun Γ Δ φ ψ ξ lev => _) - | WELit lit => let case_WELit := tt in checkit (WELit lit) (fun Γ Δ φ ψ ξ lev => _) - | WEApp e1 e2 => let case_WEApp := tt in checkit (WEApp e1 e2) (fun Γ Δ φ ψ ξ lev => - weakExprToStrongExpr e1 Γ Δ φ ψ ξ lev >>>>= fun te1 e1' => - ((weakExprToStrongExpr e2 Γ Δ φ ψ ξ lev) >>>>= fun te2 e2' => _)) - | WETyApp e t => let case_WETyApp := tt in - checkit (WETyApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) - | WECoApp e t => let case_WECoApp := tt in - checkit (WECoApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) - | WELam ev e => let case_WELam := tt in - checkit (WELam ev e) (fun Γ Δ φ ψ ξ lev => - let ξ' := @upξ ξ (ev::nil) lev in - weakExprToStrongExpr e Γ Δ φ ψ ξ' lev >>>>= fun te' e' => _) - | WECoLam cv e => let case_WECoLam := tt in - checkit (WECoLam cv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e)) - | WEBrak ec e tbody => let case_WEBrak := tt in - checkit (WEBrak ec e tbody) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ (ec::lev) >>>>= fun te' e' => _) - | WEEsc ec e tbody => - checkit (WEEsc ec e tbody) (fun Γ Δ φ ψ ξ lev => - match lev as LEV return lev=LEV -> _ with - | nil => let case_WEEsc_bogus := tt in _ - | ec'::lev' => fun ecpf => weakExprToStrongExpr e Γ Δ φ ψ ξ lev' >>>>= fun te' e' => let case_WEEsc := tt in _ - end (refl_equal _)) - | WETyLam tv e => let case_WETyLam := tt in - checkit (WETyLam tv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e)) - | WENote n e => let case_WENote := tt in - checkit (WENote n e) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) - | WECast e co => let case_WECast := tt in - checkit (WECast e co) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) - | WELet v ve e => let case_WELet := tt in - checkit (WELet v ve e) (fun Γ Δ φ ψ ξ lev => - let ξ' := upξ ξ (v::nil) lev in - ((weakExprToStrongExpr e Γ Δ φ ψ ξ lev) - >>>>= (fun te' e' => ((weakExprToStrongExpr ve Γ Δ φ ψ ξ' lev) >>>>= (fun vet' ve' => _))))) - - | WELetRec rb e => - checkit (WELetRec rb e) (fun Γ Δ φ ψ ξ lev => -let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in - ((fix mLetRecBindingsToELetRecBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) : forall Γ Δ φ ψ ξ lev, - ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars mlr φ)) := - match mlr as MLR return forall Γ Δ φ ψ ξ lev, - ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars MLR φ)) with - | T_Leaf None => fun Γ Δ φ ψ ξ lev => OK (ELR_nil _ _ _ _) - | T_Leaf (Some (cv,e)) => fun Γ Δ φ ψ ξ lev => - let case_mlr_leaf := tt in weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun me => _ - | T_Branch b1 b2 => - fun Γ Δ φ ψ ξ lev => - mLetRecBindingsToELetRecBindings b1 Γ Δ φ ψ ξ lev >>= fun x1' => - mLetRecBindingsToELetRecBindings b2 Γ Δ φ ψ ξ lev >>= fun x2' => - OK (ELR_branch _ _ _ _ _ _ x1' x2') - end) rb Γ Δ φ ψ ξ' lev) >>= fun rb' => (weakExprToStrongExpr e Γ Δ φ ψ ξ' lev) - >>>>= fun et' e' => - let case_MLLetRec := tt in _) - - | WECase e tbranches tc avars alts => - checkit (WECase e tbranches tc avars alts) (fun Γ Δ φ ψ ξ lev => - list2vecOrFail avars _ (fun _ _ => "number of types provided did not match the tycon's number of universal tyvars in Case") - >>= fun avars0 => - let avars' := vec_map (@weakTypeToType Γ φ) avars0 in - let tbranches' := @weakTypeToType Γ φ tbranches in - ((fix caseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) - : - ???(Tree ??{ scb : StrongCaseBranchWithVVs WeakExprVar _ tc avars' - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ avars' (weakCK'' Δ)) - (scbwv_ξ scb (cure ξ φ) (map φ lev)) - (weakLT' (tbranches'@@(map φ lev))) }) := - match alts with - | T_Leaf None => OK [] - | T_Branch b1 b2 => caseBranches b1 >>= fun b1' => caseBranches b2 >>= fun b2' => OK (b1',,b2') - | T_Leaf (Some (alt,tvars,cvars,vvars,e')) => - mkStrongAltConPlusJunk' tc alt >>= fun sac => - list2vecOrFail vvars (sac_numExprVars (sac:@StrongAltCon tc)) - (fun _ _ => "number of expression variables provided did not match the datacon's number of fields") >>= fun vars => - let scb := @Build_StrongCaseBranchWithVVs WeakExprVar _ tc Γ avars' sac vars in - let rec - := @weakExprToStrongExpr e' - (sac_Γ scb Γ) - (sac_Δ scb Γ avars' (weakCK'' Δ)) - (sacpj_φ sac Γ φ) - (let case_psi := tt in _) - ξ - lev in (let case_ECase_leaf := tt in _) - end - ) alts) >>= fun alts' => - weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => - let case_ECase := tt in _) - end))); clear weakExprToStrongExpr. - - destruct case_WEVar; intros. - matchTypes cte (fst (ξ v)) "HaskWeak EVar". - rewrite matchTypes_pf. - matchLevs (snd (ξ v)) lev "HaskWeak EVar". - rewrite <- matchLevs_pf. - apply OK. - apply (EVar _ _ (cure ξ φ)). - - destruct case_WELit; intros. - matchTypes (WTyCon (haskLiteralToTyCon lit)) cte "HaskWeak ELit". - rewrite <- matchTypes_pf. - apply OK. - replace (weakTypeToType φ (WTyCon (haskLiteralToTyCon lit))) with (@literalType lit Γ); [ idtac | reflexivity]. - apply ELit. - - destruct case_WELet; intros. - unfold ξ' in ve'. - matchTypes te' v "HaskWeak ELet". - rename matchTypes_pf into matchTypes_pf'. - matchTypes cte vet' "HaskWeak ELet". - apply OK. - eapply ELet. - apply e'. - rewrite matchTypes_pf'. - rewrite matchTypes_pf. - rewrite upξ_lemma in ve'. - apply ve'. - - destruct case_mlr_leaf; intros. - simpl. - destruct cv. - matchTypes me w "HaskWeak LetRec". - apply OK. - apply ELR_leaf. - rewrite <- matchTypes_pf. - apply X. - - destruct case_MLLetRec; intros. - matchTypes et' cte "HaskWeak LetRec". - apply OK. - unfold ξ' in rb'. - rewrite (letrec_lemma Γ ξ φ rb lev) in rb'. - apply (@ELetRec WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) (weakTypeToType φ cte) _ rb'). - rewrite <- (letrec_lemma Γ ξ φ rb lev). - rewrite <- matchTypes_pf. - apply e'. - - destruct case_WECast; intros. - apply OK. - apply (fun pf => @ECast WeakExprVar _ Γ Δ (cure ξ φ) (weakCoercionToHaskCoercion Γ Δ co) _ _ (map φ lev) pf e'). - apply assume_all_coercions_well_formed. - - destruct case_WENote; intros. - matchTypes te' cte "HaskWeak ENote". - apply OK. - apply ENote. - apply n. - rewrite <- matchTypes_pf. - apply e'. - - destruct case_WEApp; intros. - matchTypes te1 (WAppTy (WAppTy WFunTyCon te2) cte) "HaskWeak EApp". - inversion cte_pf. - destruct (weakTypeOfWeakExpr e1); try apply (Error error_message). - simpl in H0. - destruct w; try apply (Error error_message); inversion H0. - destruct w1; try apply (Error error_message); inversion H0. - destruct w1_1; try apply (Error error_message); inversion H0. - clear H0 H1 H2. - rewrite matchTypes_pf in e1'. - simpl in e1'. - rewrite <- H3. - apply (OK (EApp _ _ _ _ _ _ e1' e2')). - - destruct case_WETyApp; intros. - inversion cte_pf. - destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0. - clear H1. - destruct w; inversion H0. - simpl in cte_pf. - clear cte_pf. - rename w0 into wt. - rename t into tsubst. - rename w into wtv. - set (@ETyApp WeakExprVar _ Γ Δ wtv - (substRaw (weakTypeToType (upφ wtv φ) wt)) - (weakTypeToType φ tsubst) - (cure ξ φ) - (map φ lev) - (assume_all_types_well_formed _ _ _) - ) as q. - - (* really messy –– but it works! *) - matchTypes te' (WForAllTy wtv wt) "HaskWeak ETyApp". - apply OK. - rewrite substRaw_lemma in q. - apply q. - clear q H1 H0. - rewrite matchTypes_pf in e'. - simpl in e'. - unfold HaskTAll. - unfold substRaw. - apply e'. - - destruct case_WECoApp; intros. - inversion cte_pf. - destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0. - clear H1. - destruct w; inversion H0. - subst. - destruct t as [ct1 ct2 cc]. - set (@ECoApp WeakExprVar _ Γ Δ (weakCoercionToHaskCoercion Γ Δ (weakCoercion ct1 ct2 cc)) - (weakTypeToType φ ct1) (weakTypeToType φ ct2) (weakTypeToType φ te') (cure ξ φ) (map φ lev)) as q. - matchTypes w3 te' "HaskWeak ECoApp". - rewrite matchTypes_pf. - clear matchTypes_pf. - matchTypes (WCoFunTy ct1 ct2 te') te' "HaskWeak ECoApp". - apply OK. - apply q. - apply assume_all_coercions_well_formed. - clear q H0 cte_pf. - rewrite <- matchTypes_pf in e'. - simpl in e'. - apply e'. - - destruct case_WELam; intros. - simpl in cte_pf. - destruct ev as [evv evt]. - destruct (weakTypeOfWeakExpr e); simpl in cte_pf; inversion cte_pf; try apply (Error error_message). - matchTypes te' w "HaskWeak ELam". - rewrite <- matchTypes_pf. - apply OK. - simpl. - eapply ELam. - apply assume_all_types_well_formed. - unfold ξ' in e'. - rewrite upξ_lemma in e'. - apply e'. - - destruct case_WETyLam; intros. - inversion cte_pf. - destruct tv. - destruct (weakTypeOfWeakExpr e). - inversion H0. - inversion H0. - set (e' (k::Γ) (weakCE Δ) (upφ (weakTypeVar c k) φ) (fun x => weakCV (ψ x)) ξ lev) as e''. - inversion e''; try apply (Error error_message). - inversion X; try apply (Error error_message). - apply (Error "FIXME: HaskWeakToStrong: type lambda not yet implemented"). - - destruct case_WECoLam; intros. - inversion cte_pf. - destruct cv. - destruct (weakTypeOfWeakExpr e). - inversion H0. - inversion H0. - set (e' Γ (weakTypeToType φ w ∼∼∼ weakTypeToType φ w0 :: Δ) φ (weakψ ψ) ξ lev) as q. - inversion q. - destruct X; try apply (Error error_message). - set (kindOfType (weakTypeToType φ w)) as qq. - destruct qq; try apply (Error error_message). - apply OK. - apply ECoLam with (κ:=k). - apply assume_all_types_well_formed. - apply assume_all_types_well_formed. - fold (@weakTypeToType Γ). - apply e0. - - destruct case_WEBrak; intros. - simpl in cte_pf. - destruct ec as [ecv eck]. - destruct (weakTypeOfWeakExpr e); inversion cte_pf; try apply (Error error_message). - simpl. - matchTypes te' w "HaskWeak EBrak". - apply OK. - apply EBrak. - rewrite matchTypes_pf in e'. - apply e'. - - destruct case_WEEsc_bogus; intros. - apply (Error "attempt to use escape symbol at level zero"). - - destruct case_WEEsc; intros. - rewrite ecpf. - clear ecpf lev. - matchTypes te' (WCodeTy ec' cte) "HaskWeak EEsc". - apply OK. - apply EEsc. - rewrite matchTypes_pf in e'. - simpl in e'. - apply e'. - - destruct case_psi. - apply (sacpj_ψ sac Γ Δ avars' ψ). - - destruct case_ECase_leaf. - inversion rec; try apply (Error error_message). - destruct X; try apply (Error error_message). - matchTypes tbranches t "HaskWeak ECase". - apply OK. - apply T_Leaf. - apply Some. - apply (existT _ {| scbwv_sac := scb ; scbwv_exprvars := vars |}). - simpl. - unfold tbranches'. - rewrite matchTypes_pf. - rewrite case_lemma1. - rewrite <- case_lemma2. - rewrite case_lemma3. - apply e0. - - destruct case_ECase; intros. - matchTypes cte tbranches "HaskWeak ECase". - rewrite matchTypes_pf. - clear matchTypes_pf. - matchTypes te' (fold_left WAppTy (vec2list avars0) (WTyCon tc)) "HaskWeak ECase". - apply OK. - apply (fun e => @ECase WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) tc _ _ e alts'). - unfold caseType. - unfold avars'. - replace (fold_left HaskAppT (vec2list (vec_map (weakTypeToType φ) avars0)) (HaskTCon tc)) - with (weakTypeToType φ (fold_left WAppTy (vec2list avars0) (WTyCon tc))). - rewrite <- matchTypes_pf. - apply e'. - symmetry. - rewrite <- vec2list_map_list2vec. - apply case_lemma4. - apply tc. - reflexivity. - Defined. + fix weakExprToStrongExpr + (Γ:TypeEnv) + (Δ:CoercionEnv Γ) + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ) + (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + match we with + + | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v) + + | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev) + + | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv => + weakTypeOfWeakExpr e >>= fun t => + weakTypeToType' φ t ★ >>= fun τ' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' => + castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') + + | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => + castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e') + + | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' => + match lev with + | nil => Error "ill-leveled escapification" + | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e + >>= fun e' => + castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e') + end + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') + + | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv => + weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody + >>= fun ebody' => + OK (ELet _ _ _ tv _ lev v ve' ebody') + + | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 => + weakTypeToType' φ t2 ★ >>= fun t2' => + weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' => + weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' => + OK (EApp _ _ _ _ _ _ e1' e2') + + | WETyLam tv e => let φ' := upφ tv φ in + weakTypeOfWeakExpr e >>= fun te => + weakTypeToType' φ' te ★ >>= fun τ' => + weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e + >>= fun e' => + castExpr "WETyLam1" _ e' >>= fun e'' => + castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'') + + | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => + match te with + | WForAllTy wtv te' => + let φ' := upφ wtv φ in + weakTypeToType' φ' te' ★ >>= fun te'' => + weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' => + weakTypeToType' φ t wtv >>= fun t' => + castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') + | _ => Error ("weakTypeToType: WETyApp body with type "+++te) + end + + (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two + * to get them back working again *) + | WECoApp e t => Error "weakExprToStrongExpr: WECoApp not yet implemented" + | WECoLam cv e => Error "weakExprToStrongExpr: WECoLam not yet implemented" + | WECast e co => Error "weakExprToStrongExpr: WECast not yet implemented" + | WELetRec rb e => Error "weakExprToStrongExpr: WELetRec not yet implemented" + | WECase e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase not yet implemented" + end)). + Defined. + diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index b295cf1..82cf8ad 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -13,6 +13,13 @@ Require Import HaskCoreVars. Require Import HaskCoreTypes. (* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *) +Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)". +Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)". +Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon. +Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon. + +Instance TyConToString : ToString TyCon := { toString := tyConToString }. +Instance TyFunToString : ToString TyFun := { toString := tyConToString }. (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *) Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. @@ -26,7 +33,7 @@ Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. Inductive WeakType := | WTyVarTy : WeakTypeVar -> WeakType | WAppTy : WeakType -> WeakType -> WeakType -| WTyFunApp : TyCon -> list WeakType -> WeakType +| WTyFunApp : TyFun -> list WeakType -> WeakType | WTyCon : TyCon -> WeakType | WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *) | WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *) @@ -95,7 +102,7 @@ Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType := | t1' => AppTy t1' (weakTypeToCoreType' t2) end | WTyCon tc => TyConApp tc nil - | WTyFunApp tc lt => TyConApp tc (map weakTypeToCoreType' lt) + | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType' lt) | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType' lt)) | WIParam n ty => PredTy (IParam n (weakTypeToCoreType' ty)) | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t) @@ -127,6 +134,6 @@ Instance EqDecidableWeakType : EqDecidable WeakType. right; auto. Defined. -Definition weakTypeToString : WeakType -> string := - coreTypeToString ○ weakTypeToCoreType. +Instance WeakTypeToString : ToString WeakType := + { toString := coreTypeToString ○ weakTypeToCoreType }. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 782c2a2..ee8d3cf 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -47,6 +47,17 @@ 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) := + General.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 tyFunResultKind : CoreTyCon -> Kind. Extract Inlined Constant tyFunResultKind => "tyFunResultKind". +Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) := + ((map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc)) , (tyFunResultKind tc)). + (* EqDecidable instances for all of the above *) Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar. apply Build_EqDecidable. @@ -85,3 +96,8 @@ Instance WeakVarEqDecidable : EqDecidable WeakVar. left; auto. right; intro X; apply n; inversion X; auto. Defined. + + + +Instance WeakVarToString : ToString WeakVar := + { toString := fun x => toString (weakVarToCoreVar x) }. \ No newline at end of file diff --git a/src/Preamble.v b/src/Preamble.v index 6abdd71..17174b3 100644 --- a/src/Preamble.v +++ b/src/Preamble.v @@ -85,7 +85,7 @@ Reserved Notation "Γ '∌∌' x" (at level 10). Reserved Notation "Γ '∋∋' x : a ∼ b" (at level 10, x at level 99). Reserved Notation "Γ '∋' x : c" (at level 10, x at level 99). -Reserved Notation "a ⇛ b" (at level 40). +Reserved Notation "a ⇛ b" (at level 55, right associativity). Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity). Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80). Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99). @@ -100,7 +100,6 @@ Reserved Notation "'η'". Reserved Notation "'ε'". Reserved Notation "'★'". -Notation "a +++ b" := (append a b) (at level 100). Close Scope nat_scope. (* so I can redefine '1' *) Delimit Scope arrow_scope with arrow. @@ -109,6 +108,7 @@ Delimit Scope garrow_scope with garrow. Notation "f ○ g" := (fun x => f(g(x))). Notation "?? T" := (option T). +Notation "a && b" := (if a then b else false). (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *) Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100). -- 1.7.10.4