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

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index dd07482..c7625b8 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -46,7 +46,6 @@ Set Printing Width 130.
  *)
 Section HaskFlattener.
 
  *)
 Section HaskFlattener.
 

-

   Ltac eqd_dec_refl' :=
     match goal with
       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
   Ltac eqd_dec_refl' :=
     match goal with
       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>

@@ -232,12 +231,12 @@ Section HaskFlattener.
     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 
   Axiom flatten_commutes_with_HaskTApp :
     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 
   Axiom flatten_commutes_with_HaskTApp :

-    forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
-    flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
-    HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
+    forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
+    flatten_type  (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) =
+    HaskTApp (weakF_ (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ).

 
 

-  Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
-    flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
+  Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t,
+    flatten_leveled_type  (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).

 
   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
     flatten_type (g v) = g v.
 
   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
     flatten_type (g v) = g v.

@@ -407,6 +406,9 @@ Section HaskFlattener.
      apply precompose.
      Defined.
 
      apply precompose.
      Defined.
 

+
+
+

   (* useful for cutting down on the pretty-printed noise
   
   Notation "`  x" := (take_lev _ x) (at level 20).
   (* useful for cutting down on the pretty-printed noise
   
   Notation "`  x" := (take_lev _ x) (at level 20).

@@ -864,7 +866,7 @@ Section HaskFlattener.
       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _

-      | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
+      | RAbsT    Γ Δ Σ κ σ lev n       => let case_RAbsT := tt         in _

       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _

@@ -1161,8 +1163,8 @@ Section HaskFlattener.
       rewrite flatten_commutes_with_HaskTApp.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
       simpl.
       rewrite flatten_commutes_with_HaskTApp.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
       simpl.

-      set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
-      set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
+      set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a.
+      set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.

       assert (a=q').
         unfold a.
         unfold q'.
       assert (a=q').
         unfold a.
         unfold q'.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 84eaa0b..7f15825 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -74,8 +74,8 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
 
 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]
 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
 
 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]

-| RAbsT   : ∀ Γ Δ Σ κ σ   l,
-  Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
+| RAbsT   : ∀ Γ Δ Σ κ σ l n,
+  Rule [(list_ins n κ Γ)> (weakCE_ Δ) >  mapOptionTree weakLT_ Σ |- [ HaskTApp (weakF_ σ) (FreshHaskTyVar_ _) ]@(weakL_ l)]

        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   ]@l]
 
 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
        [Γ>Δ            >    Σ     |- [HaskTAll κ σ   ]@l]
 
 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,

@@ -131,7 +131,7 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )

-| Flat_RAbsT            : ∀ Γ   Σ κ σ a    q    ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q )
+| Flat_RAbsT            : ∀ Γ   Σ κ σ a    q n   ,  Rule_Flat (RAbsT Γ   Σ κ σ a    q n)

 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 | Flat_RAppT            : ∀ Γ Δ  Σ κ σ τ    q    ,  Rule_Flat (RAppT Γ Δ  Σ κ σ τ    q )
 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 716a983..e85bb39 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -184,7 +184,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RGlobal       _ _ _ _ _         => "Global"
     | RLam          _ _ _ _ _ _       => "Abs"
     | RCast         _ _ _ _ _ _ _     => "Cast"
     | RGlobal       _ _ _ _ _         => "Global"
     | RLam          _ _ _ _ _ _       => "Abs"
     | RCast         _ _ _ _ _ _ _     => "Cast"

-    | RAbsT         _ _ _ _ _ _       => "AbsT"
+    | RAbsT         _ _ _ _ _ _ _     => "AbsT"

     | RAppT         _ _ _ _ _ _ _     => "AppT"
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RAppT         _ _ _ _ _ _ _     => "AppT"
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index f50c586..ab10fd8 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -760,7 +760,7 @@ Section HaskProofToStrong.
       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _
       | RGlobal Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam    Γ Δ Σ tx te     x     => let case_RLam := tt          in _
       | RCast   Γ Δ Σ σ τ γ     x     => let case_RCast := tt         in _

-      | RAbsT   Γ Δ Σ κ σ a           => let case_RAbsT := tt         in _
+      | RAbsT   Γ Δ Σ κ σ a n         => let case_RAbsT := tt         in _

       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RAppT   Γ Δ Σ κ σ τ     y     => let case_RAppT := tt         in _
       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _

@@ -940,12 +940,12 @@ Section HaskProofToStrong.
     apply (ileaf X).
 
   destruct case_RAbsT.
     apply (ileaf X).
 
   destruct case_RAbsT.

-    apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
+    apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.

     rewrite mapOptionTree_compose.
     rewrite <- H.
     reflexivity.
     apply ileaf in X. simpl in *.
     rewrite mapOptionTree_compose.
     rewrite <- H.
     reflexivity.
     apply ileaf in X. simpl in *.

