X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=759dcb9ac26f04d129d21017235cd7df788fabf4;hp=d5eeecf5a160f2826a60513b07524b9723fa8071;hb=8c26722a1ee110077968a8a166eb7130266b2035;hpb=b8f6adf700fa3c67feefaea3d2cf5c4626300489

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index d5eeecf..759dcb9 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -22,35 +22,36 @@ CoInductive Fresh A T :=
 ; split : Fresh A T * Fresh A T
 }.
 
-Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))(rht:RawHaskType WeakTypeVar) {struct rht} : WeakType :=
+Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
+ {struct rht} : WeakType :=
 match rht with
-  | TVar    v                 => WTyVarTy v
+  | TVar  _  v                 => WTyVarTy v
   | TCon      tc              => WTyCon tc
-  | TCoerc  t1 t2 t3          => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
+  | TCoerc _ t1 t2 t3          => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
   | TArrow                    => WFunTyCon
-  | TApp    t1 t2             => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
+  | TApp  _ _  t1 t2             => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
   | TAll    k rht'            => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv))
   | TCode   t1 t2             => 
     match (rawHaskTypeToWeakType f t1) with
       | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2)
       | impossible  => impossible  (* TODO: find a way to convince Coq this can't happen *)
     end
-  | TFCApp    tfc tls         => WTyFunApp tfc ((fix rawHaskTypeToWeakTypeVec n v : list WeakType :=
-                                                match v with
-                                                  | vec_nil => nil
-                                                  | a:::b   => (rawHaskTypeToWeakType f a)::(rawHaskTypeToWeakTypeVec _ b)
-                                                end) _  tls)
+  | TyFunApp    tfc tls         => WTyFunApp tfc (rawHaskTypeListToWeakType f tls)
+end
+with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) :=
+match rht with
+  | TyFunApp_nil   => nil
+  | TyFunApp_cons  κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl')
 end.
 
-
 Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
-  {Γ}(τ:HaskType Γ)(φ:InstantiatedTypeEnv WeakTypeVar Γ) : WeakType :=
+  {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
   rawHaskTypeToWeakType f (τ _ φ).
 
-Variable unsafeCoerce           : WeakCoercion.
-  Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
+Variable unsafeCoerce           : WeakCoercion.    Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
 
-Definition strongCoercionToWeakCoercion {Γ}{Δ}(τ:HaskCoercion Γ Δ)(φ:InstantiatedTypeEnv WeakTypeVar Γ) : WeakCoercion.
+Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
+  : WeakCoercion.
   unfold HaskCoercion in τ.
   admit.
   Defined.
@@ -63,41 +64,45 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
   Defined.
   *)
 
-Definition updateITE {Γ:TypeEnv}{TV: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.
 
 Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev}
   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
   (exp:@Expr WeakExprVar _ Γ Δ ξ lev)
-  : InstantiatedTypeEnv WeakTypeVar Γ -> WeakExpr :=
-match exp as E in Expr G D X L return InstantiatedTypeEnv WeakTypeVar G -> WeakExpr with
+  : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
+match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
 | EVar  _ _ _ ev                => fun ite => WEVar ev
 | ELit  _ _ _ lit _             => fun ite => WELit lit
 | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
-| ELam  Γ' _ _ _ _ _ cv _ e     => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite)
+| ELam  Γ'   _ _ _ _ _ cv e     => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite)
 | ELet  Γ' _ _ _ _ _ ev e1 e2   => fun ite => WELet ev (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
 | EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
 | EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
-| ECast _ _ _ γ _ τ _ _ e       => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
+| ECast Γ Δ ξ t1 t2 γ l e       => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
 | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
-| ETyApp _ _ _ _ τ _ _ _      e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
-| ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite) (strongExprToWeakExpr ftv fcv e ite)
-| ECoApp _ _ γ _ _ _ _ _ _  e   => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
-| ECase Γ Δ ξ l   tc atypes tbranches e alts =>
-  fun ite => WECase (strongExprToWeakExpr ftv fcv e ite)
-    (@typeToWeakType ftv Γ tbranches ite) tc (map (fun t => typeToWeakType ftv t ite) (vec2list atypes))
+| ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
+| ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite)
+| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
+| ECase Γ Δ ξ l tc tbranches sac atypes e alts =>
+  fun ite => WECase
+    (strongExprToWeakExpr ftv fcv e ite)
+    (@typeToWeakType ftv Γ _ tbranches ite)
+    tc
+    (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
     ((fix caseBranches
-      (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
+      (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
                             & Expr (sac_Γ scb Γ)
                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
-                                   (update_ξ (weakLT'○ξ) (vec2list (vec_map (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
+                                   (update_ξ (weakLT'○ξ) (vec2list (vec_map
+                                     (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
                                    (weakLT' (tbranches@@l)) })
       : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
       match tree with
         | T_Leaf None     => []
         | T_Leaf (Some x) => let (scb,e) := x in
-(*          [(sac_altcon scb,
+          (*[(sac_altcon scb,
             nil, (* FIXME *)
             nil, (* FIXME *)
             (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *)
@@ -107,17 +112,18 @@ match exp as E in Expr G D X L return InstantiatedTypeEnv WeakTypeVar G -> WeakE
     ) alts)
 | ETyLam _ _ _ k _ _ e          => fun ite =>
   let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite))
-| ECoLam _ _ k _ t1 t2 _ _ _ _  e => fun ite =>
-  let t1' := typeToWeakType ftv t1 ite in 
-  let t2' := typeToWeakType ftv t2 ite in
+| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite =>
+  let t1' := typeToWeakType ftv σ₁ ite in 
+  let t2' := typeToWeakType ftv σ₂ ite in
   let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
 end
 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{lev}{vars}
   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
   (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars)
-  : InstantiatedTypeEnv WeakTypeVar Γ -> Tree ??(WeakExprVar * WeakExpr) :=
-match elrb as E in ELetRecBindings G D X L V return InstantiatedTypeEnv WeakTypeVar G -> Tree ??(WeakExprVar * WeakExpr) with
+  : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
+match elrb as E in ELetRecBindings G D X L V
+   return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
 | ELR_nil    _ _ _ _           => fun ite => []
 | ELR_leaf   _ _ _ _ cv v e    => fun ite => [(v,(strongExprToWeakExpr ftv fcv e ite))]
 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)