X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=2593a5cf12557bbc070775a21df4898aeba340e8;hp=47153085b40cfbeed316ff59bcc0d3ac264112bf;hb=2ec43bc871b579bac89707988c4855ee1d6c8eda;hpb=0126c02cc846952aa847660475e88a152c9a2574 diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 4715308..2593a5c 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -10,16 +10,14 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskCoreTypes. Require Import HaskCoreVars. -Require Import HaskCoreToWeak. Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). @@ -117,6 +115,7 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★. 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 _ @@ -149,24 +148,29 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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']. + set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err. 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:: "). + apply (Error ("Kind mismatch in WAppTy: "+++err)). 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. @@ -175,12 +179,14 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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. @@ -193,6 +199,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) apply X. destruct case_WCoFunTy. + apply (addErrorMessage "case_WCoFunTy"). destruct t1' as [ k1' t1' ]. destruct t2' as [ k2' t2' ]. destruct t3' as [ k3' t3' ]. @@ -204,6 +211,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')). destruct case_WForAllTy. + apply (addErrorMessage "case_WForAllTy"). destruct t1. matchThings ★ κ "Kind mismatch in WForAllTy: ". subst. @@ -224,6 +232,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★). intro avars. intro ct. + 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 φ'. @@ -250,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds Definition mkStrongAltCon : @StrongAltCon tc. refine - {| sac_altcon := DataAlt dc + {| sac_altcon := WeakDataAlt dc ; sac_numCoerVars := length (dataConCoerKinds dc) ; sac_numExprVars := length (dataConFieldTypes dc) ; sac_ekinds := dataConExKinds dc @@ -339,7 +348,7 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. End StrongAltCon. -Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc). +Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc). destruct alt. set (c:DataCon _) as dc. set ((dataConTyCon c):TyCon) as tc' in *. @@ -353,14 +362,14 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil - ; sac_altcon := LitAlt h + ; sac_altcon := WeakLitAlt h |} |}. intro; intro φ; apply φ. 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 |} |}. + ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. rewrite weakCK'_nil_inert. apply ψ. @@ -384,13 +393,22 @@ Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Defined. (* 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 _ CoreVarEqDecidable Γ Δ ξ τ) +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: "+++err_msg)) ]. - destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ]. + 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. @@ -400,12 +418,12 @@ Definition coVarKind (wcv:WeakCoerVar) : Kind := match wcv with weakCoerVar _ κ _ _ => κ end. Coercion coVarKind : WeakCoerVar >-> Kind. -Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ). +Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ). intros. set (weakTypeToType φ t) as wt. destruct wt; try apply (Error error_message). destruct h. - matchThings κ κ0 "Kind mismatch in weakTypeToType'': ". + matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in "). subst. apply OK. apply h. @@ -414,14 +432,13 @@ Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakTyp 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 _ => [] + | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with | 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 @@ -431,7 +448,7 @@ match lk as LK return ???(IList Kind (HaskType Γ) LK) with | k::lk' => match wtl with | nil => Error "length mismatch in mkAvars" | wt::wtl' => - weakTypeToType'' φ wt k >>= fun t => + weakTypeToTypeOfKind φ wt k >>= fun t => mkAvars wtl' lk' φ >>= fun rest => OK (ICons _ _ t rest) end @@ -456,63 +473,66 @@ Definition weakExprToStrongExpr : forall (τ:HaskType Γ ★) (lev:HaskLevel Γ) (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + addErrorMessage ("in weakExprToStrongExpr " +++ we) match we with - | WEVar v => castExpr ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) + | WEVar v => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) - | WELit lit => castExpr ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev) + | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev) - | WELam ev ebody => weakTypeToType'' φ ev ★ >>= fun tv => + | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => weakTypeOfWeakExpr ebody >>= fun tbody => - weakTypeToType'' φ tbody ★ >>= fun tbody' => + weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' => - castExpr "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') + castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' => - weakTypeToType'' φ tbody ★ >>= fun tbody' => + weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' => - castExpr "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e') + castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e') | WEEsc _ ec e tbody => φ ec >>= fun ec'' => - weakTypeToType'' φ tbody ★ >>= fun tbody' => + weakTypeToTypeOfKind φ 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' tbody' lev' e') + >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e') end + | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage" + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') - | WELet v ve ebody => weakTypeToType'' φ v ★ >>= fun tv => + | 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 => - weakTypeToType'' φ t2 ★ >>= 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 => - weakTypeToType'' φ' te ★ >>= fun τ' => + weakTypeToTypeOfKind φ' te ★ >>= fun τ' => weakExprToStrongExpr _ (weakCE Δ) φ' (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e >>= fun e' => - castExpr "WETyLam1" _ e' >>= fun e'' => - castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 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'' => + weakTypeToTypeOfKind φ' te' ★ >>= fun te'' => weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' => - weakTypeToType'' φ t (wtv:Kind) >>= fun t' => - castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev 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 @@ -522,10 +542,10 @@ Definition weakExprToStrongExpr : forall weakTypeToType φ t1 >>= fun t1' => match t1' with haskTypeOfSomeKind κ t1'' => - weakTypeToType'' φ t2 κ >>= fun t2'' => - weakTypeToType'' φ t3 ★ >>= fun t3'' => + weakTypeToTypeOfKind φ t2 κ >>= fun t2'' => + weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' => weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => - castExpr "WECoApp" _ e' >>= fun e'' => + castExpr we "WECoApp" _ e' >>= fun e'' => OK (ECoApp Γ Δ κ t1'' t2'' (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'') end @@ -534,17 +554,17 @@ Definition weakExprToStrongExpr : forall | 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' => + weakTypeToTypeOfKind φ te ★ >>= fun te' => + weakTypeToTypeOfKind φ t1 cv >>= fun t1' => + weakTypeToTypeOfKind φ t2 cv >>= fun t2' => weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' => - castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') + castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') - | WECast e co => let (κ,t1,t2,_) := co in - weakTypeToType'' φ t1 ★ >>= fun t1' => - weakTypeToType'' φ t2 ★ >>= fun t2' => + | WECast e co => let (t1,t2) := weakCoercionTypes co in + weakTypeToTypeOfKind φ t1 ★ >>= fun t1' => + weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' => - castExpr "WECast" _ + castExpr we "WECast" _ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => @@ -565,12 +585,12 @@ Definition weakExprToStrongExpr : forall OK (ELetRec Γ Δ ξ lev τ _ binds' e') | WECase vscrut ve tbranches tc avars alts => - weakTypeToType'' φ (vscrut:WeakType) ★ >>= fun tv => + 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' => - weakTypeToType'' φ tbranches ★ >>= fun tbranches' => - (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree + weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => + (fix mkTree (t:Tree ??(WeakAltCon*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 @@ -589,8 +609,8 @@ Definition weakExprToStrongExpr : forall mkTree b2 >>= fun b2' => OK (b1',,b2') end) alts >>= fun tree => - castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut => - castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut 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') @@ -598,8 +618,9 @@ Definition weakExprToStrongExpr : forall end)). destruct case_some. + apply (addErrorMessage "case_some"). simpl. - destruct (weakTypeToType'' φ wev ★); try apply (Error error_message). + destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message). matchThings h (unlev (ξ' wev)) "LetRec". destruct wev. rewrite matchTypeVars_pf.