allow rank-1 polymorphic types for globals

diff --git a/src/HaskProof.v b/src/HaskProof.v
index a5e4abd..8e4be3f 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -73,7 +73,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 (* SystemFC rules *)
 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
-| RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
+| RGlobal : forall Γ Δ l   (g:Global Γ) v,            Rule [                                 ]   [Γ>Δ>     []   |- [g v        @@l]]
 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
                    HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁@@l]        ]   [Γ>Δ>    Σ     |- [σ₂         @@l]]

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 4773eff..edac1aa 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -101,7 +101,7 @@ Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath
                                       ; let body := t1'+++(rawLatexMath " ")+++t2'
                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
                 end
-  | TyFunApp   tfc lt  => bind rest = typeListToRawLatexMath false lt
+  | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
                                  (rawLatexMath "}")+++

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 3aee219..b14a53e 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -569,7 +569,6 @@ Section HaskProofToStrong.
   destruct case_RGlobal.
     apply ILeaf; simpl; intros; refine (return ILeaf _ _).
     apply EGlobal.
-    apply wev.
 
   destruct case_RLam.
     apply ILeaf.

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 478985d..f9d9f3d 100644 (file)
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -31,7 +31,7 @@ Section HaskStrong.
   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
 
   (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
-  | EGlobal: ∀ Γ Δ ξ t,       WeakExprVar ->                                                         Expr Γ Δ ξ t
+  | EGlobal: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v @@ lev)
 
   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
@@ -79,7 +79,7 @@ Section HaskStrong.
   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
     match exp with
     | EVar  Γ' _ ξ' ev              => "var."+++ toString ev
-    | EGlobal Γ' _ ξ' t wev         => "global." +++ toString (wev:CoreVar)
+    | EGlobal Γ' _ ξ'   g v _       => "global." +++ toString (g:CoreVar)
     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++ toString cv +++":t) -> "+++ exprToString e
     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
     | ELit  _ _ _ lit _             => "lit."+++toString lit

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 13f4907..8cd5688 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -519,7 +519,7 @@ Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstype
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
-  | EGlobal  Γ Δ ξ _ _                            => []
+  | EGlobal  Γ Δ ξ _ _ _                          => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
@@ -929,7 +929,7 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
-    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
+    | EGlobal  Γ Δ ξ     g v lev                    => let case_EGlobal := tt in _
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
@@ -983,8 +983,7 @@ Definition expr2proof  :
     destruct case_EGlobal.
       apply nd_rule.
       simpl.
-      destruct t as [t lev].
-      apply (RGlobal _ _ _ _ wev).
+      apply (RGlobal _ _ _  g).
 
     destruct case_EVar.
       apply nd_rule.

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 79d954c..42790b3 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -61,7 +61,7 @@ Section HaskStrongToWeak.
                                      | WTyVarTy ec => return WCodeTy ec t2'
                                      | _           => failM  "impossible"
                                    end
-    | TyFunApp    tfc tls       => bind tls' = rawHaskTypeListToWeakType tls
+    | TyFunApp    tfc _ _ tls       => bind tls' = rawHaskTypeListToWeakType tls
                                  ; return WTyFunApp tfc tls'
   end
   with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
@@ -111,7 +111,8 @@ Section HaskStrongToWeak.
     -> UniqM WeakExpr :=
     match exp as E in @Expr _ _ G D X 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 Γ' _ ξ' t wev         => fun ite => return WEVar wev
+    | 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))
     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
                                                 ; bind ev' = mkWeakExprVar tv'
                                                 ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 224d70b..7ce04fb 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -69,7 +69,7 @@ Section Raw.
   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
   | TCode          : RawHaskType ★                       -> RawHaskType ★   -> RawHaskType ★                     (* from λ^α *)
