include URL for trfrac.sty and mathpartir in LaTeX output

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

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 759dcb9..191162b 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -11,16 +11,26 @@ Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import HaskCoreLiterals.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import HaskCoreLiterals.

+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+Require Import HaskCore.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 

-CoInductive Fresh A T :=
-{ next  : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
+Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
+  : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
+  match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
+                          (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
+  | nil    => (f,(vec_nil,ite))
+  | k::lk' =>
+    let (f',varsite') := mfresh f lk' ite
+    in  let (vars,ite') := varsite'
+    in  let (v,f'') := next _ _ f' k
+    in (f'',((v:::vars),v::::ite'))
+  end.

 
 Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
  {struct rht} : WeakType :=
 
 Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
  {struct rht} : WeakType :=

@@ -48,14 +58,6 @@ Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
   {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
   rawHaskTypeToWeakType f (τ _ φ).
 
   {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
   rawHaskTypeToWeakType f (τ _ φ).
 

-Variable unsafeCoerce           : WeakCoercion.    Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
-
-Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
-  : WeakCoercion.
-  unfold HaskCoercion in τ.
-  admit.
-  Defined.
-

 (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
  * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
 (*
 (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
  * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
 (*

@@ -67,32 +69,42 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
 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.
 

-Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev}
+Section strongExprToWeakExpr.
+
+  Context (hetmet_brak : CoreVar).
+  Context (hetmet_esc  : CoreVar).
+Axiom FIXME : forall {t}, t.
+
+Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}

   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))

-  (exp:@Expr WeakExprVar _ Γ Δ ξ lev)
+  (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)

   : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
   : 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
+match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
+| EVar  Γ' _ ξ' ev              => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★  (unlev (ξ' ev)) ite))

 | ELit  _ _ _ lit _             => fun ite => WELit lit
 | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
 | 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)
-| 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 Γ Δ ξ t1 t2 γ l e       => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
+| ELam  Γ'   _ _ _ t _ cv e     => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite)
+| ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
+| EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
+| EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)

 | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
 | 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)
 | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
 | 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 =>
+| ECast Γ Δ ξ t1 t2 γ l e       => fun ite => FIXME
+(* WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)
+
+| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => FIXME
+(* WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)
+| ECase Γ Δ ξ l tc tbranches atypes e alts =>

   fun ite => WECase
   fun ite => WECase

+    FIXME

     (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
     (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 sac atypes
+      (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes

                             & Expr (sac_Γ scb Γ)
                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
                                    (update_ξ (weakLT'○ξ) (vec2list (vec_map
                             & Expr (sac_Γ scb Γ)
                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
                                    (update_ξ (weakLT'○ξ) (vec2list (vec_map

@@ -102,11 +114,15 @@ match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar)
       match tree with
         | T_Leaf None     => []
         | T_Leaf (Some x) => let (scb,e) := x in
       match tree with
         | T_Leaf None     => []
         | T_Leaf (Some x) => let (scb,e) := x in

-          (*[(sac_altcon scb,
-            nil, (* FIXME *)
-            nil, (* FIXME *)
-            (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *)
-            strongExprToWeakExpr ftv fcv e (weakITE' ite))]*) []
+          let (ftv',evarsite') := mfresh ftv _ ite in
+          let fcv' :=  fcv in
+            let (evars,ite') := evarsite' in
+            [(sac_altcon scb,
+              vec2list evars,
+              nil (*FIXME*),
+              map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)),
+              strongExprToWeakExpr ftv' fcv' e ite'
+            )]

         | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
       end
     ) alts)
         | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
       end
     ) alts)

@@ -117,14 +133,15 @@ match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar)
   let t2' := typeToWeakType ftv σ₂ ite in
   let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
 end
   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}
+with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}

   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))

-  (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars)
+  (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars)

   : 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 => []
   : 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_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))]

 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
 end.
 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
 end.

+End strongExprToWeakExpr.
\ No newline at end of file