Require Import ProgrammingLanguage.
+Require Import HaskProofFlattener.
+Require Import HaskProofStratified.
Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+
+Require Import ReificationsIsomorphicToGeneralizedArrows.
+
+(*Require Import HaskStrongCategory.*)
Open Scope string_scope.
Extraction Language Haskell.
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".
apply t.
Defined.
+(*
Definition env := ★::nil.
Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
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)) (