X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=5be52807b489dfd1a977f4c20bc077d361130385;hp=58bc13e2ce945e7ecbd850cf911937fdca5ba7fa;hb=c64ac559ed9448b8aa24abedbc2ad5ca800d1d24;hpb=cb424978e057bc2b4868517302738d52246fba04

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 58bc13e..5be5280 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -15,7 +15,8 @@ Require Import General.
 Require Import NaturalDeduction.
 
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -160,13 +161,16 @@ Section core2proof.
     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
-      weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
+      weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
     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_flatten : WeakExprVar).
+    Context (hetmet_unflatten : WeakExprVar).
+    Context (hetmet_flattened_id : WeakExprVar).
+    Context (uniqueSupply   : UniqSupply).
 
     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
       match ut with
@@ -219,46 +223,6 @@ Section core2proof.
       exact O.
       apply t.
       Defined.
-(*
-    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-      addErrorMessage ("input CoreSyn: " +++ toString ce)
-      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
-        coreExprToWeakExpr ce >>= fun we =>
-          addErrorMessage ("WeakExpr: " +++ toString we)
-            ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
-              ((weakTypeOfWeakExpr we) >>= fun t =>
-                (addErrorMessage ("WeakType: " +++ toString t)
-                  ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-
-                    ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
-
-                      (addErrorMessage ("HaskStrong...")
-                        (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
-                         in (* insert HaskProof-to-HaskProof manipulations here *)
-                         OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
-                         >>= fun e' =>
-                           (snd e') >>= fun e'' =>
-                         strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
-                           (projT2 e'') INil
-                         >>= fun q =>
-                           OK (weakExprToCoreExpr q)
-                    )))))))))).
-
-    Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
-      match coreToCoreExpr' ce with
-        | OK x    => x
-        | Error s => Prelude_error s
-      end.
-  
-    Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
-      match binds with
-        | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
-        | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
-      end.
-
-    Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
-      map coreToCoreBind lbinds.
-  *)
 
   End CoreToCore.
 
@@ -272,12 +236,13 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
-    eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod.    
-    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
     apply nd_rule.
     apply RVar.
+    apply nd_id.
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
@@ -310,9 +275,15 @@ Section core2proof.
     Context
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
+    (hetmet_flatten : CoreVar)
+    (hetmet_unflatten : CoreVar)
+    (hetmet_flattened_id : CoreVar)
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_PGArrow_unit_TyCon : TyFun)
+    (hetmet_PGArrow_tensor_TyCon : TyFun)
+    (hetmet_PGArrow_exponent_TyCon : TyFun)
     (hetmet_pga_id : CoreVar)
     (hetmet_pga_comp : CoreVar)
     (hetmet_pga_first : CoreVar)
@@ -332,16 +303,27 @@ Section core2proof.
     (hetmet_pga_curryr : CoreVar)
     .
 
-    Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
-    Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
-      TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
-    Definition ga_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+
+    Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
+      @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+
+    Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
+      (@TyFunApp TV
+        hetmet_PGArrow_tensor_TyCon
+        (ECKind::★ ::★ ::nil) ★
+        (TyFunApp_cons _ _ ec
+          (TyFunApp_cons _ _ a
+            (TyFunApp_cons _ _ b
+          TyFunApp_nil)))).
+
+    Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
       TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) a) b) c.
+
     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 
-    Definition ga_type' {Γ}(a b c:HaskType Γ ★) : HaskType Γ ★ :=
+    Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
       fun TV ite => TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
@@ -403,22 +385,22 @@ Section core2proof.
           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
       Defined.
 
-    Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
+    Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ ec x.
 
     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
-    { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
-    ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
-    ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
-    ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
-    ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
-    ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
-    ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
-    ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
-    ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
-    ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
-    ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
-    ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
-    ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
+    { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat ec a)
+    ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat ec a)
+    ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat ec a)
+    ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
+    ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
+    ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+    ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+    ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b)
+    ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat ec a)
+    ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat ec a)
+    ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
@@ -431,6 +413,9 @@ Section core2proof.
 
     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
+    Definition hetmet_flatten'  := coreVarToWeakExprVarOrError hetmet_flatten.
+    Definition hetmet_unflatten'  := coreVarToWeakExprVarOrError hetmet_unflatten.
+    Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.
 
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString ce)
@@ -445,12 +430,14 @@ Section core2proof.
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 
                       (addErrorMessage ("HaskStrong...")
-                        (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
+                        (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
+                                            hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
                          in (* insert HaskProof-to-HaskProof manipulations here *)
                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>
-                         strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+                         strongExprToWeakExpr hetmet_brak' hetmet_esc'
+                           mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
                            (projT2 e'') INil
                          >>= fun q =>
                            OK (weakExprToCoreExpr q)
@@ -461,11 +448,21 @@ Section core2proof.
         | OK x    => x
         | Error s => Prelude_error s
       end.
-  
+
     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
       match binds with
-        | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+        | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
+
         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+                            (* FIXME: doesn't deal with the case where top level recursive binds change type *)
+(*
+          match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
+            | CoreELet (CoreRec lbe') => lbe'
+            | x                       => Prelude_error
+                                            ("coreToCoreExpr was given a letrec, " +++
+                                             "but returned something that wasn't a letrec: " +++ toString x)
+          end
+*)
       end.
 
     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
@@ -476,9 +473,15 @@ Section core2proof.
     Definition coqPassCoreToCore 
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
+    (hetmet_flatten   : CoreVar)
+    (hetmet_unflatten   : CoreVar)
+    (hetmet_flattened_id   : CoreVar)
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_PGArrow_unit_TyCon : TyFun)
+    (hetmet_PGArrow_tensor_TyCon : TyFun)
+    (hetmet_PGArrow_exponent_TyCon : TyFun)
     (hetmet_pga_id : CoreVar)
     (hetmet_pga_comp : CoreVar)
     (hetmet_pga_first : CoreVar)
@@ -499,8 +502,14 @@ Section core2proof.
     coqPassCoreToCore'
        hetmet_brak  
        hetmet_esc   
+       hetmet_flatten
+       hetmet_unflatten
+       hetmet_flattened_id
        uniqueSupply 
        hetmet_PGArrowTyCon
+       hetmet_PGArrow_unit_TyCon
+       hetmet_PGArrow_tensor_TyCon
+(*       hetmet_PGArrow_exponent_TyCon*)
        hetmet_pga_id 
        hetmet_pga_comp 
        hetmet_pga_first 
@@ -520,6 +529,7 @@ Section core2proof.
        hetmet_pga_applyr 
        hetmet_pga_curryl 
        *)
+
        .
 
 End core2proof.