From: Adam Megacz Date: Sun, 13 Mar 2011 05:54:20 +0000 (-0800) Subject: restore HaskWeakToStrong functionality that I broke over the weekend X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=1f411b48dd607e76a65903e8506d0ae5e7470321;hp=1758dade15ff584949a9e4bd6b21ce1a58e42ff3 restore HaskWeakToStrong functionality that I broke over the weekend --- diff --git a/src/Extraction.v b/src/Extraction.v index 7391246..65f3f2d 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -78,7 +78,7 @@ Section core2proof. * free tyvars in them *) Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ := match coreVarToWeakVar cv with - | WExprVar wev => match weakTypeToType' φ wev ★ with + | WExprVar wev => match weakTypeToType'' φ wev ★ with | Error s => Prelude_error ("Error in top-level xi: " +++ s) | OK t => t @@ nil end diff --git a/src/General.v b/src/General.v index f3e4379..7af1fc3 100644 --- a/src/General.v +++ b/src/General.v @@ -615,6 +615,17 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), + + +CoInductive Fresh A T := +{ next : forall a:A, (T a * Fresh A T) +; split : Fresh A T * Fresh A T +}. + + + + + Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))). diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 644d04d..b538417 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -102,7 +102,7 @@ Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion := let (t1,t2) := coreCoercionKind cc in coreTypeToWeakType t1 >>= fun t1' => coreTypeToWeakType t2 >>= fun t2' => - OK (weakCoercion t1' t2' cc). + OK (weakCoercion (kindOfCoreType t1) t1' t2' cc). Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with diff --git a/src/HaskStrong.v b/src/HaskStrong.v index b7229d0..2c418bd 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -20,8 +20,8 @@ Section HaskStrong. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{sac:@StrongAltCon tc}{atypes:IList _ (HaskType Γ) (tyConKind sac)} := - { scbwv_sac := sac + Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} := + { scbwv_sac : @StrongAltCon tc ; 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 @@ -48,9 +48,9 @@ Section HaskStrong. Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) | ETyLam : ∀ Γ Δ ξ κ σ l, Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) - | ECase : forall Γ Δ ξ l tc tbranches sac atypes, + | ECase : forall Γ Δ ξ l tc tbranches atypes, Expr Γ Δ ξ (caseType tc atypes @@ l) -> - Tree ??{ scb : StrongCaseBranchWithVVs tc sac atypes + Tree ??{ scb : StrongCaseBranchWithVVs tc atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) @@ -65,7 +65,7 @@ Section HaskStrong. (* 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 : ∀ Γ, 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_leaf : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))] | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) . diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 18e7825..753362e 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -12,11 +12,9 @@ Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskStrongTypes. Require Import HaskStrong. +Require Import HaskWeakVars. Require Import HaskProof. -Axiom fail : forall {A}, string -> A. - Extract Inlined Constant fail => "Prelude.error". - Section HaskStrongToProof. (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform @@ -89,9 +87,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? let branch_context := eLetRecContext branches in let all_contexts := (expr2antecedent body),,branch_context in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts - | ECase Γ Δ ξ l tc tbranches sac atypes e' alts => + | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) @@ -106,48 +104,41 @@ end with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => expr2antecedent e + | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2) end. -(* -Definition caseBranchRuleInfoFromEStrongAltCon - `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) : - @StrongAltConRuleInfo n tc Γ lev tbranches. - set (ecase2antecedent _ _ _ _ _ _ _ _ ecb) as Σ. - destruct ecb. - apply Build_StrongAltConRuleInfo with (pcb_scb := alt)(pcb_Σ := mapOptionTree ξ Σ). - Defined. - -Definition judgFromEStrongAltCon - `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) : - Judg. - apply caseBranchRuleInfoFromEStrongAltCon in ecb. - destruct ecb. - eapply pcb_judg. - Defined. +Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} + (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes + & Expr (sac_Γ scb Γ) + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) }) + : ProofCaseBranch tc Γ Δ l tbranches atypes. + exact + {| pcb_scb := projT1 alt + ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt))) + |}. + Defined. -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 Γ ★) := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev] + | ELR_leaf Γ Δ ξ lev v e => [ξ v] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2) end. Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV := match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => [v] + | ELR_leaf Γ Δ ξ lev v e => [v] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2) end. Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):= match elrb with | ELR_nil Γ Δ ξ lev => [] - | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)] + | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)] | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2) end. @@ -340,7 +331,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, rewrite H. clear H. - (* FIXME TOTAL BOGOSITY *) + (* FIXME: this only works because the variables are all distinct, but I need to prove that *) assert ((stripOutVars (leaves v2) v1) = v1). admit. rewrite H. @@ -424,14 +415,14 @@ admit. Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) | lrsp_leaf : forall v e, - (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [((unlev (ξ v) @@ lev))]]) -> - LetRecSubproofs Γ Δ ξ lev [(v, (unlev (ξ v)))] (ELR_leaf _ _ _ _ _ _ e) + (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) -> + LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e) | lrsp_cons : forall t1 t2 b1 b2, LetRecSubproofs Γ Δ ξ lev t1 b1 -> LetRecSubproofs Γ Δ ξ lev t2 b2 -> LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2). -Lemma dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), +Lemma cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree), eLetRecTypes branches = mapOptionTree (update_ξ'' ξ tree lev) @@ -460,7 +451,8 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches apply REmptyGroup. unfold mapOptionTree. simpl. - apply n. +admit. +(* apply n.*) eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. @@ -520,7 +512,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; auto. - rewrite dork in q. + rewrite cheat9 in q. set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz. unfold update_ξ'' in *. rewrite <- zz in q. @@ -533,9 +525,26 @@ Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (L admit. Qed. *) -Lemma cheat : forall {T} (a b:T), a=b. - admit. - Defined. + +Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts', +mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) += +(* +((mapOptionTreeAndFlatten +(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) + (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)). +*) +((mapOptionTreeAndFlatten pcb_freevars + (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). +admit. +Defined. + +Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l). + admit. + Defined. +Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t. +admit. +Defined. Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), @@ -562,7 +571,7 @@ Definition expr2proof : : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' := match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ - | ELR_leaf Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e) + | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e) | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) end ) _ _ _ _ tree branches) in @@ -575,24 +584,23 @@ Definition expr2proof : | 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 => -(* + | ECase Γ Δ ξ l tc tbranches atypes e alts' => let dcsp := ((fix mkdcsp (alts: - Tree ??{ scb : StrongCaseBranchWithVVs tc avars + Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) - (weakLT' (tbranches@@lev)) }) - : ND Rule [] (mapOptionTree judgFromEStrongAltCon alts) := - match alts as ALTS return ND Rule [] (mapOptionTree judgFromEStrongAltCon ALTS) with + (sac_Δ scb Γ atypes (weakCK'' Δ)) + (scbwv_ξ scb ξ l) + (weakLT' (tbranches@@l)) }) + : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) := + match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with | T_Leaf None => let case_nil := tt in _ | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x)) - | T_Branch b1 b2 => let case_branch := tt in _ - end) alts) - in *) let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | T_Branch b1 b2 => let case_branch := tt in _ + end) alts') + in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) end -); clear exp ξ' τ' Γ' Δ'; simpl in *. +); clear exp ξ' τ' Γ' Δ'. destruct case_EVar. apply nd_rule. @@ -630,7 +638,7 @@ Definition expr2proof : auto. inversion H. - destruct case_ELet; intros. + destruct case_ELet; intros; simpl in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | apply pf_let]. @@ -670,63 +678,58 @@ Definition expr2proof : apply e'. auto. - destruct case_ETyApp; intros. + destruct case_ETyApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ]. apply e'. auto. - destruct case_ECoLam; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. - apply e'. - - destruct case_ECoApp; intros. + destruct case_ECoApp; simpl in *; intros. eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ]. apply e'. auto. - destruct case_ETyLam; intros. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. - unfold mapOptionTree in e'. - rewrite mapOptionTree_compose in e'. - unfold mapOptionTree. - apply e'. - - destruct case_ECase. - unfold mapOptionTree; simpl; fold (mapOptionTree ξ). - apply (fail "ECase not implemented"). - (* - eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod. - rewrite <- mapOptionTree_compose. - apply dcsp. - apply e'. - *) - - destruct case_elr_leaf; intros. - assert (unlev (ξ0 v) = t0). - apply cheat. - set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q. - rewrite H in q. - apply q. - apply e'0. - - destruct case_ELetRec; intros. - set (@letRecSubproofsToND') as q. - simpl in q. - apply q. - clear q. - apply e'. - apply subproofs. - - (* destruct case_leaf. unfold pcb_judg. simpl. - clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u. repeat rewrite <- mapOptionTree_compose in *. - set (nd_comp ecb' - (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q. - idtac. + set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ + (unleaves (vec2list (scbwv_exprvars (projT1 x)))) + (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*) + _ _ + ))) as q. + +rewrite cheat2 in q. +rewrite cheat1. +unfold weakCK'' in q. +simpl in q. +admit. +(* +replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ) + (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) + (expr2antecedent (projT2 x)))) +with (mapOptionTree (scbwv_ξ (projT1 x) ξ l) + (stripOutVars (vec2list (scbwv_exprvars (projT1 x))) + (expr2antecedent (projT2 x)))). +rewrite <- cheat1 in q. +rewrite vec2list_map_list2vec in q. +unfold mapOptionTree. +fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★) + (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)). +admit. +*) +admit. + +(* +assert ( + +unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x)))) += +unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l). +admit. +Set Printing Implicit. +idtac. +rewrite <- H. + assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))). apply update_ξ_and_reapply. rewrite H. @@ -745,15 +748,43 @@ Definition expr2proof : (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0). apply q. apply cheat. +*) destruct case_branch. simpl; eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply (mkdcsp b1). apply (mkdcsp b2). - *) - Defined. + destruct case_ECase. + rewrite cheat0. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod. + rewrite <- mapOptionTree_compose. + apply dcsp. + apply e'. + + destruct case_ELetRec; simpl in *; intros. + set (@letRecSubproofsToND') as q. + simpl in q. + apply q. + clear q. + apply e'. + apply subproofs. + + (* + destruct case_ECoLam; simpl in *; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ]. + apply e'. + + destruct case_ETyLam; intros. + eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ]. + unfold mapOptionTree in e'. + rewrite mapOptionTree_compose in e'. + unfold mapOptionTree. + apply e'. + *) + Admitted. End HaskStrongToProof. @@ -769,3 +800,4 @@ Inductive Decl :=. Inductive Pgm Γ Δ := mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ. *) + diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 1530e91..a7f6b77 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -18,10 +18,17 @@ Require Import HaskWeak. Require Import HaskStrongTypes. Require Import HaskStrong. -CoInductive Fresh A T := -{ next : forall a:A, (T a * Fresh A T) -; split : Fresh A T * Fresh A T -}. +Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ) + : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) := + match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) * + (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with + | nil => (f,(vec_nil,ite)) + | k::lk' => + let (f',varsite') := mfresh f lk' ite + in let (vars,ite') := varsite' + in let (v,f'') := next _ _ f' k + in (f'',((v:::vars),v::::ite')) + end. Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : WeakType := @@ -52,10 +59,7 @@ Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)) Variable unsafeCoerce : WeakCoercion. Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce". Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) - : WeakCoercion. - unfold HaskCoercion in τ. - admit. - Defined. + : WeakCoercion := unsafeCoerce. (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *) @@ -68,9 +72,6 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH} Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) := tv::::ite. -Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := - match lht with t@@l => t end. - Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) @@ -89,14 +90,14 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp | 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 => +| ECase Γ Δ ξ l tc tbranches 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 sac atypes + (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes & Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) (update_ξ (weakLT'○ξ) (vec2list (vec_map @@ -106,11 +107,15 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp match tree with | T_Leaf None => [] | T_Leaf (Some x) => let (scb,e) := x in - (*[(sac_altcon scb, - nil, (* FIXME *) - nil, (* FIXME *) - (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *) - strongExprToWeakExpr ftv fcv e (weakITE' ite))]*) [] + let (ftv',evarsite') := mfresh ftv _ ite in + let fcv' := fcv in + let (evars,ite') := evarsite' in + [(sac_altcon scb, + vec2list evars, + nil (*FIXME*), + map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)), + strongExprToWeakExpr ftv' fcv' e ite' + )] | T_Branch b1 b2 => (caseBranches b1),,(caseBranches b2) end ) alts) @@ -129,6 +134,6 @@ with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars} 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 _ _ _ t cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv t ite)),(strongExprToWeakExpr ftv fcv e ite))] +| ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))] | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite) end. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 87d02a1..1bab8f5 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -9,11 +9,11 @@ Require Import Coq.Lists.List. Require Import General. Require Import HaskKinds. Require Import HaskCoreLiterals. -Require Import HaskCoreTypes. (* FIXME *) -Require Import HaskCoreVars. (* FIXME *) +Require Import HaskCoreTypes. +Require Import HaskCoreVars. Require Import HaskWeakTypes. -Require Import HaskWeakVars. (* FIXME *) -Require Import HaskCoreToWeak. (* FIXME *) +Require Import HaskWeakVars. +Require Import HaskCoreToWeak. Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars". @@ -175,6 +175,7 @@ Inductive HaskTypeOfSomeKind (Γ:TypeEnv) := 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). @@ -216,6 +217,8 @@ 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). +Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := + match lht with t@@l => t end. @@ -311,11 +314,15 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ 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 weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := + map weakCK' hck. Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)). Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : @@ -351,7 +358,7 @@ Record StrongAltCon {tc:TyCon} := ; sac_numExprVars : nat ; sac_ekinds : vec Kind sac_numExTyVars ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds) -; sac_Γ := fun Γ => app (tyConKind tc) Γ +; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ ; 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)) Δ diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 78cd6ae..f177e1f 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -119,11 +119,11 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := 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') - | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t') + | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t') | WELet ev ve e => weakTypeOfWeakExpr e | WELetRec rb e => weakTypeOfWeakExpr e | WENote n e => weakTypeOfWeakExpr e - | WECast e (weakCoercion t1 t2 _) => OK t2 + | WECast e (weakCoercion _ t1 t2 _) => OK t2 | WECase scrutinee tbranches tc type_params alts => OK tbranches (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *) diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index f0a8300..cfaf65e 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -31,40 +31,35 @@ Variable trustMeCoercion : CoreCoercion. Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". -(* a dummy variable which is never referenced but needed for a binder *) -Variable dummyVariable : CoreVar. - (* FIXME this doesn't actually work *) - Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")". - Section HaskWeakToCore. (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *) Context (hetmet_brak_var : CoreVar). Context (hetmet_esc_var : CoreVar). - (* FIXME: do something more intelligent here *) Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := fun _ => trustMeCoercion. - Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := + Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar := match me with | WEVar (weakExprVar v _) => CoreEVar v | WELit lit => CoreELit lit - | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) - | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) - | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) + | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2) + | WETyApp e t => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t)) + | WECoApp e co => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) - | WENote n e => CoreENote n (weakExprToCoreExpr e ) - | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e ) - | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e ) - | WECoLam (weakCoerVar cv _ _) e => CoreELam cv (weakExprToCoreExpr e ) - | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co) + | WENote n e => CoreENote n (weakExprToCoreExpr f e ) + | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr f e ) + | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr f e ) + | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr f e ) + | WECast e co => CoreECast (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co) | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t)) | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t)) - | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) - | WECase e tbranches tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches) + | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr f ve)) (weakExprToCoreExpr f e) + | WECase e tbranches tc types alts => let (v,f') := next _ _ f tt in + CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches) (sortAlts (( fix mkCaseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := @@ -77,17 +72,17 @@ Section HaskWeakToCore. (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) (map (fun v:WeakExprVar => weakVarToCoreVar v) evars)) - (weakExprToCoreExpr e))::nil + (weakExprToCoreExpr f' e))::nil end ) alts)) | WELetRec mlr e => CoreELet (CoreRec ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) := match mlr with | T_Leaf None => nil - | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil + | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2) end) mlr)) - (weakExprToCoreExpr e) + (weakExprToCoreExpr f e) end. End HaskWeakToCore. diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index fbd47fb..3317445 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -213,23 +213,31 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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'. + 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. @@ -244,7 +252,6 @@ Definition mkStrongAltCon : @StrongAltCon tc. {| 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 _ @@ -254,25 +261,48 @@ Definition mkStrongAltCon : @StrongAltCon tc. 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. @@ -295,47 +325,50 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. 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). 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 "+++tc+++", found a branch with datacon "+++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 ψ. + intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + rewrite weakCK'_nil_inert. 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. -*) - Definition weakExprVarToWeakType : WeakExprVar -> WeakType := fun wev => match wev with weakExprVar _ t => t end. Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType. -(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*) +Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ. Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) : WeakCoerVar -> HaskCoVar Γ (κ::Δ). @@ -359,17 +392,47 @@ Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarE apply e. Defined. -Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ). +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': ". + matchThings κ κ0 "Kind mismatch in weakTypeToType'': ". subst. apply OK. apply h. Defined. +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 (Γ:TypeEnv) (Δ:CoercionEnv Γ) @@ -395,9 +458,9 @@ Definition weakExprToStrongExpr : forall | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev) - | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv => + | WELam ev e => weakTypeToType'' φ ev ★ >>= fun tv => weakTypeOfWeakExpr e >>= fun t => - weakTypeToType' φ t ★ >>= fun τ' => + weakTypeToType'' φ t ★ >>= fun τ' => weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil)) τ' _ e >>= fun e' => castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') @@ -405,7 +468,7 @@ Definition weakExprToStrongExpr : forall | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e') - | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' => + | WEEsc ec e tbody => weakTypeToType'' φ tbody ★ >>= fun tbody' => match lev with | nil => Error "ill-leveled escapification" | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e @@ -414,21 +477,21 @@ Definition weakExprToStrongExpr : forall end | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') - | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv => + | 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' => + 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 τ' => + weakTypeToType'' φ' te ★ >>= fun τ' => weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e >>= fun e' => castExpr "WETyLam1" _ e' >>= fun e'' => @@ -438,20 +501,107 @@ Definition weakExprToStrongExpr : forall match te with | WForAllTy wtv te' => let φ' := upφ wtv φ in - weakTypeToType' φ' te' ★ >>= fun te'' => + weakTypeToType'' φ' te' ★ >>= fun te'' => weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' => - weakTypeToType' φ t wtv >>= fun t' => + 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" + | 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 "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 "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') + + | WECast e co => let (κ,t1,t2,_) := co in + weakTypeToType'' φ t1 ★ >>= fun t1' => + weakTypeToType'' φ t2 ★ >>= fun t2' => + weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' => + castExpr "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 e tbranches tc avars alts => + mkAvars avars (tyConKind tc) φ >>= fun avars' => + weakTypeToType'' φ tbranches ★ >>= fun tbranches' => + weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' => +(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 "ECase" _ (ECase Γ Δ ξ lev tc tbranches' avars' e' tree) end)). + + destruct case_some. + simpl. + 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. + apply e1. + + destruct case_case. + clear mkTree t o e' p e p0 p1 p2 alts weakExprToStrongExpr ebranch. + exists scb. + apply ebranch'. Defined. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 8d84610..8a77e09 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -14,10 +14,10 @@ Require Import HaskCoreTypes. Require Import HaskWeakTypes. (* TO DO: finish this *) -Inductive WeakCoercion : Type := weakCoercion : WeakType -> WeakType -> CoreCoercion -> WeakCoercion. +Inductive WeakCoercion : Type := weakCoercion : Kind -> WeakType -> WeakType -> CoreCoercion -> WeakCoercion. (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) -Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar. +Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar. (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *) Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar. @@ -37,9 +37,9 @@ Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind := Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := match wv with - | WExprVar (weakExprVar v _ ) => v - | WTypeVar (weakTypeVar v _ ) => v - | WCoerVar (weakCoerVar v _ _ ) => v + | WExprVar (weakExprVar v _ ) => v + | WTypeVar (weakTypeVar v _ ) => v + | WCoerVar (weakCoerVar v _ _ _) => v end. Coercion weakVarToCoreVar : WeakVar >-> CoreVar.