X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=ba0c2418490cdefd3e1338571ecd1fead1de7f8d;hp=59183c97f5187496161c3564d321f5507e4320bc;hb=fd337b235014f43000773eb0d95168d89e93a893;hpb=743099bc348cfa97fb4d94c7e7ae3e53d2717e87

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 59183c9..ba0c241 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -34,12 +34,11 @@ Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
 Require Import HaskProofToStrong.
 
-Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
 Require Import ProgrammingLanguage.
-*)
+Require Import HaskProofCategory.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
+
+(*Require Import HaskStrongCategory.*)
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -61,7 +60,7 @@ Extract Inlined Constant string_dec => "(==)".
 Extract Inlined Constant ascii_dec => "(==)".
 
 (* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
 Extract Constant zero   => "'\000'".
 Extract Constant one    => "'\001'".
 Extract Constant shift  => "shiftAscii".
@@ -88,7 +87,7 @@ Section core2proof.
   Definition Δ : CoercionEnv Γ := nil.
 
   Definition φ : TyVarResolver Γ :=
-    fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
+    fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
 
   Definition ψ : CoVarResolver Γ Δ :=
@@ -99,7 +98,8 @@ Section core2proof.
   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
     match coreVarToWeakVar cv with
       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
-                          | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+                          | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
+                                                         toString cv+++": " +++ s)
                           | OK    t => t @@ nil
                         end
       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
@@ -128,20 +128,19 @@ Section core2proof.
     eol.
 
 
-  Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := Error "Temporarily Disabled".
-(*
-    addErrorMessage ("input CoreSyn: " +++ ce)
-    (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+  Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
+    addErrorMessage ("input CoreSyn: " +++ toString ce)
+    (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
       coreExprToWeakExpr ce >>= fun we =>
-        addErrorMessage ("WeakExpr: " +++ we)
-          ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+        addErrorMessage ("WeakExpr: " +++ toString we)
+          ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
             ((weakTypeOfWeakExpr we) >>= fun t =>
-              (addErrorMessage ("WeakType: " +++ t)
+              (addErrorMessage ("WeakType: " +++ toString t)
                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-                  addErrorMessage ("HaskType: " +++ τ)
+                  addErrorMessage ("HaskType: " +++ toString τ)
                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
-                    OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
-                  )))))))).*)
+                    OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+                  )))))))).
 
   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
     match coreToStringExpr' ce with
@@ -227,6 +226,7 @@ Section core2proof.
       apply t.
       Defined.
 
+(*
     Definition env := ★::nil.
     Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
     Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
@@ -234,43 +234,23 @@ Section core2proof.
       eapply nd_comp.
       eapply nd_rule.
       apply RVar.
-      eapply nd_rule.
-      eapply (RURule _ _ _ _ (RuCanL _ _)) .
+      eapply nd_rule
+      eapply (RArrange _ _ _ _ (RuCanL _ _)) .
       eapply nd_rule.
       eapply RLam.
       Defined.
-(*
-    Definition TInt : HaskType nil ★.
-      assert (tyConKind' intPrimTyCon = ★).
-        rewrite <- H.
-        unfold HaskType; intros.
-        apply TCon.
-        Defined.
-
-    Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
-      apply nd_rule.
-      apply RVar.
-      Defined.
 
-    Definition idtype :=
-        HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
 
-    Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
-      eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
-      apply idproof0.
-      Defined.
-*)
-(*
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-    addErrorMessage ("input CoreSyn: " +++ ce)
-    (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+    addErrorMessage ("input CoreSyn: " +++ toString ce)
+    (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
       coreExprToWeakExpr ce >>= fun we =>
-        addErrorMessage ("WeakExpr: " +++ we)
-          ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+        addErrorMessage ("WeakExpr: " +++ toString we)
+          ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
             ((weakTypeOfWeakExpr we) >>= fun t =>
-              (addErrorMessage ("WeakType: " +++ t)
+              (addErrorMessage ("WeakType: " +++ toString t)
                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-                  addErrorMessage ("HaskType: " +++ τ)
+                  addErrorMessage ("HaskType: " +++ toString τ)
                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
                         (let haskProof := @expr2proof _ _ _ _ _ _ e
                           in (* insert HaskProof-to-HaskProof manipulations here *)
@@ -289,17 +269,17 @@ Section core2proof.
                          INil
                          >>= fun q => Error (toString q)
                   ))))))))).
-*)
-*)
+*)*)
+
 
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-      addErrorMessage ("input CoreSyn: " +++ ce)
-      (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+      addErrorMessage ("input CoreSyn: " +++ toString ce)
+      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
         coreExprToWeakExpr ce >>= fun we =>
-          addErrorMessage ("WeakExpr: " +++ we)
-            ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+          addErrorMessage ("WeakExpr: " +++ toString we)
+            ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
               ((weakTypeOfWeakExpr we) >>= fun t =>
-                (addErrorMessage ("WeakType: " +++ t)
+                (addErrorMessage ("WeakType: " +++ toString t)
                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>