(*********************************************************************************************************************************) (* 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".