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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 88714c7..9f0fc1a 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -179,9 +179,11 @@ Section core2proof.
     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 
-    Context (hetmet_brak    : WeakExprVar).
-    Context (hetmet_esc     : WeakExprVar).
-    Context (uniqueSupply   : UniqSupply).
+    Context (hetmet_brak      : WeakExprVar).
+    Context (hetmet_esc       : WeakExprVar).
+    Context (hetmet_kappa     : WeakExprVar).
+    Context (hetmet_kappa_app : WeakExprVar).
+    Context (uniqueSupply     : UniqSupply).
 
     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
       match ut with
@@ -311,6 +313,8 @@ Section core2proof.
     (do_skolemize : bool)
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
+    (hetmet_kappa     : WeakExprVar)
+    (hetmet_kappa_app : WeakExprVar)
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
@@ -451,6 +455,8 @@ Section core2proof.
 
     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
+    Definition hetmet_kappa'  := coreVarToWeakExprVarOrError hetmet_kappa.
+    Definition hetmet_kappa_app'  := coreVarToWeakExprVarOrError hetmet_kappa_app.
 
     Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString cex)
@@ -472,7 +478,7 @@ Section core2proof.
                               OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                               >>= fun e' => (snd e') >>= fun e'' =>
-                              strongExprToWeakExpr hetmet_brak' hetmet_esc'
+                              strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
                                 (projT2 e'') INil
                               >>= fun q => OK (weakExprToCoreExpr q))
@@ -483,7 +489,7 @@ Section core2proof.
                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                               >>= fun e' => (snd e') >>= fun e'' =>
-                              strongExprToWeakExpr hetmet_brak' hetmet_esc'
+                              strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
                                 (projT2 e'') INil
                               >>= fun q => OK (weakExprToCoreExpr q))
@@ -493,7 +499,7 @@ Section core2proof.
                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                               >>= fun e' => (snd e') >>= fun e'' =>
-                              strongExprToWeakExpr hetmet_brak' hetmet_esc'
+                              strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
                                 (projT2 e'') INil
                               >>= fun q => OK (weakExprToCoreExpr q))))
@@ -538,6 +544,8 @@ Section core2proof.
     : CoreM (list (@CoreBind CoreVar)) :=
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+      dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
+      dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
       dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
       dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
       dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
@@ -569,6 +577,10 @@ Section core2proof.
        do_skolemize
        hetmet_brak  
        hetmet_esc   
+       (*
+       hetmet_kappa
+       hetmet_kappa_app
+       *)
        uniqueSupply 
        hetmet_PGArrow
        hetmet_PGArrow_unit

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 7669e5d..a287b20 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -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))
@@ -216,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

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 4740acb..a7bd11a 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -66,6 +66,9 @@ Section Raw.
   | TVar           : ∀ κ, TV κ                                              -> RawHaskType κ                     (* a        *)
   | TCon           : ∀ tc,                                                     RawHaskType (tyConKind' tc)       (* T        *)
   | TArrow         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (->)     *)
+  (*
+  | TKappa         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (~~>)    *)
+  *)
   | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
@@ -111,6 +114,7 @@ Implicit Arguments TApp   [ [TV] [κ₁] [κ₂] ].
 Implicit Arguments TAll   [ [TV] ].
 
 Notation "t1 ---> t2"        := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
+(*Notation "t1 ~~~> t2"        := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
 
 (* Kind and Coercion Environments *)

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 077f7b5..9d39f44 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -31,6 +31,10 @@ Inductive WeakExpr :=
 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+(*
+| WEKappa     : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+| WEKappaApp  : WeakExpr                        -> WeakExpr                  -> WeakExpr
+*)
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
 

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index c3e90a4..7d24277 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -84,6 +84,10 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                                      (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)
+  (*
+  | WEKappa     v e      => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappa"
+  | WEKappaApp  e1 e2    => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappaApp"
+  *)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
   | WECase  vscrut escrut tbranches tc types alts  =>
                                             CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 0acc0af..f6dc701 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -489,6 +489,10 @@ Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
     | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
     | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
     | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+(*
+    | WEKappaApp  e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+    | WEKappa  cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+*)
     | WETyLam  cv e     => doesWeakVarOccur wev e
     | WECoLam  cv e     => doesWeakVarOccur wev e
     | WECase vscrut escrut tbranches tc avars alts =>