From: Adam Megacz Date: Mon, 7 Mar 2011 13:41:43 +0000 (-0800) Subject: better names for the auxiliary CaseBranch records X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=8282f5a7639dbe862bba29d3170d58b81bbb1446 better names for the auxiliary CaseBranch records --- diff --git a/src/HaskProof.v b/src/HaskProof.v index 606b667..2508976 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -49,12 +49,13 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := (* information needed to define a case branch in a HaskProof *) Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} := -{ cbi_cbi : @StrongAltConInContext n tc Γ avars -; cbri_freevars : Tree ??(LeveledHaskType Γ) -; cbri_judg := cbi_Γ cbi_cbi > cbi_Δ cbi_cbi - > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi))) +{ pcb_scb : @StrongCaseBranch n tc Γ avars +; pcb_freevars : Tree ??(LeveledHaskType Γ) +; pcb_judg := scb_Γ pcb_scb > scb_Δ pcb_scb + > (mapOptionTree weakLT' pcb_freevars),,(unleaves (vec2list (scb_types pcb_scb))) |- [weakLT' (branchtype @@ lev)] }. +Coercion pcb_scb : ProofCaseBranch >-> StrongCaseBranch. Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) @@ -108,9 +109,9 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RCase : forall Γ Δ lev n tc Σ avars tbranches (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)), Rule - ((mapOptionTree cbri_judg alts),, + ((mapOptionTree pcb_judg alts),, [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) - [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches @@ lev ] ] + [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches @@ lev ] ] . Coercion RURule : URule >-> Rule. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index bab6e04..2582fb4 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -16,14 +16,14 @@ Section HaskStrong. (* any type with decidable equality may be used to represent value variables *) Context `{EQD_VV:EqDecidable VV}. - (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *) - Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := - { cbi_sacic : @StrongAltConInContext n tc Γ atypes - ; cbi_vars : vec VV (tagNumValVars (cbi_tag cbi_sacic)) - ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic)) + (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) + Record StrongCaseBranchWithVVs {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := + { scbwv_scb : @StrongCaseBranch n tc Γ atypes + ; scbwv_exprvars : vec VV (saci_numExprVars scbwv_scb) + ; scbwv_varstypes := vec2list (vec_zip scbwv_exprvars (scb_types scbwv_scb)) }. - Implicit Arguments ExprCaseBranch [[n][Γ]]. - Coercion cbi_sacic : ExprCaseBranch >-> StrongAltConInContext. + Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]]. + Coercion scbwv_scb : StrongCaseBranchWithVVs >-> StrongCaseBranch. Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type := | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) @@ -43,8 +43,8 @@ Section HaskStrong. | ECase : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches, Expr Γ Δ ξ (caseType tc atypes @@ l) -> - Tree ??{ scb : ExprCaseBranch tc atypes - & Expr (cbi_Γ scb) (cbi_Δ scb) (update_ξ (weakLT'○ξ) (cbi_varstypes scb)) (weakLT' (tbranches@@l)) } -> + Tree ??{ scb : StrongCaseBranchWithVVs tc atypes + & Expr (scb_Γ scb) (scb_Δ scb) (update_ξ (weakLT'○ξ) (scbwv_varstypes scb)) (weakLT' (tbranches@@l)) } -> Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in @@ -60,3 +60,4 @@ Section HaskStrong. . End HaskStrong. +Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]]. \ No newline at end of file diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index e9f3520..614a09c 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -125,48 +125,22 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). - -(* A "tag" is something that distinguishes one case branch from another; it's a lot like Core's AltCon *) -Inductive Tag {n:nat}(tc:TyCon n) : Type := -| TagDefault : Tag tc -| TagLiteral : forall lit:HaskLiteral , Tag tc (* FIXME: solution is a new StrongLiteral indexed by a tycon *) -| TagDataCon : forall m q z, DataCon tc m q z -> Tag tc. - -(* the number of value variables bound in branches with the given tag *) -Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat := - match tag with - | TagDefault => 0 - | TagLiteral lit => 0 - | TagDataCon m q z dc => z - end. - -(* the number of existential type variables bound in branches with the given tag *) -Definition tagNumExVars {n}{tc:TyCon n}(tag:Tag tc) : nat := - match tag with - | TagDefault => 0 - | TagLiteral lit => 0 - | TagDataCon m q z dc => m - end. - -(* the number of coercion variables bound in branches with the given tag *) -Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat := - match tag with - | TagDefault => 0 - | TagLiteral lit => 0 - | TagDataCon m q z dc => q - end. +(* like a GHC DataCon, but using PHOAS representation for types and coercions *) +Record StrongAltConInfo {n}{tc:TyCon n} := +{ saci_numExTyVars : nat +; saci_numCoerVars : nat +; saci_numExprVars : nat +; saci_akinds : vec Kind n +; saci_ekinds : vec Kind saci_numExTyVars +; saci_kinds := app (vec2list saci_akinds) (vec2list saci_ekinds) +; saci_coercions : vec (HaskType saci_kinds * HaskType saci_kinds) saci_numCoerVars +; saci_types : vec (HaskType saci_kinds) saci_numExprVars +}. +Implicit Arguments StrongAltConInfo [[n]]. Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). -Record StrongAltCon {n}{tc:TyCon n}{alt:Tag tc} := -{ cb_akinds : vec Kind n -; cb_ekinds : vec Kind (tagNumExVars alt) -; cb_kinds := app (vec2list cb_akinds) (vec2list cb_ekinds) -; cb_coercions : vec (HaskType cb_kinds * HaskType cb_kinds) (tagNumCoVars alt) -; cb_types : vec (HaskType cb_kinds) (tagNumValVars alt) -}. -Implicit Arguments StrongAltCon [[n][tc]]. @@ -300,7 +274,7 @@ with ListWellKinded_RawHaskType (TV:Type) Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind := match rht with | TVar k => k - | TCon n tc => ̱★ (* FIXME: use the StrongAltCon *) + | TCon n tc => ̱★ (* FIXME: use the StrongAltConInfo *) | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ )) | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) @@ -411,12 +385,12 @@ Fixpoint update_ξ (* just like GHC's AltCon, but using PHOAS types and coercions *) -Record StrongAltConInContext {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := -{ cbi_tag : Tag tc -; cbi_cb : StrongAltCon cbi_tag -; cbi_Γ : TypeEnv := app (vec2list (cb_ekinds cbi_cb)) Γ -; cbi_Δ : CoercionEnv cbi_Γ -; cbi_types : vec (LeveledHaskType (app (vec2list (cb_ekinds cbi_cb)) Γ)) (tagNumValVars cbi_tag) +Record StrongCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := +{ scb_saci : @StrongAltConInfo _ tc +; scb_Γ : TypeEnv := app (vec2list (saci_ekinds scb_saci)) Γ +; scb_Δ : CoercionEnv scb_Γ +; scb_types : vec (LeveledHaskType (app (vec2list (saci_ekinds scb_saci)) Γ)) (saci_numExprVars scb_saci) }. -Implicit Arguments StrongAltConInContext [[n][Γ]]. +Coercion scb_saci : StrongCaseBranch >-> StrongAltConInfo. +Implicit Arguments StrongCaseBranch [[n][Γ]]. diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 959133d..6e6a87d 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -91,4 +91,4 @@ Section HaskWeakToCore. (weakExprToCoreExpr e) end. -End HaskWeakToCore. \ No newline at end of file +End HaskWeakToCore.