final batch of fixups before enabling -fcoqpass

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 6a6e487..b4b0caa 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -67,9 +67,8 @@ 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 coercionToWeakCoercion : forall Γ Δ κ t1 t2 (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)), WeakCoercion.
-  admit.
-  Defined.
+Definition coercionToWeakCoercion Γ Δ κ t1 t2 ftv ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)) : WeakCoercion :=
+  WCoUnsafe (@typeToWeakType ftv Γ κ t1 ite) (@typeToWeakType ftv Γ κ t2 ite).
 
 Section strongExprToWeakExpr.
 
@@ -93,8 +92,10 @@ 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 => WECast  (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
-  | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
+  | ECast Γ Δ ξ t1 t2 γ l e      => fun ite => WECast  (strongExprToWeakExpr ftv fcv fev e ite)
+                                                 (coercionToWeakCoercion _ _ _ _ _ ftv ite γ)
+  | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite)
+                                                 (coercionToWeakCoercion _ _ _ _ _ ftv ite γ)
   | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite =>
     let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in
      WECase

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index f849be1..e721de9 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -21,7 +21,7 @@ Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Const
 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
-(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
+(* TODO: might be a better idea to panic here than simply drop things that look wrong *)
 Definition dataConExTyVars cdc :=
   filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
   Opaque dataConExTyVars.

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 39871a3..c97a63c 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -60,10 +60,8 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
                                             (weakTypeToCoreType t3)
   end.
 
-Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion.
-  admit.
-  Defined.
-  (*mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).*)
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with