-  | TyFunApp       : ∀ tf, RawHaskTypeList (fst (tyFunKind tf))             -> RawHaskType (snd (tyFunKind tf))  (* S_n      *)
+  | TyFunApp       : forall (tf:TyFun) kl k, RawHaskTypeList kl             -> RawHaskType k                     (* S_n      *)
   with RawHaskTypeList : list Kind -> Type :=
   | TyFunApp_nil   : RawHaskTypeList nil
   | TyFunApp_cons  : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
@@ -168,27 +168,31 @@ Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskTy
 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
  fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
 
-(* PHOAS substitution on types *)
-Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
-  : @HaskType Γ κ₂ :=
-fun TV env => 
-    (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
+Section Flatten.
+  Context {TV:Kind -> Type }.
+Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
      match exp with
     | TVar    _  x        => x
-    | TAll     _ y        => TAll   _  (fun v => flattenT _ (y (TVar v)))
-    | TApp   _ _ x y      => TApp      (flattenT _ x) (flattenT _ y)
+    | TAll     _ y        => TAll   _  (fun v => flattenT  (y (TVar v)))
+    | TApp   _ _ x y      => TApp      (flattenT  x) (flattenT  y)
     | TCon       tc       => TCon      tc
-    | TCoerc _ t1 t2 t    => TCoerc    (flattenT _ t1) (flattenT _ t2)   (flattenT _ t)
+    | TCoerc _ t1 t2 t    => TCoerc    (flattenT  t1) (flattenT  t2)   (flattenT  t)
     | TArrow              => TArrow
-    | TCode      v e      => TCode     (flattenT _ v) (flattenT _ e)
-    | TyFunApp       tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
+    | TCode      v e      => TCode     (flattenT  v) (flattenT  e)
+    | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
     end
     with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
     | TyFunApp_nil               => TyFunApp_nil
-    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
-    end
-    for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
+    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flattenT  t) (flattenTyFunApp _ rest)
+    end.
+End Flatten.
+
+(* PHOAS substitution on types *)
+Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
+  : @HaskType Γ κ₂ :=
+  fun TV env =>
+    flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
 
 Notation "t @@  l" := (@mkLeveledHaskType _ _ t l) (at level 20).
 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
@@ -197,6 +201,13 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
   match lht with t@@l => t end.
 
+Structure Global Γ :=
+{ glob_wv    : WeakExprVar
+; glob_kinds : list Kind
+; glob_tf    : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
+}.
+Coercion glob_tf : Global >-> Funclass.
+Coercion glob_wv : Global >-> WeakExprVar.
 
 
 
@@ -461,7 +472,7 @@ match t1 with
 | TArrow           => match t2 with TArrow => true | _ => false end
 | TCode      ec t  => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
 | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
-| TyFunApp tfc lt  => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
+| TyFunApp tfc kl k lt  => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
 end
 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
 match t1 with
@@ -556,7 +567,7 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat)
                               in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
                                    typeToString' false (S n) (f n)
     | TCode  ec t          => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
-    | TyFunApp   tfc lt    => toString tfc+++ "_" +++ toString n+++" ["+++
+    | TyFunApp   tfc kl k lt    => toString tfc+++ "_" +++ toString n+++" ["+++
       (fold_left (fun x y => " \  "+++x+++y) (typeList2string false n lt) "")+++"]"
   end
   with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 6d4bf16..b9ac068 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -176,7 +176,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
-    apply TyFunApp.
+    apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
     apply lt'.
     apply X.
 
@@ -519,6 +519,14 @@ Definition checkDistinct :
   exact (Error "checkDistinct failed").
   Defined.
 
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+  refine {| glob_kinds := nil |}.
+  apply wev.
+  intros.
+  apply τ.
+  Defined.
+
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
@@ -544,7 +552,7 @@ Definition weakExprToStrongExpr : forall
     match we with
 
     | WEVar   v                         => if ig v
-                                              then OK (EGlobal Γ Δ ξ (τ@@lev) v)
+                                              then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
                                               else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 
     | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)