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 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 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 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".
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".
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.
(*********************************************************************************************************************************)
-(* HaskLiteralsAndTyCons: representation of compile-time constants (literals) *)
+(* HaskLiterals: representation of compile-time constants (literals) *)
(*********************************************************************************************************************************)
Generalizable All Variables.
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".
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
| 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".
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 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 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 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 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 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.
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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".
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 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 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 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 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 HaskKinds.
Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskProof.
Require Import NaturalDeduction.