reshuffle definitions in an attempt to iron out inter-file dependenceies

diff --git a/src/Extraction.v b/src/Extraction.v
index ae55381..53b1185 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -12,7 +12,7 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.
 Require Import NaturalDeductionToLatex.
 
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

diff --git a/src/HaskCore.v b/src/HaskCore.v
index abd1428..9024828 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -7,7 +7,7 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 

@@ -18,7 +18,7 @@ Inductive CoreExpr {b:Type} :=
 | CoreEApp   : CoreExpr        ->  CoreExpr     -> CoreExpr
 | CoreELam   : b               ->  CoreExpr     -> CoreExpr
 | CoreELet   : CoreBind        ->  CoreExpr     -> CoreExpr
 | CoreEApp   : CoreExpr        ->  CoreExpr     -> CoreExpr
 | CoreELam   : b               ->  CoreExpr     -> CoreExpr
 | CoreELet   : CoreBind        ->  CoreExpr     -> CoreExpr

-| CoreECase  : CoreExpr   -> b ->  CoreType     -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
+| CoreECase  : CoreExpr   -> b ->  CoreType     -> list (@triple CoreAltCon (list b) CoreExpr) -> CoreExpr

 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
 | CoreEType  : CoreType                         -> CoreExpr
 | CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
 | CoreENote  : Note            ->  CoreExpr     -> CoreExpr
 | CoreEType  : CoreType                         -> CoreExpr

@@ -40,4 +40,7 @@ Extract Inductive CoreBind =>
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
 
 Variable coreExprToString : @CoreExpr CoreVar -> string.  Extract Inlined Constant coreExprToString => "outputableToString".
   "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ].
 
 Variable coreExprToString : @CoreExpr CoreVar -> string.  Extract Inlined Constant coreExprToString => "outputableToString".

-Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
\ No newline at end of file
+Instance CoreExprToString : ToString (@CoreExpr CoreVar) := { toString := coreExprToString }.
+
+Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
+  Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1be33fd..c4bd768 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -7,7 +7,7 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

@@ -15,6 +15,9 @@ Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 

+Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
+

 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
 Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
 Variable coreViewDeep : CoreType  -> CoreType.        Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.

@@ -84,37 +87,46 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)

-Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None

-        | WTypeVar tv => Some (v,tv,tbody)

         | WCoerVar _  => None
         | WCoerVar _  => None

+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end

       end else None
   | _ => None
 end.
 
       end else None
   | _ => None
 end.
 

-Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None

-        | WTypeVar tv => Some (v,tv,tbody)
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end

         | WCoerVar _  => None
       end else None
   | _ => None
 end.
 
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
 

