X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=1b348657c654a276702f68eefe878d6b7047d097;hp=38a430466e67595f4aa2c6ca33725c6cb6335f44;hb=c3b1fb9622a65ad01e54b6e35785cee672d25bdc;hpb=f7a6e08c97cae1c1b278c18a1904eadec4e5f010 diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 38a4304..1b34865 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,9 +19,6 @@ Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreVars. -(* can remove *) -Require Import HaskStrongToWeak. - Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). @@ -97,7 +94,7 @@ 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)) ]. + [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ]. Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★). intros. @@ -118,7 +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) + addErrorMessage ("weakTypeToType " +++ toString t) match t with | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow)) | WTyCon tc => let case_WTyCon := tt in _ @@ -149,6 +146,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) end ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _ end ); clear weakTypeToType. + apply ConcatenableString. destruct case_WTyVarTy. apply (addErrorMessage "case_WTyVarTy"). @@ -159,7 +157,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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. + set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++ + toString t2'+++" of kind "+++toString 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)))); @@ -224,9 +223,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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). @@ -357,7 +353,7 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAlt set ((dataConTyCon c):TyCon) as tc' in *. set (eqd_dec tc tc') as eqpf; destruct eqpf; [ idtac - | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst. + | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst. apply OK. eapply mkStrongAltConPlusJunk. simpl in *. @@ -404,13 +400,13 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex 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') "") + " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++ + " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "") )) ]. destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++ - " got: " +++τ+++eol+++ - " wanted: "+++τ' + " got: " +++toString τ+++eol+++ + " wanted: "+++toString τ' )) ]. subst. apply OK. @@ -467,6 +463,55 @@ Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool := else update_ig ig vars' v' end. +(* does the specified variable occur free in the expression? *) +Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool := + match me with + | WELit _ => false + | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false + | WECast e co => doesWeakVarOccur wev e + | WENote n e => doesWeakVarOccur wev e + | WETyApp e t => doesWeakVarOccur wev e + | WECoApp e co => doesWeakVarOccur wev e + | WEBrak _ ec e _ => doesWeakVarOccur wev e + | WEEsc _ ec e _ => doesWeakVarOccur wev e + | WECSP _ ec e _ => doesWeakVarOccur wev e + | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2) + | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2 + | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e + | WETyLam cv e => doesWeakVarOccur wev e + | WECoLam cv e => doesWeakVarOccur wev e + | WECase vscrut escrut tbranches tc avars alts => + doesWeakVarOccur wev escrut || + if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else + ((fix doesWeakVarOccurAlts alts {struct alts} : bool := + match alts with + | T_Leaf None => false + | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *) + | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2 + end) alts) + | WELetRec mlr e => + doesWeakVarOccur wev e || + (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool := + match mlr with + | T_Leaf None => false + | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e + | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2 + end) mlr + end. +Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar) + (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool := + match alts with + | T_Leaf None => false + | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *) + | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2 + end. + +(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *) + Definition weakExprToStrongExpr : forall (Γ:TypeEnv) (Δ:CoercionEnv Γ) @@ -488,19 +533,19 @@ Definition weakExprToStrongExpr : forall (τ:HaskType Γ ★) (lev:HaskLevel Γ) (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := - addErrorMessage ("in weakExprToStrongExpr " +++ we) + addErrorMessage ("in weakExprToStrongExpr " +++ toString we) match we with | WEVar v => if ig v then OK (EGlobal Γ Δ ξ (τ@@lev) v) - else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) + else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) - | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev) + | WELit lit => castExpr we ("WELit "+++toString 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 + let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in let ig' := update_ig ig ((ev:CoreVar)::nil) in weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' => castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') @@ -524,7 +569,7 @@ Definition weakExprToStrongExpr : forall | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil)) (update_ig ig ((v:CoreVar)::nil)) τ lev ebody >>= fun ebody' => OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') @@ -550,7 +595,7 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ Δ φ ψ ξ ig (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) + | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te) end | WECoApp e co => weakTypeOfWeakExpr e >>= fun te => @@ -566,7 +611,7 @@ Definition weakExprToStrongExpr : forall OK (ECoApp Γ Δ κ t1'' t2'' (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'') end - | _ => Error ("weakTypeToType: WECoApp body with type "+++te) + | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te) end | WECoLam cv e => let (_,_,t1,t2) := cv in @@ -585,7 +630,7 @@ Definition weakExprToStrongExpr : forall (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => - let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in + let ξ' := update_ξ ξ lev _ in let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in let binds := (fix binds (t:Tree ??(WeakExprVar * WeakExpr)) @@ -605,28 +650,25 @@ Definition weakExprToStrongExpr : forall | WECase vscrut escrut tbranches tc avars alts => weakTypeOfWeakExpr escrut >>= fun tscrut => weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' => -(* - let ξ' := update_ξ ξ (((vscrut:CoreVar),tscrut'@@lev)::nil) in - let ig' := update_ig ig ((vscrut:CoreVar)::nil) in -*) - let ξ' := ξ in - let ig' := ig in - mkAvars avars (tyConKind tc) φ >>= fun avars' => + if doesWeakVarOccurAlts vscrut alts + then Error "encountered a Case which actually used its binder - these should have been desugared away!!" + else mkAvars avars (tyConKind tc) φ >>= fun avars' => 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))}) := + ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac & + Expr (sac_Γ sac Γ) (sac_Δ sac Γ 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 _ φ) + (let case_pf := tt in _) >>= fun pf => + let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in + weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ' lev) - (update_ig ig' (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) + (scbwv_ξ scb ξ lev) + (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => let case_case := tt in OK [ _ ] | T_Branch b1 b2 => @@ -635,17 +677,10 @@ Definition weakExprToStrongExpr : forall OK (b1',,b2') end) alts >>= fun tree => - weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' => - castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ' lev tc tbranches' avars' escrut' tree) -(* - weakExprToStrongExpr Γ Δ φ ψ ξ ig tscrut' lev escrut >>= fun escrut' => - castExpr we "ECaseScrut" (caseType tc avars' @@ lev) (EVar Γ Δ ξ' vscrut) >>= fun evscrut' => - castExpr we "ECase" (τ@@lev) - (ELet Γ Δ ξ tscrut' tbranches' lev (vscrut:CoreVar) escrut' - (ECase Γ Δ ξ' lev tc tbranches' avars' evscrut' tree)) -*) - end)). - + weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' => + castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree) + end)); try clear binds; try apply ConcatenableString. + destruct case_some. apply (addErrorMessage "case_some"). simpl. @@ -658,9 +693,21 @@ Definition weakExprToStrongExpr : forall destruct e''; try apply (Error error_message). apply OK. apply ELR_leaf. + unfold ξ'. + simpl. + induction (leaves (varsTypes rb φ)). + simpl; auto. + destruct (ξ c). + simpl. apply e1. + destruct case_pf. + set (distinct_decidable (vec2list exprvars')) as dec. + destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ]. + apply OK; auto. + destruct case_case. + exists sac. exists scb. apply ebranch'.