X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=78223cf4d10c87d14e22ea6f1c9b161784220466;hp=c4bd768d69ca1e4b373242bce7ceb4f5b112d0d3;hb=164cdbf41ca206079b0dcfc18cd13625b286c38c;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index c4bd768..78223cf 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -4,10 +4,11 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Coq.Lists.List.
+Require Import General.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -15,9 +16,6 @@ Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 
-Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
-
 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
 Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
@@ -56,7 +54,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
                                   end
-                                | _                           => Error ("mis-applied modal box tycon: " +++ ct)
+                                | _                           => Error ("mis-applied modal box tycon: " +++ toString ct)
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
@@ -71,9 +69,11 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                 coreTypeToWeakType' t2 >>= fun t2' => 
                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
   | ForAllTy cv t            => match coreVarToWeakVar cv with
-                                  | WExprVar _  => Error "encountered expression variable in a type"
+                                  | WExprVar _  => Error "encountered expression variable in a type abstraction"
                                   | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
-                                  | WCoerVar _  => Error "encountered coercion variable in a type"
+                                  | WCoerVar (weakCoerVar v t1' t2') => 
+                                        coreTypeToWeakType' t >>= fun t3' => 
+                                          OK (WCoFunTy t1' t2' t3')
                                 end
   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with 
                                                   | nil => OK nil
@@ -84,7 +84,8 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 
-Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
+Definition coreTypeToWeakType t :=
+  addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
@@ -137,8 +138,8 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak
   match wt with
     | WTyCon tc        => OK (tc,acc)
     | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
-    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
-    | _                => Error ("expectTyConApp encountered " +++ wt)
+    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+    | _                => Error ("expectTyConApp encountered " +++ toString wt)
   end.
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
@@ -218,9 +219,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
-        coreExprToWeakExpr e >>= fun e' =>
           expectTyConApp te' nil >>= fun tca =>
-            let (tc,lt) := tca in
+            let (tc,lt) := tca:(TyCon * list WeakType) in
           ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
             match branches with
@@ -233,9 +233,9 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                       | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
                         OK (((WeakDataAlt dc),
-                        (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
                         e')::rest')
                     end
             end) alts)