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