-Definition isCSP (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
       match coreVarToWeakVar ec with
         | WExprVar _  => None

-        | WTypeVar tv => Some (v,tv,tbody)
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => None
+                         end

         | WCoerVar _  => None
       end else None
   | _ => None
         | WCoerVar _  => None
       end else None
   | _ => None

@@ -209,18 +221,18 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         coreExprToWeakExpr e >>= fun e' =>
           expectTyConApp te' nil >>= fun tca =>
             let (tc,lt) := tca in
         coreExprToWeakExpr e >>= fun e' =>
           expectTyConApp te' nil >>= fun tca =>
             let (tc,lt) := tca in

-          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
-                : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+          ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
+                : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

             match branches with
               | nil => OK nil
               | (mkTriple alt vars e)::rest =>
                   mkBranches rest >>= fun rest' => 
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with
             match branches with
               | nil => OK nil
               | (mkTriple alt vars e)::rest =>
                   mkBranches rest >>= fun rest' => 
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with

-                      | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
-                      | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
+                      | DEFAULT                => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
+                      | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')

                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in

-                        OK (((DataAlt dc),
+                        OK (((WeakDataAlt dc),

                         (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
                         (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
                         (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
                         (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
                         (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
                         (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 33ed7a7..8aa81ee 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -9,17 +9,12 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreVars.

+Require Import HaskLiteralsAndTyCons.

 
 

-Variable CoreTyCon           : Type.                      Extract Inlined Constant CoreTyCon             => "TyCon.TyCon".
-Variable CoreDataCon         : Type.                      Extract Inlined Constant CoreDataCon           => "DataCon.DataCon".
-Variable CoreName            : Type.                      Extract Inlined Constant CoreName              => "Name.Name".

 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".
 Variable CoreCoercion        : Type.                      Extract Inlined Constant CoreCoercion          => "Coercion.Coercion".

-Variable Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".

 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".
 Variable classTyCon          : Class_ -> CoreTyCon.       Extract Inlined Constant classTyCon            => "Class.classTyCon".

-Variable tyConToString       : CoreTyCon      -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
-Variable dataConToString     : CoreDataCon-> string.      Extract Inlined Constant dataConToString       => "outputableToString".
-Variable CoreIPName          : Type -> Type.              Extract         Constant CoreIPName "’a"       => "BasicTypes.IPName".
-                                                          Extraction Inline CoreIPName.
+Variable coreTyConToString   : CoreTyCon   -> string.     Extract Inlined Constant coreTyConToString     => "outputableToString".
+Variable coreDataConToString : CoreDataCon -> string.     Extract Inlined Constant coreDataConToString   => "outputableToString".

 
 (* this exracts onto TypeRep.Type, on the nose *)
 Inductive CoreType :=
 
 (* this exracts onto TypeRep.Type, on the nose *)
 Inductive CoreType :=

@@ -44,10 +39,6 @@ Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined C
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
 
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
 

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

 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
 Variable tyCon_eq             : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".
 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".
 Variable tyCon_eq             : EqDecider TyCon.           Extract Inlined Constant tyCon_eq              => "(==)".

@@ -62,5 +53,6 @@ Instance CoreNameEqDecidable  : EqDecidable CoreName    := { eqd_dec := coreName
 Instance CoreTypeToString     : ToString CoreType       := { toString := coreTypeToString }.
 Instance CoreNameToString     : ToString CoreName       := { toString := coreNameToString }.
 Instance CoreCoercionToString : ToString CoreCoercion   := { toString := coreCoercionToString }.
 Instance CoreTypeToString     : ToString CoreType       := { toString := coreTypeToString }.
 Instance CoreNameToString     : ToString CoreName       := { toString := coreNameToString }.
 Instance CoreCoercionToString : ToString CoreCoercion   := { toString := coreCoercionToString }.

-Instance CoreDataConToString  : ToString CoreDataCon    := { toString := dataConToString }.
-Instance CoreTyConToString    : ToString CoreTyCon      := { toString := tyConToString }.
+Instance CoreDataConToString  : ToString CoreDataCon    := { toString := coreDataConToString }.
+Instance CoreTyConToString    : ToString CoreTyCon      := { toString := coreTyConToString }.
+

diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v
index 562b478..d158f05 100644 (file)
--- a/src/HaskCoreVars.v
+++ b/src/HaskCoreVars.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.

+Require Import HaskLiteralsAndTyCons.

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

@@ -13,3 +14,18 @@ Variable coreVar_eq         : forall (a b:CoreVar), sumbool (a=b) (not (a=b)).
 Variable coreVarToString    : CoreVar      -> string.             Extract Inlined Constant coreVarToString => "outputableToString".
 Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec  := coreVar_eq      }.
 Instance CoreVarToString    : ToString CoreVar    := { toString := coreVarToString }.
 Variable coreVarToString    : CoreVar      -> string.             Extract Inlined Constant coreVarToString => "outputableToString".
 Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec  := coreVar_eq      }.
 Instance CoreVarToString    : ToString CoreVar    := { toString := coreVarToString }.

+
+Variable CoreTyCon       : Type.                      Extract Inlined Constant CoreTyCon            => "TyCon.TyCon".
+
+(* 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 CoreAltCon :=
+| DataAlt : CoreDataCon -> CoreAltCon
+| LitAlt  : HaskLiteral -> CoreAltCon
+| DEFAULT :                CoreAltCon.
+Extract Inductive CoreAltCon =>
+  "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].

diff --git a/src/HaskCoreLiterals.v b/src/HaskLiteralsAndTyCons.v
similarity index 74%
rename from src/HaskCoreLiterals.v
rename to src/HaskLiteralsAndTyCons.v
index 05cace2..24fc00f 100644 (file)
--- a/src/HaskCoreLiterals.v
+++ b/src/HaskLiteralsAndTyCons.v
@@ -1,5 +1,5 @@
 (*********************************************************************************************************************************)
 (*********************************************************************************************************************************)

-(* HaskCoreLiterals: representation of compile-time constants (literals)                                                             *)
+(* HaskLiteralsAndTyCons: representation of compile-time constants (literals)                                                    *)

 (*********************************************************************************************************************************)
 
 Generalizable All Variables.
 (*********************************************************************************************************************************)
 
 Generalizable All Variables.

@@ -7,7 +7,12 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import HaskKinds.

-Require Import HaskCoreTypes.
+
+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".

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

@@ -16,6 +21,11 @@ Variable HaskFastString          : Type.      Extract Inlined Constant HaskFastS
 Variable HaskInteger             : Type.      Extract Inlined Constant HaskInteger         => "Prelude.Integer".
 Variable HaskRational            : Type.      Extract Inlined Constant HaskRational        => "Prelude.Rational".
 
 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
 (* This type extracts exactly onto GHC's Literal.Literal type *)
 Inductive HaskLiteral :=
 | HaskMachChar     : HaskChar                                               -> HaskLiteral

@@ -47,19 +57,6 @@ Extract Inductive HaskFunctionOrData =>
 Variable haskLiteralToString : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
 Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
 
 Variable haskLiteralToString : HaskLiteral -> string.    Extract Inlined Constant haskLiteralToString     => "outputableToString".
 Instance HaskLiteralToString : ToString HaskLiteral := { toString := haskLiteralToString }.
 

-(* 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 : CoreDataCon -> AltCon
-| LitAlt  : HaskLiteral -> AltCon
-| DEFAULT :                AltCon.
-Extract Inductive AltCon =>
-  "CoreSyn.AltCon" [ "CoreSyn.DataAlt" "CoreSyn.LitAlt" "CoreSyn.DEFAULT" ].
-

 (* the TyCons for each of the literals above *)
 Variable addrPrimTyCon       : TyCon.   Extract Inlined Constant addrPrimTyCon   => "TysPrim.addrPrimTyCon".
 Variable intPrimTyCon        : TyCon.   Extract Inlined Constant intPrimTyCon    => "TysPrim.intPrimTyCon".
 (* the TyCons for each of the literals above *)
 Variable addrPrimTyCon       : TyCon.   Extract Inlined Constant addrPrimTyCon   => "TysPrim.addrPrimTyCon".
 Variable intPrimTyCon        : TyCon.   Extract Inlined Constant intPrimTyCon    => "TysPrim.intPrimTyCon".

@@ -84,3 +81,8 @@ match lit with
   | HaskMachDouble _    => doublePrimTyCon
   | HaskMachLabel _ _ _ => addrPrimTyCon
 end.
   | 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 }.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index efb9220..6474665 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -14,7 +14,7 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskStrongTypes.
 
 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
 Require Import HaskStrongTypes.
 
 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index f315603..7624c31 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -12,7 +12,7 @@ Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 2c418bd..8efd0af 100644 (file)
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -8,10 +8,10 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskWeakVars.

 Require Import HaskCoreTypes.
 Require Import HaskCoreTypes.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskStrongTypes.
 Require Import HaskStrongTypes.

+Require Import HaskWeakVars.

 
 Section HaskStrong.
 
 
 Section HaskStrong.
 

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 3798a36..1efc666 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -12,7 +12,6 @@ Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

-Require Import HaskWeakVars.

 Require Import HaskProof.
 
 Section HaskStrongToProof.
 Require Import HaskProof.
 
 Section HaskStrongToProof.

@@ -783,16 +782,3 @@ Definition expr2proof  :
 
 End HaskStrongToProof.
 
 
 End HaskStrongToProof.
 

-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
-| DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
-| DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
-  mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
-

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index f7fc56e..71994c6 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,15 +10,13 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
-Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-Require Import HaskCore.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

+Require Import HaskCoreVars.

 
 Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
   : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
 
 Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
   : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=

@@ -73,8 +71,8 @@ Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Pre
 
 Section strongExprToWeakExpr.
 
 
 Section strongExprToWeakExpr.
 

-  Context (hetmet_brak : CoreVar).
-  Context (hetmet_esc  : CoreVar).
+  Context (hetmet_brak : WeakExprVar).
+  Context (hetmet_esc  : WeakExprVar).

 
   Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
     (ftv:Fresh Kind                (fun _ => WeakTypeVar))
 
   Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
     (ftv:Fresh Kind                (fun _ => WeakTypeVar))

@@ -110,7 +108,7 @@ Section strongExprToWeakExpr.
                                      (update_ξ (weakLT'○ξ) (vec2list (vec_map
                                        (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
                                      (weakLT' (tbranches@@l)) })
                                      (update_ξ (weakLT'○ξ) (vec2list (vec_map
                                        (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
                                      (weakLT' (tbranches@@l)) })

-        : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
+        : Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=

         match tree with
           | T_Leaf None     => []
           | T_Leaf (Some x) => let (scb,e) := x in
         match tree with
           | T_Leaf None     => []
           | T_Leaf (Some x) => let (scb,e) := x in

@@ -145,4 +143,4 @@ Section strongExprToWeakExpr.
   | ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))]
   | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite)
   end.
   | ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))]
   | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite)
   end.

-End strongExprToWeakExpr.
\ No newline at end of file
+End strongExprToWeakExpr.

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index e79927a..9bc4219 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,7 +8,7 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.

@@ -353,7 +353,7 @@ Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc))
 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 Record StrongAltCon {tc:TyCon} :=
 { sac_tc          := tc
 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 Record StrongAltCon {tc:TyCon} :=
 { sac_tc          := tc

-; sac_altcon      :  AltCon
+; sac_altcon      :  WeakAltCon

 ; sac_numExTyVars :  nat
 ; sac_numCoerVars :  nat
 ; sac_numExprVars :  nat
 ; sac_numExTyVars :  nat
 ; sac_numCoerVars :  nat
 ; sac_numExprVars :  nat

@@ -365,7 +365,7 @@ Record StrongAltCon {tc:TyCon} :=
 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 }.
 Coercion sac_tc     : StrongAltCon >-> TyCon.
 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 }.
 Coercion sac_tc     : StrongAltCon >-> TyCon.

-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.

   
 
 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
   
 
 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 60b7d04..d5d66c0 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -7,14 +7,15 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
-Require Import HaskCore.
-Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-Require Import HaskCoreTypes.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 

+Inductive WeakAltCon :=
+| WeakDataAlt : CoreDataCon  -> WeakAltCon
+| WeakLitAlt  : HaskLiteral  -> WeakAltCon
+| WeakDEFAULT :                 WeakAltCon.
+

 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr
 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr

@@ -33,20 +34,18 @@ Inductive WeakExpr :=
 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
 (* or hetmet_esc identifier                                                *)
 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
 (* or hetmet_esc identifier                                                *)

-| WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
-| WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
-| WECSP       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WEBrak      : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WEEsc       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WECSP       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr

 
 | WECase      : forall (vscrut:WeakExprVar)
                        (scrutinee:WeakExpr)
                        (tbranches:WeakType)
                        (tc:TyCon)
                        (type_params:list WeakType)
 
 | WECase      : forall (vscrut:WeakExprVar)
                        (scrutinee:WeakExpr)
                        (tbranches:WeakType)
                        (tc:TyCon)
                        (type_params:list WeakType)

-                       (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
+                       (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),

                        WeakExpr.
 
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 
                        WeakExpr.
 
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 

-Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
-  Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 9607d5f..c97a63c 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -8,7 +8,7 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

@@ -20,7 +20,7 @@ Require Import HaskCoreToWeak.
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 

-Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
+Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).

   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 

@@ -31,6 +31,35 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 

+Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
+Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
+
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+  match wa with
+  | WeakDataAlt cdc => DataAlt cdc
+  | WeakLitAlt  lit => LitAlt lit
+  | WeakDEFAULT     => DEFAULT
+  end.
+
+Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
+  match wt with
+    | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
+    | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
+                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
+                                           | t1'             => AppTy t1' (weakTypeToCoreType t2)
+                                         end
+    | WTyCon    tc                    => TyConApp tc nil
+    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
+    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
+    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
+    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
+    | WFunTyCon                       => TyConApp ArrowTyCon nil
+    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
+    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
+                                            (weakTypeToCoreType t3)
+  end.
+

 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
   mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
   mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 

@@ -70,12 +99,12 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 

-                                                  ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+                                                  ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>

-                                                    (mkTriple (ac:AltCon)
+                                                    (mkTriple (weakAltConToCoreAltCon ac)

                                                       (app (app 
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
                                                       (app (app 
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))

@@ -99,3 +128,4 @@ Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 

+

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 04e1055..2593a5c 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,14 +10,13 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

-Require Import HaskCoreTypes.

 Require Import HaskCoreVars.
 
 Open Scope string_scope.
 Require Import HaskCoreVars.
 
 Open Scope string_scope.

@@ -260,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine

-   {| sac_altcon      := DataAlt dc
+   {| sac_altcon      := WeakDataAlt dc

     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc
     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc

@@ -349,7 +348,7 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
   
 End StrongAltCon.
 
   
 End StrongAltCon.
 

-Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
+Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).

   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.
   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.

@@ -363,14 +362,14 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                    ; sac_altcon := LitAlt h
+                    ; sac_altcon := WeakLitAlt h

                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                      ; sac_altcon := DEFAULT |} |}.
+                      ; sac_altcon := WeakDEFAULT |} |}.

             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.

@@ -591,7 +590,7 @@ Definition weakExprToStrongExpr : forall
             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
             let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
               mkAvars avars (tyConKind tc) φ >>= fun avars' =>
                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>

-                  (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+                  (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree

                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
                     match t with
                       ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
                         Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
                     match t with

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 8f55346..4d6500d 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -8,17 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreVars.

-Require Import HaskCoreTypes.
-
-Variable tyConToCoreTyCon : TyCon -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
-Variable tyFunToCoreTyCon : TyFun -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
-Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
-Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
-
-Instance TyConToString : ToString TyCon := { toString := tyConToString }.
-Instance TyFunToString : ToString TyFun := { toString := tyConToString }.

 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.

@@ -87,28 +78,13 @@ match wc with
 | WCoUnsafe  t1 t2                   => (t1,t2)
 end.
 
 | WCoUnsafe  t1 t2                   => (t1,t2)
 end.
 

-Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".

 
 

-Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
-  match wt with
-    | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
-    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
-    | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
-                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
-                                           | t1'             => AppTy t1' (weakTypeToCoreType t2)
-                                         end
-    | WTyCon    tc                    => TyConApp tc nil
-    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
-    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
-    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
-    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
-    | WFunTyCon                       => TyConApp ArrowTyCon nil
-    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
-    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
-                                            (weakTypeToCoreType t3)
-  end.
-
-Instance WeakTypeToString : ToString WeakType :=
-  { toString := coreTypeToString ○ weakTypeToCoreType }.
+(* this is a trick to allow circular definitions, post-extraction *)
+Variable weakTypeToString : WeakType -> string.
+    Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)".
+Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }.

 
 

+Variable tyConToCoreTyCon : TyCon  -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
+Variable tyFunToCoreTyCon : TyFun  -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
+Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
+Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index 44e267d..61eafca 100644 (file)
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -8,7 +8,7 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.

@@ -46,54 +46,12 @@ Variable getTyConTyVars_   : CoreTyCon   -> list CoreVar.  Extract Inlined Const
 Definition tyConTyVars (tc:CoreTyCon) :=
   General.filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
   Opaque tyConTyVars.
 Definition tyConTyVars (tc:CoreTyCon) :=
   General.filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
   Opaque tyConTyVars.

-Definition tyConKind (tc:TyCon) : list Kind :=
-  map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
+Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).

 
 Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)".
 
 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
   splitKind (rawTyFunKind tc).
 
 
 Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)".
 
 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
   splitKind (rawTyFunKind tc).
 

-(*
-(* EqDecidable instances for all of the above *)
-Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
-  apply Build_EqDecidable.
-  intros.
-  destruct v1 as [cv1 t1a t1b].
-  destruct v2 as [cv2 t2a t2b].
-  destruct (eqd_dec cv1 cv2); subst.
-    destruct (eqd_dec t1a t2a); subst.
-    destruct (eqd_dec t1b t2b); subst.
-    left; auto.
-    right; intro; apply n; inversion H; subst; auto.
-    right; intro; apply n; inversion H; subst; auto.
-    right; intro; apply n; inversion H; subst; auto.
-    Defined.
-
-Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
-  apply Build_EqDecidable.
-  intros.
-  destruct v1 as [cv1 k1].
-  destruct v2 as [cv2 k2].
-  destruct (eqd_dec cv1 cv2); subst.
-    destruct (eqd_dec k1 k2); subst.
-    left; auto.
-    right; intro; apply n; inversion H; subst; auto.
-    right; intro; apply n; inversion H; subst; auto.
-    Defined.
-
-Instance WeakVarEqDecidable : EqDecidable WeakVar.
-  apply Build_EqDecidable.
-  induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
-     destruct (eqd_dec w w0); subst.
-     left; auto.
-     right; intro X; apply n; inversion X; auto.
-     left; auto.
-     right; intro X; apply n; inversion X; auto.
-     left; auto.
-     right; intro X; apply n; inversion X; auto.
-  Defined.
-*)
-

 Instance WeakVarToString : ToString WeakVar :=
 Instance WeakVarToString : ToString WeakVar :=

-  { toString := fun x => toString (weakVarToCoreVar x) }.
\ No newline at end of file
+  { toString := fun x => toString (weakVarToCoreVar x) }.