fix bug in GeneralizedArrowFromReification

[coq-hetmet.git] / src / HaskCoreToWeak.v

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1734637..abcd6b8 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -4,20 +4,29 @@
 
 Generalizable All Variables.
 Require Import Preamble.
 
 Generalizable All Variables.
 Require Import Preamble.

-Require Import General.

 Require Import Coq.Lists.List.
 Require Import Coq.Lists.List.

+Require Import General.

 Require Import HaskKinds.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.

-Require Import HaskWeakToCore.

 
 

-Axiom    tycons_distinct       : ~(ArrowTyCon=ModalBoxTyCon).
-Variable tyConOrTyFun          : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun      => "tyConOrTyFun".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
+  Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
+
+(* extracts the Name from a CoreVar *)
+Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
+
+(* the magic wired-in name for the modal type introduction/elimination forms *)
+Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
+Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
+Variable hetmet_csp_name    : CoreName.              Extract Inlined Constant hetmet_csp_name  => "PrelNames.hetmet_csp_name".

 
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with
 
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with

@@ -44,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
                                     | 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"
+                                | _                           => Error ("mis-applied modal box tycon: " +++ toString ct)

                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon

@@ -72,41 +81,62 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 

-Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
-
-Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
-  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).

 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 
 (* 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
 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
         | WCoerVar _  => None

+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end

       end else None
   | _ => 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
 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.
 
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
 

-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
-  let (t1,t2) := coreCoercionKind cc
-  in  coreTypeToWeakType t1 >>= fun t1' =>
-    coreTypeToWeakType t2 >>= fun t2' =>
-    OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
+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 => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end
+        | WCoerVar _  => None
+      end else None
+  | _ => None
+end.
+
+(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
+Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
+  match wt with
+    | WTyCon tc        => OK (tc,acc)
+    | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
+    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+    | _                => Error ("expectTyConApp encountered " +++ toString wt)
+  end.

 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with

@@ -114,8 +144,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>

-                            coreCoercionToWeakCoercion co >>= fun co' =>
-                              OK (WECast e' co')
+                              OK (WECast e' (coreCoercionToWeakCoercion co))

 
     | CoreEVar   v     => match coreVarToWeakVar v with
                             | WExprVar ev => OK (WEVar ev)
 
     | CoreEVar   v     => match coreVarToWeakVar v with
                             | WExprVar ev => OK (WEVar ev)

@@ -133,13 +162,20 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
                                                  OK (WEEsc v tv e' t')
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
                                                  OK (WEEsc v tv e' t')

-                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
-                                             match e2 with
-                                               | CoreEType t => 
-                                                 coreTypeToWeakType t >>= fun t' =>
-                                                   OK (WETyApp e1' t')
-                                               | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
-                                             end
+                                           | None    => match isCSP e1 with
+                                                          | Some (v,tv,t) =>
+                                                            coreExprToWeakExpr e2 >>= fun e' =>
+                                                              coreTypeToWeakType t >>= fun t' =>
+                                                                OK (WECSP v tv e' t')
+                                                          | None    => coreExprToWeakExpr e1 >>= fun e1' =>
+                                                            match e2 with
+                                                              | CoreEType t => 
+                                                                coreTypeToWeakType t >>= fun t' =>
+                                                                  OK (WETyApp e1' t')
+                                                              | _           => coreExprToWeakExpr e2
+                                                                >>= fun e2' => OK (WEApp e1' e2')
+                                                            end
+                                                        end

                                          end
                           end
 
                                          end
                           end
 

@@ -178,26 +214,24 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 

-      coreExprToWeakExpr e >>= fun e' =>
-        weakTypeOfWeakExpr e' >>= fun te' =>
-          (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
-             >>= 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)) :=
+        coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
+          expectTyConApp te' nil >>= fun tca =>
+            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
             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
                       | 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)
                         e')::rest')
                     end
             end) alts)