X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=05e9c0b78b0b3a20f65d257e703dc9852b56c08f;hp=2e51d0e410a111c5911419869953a7c98c82453e;hb=3a2879d925d4e13e9c89bc768df111684d2b4a59;hpb=4c5c94487aa2bf5489371f112607f0a4c4f01a94

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2e51d0e..05e9c0b 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -71,10 +71,22 @@ Variable mkSystemName : Unique -> string -> nat -> Name.
 Variable mkTyVar : Name -> Kind -> CoreVar.
   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
-  Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
+  Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))".
 Variable mkExVar : Name -> CoreType -> CoreVar.
   Extract Inlined Constant mkExVar => "Id.mkLocalId".
 
+Variable CoreM : Type -> Type.
+  Extract Constant CoreM "a" => "CoreMonad.CoreM".
+  Extraction Inline CoreM.
+Variable CoreMreturn : forall a, a -> CoreM a.
+  Extraction Implicit CoreMreturn [a].
+  Implicit Arguments CoreMreturn [[a]].
+  Extract Inlined Constant CoreMreturn => "Prelude.return".
+Variable CoreMbind : forall a b, CoreM a -> (a -> CoreM b) -> CoreM b.
+  Extraction Implicit CoreMbind [a b].
+  Implicit Arguments CoreMbind [[a] [b]].
+  Extract Inlined Constant CoreMbind => "(Prelude.>>=)".
+
 Section core2proof.
   Context (ce:@CoreExpr CoreVar).
 
@@ -169,9 +181,6 @@ Section core2proof.
 
     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 :=
@@ -281,9 +290,6 @@ Section core2proof.
     (do_skolemize : bool)
     (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)
@@ -307,6 +313,8 @@ Section core2proof.
     (hetmet_pga_applyr : CoreVar)
     (hetmet_pga_curryl : CoreVar)
     (hetmet_pga_curryr : CoreVar)
+    (hetmet_pga_loopl : CoreVar)
+    (hetmet_pga_loopr : CoreVar)
     .
 
 
@@ -411,6 +419,8 @@ Section core2proof.
 (*  ; 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))*)
 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
+    ; ga_loopl     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopl (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_loopr     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_loopr (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
@@ -419,9 +429,6 @@ 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' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString cex)
@@ -438,8 +445,7 @@ Section core2proof.
                       (addErrorMessage ("HaskStrong...")
                         (if do_skolemize
                         then
-                             (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
-                                                 hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
+                             (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
                               in (* insert HaskProof-to-HaskProof manipulations here *)
                               OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
@@ -450,8 +456,7 @@ Section core2proof.
                               >>= fun q => OK (weakExprToCoreExpr q))
                         else (if do_flatten
                         then
-                          (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
-                                                 hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
+                          (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
                               in (* insert HaskProof-to-HaskProof manipulations here *)
                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
@@ -499,49 +504,52 @@ Section core2proof.
 
   End coqPassCoreToCore.
 
+  Notation "a >>= b" := (@CoreMbind _ _ a b).
+
     Definition coqPassCoreToCore 
-    (do_flatten  : bool)
-    (do_skolemize  : bool)
-    (hetmet_brak  : CoreVar)
-    (hetmet_esc   : CoreVar)
-    (hetmet_flatten   : CoreVar)
-    (hetmet_unflatten   : CoreVar)
-    (hetmet_flattened_id   : CoreVar)
+    (do_flatten   : bool)
+    (do_skolemize : bool)
+    (dsLookupVar  : string -> string -> CoreM CoreVar)
+    (dsLookupTyc  : string -> string -> CoreM TyFun)
     (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)
-    (hetmet_pga_second : CoreVar)
-    (hetmet_pga_cancell : CoreVar)
-    (hetmet_pga_cancelr : CoreVar)
-    (hetmet_pga_uncancell : CoreVar)
-    (hetmet_pga_uncancelr : CoreVar)
-    (hetmet_pga_assoc : CoreVar)
-    (hetmet_pga_unassoc : CoreVar)
-    (hetmet_pga_copy : CoreVar)
-    (hetmet_pga_drop : CoreVar)
-    (hetmet_pga_swap : CoreVar)
-    (hetmet_pga_applyl : CoreVar)
-    (hetmet_pga_applyr : CoreVar)
-    (hetmet_pga_curryl : CoreVar)
-    (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
-    coqPassCoreToCore'
+    (lbinds       : list (@CoreBind CoreVar))
+    : CoreM (list (@CoreBind CoreVar)) :=
+      dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
+      dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+      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 =>
+      dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
+      dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
+      dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
+      dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
+      dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
+      dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
+      dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
+      dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
+      dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
+      dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
+      dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
+      dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
+      dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
+      dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
+      dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
+      dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
+      dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
+      dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
+      dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
+      dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
+
+    CoreMreturn
+    (coqPassCoreToCore'
        do_flatten
        do_skolemize
        hetmet_brak  
        hetmet_esc   
-       hetmet_flatten
-       hetmet_unflatten
-       hetmet_flattened_id
        uniqueSupply 
-       hetmet_PGArrowTyCon
-       hetmet_PGArrow_unit_TyCon
-       hetmet_PGArrow_tensor_TyCon
+       hetmet_PGArrow
+       hetmet_PGArrow_unit
+       hetmet_PGArrow_tensor
 (*       hetmet_PGArrow_exponent_TyCon*)
        hetmet_pga_id 
        hetmet_pga_comp 
@@ -556,13 +564,15 @@ Section core2proof.
        hetmet_pga_copy 
        hetmet_pga_drop 
        hetmet_pga_swap 
+       hetmet_pga_loopl 
+       hetmet_pga_loopr 
        lbinds
        (*
        hetmet_pga_applyl 
        hetmet_pga_applyr 
        hetmet_pga_curryl 
        *)
-
+       )
        .
 
 End core2proof.