replace UJudg with Arrange

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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 2b65a18..ba0c241 100644 (file)
--- 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".
@@ -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"
@@ -226,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]].
@@ -233,13 +234,13 @@ 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 coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
     addErrorMessage ("input CoreSyn: " +++ toString ce)
     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (