give HaskWeak its own type representation, fix numerous bugs

[coq-hetmet.git] / src / HaskCoreLiterals.v

diff --git a/src/HaskLiterals.v b/src/HaskCoreLiterals.v
similarity index 74%
rename from src/HaskLiterals.v
rename to src/HaskCoreLiterals.v
index f41bcfb..d332ccf 100644 (file)
--- a/src/HaskLiterals.v
+++ b/src/HaskCoreLiterals.v
@@ -1,12 +1,13 @@
 (*********************************************************************************************************************************)
-(* HaskLiterals: representation of compile-time constants (literals)                                                             *)
+(* HaskCoreLiterals: representation of compile-time constants (literals)                                                             *)
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
-Require Import HaskGeneral.
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
 
 (* 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".
@@ -43,18 +44,26 @@ Extract Inductive HaskLiteral => "Literal.Literal"
 Extract Inductive HaskFunctionOrData =>
   "BasicTypes.FunctionOrData" [ "BasicTypes.IsFunction" "BasicTypes.IsData" ].
 
+Variable haskLiteralToString  : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
+
+(* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
+Inductive triple {A B C:Type} :=
+| mkTriple : A -> B -> C -> triple.
+Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
+Extract Inductive triple => "(,,)" [ "(,,)" ].
+
 (* the TyCons for each of the literals above *)
-Variable addrPrimTyCon       : TyCon 0.   Extract Inlined Constant addrPrimTyCon   => "TysPrim.addrPrimTyCon".
-Variable intPrimTyCon        : TyCon 0.   Extract Inlined Constant intPrimTyCon    => "TysPrim.intPrimTyCon".
-Variable wordPrimTyCon       : TyCon 0.   Extract Inlined Constant wordPrimTyCon   => "TysPrim.wordPrimTyCon".
-Variable int64PrimTyCon      : TyCon 0.   Extract Inlined Constant int64PrimTyCon  => "TysPrim.int64PrimTyCon".
-Variable word64PrimTyCon     : TyCon 0.   Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
-Variable floatPrimTyCon      : TyCon 0.   Extract Inlined Constant floatPrimTyCon  => "TysPrim.floatPrimTyCon".
-Variable doublePrimTyCon     : TyCon 0.   Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
-Variable charPrimTyCon       : TyCon 0.   Extract Inlined Constant charPrimTyCon   => "TysPrim.charPrimTyCon".
+Variable addrPrimTyCon       : TyCon.   Extract Inlined Constant addrPrimTyCon   => "TysPrim.addrPrimTyCon".
+Variable intPrimTyCon        : TyCon.   Extract Inlined Constant intPrimTyCon    => "TysPrim.intPrimTyCon".
+Variable wordPrimTyCon       : TyCon.   Extract Inlined Constant wordPrimTyCon   => "TysPrim.wordPrimTyCon".
+Variable int64PrimTyCon      : TyCon.   Extract Inlined Constant int64PrimTyCon  => "TysPrim.int64PrimTyCon".
+Variable word64PrimTyCon     : TyCon.   Extract Inlined Constant word64PrimTyCon => "TysPrim.word64PrimTyCon".
+Variable floatPrimTyCon      : TyCon.   Extract Inlined Constant floatPrimTyCon  => "TysPrim.floatPrimTyCon".
+Variable doublePrimTyCon     : TyCon.   Extract Inlined Constant doublePrimTyCon => "TysPrim.doublePrimTyCon".
+Variable charPrimTyCon       : TyCon.   Extract Inlined Constant charPrimTyCon   => "TysPrim.charPrimTyCon".
 
 (* retrieves the TyCon for a given Literal *)
-Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon 0 :=
+Definition haskLiteralToTyCon (lit:HaskLiteral) : TyCon :=
 match lit with
   | HaskMachNullAddr    => addrPrimTyCon
   | HaskMachChar _      => charPrimTyCon
@@ -68,18 +77,9 @@ match lit with
   | HaskMachLabel _ _ _ => addrPrimTyCon
 end.
 
-Variable haskLiteralToString  : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
-
-(* because Haskell's 3-tuples (triples) are distinct from both ((x,y),z) and (x,(y,z)), we need a new type: *)
-Inductive triple {A B C:Type} :=
-| mkTriple : A -> B -> C -> triple.
-Notation "a ** b ** c" := (mkTriple a b c) (at level 20).
-Extract Inductive triple => "(,,)" [ "(,,)" ].
-
 Inductive AltCon :=
-| DataAlt : forall {n:nat}(tc:TyCon n){m q r:nat}, @DataCon n tc m q r -> AltCon
+| DataAlt : CoreDataCon -> AltCon
 | LitAlt  : HaskLiteral -> AltCon
-| DEFAULT :            AltCon.
+| DEFAULT :                AltCon.
 Extract Inductive AltCon =>
   "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
-