X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=6a6e487d0650b10ef1d19112c288bdb2fc826fed;hp=f7fc56e1144473c7d5c6f1c8d84010c00e6e804a;hb=c9a110c17f24f89f0375c3207b7c544e87a3cee8;hpb=825fa62636c32762ac2e1c1357209119de74c281

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index f7fc56e..6a6e487 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,15 +10,13 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
-Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-Require Import HaskCore.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
+Require Import HaskCoreVars.
 
 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 Γ))) :=
@@ -69,12 +67,14 @@ 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.
 
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+Definition coercionToWeakCoercion : forall Γ Δ κ t1 t2 (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)), WeakCoercion.
+  admit.
+  Defined.
 
 Section strongExprToWeakExpr.
 
-  Context (hetmet_brak : CoreVar).
-  Context (hetmet_esc  : CoreVar).
+  Context (hetmet_brak : WeakExprVar).
+  Context (hetmet_esc  : WeakExprVar).
 
   Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
     (ftv:Fresh Kind                (fun _ => WeakTypeVar))
@@ -93,8 +93,8 @@ Section strongExprToWeakExpr.
   | 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"
+  | ECast Γ Δ ξ t1 t2 γ l e      => fun ite => WECast  (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
+  | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
   | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite =>
     let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in
      WECase
@@ -110,7 +110,7 @@ Section strongExprToWeakExpr.
                                      (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) :=
+        : Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
         match tree with
           | T_Leaf None     => []
           | T_Leaf (Some x) => let (scb,e) := x in
@@ -145,4 +145,4 @@ Section strongExprToWeakExpr.
   | 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.
\ No newline at end of file
+End strongExprToWeakExpr.