X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrong.v;h=2582fb41f063a7b4aae15bf70da658be14aca66d;hb=8282f5a7639dbe862bba29d3170d58b81bbb1446;hp=6f0efa096b901451c95dc07a4e299e0daffa7745;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f;p=coq-hetmet.git

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 6f0efa0..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,20 +43,21 @@ 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
-    ELetRecBindings Γ Δ ξ'     l (mapOptionTree (@snd _ _) vars) ->
+    ELetRecBindings Γ Δ ξ'     l vars ->
     Expr            Γ Δ ξ' (τ@@l) ->
     Expr            Γ Δ ξ  (τ@@l)
 
   (* 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 : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(HaskType Γ) -> Type :=
+  with ELetRecBindings : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ) -> Type :=
   | ELR_nil    : ∀ Γ Δ ξ l  ,                                                                 ELetRecBindings Γ Δ ξ l []
-  | ELR_leaf   : ∀ Γ Δ ξ t l,                                          Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [t]
+  | ELR_leaf   : ∀ Γ Δ ξ t l v,                                        Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
   | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
   .
 
 End HaskStrong.
+Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]].
\ No newline at end of file