X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrong.v;h=c5f46dc5bf216017125b123131c766d639b20843;hp=1e1ce432a53c208b0a619fd0cfb9f4a01562219f;hb=2d963cf6994fa510fe67d5bf3852ffcc8090496c;hpb=7b2698b0dfe1d271a68a0efe2bf0d129b5f1f93e diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 1e1ce43..c5f46dc 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -12,6 +12,7 @@ Require Import HaskCoreTypes. Require Import HaskLiteralsAndTyCons. Require Import HaskStrongTypes. Require Import HaskWeakVars. +Require Import HaskCoreVars. Section HaskStrong. @@ -19,16 +20,13 @@ Section HaskStrong. Context `{EQD_VV:EqDecidable VV}. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - - 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 - (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes)) + Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} := + { scbwv_exprvars : vec VV (sac_numExprVars sac) + ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) + ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes) + ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. - Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon. Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := @@ -38,8 +36,8 @@ Section HaskStrong. | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) - | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) - | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) + | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, @@ -54,14 +52,16 @@ Section HaskStrong. Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) | ECase : forall Γ Δ ξ l tc tbranches atypes, Expr Γ Δ ξ (caseType tc atypes @@ l) -> - Tree ??{ scb : StrongCaseBranchWithVVs tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ + & { scb : StrongCaseBranchWithVVs tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) } -> + (weakLT' (tbranches@@l)) } } -> Expr Γ Δ ξ (tbranches @@ l) - | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in + | ELetRec : ∀ Γ Δ ξ l τ vars, + let ξ' := update_ξ ξ l (leaves vars) in ELetRecBindings Γ Δ ξ' l vars -> Expr Γ Δ ξ' (τ@@l) -> Expr Γ Δ ξ (τ@@l) @@ -69,27 +69,24 @@ 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 : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))] + | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)] | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) . - Context {ToStringVV:ToString VV}. - - Require Import HaskCoreVars. - + Context {ToLatexVV:ToLatex VV}. Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string := match exp with - | EVar Γ' _ ξ' ev => "var."+++ev - | EGlobal Γ' _ ξ' t wev => "global." +++(wev:CoreVar) - | ELam Γ' _ _ tv _ _ cv e => "\("+++cv+++":t) -> "+++ exprToString e - | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++ev+++" = "+++exprToString e1+++" in "+++exprToString e2 - | ELit _ _ _ lit _ => "lit."+++lit + | EVar Γ' _ ξ' ev => "var."+++ toString ev + | EGlobal Γ' _ ξ' t wev => "global." +++ toString (wev:CoreVar) + | ELam Γ' _ _ tv _ _ cv e => "\("+++ toString cv +++":t) -> "+++ exprToString e + | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2 + | ELit _ _ _ lit _ => "lit."+++toString lit | EApp Γ' _ _ _ _ _ e1 e2 => "("+++exprToString e1+++")("+++exprToString e2+++")" | EEsc Γ' _ _ ec t _ e => "~~("+++exprToString e+++")" | EBrak Γ' _ _ ec t _ e => "<["+++exprToString e+++"]>" | ENote _ _ _ _ n e => "note."+++exprToString e - | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++τ+++")" + | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")" | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)" | ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2" | ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e