better names for the auxiliary CaseBranch records

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 606b667..2508976 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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.