src/HaskTyCons.v

   1 (*********************************************************************************************************************************)
   2 (* HaskTyCons: representation of type constructors, type functions, and data constructors                                        *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import HaskKinds.
  10
  11 Variable CoreDataCon     : Type.                      Extract Inlined Constant CoreDataCon          => "DataCon.DataCon".
  12
  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".
  16
  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.
  21
  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) }.
  28
  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".