From 1c1cdb9014f409248ca96b677503719916b2b477 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 9 May 2011 16:26:46 -0700 Subject: [PATCH] split HaskLiteralsAndTyCons into two files --- src/ExtractionMain.v | 3 ++- src/HaskCore.v | 3 ++- src/HaskCoreToWeak.v | 3 ++- src/HaskCoreTypes.v | 3 ++- src/HaskCoreVars.v | 3 ++- src/HaskFlattener.v | 3 ++- src/{HaskLiteralsAndTyCons.v => HaskLiterals.v} | 26 ++---------------- src/HaskProgrammingLanguage.v | 3 ++- src/HaskProof.v | 3 ++- src/HaskProofToLatex.v | 3 ++- src/HaskStrong.v | 3 ++- src/HaskStrongToWeak.v | 3 ++- src/HaskStrongTypes.v | 3 ++- src/HaskTyCons.v | 32 +++++++++++++++++++++++ src/HaskWeak.v | 3 ++- src/HaskWeakToCore.v | 3 ++- src/HaskWeakToStrong.v | 3 ++- src/HaskWeakTypes.v | 3 ++- src/HaskWeakVars.v | 3 ++- src/PCF.v | 3 ++- 20 files changed, 70 insertions(+), 42 deletions(-) rename src/{HaskLiteralsAndTyCons.v => HaskLiterals.v} (67%) create mode 100644 src/HaskTyCons.v diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index ea89cf4..cae7174 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -15,7 +15,8 @@ Require Import General. Require Import NaturalDeduction. Require Import HaskKinds. -Require Import HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. diff --git a/src/HaskCore.v b/src/HaskCore.v index 9024828..b05c34f 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreTypes. Require Import HaskCoreVars. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index abcd6b8..ac2da8c 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 0fbaeb5..677287a 100644 --- 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 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". diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index d158f05..8b0aabb 100644 --- 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 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". diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index e8aceb1..ae99605 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. 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 --- 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. @@ -7,12 +7,7 @@ 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". +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". @@ -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 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 @@ -81,15 +71,3 @@ match lit with | 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 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskProof. Require Import NaturalDeduction. diff --git a/src/HaskProof.v b/src/HaskProof.v index 8e4be3f..0b0200b 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskWeakVars. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 0d33b0a..d35a870 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskProof. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index f9d9f3d..d52acb9 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskWeakVars. Require Import HaskCoreVars. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 42790b3..25ecd7b 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index aafbe9b..f8176a2 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreTypes. Require Import HaskCoreVars. Require Import HaskWeakTypes. diff --git a/src/HaskTyCons.v b/src/HaskTyCons.v new file mode 100644 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 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskWeakVars. Require Import HaskWeakTypes. diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 290d634..f5a3f1a 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 122db2a..0055a17 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 5b73a41..9b34188 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. 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 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskWeakTypes. diff --git a/src/PCF.v b/src/PCF.v index 00ffd77..e06cfec 100644 --- 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 HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskStrongTypes. Require Import HaskProof. Require Import NaturalDeduction. -- 1.7.10.4