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
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)
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.
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)).*)
(* 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+++
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 :=
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 *)
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 []
"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} :=
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".
| 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" ].
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"
| 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
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.
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
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 }.
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 }.
(*********************************************************************************************************************************)
-(* 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.
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).
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).
* 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).
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))))
(* 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 [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
| 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)
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 *.
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,
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.
| KindTypeFunction k1 k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
| KindUnliftedType => "\text{\tt{\#}}"
| KindUnboxedTuple => "\text{\tt{(\#)}}"
- | KindArgType => "\text{\tt{?}}"
+ | KindArgType => "\text{\tt{??}}"
| KindOpenType => "\text{\tt{?}}"
end.
| 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.
| 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) "")+++"}"
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{:}"*)
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.
{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 *)
| 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 _
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.
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.
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
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)
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)
(* 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 τ :
| 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 => []
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]
| 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)]
Lemma stripping_nothing_is_inert
{Γ:TypeEnv}
- (ξ:VV -> LeveledHaskType Γ)
+ (ξ:VV -> LeveledHaskType Γ ★)
tree :
stripOutVars nil tree = tree.
induction tree.
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 *)
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.
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).
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).
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.
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.
| 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
| 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
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:
apply n.
auto.
inversion H.
- apply pf.
destruct case_ELet; intros.
eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
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.
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.
; 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.
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 *)
) 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)
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.
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 (* γ γ *)
| 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
*)
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).
-
-
-
-
-
-
-
(* 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.
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 Γ :=
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.
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 *)
| 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 κ) ->
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 }.
| 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')
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.
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'' Δ)))
}.
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 φ'.
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.
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 *.
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 Γ (κ::Δ).
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.
+
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.
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 *)
| 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)
right; auto.
Defined.
-Definition weakTypeToString : WeakType -> string :=
- coreTypeToString ○ weakTypeToCoreType.
+Instance WeakTypeToString : ToString WeakType :=
+ { toString := coreTypeToString ○ weakTypeToCoreType }.
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.
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
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).
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.
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).