add partial support for flattening kappa-expressions (mostly commented out)

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

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 673b999..a287b20 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -16,10 +16,10 @@ Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 
-Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
-Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Variable getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType).
-  Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun.          Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType  -> CoreType.                 Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
+   Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
 
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
@@ -28,6 +28,9 @@ Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant co
 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".
+Variable hetmet_kappa_name  : CoreName.              Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name".
+Variable hetmet_kappa_app_name: CoreName.
+Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name".
 
 Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
   split_list lwt (length (fst (tyFunKind tf))) >>=
@@ -146,6 +149,32 @@ match ce with
   | _ => None
 end.
 
+Definition isKappa (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+  | (CoreEApp
+    (CoreEApp
+    (CoreEApp
+      (CoreEVar v)
+      (CoreEType t1))
+      (CoreEType t2))
+      (CoreEType t3))
+    => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false
+  | _ => false
+end.
+
+Definition isKappaApp (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+  | (CoreEApp (CoreEApp
+    (CoreEApp
+    (CoreEApp
+      (CoreEVar v)
+      (CoreEType t1))
+      (CoreEType t2))
+      (CoreEType t3)) _)
+    => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false
+  | _ => false
+end.
+
 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
@@ -188,8 +217,9 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
     | CoreELit   lit   => OK (WELit lit)
     | 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"
+    | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
-                            let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co
+                            let (ct1,ct2) := coercionKind co
                              in coreTypeToWeakType ct1 >>= fun t1 =>
                                   coreTypeToWeakType ct2 >>= fun t2 =>
                                     OK (WECast e' (WCoUnsafe t1 t2))
@@ -215,16 +245,38 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                                                             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
+                                           | None    =>
+                                             (*
+                                             if isKappa e1
+                                             then match e2 with
+                                                    | CoreELam v e => match coreVarToWeakVar' v with
+                                                                        | OK (WExprVar ev) => 
+                                                                          coreExprToWeakExpr e >>= fun e' =>
+                                                                            OK (WEKappa ev e')
+                                                                        | _ => Error "bogus"
+                                                                      end
+                                                    | _ => Error "bogus"
+                                                  end
+                                             else if isKappaApp e1
+                                             then match e1 with
+                                                    | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
+                                                      coreExprToWeakExpr e1' >>= fun e1'' =>
+                                                      coreExprToWeakExpr e2  >>= fun e2'' =>
+                                                        OK (WEKappaApp e1'' e2'')
+                                                    | _ => Error "bogus"
+                                                  end
+                                               else
+                                               *)
+                                                 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
 
     | CoreELam   v e => coreVarToWeakVar' v >>= fun v' => match v' with