1 (*********************************************************************************************************************************)
2 (* HaskTyCons: representation of type constructors, type functions, and data constructors *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import HaskKinds.
11 Variable CoreDataCon : Type. Extract Inlined Constant CoreDataCon => "DataCon.DataCon".
13 (* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *)
14 Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon".
15 Variable TyFun : Type. Extract Inlined Constant TyFun => "TyCon.TyCon".
17 Variable CoreName : Type. Extract Inlined Constant CoreName => "Name.Name".
18 Variable Class_ : Type. Extract Inlined Constant Class_ => "Class.Class".
19 Variable CoreIPName : Type -> Type. Extract Constant CoreIPName "’a" => "BasicTypes.IPName".
20 Extraction Inline CoreIPName.
22 Variable tyConToString : TyCon -> string. Extract Inlined Constant tyConToString => "outputableToString".
23 Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString".
24 Instance TyConToString : ToString TyCon := { toString := tyConToString }.
25 Instance TyFunToString : ToString TyFun := { toString := tyFunToString }.
26 Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
27 Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
29 Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
30 Variable PairTyCon : TyFun. Extract Inlined Constant PairTyCon => "TysWiredIn.pairTyCon".
31 Variable UnitTyCon : TyFun. Extract Inlined Constant UnitTyCon => "TysWiredIn.unitTyCon".
32 Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".