Require Import HaskWeakToCore.
Require Import HaskProofToStrong.
-Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
Require Import ProgrammingLanguage.
-*)
+
+Require Import HaskProofFlattener.
+Require Import HaskProofStratified.
+Require Import HaskProofCategory.
+
+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".
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"
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)) (