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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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
-| 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
@@ -40,4 +40,7 @@ Extract Inductive CoreBind =>
   "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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -15,6 +15,9 @@ Require Import HaskWeakVars.
 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.
@@ -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 *)
-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
-        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
+        | WTypeVar tv => match coreVarToWeakVar v with
+                           | WExprVar v' => Some (v',tv,tbody)
+                           | _ => 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
-        | 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.
 
-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
-        | 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
@@ -209,18 +221,18 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         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
-                      | 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
-                        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)),

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 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 Class_              : Type.                      Extract Inlined Constant Class_                => "Class.Class".
 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 :=
@@ -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)".
 
-(* 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              => "(==)".
@@ -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 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 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".
@@ -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 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.
@@ -7,7 +7,12 @@ Require Import Preamble.
 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".
@@ -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 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
@@ -47,19 +57,6 @@ Extract Inductive HaskFunctionOrData =>
 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".
@@ -84,3 +81,8 @@ match lit with
   | 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 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

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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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 HaskWeakVars.
 Require Import HaskCoreTypes.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
 
 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 HaskWeakVars.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
@@ -783,16 +782,3 @@ Definition expr2proof  :
 
 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 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 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 Γ))) :=
@@ -73,8 +71,8 @@ Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Pre
 
 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))
@@ -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)) })
-        : 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
@@ -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.
-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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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
-; sac_altcon      :  AltCon
+; sac_altcon      :  WeakAltCon
 ; 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.
-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
   
 
 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 HaskCoreLiterals.
-Require Import HaskCore.
-Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-Require Import HaskCoreTypes.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 
+Inductive WeakAltCon :=
+| WeakDataAlt : CoreDataCon  -> WeakAltCon
+| WeakLitAlt  : HaskLiteral  -> WeakAltCon
+| WeakDEFAULT :                 WeakAltCon.
+
 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                                                *)
-| 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)
-                       (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)).
 
-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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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 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]].
 
@@ -31,6 +31,35 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
 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))).
 
@@ -70,12 +99,12 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                             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)) =>
-                                                    (mkTriple (ac:AltCon)
+                                                    (mkTriple (weakAltConToCoreAltCon ac)
                                                       (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) }.
 
+

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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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.
@@ -260,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds
 
 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
@@ -349,7 +348,7 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
   
 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 *.
@@ -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
-                    ; 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
-                      ; 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 ψ.
@@ -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' =>
-                  (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

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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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.
@@ -87,28 +78,13 @@ match wc with
 | 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 HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 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 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).
 
-(*
-(* 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 :=
-  { toString := fun x => toString (weakVarToCoreVar x) }.
\ No newline at end of file
+  { toString := fun x => toString (weakVarToCoreVar x) }.