Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
+Require Import HaskWeakToCore.
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 OK _
+ else φ tv' >>= fun tv'' => OK (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 Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
- (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
+; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
+; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
}.
Implicit Arguments StrongAltConPlusJunk [ ].
Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
(* yes, I know, this is really clumsy *)
-Variable emptyφ : WeakTypeVar -> HaskTyVar nil.
+Variable emptyφ : TyVarResolver nil.
Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
Definition mkPhi (lv:list WeakTypeVar)
- : (WeakTypeVar -> HaskTyVar (map (fun x:WeakTypeVar => x:Kind) lv)).
+ : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
set (upφ'(Γ:=nil) lv emptyφ) as φ'.
rewrite <- app_nil_end in φ'.
apply φ'.
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 Γ) :=
+ addErrorMessage ("weakTypeToType " +++ t)
+ 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 φ v >>= fun v' => _
+ | 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' => φ (@fixkind ★ ec) >>= fun ec' => _
+ | 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 (addErrorMessage "case_WTyVarTy").
+ apply OK.
+ exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
+
+ destruct case_WAppTy.
+ apply (addErrorMessage "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.
+ apply (addErrorMessage "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 (addErrorMessage "case_WTyFunApp").
+ apply OK.
+ eapply haskTypeOfSomeKind.
+ unfold HaskType; intros.
+ apply TyFunApp.
+ apply lt'.
+ apply X.
+
+ destruct case_WTyCon.
+ apply (addErrorMessage "case_WTyCon").
+ apply OK.
+ eapply haskTypeOfSomeKind.
+ unfold HaskType; intros.
+ apply (TCon tc).
+
+ destruct case_WCodeTy.
+ apply (addErrorMessage "case_WCodeTy").
+ destruct tbody'.
+ matchThings κ ★ "Kind mismatch in WCodeTy: ".
+ apply OK.
+ eapply haskTypeOfSomeKind.
+ unfold HaskType; intros.
+ apply TCode.
+ apply (TVar (ec' TV X)).
+ subst.
+ apply h.
+ apply X.
+
+ destruct case_WCoFunTy.
+ apply (addErrorMessage "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.
+ apply (addErrorMessage "case_WForAllTy").
+ destruct t1.
+ matchThings ★ κ "Kind mismatch in WForAllTy: ".
+ subst.
+ apply OK.
+ apply (@haskTypeOfSomeKind _ ★).
+ apply (@mkTAll wtv).
+ apply h.
+ Defined.
+
+
+Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
+
(* 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)) Γ).
+Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
+ -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
intro avars.
intro ct.
- set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
+ apply (addErrorMessage "weakTypeToType'").
+ set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
set (@substφ _ _ avars') as q.
set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
set (@weakTypeToType _ φ' ct) as t.
- set (@weakT'' _ Γ t) as t'.
- set (@lamer _ _ _ t') as t''.
+ destruct t as [|t]; try apply (Error error_message).
+ destruct t as [tk t].
+ matchThings tk ★ "weakTypeToType'".
+ subst.
+ apply OK.
+ set (@weakT'' _ Γ _ t) as t'.
+ set (@lamer _ _ _ _ t') as t''.
fold (tyConKinds tc) in t''.
fold (dataConExKinds dc) in t''.
- apply (q (tyConKinds tc)).
+ apply q.
+ clear q.
unfold tyConKinds.
unfold dataConExKinds.
rewrite <- vec2list_map_list2vec.
{| sac_altcon := DataAlt dc
; sac_numCoerVars := length (dataConCoerKinds dc)
; sac_numExprVars := length (dataConFieldTypes dc)
- ; sac_akinds := tyConKinds tc
; sac_ekinds := dataConExKinds dc
; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
; sac_types := fun Γ avars => let case_sac_types := tt in _
refine (vec_map _ (list2vec (dataConCoerKinds dc))).
intro.
destruct X.
- apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ apply (
+ match
+ q avars w >>= fun t1 =>
+ q avars w0 >>= fun t2 =>
+ OK (mkHaskCoercionKind t1 t2)
+ with
+ | Error s => Prelude_error s
+ | OK y => y
+ end).
destruct case_sac_types.
refine (vec_map _ (list2vec (dataConFieldTypes dc))).
intro X.
- apply (weakTypeToType' avars).
- apply X.
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ set (q avars X) as y.
+ apply (match y with
+ | Error s =>Prelude_error s
+ | OK y' => y'
+ end).
Defined.
-
+
+
Lemma weakCV' : forall {Γ}{Δ} Γ',
HaskCoVar Γ Δ
-> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
intros.
unfold HaskCoVar in *.
intros; apply (X TV CV).
- apply vec_chop' in env; auto.
+ apply ilist_chop' in env; auto.
unfold InstantiatedCoercionEnv in *.
unfold weakCK'' in cenv.
destruct Γ'.
+ rewrite <- map_preserves_length in cenv.
apply cenv.
rewrite <- map_preserves_length in cenv.
apply cenv.
Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
refine
{| sacpj_sac := mkStrongAltCon
- ; sacpj_φ := fun Γ φ => (fun htv => weakV' (φ htv))
- ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
+ ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
+ ; sacpj_ψ :=
+ fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
|}.
intro.
unfold sac_Γ.
apply vec_chop' in cenv.
apply cenv.
Defined.
+
+ Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
+ intros.
+ induction Δ.
+ reflexivity.
+ simpl.
+ rewrite IHΔ.
+ reflexivity.
+ Qed.
+
End StrongAltCon.
Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
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:CoreDataCon))) ]; subst.
apply OK.
eapply mkStrongAltConPlusJunk.
simpl in *.
apply dc.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
; sac_altcon := LitAlt h
|} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
; sac_altcon := DEFAULT |} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
-Defined.
-
-Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) :=
- match mlr with
- | T_Leaf None => []
- | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
- | 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).
+ intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
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 Γ Δ κ.
-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.
-
-Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
- WeakCoerVar -> HaskCoVar Γ (κ::Δ).
+Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
+ WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
intros.
+ refine (ψ X >>= _).
unfold HaskCoVar.
intros.
- apply (ψ X TV CV env).
+ apply OK.
+ intros.
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 (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
+ : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
+ apply (addErrorMessage ("castExpr " +++ err_msg)).
+ intros.
+ destruct τ as [τ l].
+ destruct τ' as [τ' l'].
+ destruct (eqd_dec l l'); [ idtac
+ | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
+ " got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
+ " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
+ )) ].
+ destruct (eqd_dec τ τ'); [ idtac
+ | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
+ " got: " +++τ+++eol+++
+ " wanted: "+++τ'
+ )) ].
+ subst.
+ apply OK.
+ apply e.
+ Defined.
+
+Definition coVarKind (wcv:WeakCoerVar) : Kind :=
+ match wcv with weakCoerVar _ κ _ _ => κ end.
+ Coercion coVarKind : WeakCoerVar >-> Kind.
+
+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.
-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.
+Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
+ match t with
+ | T_Leaf None => []
+ | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with
+ | Error _ => []
+ | OK t' => [((wev:CoreVar),t')]
+ end
+ | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
+ end.
+
+
+Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
+match lk as LK return ???(IList Kind (HaskType Γ) LK) with
+ | nil => match wtl with
+ | nil => OK INil
+ | _ => Error "length mismatch in mkAvars"
+ end
+ | k::lk' => match wtl with
+ | nil => Error "length mismatch in mkAvars"
+ | wt::wtl' =>
+ weakTypeToType'' φ wt k >>= fun t =>
+ mkAvars wtl' lk' φ >>= fun rest =>
+ OK (ICons _ _ t rest)
+ end
+end.
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 Γ Δ)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
+ (τ:HaskType Γ ★)
+ (lev:HaskLevel Γ),
+ WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ 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.
+ fix weakExprToStrongExpr
+ (Γ:TypeEnv)
+ (Δ:CoercionEnv Γ)
+ (φ:TyVarResolver Γ)
+ (ψ:CoVarResolver Γ Δ)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
+ (τ:HaskType Γ ★)
+ (lev:HaskLevel Γ)
+ (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
+ match we with
+
+ | WEVar v => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+
+ | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+
+ | WELam ev ebody => weakTypeToType'' φ ev ★ >>= fun tv =>
+ weakTypeOfWeakExpr ebody >>= fun tbody =>
+ weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+ let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
+ weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
+ castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
+
+ | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
+ weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
+ castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
+
+ | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
+ weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+ match lev with
+ | nil => Error "ill-leveled escapification"
+ | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
+ >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' 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:CoreVar),tv@@lev)::nil)) τ lev ebody
+ >>= fun ebody' =>
+ OK (ELet _ _ _ tv _ lev (v:CoreVar) 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 Δ) φ'
+ (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
+ >>= fun e' =>
+ castExpr we "WETyLam1" _ e' >>= fun e'' =>
+ castExpr we "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:Kind) >>= fun t' =>
+ castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
+ | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
+ end
+
+ | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | WCoFunTy t1 t2 t3 =>
+ weakTypeToType φ t1 >>= fun t1' =>
+ match t1' with
+ haskTypeOfSomeKind κ t1'' =>
+ weakTypeToType'' φ t2 κ >>= fun t2'' =>
+ weakTypeToType'' φ t3 ★ >>= fun t3'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
+ castExpr we "WECoApp" _ e' >>= fun e'' =>
+ OK (ECoApp Γ Δ κ t1'' t2''
+ (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
+ end
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
+ end
+
+ | WECoLam cv e => let (_,_,t1,t2) := cv in
+ weakTypeOfWeakExpr e >>= fun te =>
+ weakTypeToType'' φ te ★ >>= fun te' =>
+ weakTypeToType'' φ t1 cv >>= fun t1' =>
+ weakTypeToType'' φ t2 cv >>= fun t2' =>
+ weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
+ castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+
+ | WECast e co => let (t1,t2) := weakCoercionTypes co in
+ weakTypeToType'' φ t1 ★ >>= fun t1' =>
+ weakTypeToType'' φ t2 ★ >>= fun t2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
+ castExpr we "WECast" _
+ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
+
+ | WELetRec rb e =>
+ let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
+ in let binds :=
+ (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
+ : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
+ match t with
+ | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
+ | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
+ | T_Branch b1 b2 =>
+ binds b1 >>= fun b1' =>
+ binds b2 >>= fun b2' =>
+ OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
+ end) rb
+ in binds >>= fun binds' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
+ OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+
+ | WECase vscrut ve tbranches tc avars alts =>
+ weakTypeToType'' φ (vscrut:WeakType) ★ >>= fun tv =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
+ let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
+ mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
+ (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+ ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
+ Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
+ match t with
+ | T_Leaf None => OK []
+ | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
+ mkStrongAltConPlusJunk' tc ac >>= fun sac =>
+ list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
+ >>= fun exprvars' =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
+ weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+ (sacpj_ψ sac _ _ avars' ψ)
+ (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+ let case_case := tt in OK [ _ ]
+ | T_Branch b1 b2 =>
+ mkTree b1 >>= fun b1' =>
+ mkTree b2 >>= fun b2' =>
+ OK (b1',,b2')
+ end) alts >>= fun tree =>
+ castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
+ castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
+ >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
+
+
+
+ end)).
+
+ destruct case_some.
+ apply (addErrorMessage "case_some").
simpl.
- destruct cv.
- matchTypes me w "HaskWeak LetRec".
+ destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
+ matchThings h (unlev (ξ' wev)) "LetRec".
+ destruct wev.
+ rewrite matchTypeVars_pf.
+ clear matchTypeVars_pf.
+ set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
+ destruct e''; try apply (Error error_message).
apply OK.
apply ELR_leaf.
- rewrite <- matchTypes_pf.
- apply X.
+ apply e1.
- 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_case.
+ exists scb.
+ apply ebranch'.
- 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").
+ Defined.
- 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.