-    apply ETyLam.
+    apply (ETyLam _ _ _ _ _ _ n).

     apply X.
 
   destruct case_RAppCo.
     apply X.
 
   destruct case_RAppCo.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index eaf1341..0d1cecb 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -226,7 +226,7 @@ Section HaskSkolemizer.
       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _

-      | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
+      | RAbsT    Γ Δ Σ κ σ lev n       => let case_RAbsT := tt         in _

       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _

@@ -472,7 +472,10 @@ Section HaskSkolemizer.
 
       destruct case_RAbsT.
         simpl.
 
       destruct case_RAbsT.
         simpl.

-        destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+        destruct lev; simpl.
+          apply nd_rule.
+          apply SFlat.
+          apply (@RAbsT Γ Δ Σ κ σ nil n).

         apply (Prelude_error "RAbsT at depth>0").
 
       destruct case_RAppCo.
         apply (Prelude_error "RAbsT at depth>0").
 
       destruct case_RAppCo.

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 874b368..6629511 100644 (file)
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -47,8 +47,8 @@ Section HaskStrong.
   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ) l                   -> Expr Γ Δ ξ (substT σ τ) l
   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ) l
   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l  -> Expr Γ Δ ξ σ l
   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ) l                   -> Expr Γ Δ ξ (substT σ τ) l
   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ) l
   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l  -> Expr Γ Δ ξ σ l

-  | ETyLam : ∀ Γ Δ ξ κ σ l,
-    Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
+  | ETyLam : ∀ Γ Δ ξ κ σ l n,
+    Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l

   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
                Expr Γ Δ ξ (caseType tc atypes) l ->
                Tree ??{ sac : _
   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
                Expr Γ Δ ξ (caseType tc atypes) l ->
                Tree ??{ sac : _

@@ -90,7 +90,7 @@ Section HaskStrong.
     | ETyApp  Γ Δ κ σ τ ξ l       e => "("+++exprToString e+++")@("+++toString τ+++")"
     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => "("+++exprToString e+++")~(co)"
     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
     | 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
+    | ETyLam _ _ _ k _ _ _ e        => "\@_ ->"+++ exprToString e

     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
     | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
     | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
     | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
     | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8ae0d09..e93ddd9 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -520,7 +520,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') :
   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
   | ENote    Γ Δ ξ t l n e                        => expr2antecedent e
   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
   | ENote    Γ Δ ξ t l n e                        => expr2antecedent e

-  | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
+  | ETyLam   Γ Δ ξ κ σ l n e                      => expr2antecedent e

   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e

@@ -1117,7 +1117,7 @@ Definition expr2proof  :
     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)

-    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ETyLam   Γ Δ ξ κ σ l n e                      => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)

     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index deb7adc..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}{κ}(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
   Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
     : UniqM WeakCoercion
     := bind t1' = @typeToWeakType Γ κ t1 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'
     | 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
                                                 ; return WETyLam tv e'
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
                                                 ; bind t2' = typeToWeakType σ₂ ite

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index e5a10ba..46d74cc 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -155,6 +155,7 @@ Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@Ins
 Inductive  LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
 
 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
 Inductive  LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
 
 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.

+

 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
   := fun TV env => TAll κ (σ TV env).
 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
   := fun TV env => TAll κ (σ TV env).
 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)

@@ -350,21 +351,41 @@ Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:Instanti
   unfold InstantiatedCoercionEnv; simpl. 
   apply vec_cons; auto.
   Defined.
   unfold InstantiatedCoercionEnv; simpl. 
   apply vec_cons; auto.
   Defined.

+

 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)

-Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
-  := ilist_tail ite.
+Definition weakITE  {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite.
+Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
+Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)).
+Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite).
+Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
+Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end.
+Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
+  : InstantiatedCoercionEnv TV CV Γ Δ.
+  intros.
+  unfold InstantiatedCoercionEnv; intros.
+  unfold InstantiatedCoercionEnv in ice.
+  unfold weakCE in ice.
+  simpl in ice.
+  rewrite <- map_preserves_length in ice.
+  apply ice.
+  Defined.
+Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
+  unfold HaskCoercionKind in *.
+  intros.
+  apply hck; clear hck.
+  inversion X; subst; auto.
+  Defined.
+Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
+  fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
+Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : 
+  forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
+  := fun TV ite tv => (f TV (weakITE ite) tv).
+
+

 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
   induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.

