allow quantification over any tyvar in the environment, not just the first

[coq-hetmet.git] / src / HaskStrongToWeak.v

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index d86d05b..8bb52e1 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -79,6 +79,18 @@ Section HaskStrongToWeak.
   Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
     := tv::::ite.
   
+  Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+    : InstantiatedTypeEnv TV (list_ins n κ Γ).
+    rewrite list_ins_app.
+    rewrite <- (list_take_drop _ Γ n) in ite.
+    apply ilist_app.
+    apply ilist_chop in ite; auto.
+    apply ICons.
+    apply tv.
+    apply ilist_chop' in ite.
+    apply ite.
+    Defined.
+  
   Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
     : UniqM WeakCoercion
     := bind t1' = @typeToWeakType Γ κ t1 ite
@@ -107,10 +119,10 @@ Section HaskStrongToWeak.
       | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
     end.
 
-  Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
+  Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
     : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
     -> UniqM WeakExpr :=
-    match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
+    match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
     | EVar  Γ' _ ξ' ev              => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
     | EGlobal Γ' _ ξ'   g v lev     => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
                                                 ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
@@ -133,7 +145,7 @@ Section HaskStrongToWeak.
     | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
                                                 ; bind e' = exprToWeakExpr χ e ite
                                                 ; return WEBrak hetmet_brak (ec _ ite) e' t'
-    | ENote _ _ _ _ n e             => fun ite => bind e' = exprToWeakExpr χ e ite
+    | ENote _ _ _ _ _ n e           => fun ite => bind e' = exprToWeakExpr χ e ite
                                                 ; return WENote n e'
     | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
                                                 ; bind e' = exprToWeakExpr χ e ite
@@ -144,8 +156,8 @@ Section HaskStrongToWeak.
     | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
                                                 ; return WECast e' c'
-    | ETyLam _ _ _ k _ _ e          => fun ite => bind tv = mkWeakTypeVar k
-                                                ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
+    | ETyLam _ _ _ k _ _ n e        => fun ite => bind tv = mkWeakTypeVar k
+                                                ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
                                                 ; return WETyLam tv e'
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
                                                 ; bind t2' = typeToWeakType σ₂ ite
@@ -158,7 +170,7 @@ Section HaskStrongToWeak.
                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
                   ; bind escrut'    = exprToWeakExpr χ escrut ite
                   ; bind branches'  =
-                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
+                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
                             match tree with
                               | T_Leaf None           => return []
@@ -208,7 +220,7 @@ Section HaskStrongToWeak.
   end.
 
 
-  Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
+  Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
     : ???WeakExpr :=
     match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with