X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;fp=src%2FHaskWeak.v;h=d5d66c0b7460b052e1fa28c9c52893aea810589e;hp=60b7d0425ddaa8b5a8cb85e47c1eeb07f93e95cf;hb=2ec43bc871b579bac89707988c4855ee1d6c8eda;hpb=24445b56cb514694c603c342d77cbc8329a4b0aa

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 60b7d04..d5d66c0 100644
--- 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".