- 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) ) :=
+ addErrorMessage ("in weakExprToStrongExpr " +++ we)
+ 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 => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
+ weakTypeOfWeakExpr ebody >>= fun tbody =>
+ weakTypeToTypeOfKind φ 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' =>
+ weakTypeToTypeOfKind φ 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'' =>
+ weakTypeToTypeOfKind φ 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 => weakTypeToTypeOfKind φ 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 =>
+ weakTypeToTypeOfKind φ 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 =>
+ weakTypeToTypeOfKind φ' 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
+ weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
+ weakTypeToTypeOfKind φ 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'' =>
+ weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
+ weakTypeToTypeOfKind φ 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 =>
+ weakTypeToTypeOfKind φ te ★ >>= fun te' =>
+ weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
+ weakTypeToTypeOfKind φ 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
+ weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
+ weakTypeToTypeOfKind φ 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 =>
+ weakTypeToTypeOfKind φ (vscrut:WeakType) ★ >>= fun tv =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
+ let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
+ mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToTypeOfKind φ 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").