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

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 759dcb9..71994c6 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,17 +10,25 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
+Require Import HaskCoreVars.
 
-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 :=
@@ -48,14 +56,6 @@ Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
   {Γ}{κ}(τ: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) *)
 (*
@@ -67,64 +67,80 @@ 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.
 
-Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev}
-  (ftv:Fresh Kind                (fun _ => WeakTypeVar))
-  (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
-  (exp:@Expr WeakExprVar _ Γ Δ ξ lev)
-  : 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)
-| 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)
-| 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 =>
-  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 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))))
-                                   (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,
-            nil, (* FIXME *)
-            nil, (* FIXME *)
-            (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *)
-            strongExprToWeakExpr ftv fcv e (weakITE' ite))]*) []
-        | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
-      end
-    ) alts)
-| ETyLam _ _ _ k _ _ e          => fun ite =>
-  let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite))
-| 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 (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)
-end.
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+
+Section strongExprToWeakExpr.
+
+  Context (hetmet_brak : WeakExprVar).
+  Context (hetmet_esc  : WeakExprVar).
+
+  Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
+    (ftv:Fresh Kind                (fun _ => WeakTypeVar))
+    (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
+    (fev:Fresh WeakType            (fun _ => WeakExprVar))
+    (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
+    : 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 (weakExprVar ev (@typeToWeakType ftv Γ' ★  (unlev (ξ' ev)) ite))
+  | ELit  _ _ _ lit _             => fun ite => WELit lit
+  | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite)
+  | ELam  Γ'   _ _ _ t _ cv e     => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e ite)
+  | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite)
+  | EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite)
+  | EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite)
+  | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv fev e ite)
+  | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv τ ite)
+  | ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv fev elrb ite)(strongExprToWeakExpr ftv fcv fev e ite)
+  | ECast Γ Δ ξ t1 t2 γ l e       => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECast not implemented"
+  | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECoApp not implemented"
+  | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite =>
+    let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in
+     WECase
+      ev
+      (strongExprToWeakExpr ftv fcv fev' 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
+                              & Expr (sac_Γ scb Γ)
+                                     (sac_Δ scb Γ atypes (weakCK'' Δ))
+                                     (update_ξ (weakLT'○ξ) (vec2list (vec_map
+                                       (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
+                                     (weakLT' (tbranches@@l)) })
+        : Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
+        match tree with
+          | T_Leaf None     => []
+          | T_Leaf (Some x) => let (scb,e) := x in
+            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' fev' e ite'
+              )]
+          | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
+        end
+      ) alts)
+  | ETyLam _ _ _ k _ _ e          => fun ite =>
+    let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv fev e (updateITE tv ite))
+  | 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' fev e ite)
+  end
+  with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}
+    (ftv:Fresh Kind                (fun _ => WeakTypeVar))
+    (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
+    (fev:Fresh WeakType            (fun _ => WeakExprVar))
+    (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 => []
+  | ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))]
+  | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite)
+  end.
+End strongExprToWeakExpr.