split HaskLiteralsAndTyCons into two files

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index ea89cf4..cae7174 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -15,7 +15,8 @@ Require Import General.
 Require Import NaturalDeduction.
 
 Require Import HaskKinds.
 Require Import NaturalDeduction.
 
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 9024828..b05c34f 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index abcd6b8..ac2da8c 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 0fbaeb5..677287a 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -9,7 +9,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
 
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".

diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v
index d158f05..8b0aabb 100644 (file)
--- a/src/HaskCoreVars.v
+++ b/src/HaskCoreVars.v
@@ -6,7 +6,8 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 
 (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *)
 Variable CoreVar            : Type.                                               Extract Inlined Constant CoreVar    => "Var.Var".
 
 (* GHC uses a single type for expression variables, type variables, and coercion variables; this is that type *)
 Variable CoreVar            : Type.                                               Extract Inlined Constant CoreVar    => "Var.Var".

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index e8aceb1..ae99605 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -17,7 +17,8 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.

diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiterals.v
similarity index 67%
rename from src/HaskLiteralsAndTyCons.v
rename to src/HaskLiterals.v
index 38e7f95..c8a2651 100644 (file)
--- a/src/HaskLiteralsAndTyCons.v
+++ b/src/HaskLiterals.v
@@ -1,5 +1,5 @@
 (*********************************************************************************************************************************)
 (*********************************************************************************************************************************)

-(* HaskLiteralsAndTyCons: representation of compile-time constants (literals)                                                    *)
+(* HaskLiterals: representation of compile-time constants (literals)                                                             *)

 (*********************************************************************************************************************************)
 
 Generalizable All Variables.
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.

@@ -7,12 +7,7 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.

-
-Variable CoreDataCon     : Type.                      Extract Inlined Constant CoreDataCon          => "DataCon.DataCon".
-
-(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
-Variable TyCon           : Type.                      Extract Inlined Constant TyCon                => "TyCon.TyCon".
-Variable TyFun           : Type.                      Extract Inlined Constant TyFun                => "TyCon.TyCon".
+Require Import HaskTyCons.

 
 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
 Variable HaskInt         : Type.                      Extract Inlined Constant HaskInt               => "Prelude.Int".
 
 (* Since GHC is written in Haskell, compile-time Haskell constants are represented using Haskell (Prelude) types *)
 Variable HaskInt         : Type.                      Extract Inlined Constant HaskInt               => "Prelude.Int".

@@ -21,11 +16,6 @@ Variable HaskFastString  : Type.                      Extract Inlined Constant H
 Variable HaskInteger     : Type.                      Extract Inlined Constant HaskInteger           => "Prelude.Integer".
 Variable HaskRational    : Type.                      Extract Inlined Constant HaskRational          => "Prelude.Rational".
 
 Variable HaskInteger     : Type.                      Extract Inlined Constant HaskInteger           => "Prelude.Integer".
 Variable HaskRational    : Type.                      Extract Inlined Constant HaskRational          => "Prelude.Rational".
 

-Variable CoreName        : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
-Variable Class_          : Type.                      Extract Inlined Constant Class_                => "Class.Class".
-Variable CoreIPName      : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
-                                                      Extraction Inline CoreIPName.
-

 (* This type extracts exactly onto GHC's Literal.Literal type *)
 Inductive HaskLiteral :=
 | HaskMachChar     : HaskChar                                               -> HaskLiteral
 (* This type extracts exactly onto GHC's Literal.Literal type *)
 Inductive HaskLiteral :=
 | HaskMachChar     : HaskChar                                               -> HaskLiteral

@@ -81,15 +71,3 @@ match lit with
   | HaskMachDouble _    => doublePrimTyCon
   | HaskMachLabel _ _ _ => addrPrimTyCon
 end.
   | HaskMachDouble _    => doublePrimTyCon
   | HaskMachLabel _ _ _ => addrPrimTyCon
 end.

-
-Variable tyConToString   : TyCon   -> string.     Extract Inlined Constant tyConToString         => "outputableToString".
-Variable tyFunToString   : TyFun   -> string.     Extract Inlined Constant tyFunToString         => "outputableToString".
-Instance TyConToString   : ToString TyCon := { toString := tyConToString }.
-Instance TyFunToString   : ToString TyFun := { toString := tyFunToString }.
-Instance TyConToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
-Instance TyFunToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
-
-Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable PairTyCon       : TyFun.        Extract Inlined Constant PairTyCon     => "TysWiredIn.pairTyCon".
-Variable UnitTyCon       : TyFun.        Extract Inlined Constant UnitTyCon     => "TysWiredIn.unitTyCon".
-Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".

diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v
index 9801168..8aba304 100644 (file)
--- a/src/HaskProgrammingLanguage.v
+++ b/src/HaskProgrammingLanguage.v
@@ -27,7 +27,8 @@ Require Import Coherence_ch7_8.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 8e4be3f..0b0200b 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -14,7 +14,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 
 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 0d33b0a..d35a870 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -11,7 +11,8 @@ Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index f9d9f3d..d52acb9 100644 (file)
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -9,7 +9,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.
 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 42790b3..25ecd7b 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index aafbe9b..f8176a2 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,7 +8,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.

diff --git a/src/HaskTyCons.v b/src/HaskTyCons.v
new file mode 100644 (file)
index 0000000..617cd59
--- /dev/null
+++ b/src/HaskTyCons.v
@@ -0,0 +1,32 @@
+(*********************************************************************************************************************************)
+(* HaskTyCons: representation of type constructors, type functions, and data constructors                                        *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import HaskKinds.
+
+Variable CoreDataCon     : Type.                      Extract Inlined Constant CoreDataCon          => "DataCon.DataCon".
+
+(* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
+Variable TyCon           : Type.                      Extract Inlined Constant TyCon                => "TyCon.TyCon".
+Variable TyFun           : Type.                      Extract Inlined Constant TyFun                => "TyCon.TyCon".
+
+Variable CoreName        : Type.                      Extract Inlined Constant CoreName              => "Name.Name".
+Variable Class_          : Type.                      Extract Inlined Constant Class_                => "Class.Class".
+Variable CoreIPName      : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
+                                                      Extraction Inline CoreIPName.
+
+Variable tyConToString   : TyCon   -> string.     Extract Inlined Constant tyConToString         => "outputableToString".
+Variable tyFunToString   : TyFun   -> string.     Extract Inlined Constant tyFunToString         => "outputableToString".
+Instance TyConToString   : ToString TyCon := { toString := tyConToString }.
+Instance TyFunToString   : ToString TyFun := { toString := tyFunToString }.
+Instance TyConToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
+Instance TyFunToLatex    : ToLatex  TyCon := { toLatex  := fun x => toLatex (toString x) }.
+
+Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable PairTyCon       : TyFun.        Extract Inlined Constant PairTyCon     => "TysWiredIn.pairTyCon".
+Variable UnitTyCon       : TyFun.        Extract Inlined Constant UnitTyCon     => "TysWiredIn.unitTyCon".
+Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index d5d66c0..85f5b24 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 290d634..f5a3f1a 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -8,7 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 122db2a..0055a17 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 5b73a41..9b34188 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -8,7 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
 Require Import HaskCoreVars.
 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index 5169046..8cb9da6 100644 (file)
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -8,7 +8,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.

diff --git a/src/PCF.v b/src/PCF.v
index 00ffd77..e06cfec 100644 (file)
--- a/src/PCF.v
+++ b/src/PCF.v
@@ -29,7 +29,8 @@ Require Import Coherence_ch7_8.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.