-Definition weakCE   {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
-  := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
-Definition weakV  {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
-  := fun TV ite => (cv' TV (weakITE ite)).

 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
   induction κ; auto. apply weakV; auto. Defined.
 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
   induction κ; auto. apply weakV; auto. Defined.

-Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
-  := fun TV ite => lt TV (weakITE ite).
-Definition weakL  {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
-  := map weakV lt.

 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
   induction κ; auto. apply weakT; auto. Defined.
 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
   induction κ; auto. apply weakT; auto. Defined.
 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.

@@ -375,34 +396,12 @@ Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ)
   apply lt.
   apply X.
   Defined.
   apply lt.
   apply X.
   Defined.

-Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
-  rewrite <- ass_app in lt.
-  exact lt.
-  Defined.

 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
   induction κ; auto. apply weakL; auto. Defined.
 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
   induction κ; auto. apply weakL; auto. Defined.

-Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
-  := match lt with t @@ l => weakT t @@ weakL l end.

 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
   := match lt with t @@ l => weakT' t @@ weakL' l end.
 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
   induction κ; auto. apply weakCE; auto. Defined.
 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
   := match lt with t @@ l => weakT' t @@ weakL' l end.
 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
   induction κ; auto. apply weakCE; auto. Defined.

-Definition weakICE  {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
-  : InstantiatedCoercionEnv TV CV Γ Δ.
-  intros.
-  unfold InstantiatedCoercionEnv; intros.
-  unfold InstantiatedCoercionEnv in ice.
-  unfold weakCE in ice.
-  simpl in ice.
-  rewrite <- map_preserves_length in ice.
-  apply ice.
-  Defined.
-Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
-  unfold HaskCoercionKind in *.
-  intros.
-  apply hck; clear hck.
-  inversion X; subst; auto.
-  Defined.

 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
   induction κ; auto.
   apply weakCK.
 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
   induction κ; auto.
   apply weakCK.

@@ -410,11 +409,80 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ
   Defined.
 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
   map weakCK' hck.
   Defined.
 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
   map weakCK' hck.

-Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
-  fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
-Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : 
-  forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
-  := fun TV ite tv => (f TV (weakITE ite) tv).
+
+Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
+  rewrite list_ins_app in ite.
+  set (weakITE' ite) as ite'.
+  set (ilist_chop ite) as a.
+  rewrite <- (list_take_drop _ Γ n).
+  apply ilist_app; auto.
+  inversion ite'; auto.
+  Defined.
+
+Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
+  unfold HaskTyVar; intros.
+  unfold HaskTyVar in cv'.
+  apply (cv' TV).
+  apply weakITE_ in env.
+  apply env.
+  Defined.
+
+Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
+  unfold HaskType; intros.
+  apply lt.
+  apply weakITE_ in X.
+  apply X.
+  Defined.
+Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
+  unfold HaskLevel; intros.
+  unfold HaskLevel in lev.
+  eapply map.
+  apply weakV_.
+  apply lev.
+  Defined.
+Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
+  match lt with t@@l => weakT_ t @@ weakL_ l end.
+Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
+  unfold HaskCoercionKind; intros.
+  unfold HaskCoercionKind in hck.
+  apply hck.
+  apply weakITE_ in X.
+  apply X.
+  Defined.
+Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
+Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : 
+  forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
+  intros.
+  apply f.
+  apply weakITE_ in env.
+  apply env.
+  apply X.
+  Defined.
+Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
+  unfold HaskCoVar; intros.
+  unfold HaskCoVar in cv'.  
+  apply (cv' TV).
+  apply weakITE_ in env.
+  apply env.
+  unfold InstantiatedCoercionEnv.
+  unfold InstantiatedCoercionEnv in cenv.
+  replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
+  apply cenv.
+  unfold weakCE_.
+  rewrite <- map_preserves_length.
+  reflexivity.
+  Defined.
+
+Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
+  intros.
+  unfold HaskTyVar.
+  intros.
+  rewrite list_ins_app in env.
+  apply weakITE' in env.
+  inversion env; subst; auto.
+  Defined.
+
+

 
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->
 
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d8dcf42..0acc0af 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -26,6 +26,11 @@ Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
 
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
 

+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
+  rewrite <- ass_app in lt.
+  exact lt.
+  Defined.
+

 Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
   unfold TyVarResolver.
   refine (fun tv' =>
 Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
   unfold TyVarResolver.
   refine (fun tv' =>

@@ -604,9 +609,11 @@ Definition weakExprToStrongExpr : forall
     | WETyLam tv e                      => let φ2 := upPhi tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
     | WETyLam tv e                      => let φ2 := upPhi tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>

-                                                 weakExprToStrongExpr _ (weakCE Δ) φ2
-                                                   (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
-                                                     >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+                                                 weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+                                                   (fun x => (ψ x) >>= fun y =>
+                                                     OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+                                                   >>= fun e' => castExpr we "WETyLam2" _ _
+                                                     (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')

 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with
 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with