X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=abcd6b8babfe78affc8d08d5645e53d2532f1765;hp=1be33fde13c69d9212496a95a1e59d86a05b7e9a;hb=fa3f21c9f6460d761f3b33f00e4414ad2710099d;hpb=24445b56cb514694c603c342d77cbc8329a4b0aa

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1be33fd..abcd6b8 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -4,10 +4,10 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Coq.Lists.List.
+Require Import General.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -53,7 +53,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
@@ -84,37 +84,46 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end
       end else None
   | _ => None
 end.
 
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (v,tv,tbody)
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
 
-Definition isCSP (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (v,tv,tbody)
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end
         | WCoerVar _  => None
       end else None
   | _ => None
@@ -125,8 +134,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 :=
@@ -206,24 +215,23 @@ 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
-          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
-                : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+            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
               | nil => OK nil
               | (mkTriple alt vars e)::rest =>
                   mkBranches rest >>= fun rest' => 
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with
-                      | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
-                      | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
+                      | DEFAULT                => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
+                      | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
-                        OK (((DataAlt 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)),
+                        OK (((WeakDataAlt dc),
+                        (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)