Added WeakVar, a separate variable representation for HaskWeak

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 68c40e5..595b8d1 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -36,7 +36,8 @@ import qualified Data.Char
 import Data.Bits ((.&.), shiftL, (.|.))
 import Prelude ( (++), (+), (==), Show, show, Char )
 
 import Data.Bits ((.&.), shiftL, (.|.))
 import Prelude ( (++), (+), (==), Show, show, Char )
 

-{-
+dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc)
+

 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 nat2int (S x) = 1 + (nat2int x)
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 nat2int (S x) = 1 + (nat2int x)

@@ -74,4 +75,4 @@ coreVarSort v | otherwise     = Prelude.error "Var.Var that is neither an expres
 
 outputableToString :: Outputable -> String
 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 
 outputableToString :: Outputable -> String
 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))

--}
+

diff --git a/src/General.v b/src/General.v
index ad8e590..c78daa1 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -17,7 +17,6 @@ Require Import Omega.
 Class EqDecidable (T:Type) :=
 { eqd_type           := T
 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
 Class EqDecidable (T:Type) :=
 { eqd_type           := T
 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))

-; eqd_dec_reflexive  :  forall v, (eqd_dec v v) = (left _ (refl_equal _))

 }.
 Coercion eqd_type : EqDecidable >-> Sortclass.
 
 }.
 Coercion eqd_type : EqDecidable >-> Sortclass.
 

diff --git a/src/HaskCore.v b/src/HaskCore.v
index 2242e48..e9f3929 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -42,9 +42,6 @@ Extract Inductive CoreBind =>
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
 
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
 

-Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
-  Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
-

 Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
 Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
 Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].
 Extract Constant ArrowTyCon           => "Type.funTyCon".     (* Figure 7, (->) *)
 Extract Constant CoFunConst           => "TyCon.TyCon".                        Extraction Implicit CoFunConst [ 1 ].
 Extract Constant TyFunConst           => "TyCon.TyCon".                        Extraction Implicit TyFunConst [ 1 ].

@@ -59,18 +56,4 @@ Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant he
 (* the magic wired-in name for the modal type elimination form *)
 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
 
 (* the magic wired-in name for the modal type elimination form *)
 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
 

-(* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
-  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
-    => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
-  | _ => None
-end.
-Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
-  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
-    => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None
-  | _ => None
-end.
-

 
 

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1b3ffcf..061a6e6 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -5,24 +5,57 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.

+Require Import Coq.Lists.List.

 Require Import HaskGeneral.
 Require Import HaskLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskGeneral.
 Require Import HaskLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

+Require Import HaskWeakVars.

 Require Import HaskWeak.
 
 Require Import HaskWeak.
 

+Variable coreVarToWeakVar      : CoreVar  -> WeakVar.   Extract Inlined Constant coreVarToWeakVar    => "coreVarToWeakVar".
+
+(* detects our crude Core-encoding of modal type introduction/elimination forms *)
+Definition isBrak (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+match ce with
+  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+    => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
+      match coreVarToWeakVar v with
+        | WExprVar _  => None
+        | WTypeVar tv => Some tv
+        | WCoerVar _  => None
+      end else None
+  | _ => None
+end.
+Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+match ce with
+  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+    => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
+      match coreVarToWeakVar v with
+        | WExprVar _  => None
+        | WTypeVar tv => Some tv
+        | WCoerVar _  => None
+      end else None
+  | _ => None
+end.
+
+Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
+  let (t1,t2) := coreCoercionKind cc
+  in  weakCoercion t1 t2 cc.
+

 Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"

-    | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co)
+    | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
+                            OK (WECast e' (coreCoercionToWeakCoercion co))

 
 

-    | CoreEVar   v     => match coreVarSort v with
-                            | CoreExprVar _ => OK (WEVar v)
-                            | CoreTypeVar _ => Error "found a type variable inside an EVar!"
-                            | CoreCoerVar _ => Error "found a coercion variable inside an EVar!"
+    | CoreEVar   v     => match coreVarToWeakVar v with
+                            | WExprVar ev => OK (WEVar ev)
+                            | WTypeVar _  => Error "found a type variable inside an EVar!"
+                            | WCoerVar _  => Error "found a coercion variable inside an EVar!"

                           end
 
     | CoreEApp   e1 e2 => match isBrak e1 with
                           end
 
     | CoreEApp   e1 e2 => match isBrak e1 with

@@ -37,60 +70,64 @@ Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
                                          end
                           end
 
                                          end
                           end
 

-    | CoreELam   v e => match coreVarSort v with
-                         | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam   v e')
-                         | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e')
-                         | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e')
+    | CoreELam   v e => match coreVarToWeakVar v with
+                         | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
+                         | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
+                         | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')

                        end
 
                        end
 

-    | CoreELet   (CoreNonRec v ve) e => match coreVarSort v with
-                         | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' =>
-                                            coreExprToWeakExpr e  >>= fun e'  => OK (WELet v ve' e')
-                         | CoreTypeVar _ => match e with
+    | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
+                         | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
+                                            coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
+                         | WTypeVar _ => match e with

                                               | CoreEType t => Error "saw a type-let"
                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
                                             end
                                               | CoreEType t => Error "saw a type-let"
                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
                                             end

-                         | CoreCoerVar _ => Error "saw an (ELet <coercionVar>)"
+                         | WCoerVar _ => Error "saw an (ELet <coercionVar>)"

                        end
 
     | CoreELet   (CoreRec rb)      e =>
                        end
 
     | CoreELet   (CoreRec rb)      e =>

-      ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) :=
+      ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=

         match cel with
           | nil => OK nil
           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
         match cel with
           | nil => OK nil
           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>

-            match coreVarSort v' with
-              | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t')
-              | CoreTypeVar _ => Error "found a type variable in a recursive let"
-              | CoreCoerVar _ => Error "found a coercion variable in a recursive let"
+            match coreVarToWeakVar v' with
+              | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
+              | WTypeVar _  => Error "found a type variable in a recursive let"
+              | WCoerVar _  => Error "found a coercion variable in a recursive let"

             end
         end) rb) >>= fun rb' =>
       coreExprToWeakExpr e >>= fun e' =>
       OK (WELetRec (unleaves' rb') e')
 
     | CoreECase  e v tbranches alts => 
             end
         end) rb) >>= fun rb' =>
       coreExprToWeakExpr e >>= fun e' =>
       OK (WELetRec (unleaves' rb') e')
 
     | CoreECase  e v tbranches alts => 

+      match coreVarToWeakVar v with
+        | WTypeVar _  => Error "found a type variable in a case"
+        | WCoerVar _  => Error "found a coercion variable in a case"
+        | WExprVar ev => 

       coreExprToWeakExpr e
       >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
       match te' with
         | TyConApp _ tc lt =>
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
       coreExprToWeakExpr e
       >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
       match te' with
         | TyConApp _ tc lt =>
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))

-                : ???(list (AltCon*list CoreVar*WeakExpr)) :=
+                : ???(list (AltCon*list WeakVar*WeakExpr)) :=

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

-                  mkBranches rest
-                  >>= fun rest' => 
+                  mkBranches rest >>= fun rest' => 

                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with
                       | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
                       | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with
                       | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
                       | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')

-                      | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),vars,e')::rest')
+                      | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')

                     end
             end) alts)
           >>= fun branches => coreExprToWeakExpr e
             >>= fun scrutinee =>
               list2vecOrError lt _ >>= fun lt' => 
                     end
             end) alts)
           >>= fun branches => coreExprToWeakExpr e
             >>= fun scrutinee =>
               list2vecOrError lt _ >>= fun lt' => 

-                OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches)))
+                  OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches)))

         | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
       end
         | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
       end

+      end

   end.
 
   end.
 

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index ec9ffcc..a567196 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -15,7 +15,6 @@ Variable coreName_eq        : forall (a b:CoreName),   sumbool (a=b) (not (a=b))
 Axiom    coreName_eq_refl   : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
 Instance CoreNameEqDecidable : EqDecidable CoreName :=
 { eqd_dec            := coreName_eq
 Axiom    coreName_eq_refl   : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
 Instance CoreNameEqDecidable : EqDecidable CoreName :=
 { eqd_dec            := coreName_eq

-; eqd_dec_reflexive  := coreName_eq_refl

 }.
 
 Inductive CoreIPName        : Type -> Type := .                               Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
 }.
 
 Inductive CoreIPName        : Type -> Type := .                               Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].

@@ -37,18 +36,6 @@ Extract Inductive CoreType =>
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 
 Extract Inductive PredType =>
    "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
 

-Variable kindOfCoreType : CoreType -> Kind.        Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
-
-Definition haskLiteralToCoreType lit : CoreType :=
-  TyConApp (haskLiteralToTyCon lit) nil.
-
-Inductive CoreVarSort : Type :=
-| CoreExprVar : CoreType            -> CoreVarSort
-| CoreTypeVar : Kind                -> CoreVarSort
-| CoreCoerVar : CoreType * CoreType -> CoreVarSort.
-
-Variable coreVarSort           : CoreVar  -> CoreVarSort.   Extract Inlined Constant coreVarSort    => "coreVarSort".
-

 Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 
 Variable coreTypeToString      : CoreType     -> string.    Extract Inlined Constant coreTypeToString       => "outputableToString".
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 

@@ -56,3 +43,12 @@ Variable CoreCoercion          : Type.                      Extract Inlined Cons
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 Variable coreCoercionKind      : CoreCoercion -> CoreType*CoreType.
  Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
 Variable coreCoercionKind      : CoreCoercion -> CoreType*CoreType.
  Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".

+
+Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
+  Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
+  Instance CoreTypeEqDecidable : EqDecidable CoreType.
+    apply Build_EqDecidable.
+    apply coretype_eq_dec.
+    Defined.
+
+Variable kindOfCoreType : CoreType -> Kind.      Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".

diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v
index be64e5b..a55c09b 100644 (file)
--- a/src/HaskCoreVars.v
+++ b/src/HaskCoreVars.v
@@ -13,6 +13,6 @@ Variable coreVar_eq       : forall (a b:CoreVar), sumbool (a=b) (not (a=b)).
 Axiom    coreVar_eq_refl  : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
 Instance CoreVarEqDecidable : EqDecidable CoreVar :=
 { eqd_dec            := coreVar_eq
 Axiom    coreVar_eq_refl  : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
 Instance CoreVarEqDecidable : EqDecidable CoreVar :=
 { eqd_dec            := coreVar_eq

-; eqd_dec_reflexive  := coreVar_eq_refl
+(*; eqd_dec_reflexive  := coreVar_eq_refl*)

 }.
 
 }.
 

diff --git a/src/HaskGeneral.v b/src/HaskGeneral.v
index 186ad1c..0c9ba33 100644 (file)
--- a/src/HaskGeneral.v
+++ b/src/HaskGeneral.v
@@ -44,6 +44,19 @@ Inductive Kind : Type :=
 Notation "'★'"   := KindType.
 Notation "a ⇛ b" := (KindTypeFunction a b).
 
 Notation "'★'"   := KindType.
 Notation "a ⇛ b" := (KindTypeFunction a b).
 

+Instance KindEqDecidable : EqDecidable Kind.
+  apply Build_EqDecidable.
+  induction v1.
+    destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+    destruct v2; try (right; intro q; inversion q; fail) ; auto.
+      destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
+      right; intro; subst; inversion H; subst; apply n; auto.
+    destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+    destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+    destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+    destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+  Defined.
+

 Variable tyConToString       : forall n, TyCon n -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
 Variable tyFunToString       : ∀ n, TyFunConst n -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
 Variable coFunToString       : ∀ n, CoFunConst n -> string.  Extract Inlined Constant coFunToString         => "outputableToString".
 Variable tyConToString       : forall n, TyCon n -> string.  Extract Inlined Constant tyConToString         => "outputableToString".
 Variable tyFunToString       : ∀ n, TyFunConst n -> string.  Extract Inlined Constant tyFunToString         => "outputableToString".
 Variable coFunToString       : ∀ n, CoFunConst n -> string.  Extract Inlined Constant coFunToString         => "outputableToString".

@@ -56,15 +69,5 @@ Variable tyCon_eq   : forall {k}(n1 n2:TyCon k),  sumbool (n1=n2) (not (n1=n2)).
     Extract Inlined Constant tyCon_eq   => "(==)".
 Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s),  sumbool (n1=n2) (not (n1=n2)).
     Extract Inlined Constant dataCon_eq => "(==)".
     Extract Inlined Constant tyCon_eq   => "(==)".
 Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s),  sumbool (n1=n2) (not (n1=n2)).
     Extract Inlined Constant dataCon_eq => "(==)".

-Axiom    tyCon_eq_reflexive    : forall `(tc:TyCon n),   (tyCon_eq tc tc) = (left _ (refl_equal tc)).
-Axiom    dataCon_eq_reflexive  : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)).
-
-Instance TyConEqDecidable {n} : EqDecidable (TyCon n) :=
-{ eqd_dec            := tyCon_eq
-; eqd_dec_reflexive  := tyCon_eq_reflexive
-}.
-
-Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) :=
-{ eqd_dec            := dataCon_eq
-; eqd_dec_reflexive  := dataCon_eq_reflexive
-}.
+Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := { eqd_dec            := tyCon_eq }.
+Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := { eqd_dec            := dataCon_eq }.

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index d6c5ecc..e9f3520 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -405,40 +405,6 @@ Fixpoint update_ξ
 
 
 
 
 
 

-(*
-Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)).
-Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ   := match lht with t @@ l => t end.
-Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end.
-(* the type of the scrutinee in a case branch *)
-Require Import Coq.Arith.EqNat.
-Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}.
-  intros.
-  destruct H.
-  exists x; omega.
-  Defined.
-Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n.
-  induction n.
-  apply vec_nil.
-  apply vec_cons.
-    exists n; omega.
-    apply (vec_map (bump _)); auto.
-    Defined.
-Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)).
-  set (hv1 _ (vecOfNats _)) as hv1'.
-  set (hv2 _ (vecOfNats _)) as hv2'.
-  destruct hv1' as [hv1_n hv1_pf].
-  destruct hv2' as [hv2_n hv2_pf].
-  clear hv1_pf.
-  clear hv2_pf.
-  set (eq_nat_decide hv1_n hv2_n) as dec.
-  destruct dec.
-    left.  admit.
-    right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl.
-  Defined.
-(* equality on levels is decidable *)
-Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2))
-  := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2.
-*)

 
 
 
 
 
 

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index b450330..ff696cc 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -5,35 +5,38 @@
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Generalizable All Variables.
 Require Import Preamble.
 Require Import General.

+Require Import Coq.Lists.List.

 Require Import HaskGeneral.
 Require Import HaskLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskGeneral.
 Require Import HaskLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.

+Require Import HaskCoreTypes.
+Require Import HaskWeakVars.

 
 Inductive WeakExpr :=
 
 Inductive WeakExpr :=

-| WEVar       : CoreVar                                                  -> WeakExpr
-| WELit       : HaskLiteral                                              -> WeakExpr
-| WELet       : CoreVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
-| WELetRec    : Tree ??(CoreVar * WeakExpr) -> WeakExpr                  -> WeakExpr
-| WECast      : WeakExpr                    -> CoreCoercion              -> WeakExpr
-| WENote      : Note                        -> WeakExpr                  -> WeakExpr
-| WEApp       : WeakExpr                    -> WeakExpr                  -> WeakExpr
-| WETyApp     : WeakExpr                    -> CoreType                  -> WeakExpr
-| WECoApp     : WeakExpr                    -> CoreCoercion              -> WeakExpr
-| WELam       : CoreVar                     -> WeakExpr                  -> WeakExpr
-| WETyLam     : CoreVar                     -> WeakExpr                  -> WeakExpr
-| WECoLam     : CoreVar                     -> WeakExpr                  -> WeakExpr
-| WEBrak      : CoreVar                     -> WeakExpr                  -> WeakExpr
-| WEEsc       : CoreVar                     -> WeakExpr                  -> WeakExpr
+| WEVar       : WeakExprVar                                                  -> WeakExpr
+| WELit       : HaskLiteral                                                  -> WeakExpr
+| WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
+| WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
+| WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
+| WENote      : Note                            -> WeakExpr                  -> WeakExpr
+| WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
+| WETyApp     : WeakExpr                        -> CoreType                  -> WeakExpr
+| WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
+| WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+| WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
+| WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
+| WEBrak      : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
+| WEEsc       : WeakTypeVar                     -> WeakExpr                  -> WeakExpr

 | WECase      : forall (scrutinee:WeakExpr)
                        (tbranches:CoreType)
                        {n:nat}(tc:TyCon n)
                        (type_params:vec CoreType n)
 | WECase      : forall (scrutinee:WeakExpr)
                        (tbranches:CoreType)
                        {n:nat}(tc:TyCon n)
                        (type_params:vec CoreType n)

-                       (alts : Tree ??(AltCon*list CoreVar*WeakExpr)),
+                       (alts : Tree ??(AltCon*list WeakVar*WeakExpr)),

                        WeakExpr.
 
                        WeakExpr.
 

-(* calculate the free CoreVar's in a WeakExpr *)
-Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
+(* calculate the free WeakVar's in a WeakExpr *)
+Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=

   match me with
     | WELit    _        =>     nil
     | WEVar    cv       => cv::nil
   match me with
     | WELit    _        =>     nil
     | WEVar    cv       => cv::nil

@@ -45,28 +48,34 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
     | WEEsc    ec e     =>                            getWeakExprFreeVars e
     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
     | WEEsc    ec e     =>                            getWeakExprFreeVars e
     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)

-    | WELam    cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
-    | WETyLam  cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
-    | WECoLam  cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
+    | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
+    | WETyLam  cv e     => getWeakExprFreeVars e
+    | WECoLam  cv e     => getWeakExprFreeVars e

 
     (* the messy fixpoints below are required by Coq's termination conditions *)
     | WECase scrutinee tbranches n tc type_params alts =>
       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
 
     (* the messy fixpoints below are required by Coq's termination conditions *)
     | WECase scrutinee tbranches n tc type_params alts =>
       mergeDistinctLists (getWeakExprFreeVars scrutinee) (

-        ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list CoreVar*WeakExpr)) {struct alts} : list CoreVar :=
+        ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) {struct alts} : list WeakExprVar :=

           match alts with
             | T_Leaf  None                                  => nil
             | T_Leaf (Some (DEFAULT,_,e))                   => getWeakExprFreeVars e
             | T_Leaf (Some (LitAlt lit,_,e))                => getWeakExprFreeVars e
           match alts with
             | T_Leaf  None                                  => nil
             | T_Leaf (Some (DEFAULT,_,e))                   => getWeakExprFreeVars e
             | T_Leaf (Some (LitAlt lit,_,e))                => getWeakExprFreeVars e

-            | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e))  => removeFromDistinctList' vars (getWeakExprFreeVars e)
+            | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e))  => removeFromDistinctList' 
+              (General.filter (map (fun v => match v with
+                               | WExprVar ev => Some ev
+                               | WTypeVar _  => None
+                               | WCoerVar _  => None
+              end) vars))
+              (getWeakExprFreeVars e)

             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
           end) alts))
             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
           end) alts))

-    | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) :=
+    | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=

       match mlr with
         | T_Leaf None          => cvl
         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
       end) mlr (mergeDistinctLists (getWeakExprFreeVars e) 
       match mlr with
         | T_Leaf None          => cvl
         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
       end) mlr (mergeDistinctLists (getWeakExprFreeVars e) 

-        ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) :=
+        ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=

           match mlr with
             | T_Leaf None          => nil
             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
           match mlr with
             | T_Leaf None          => nil
             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e

@@ -74,21 +83,21 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
           end) mlr))
   end.
 
           end) mlr))
   end.
 

-(* wrap lambdas around an expression until it has no free variables *)
+(* wrap lambdas around an expression until it has no free expression variables *)

 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
 Definition makeClosedExpression : WeakExpr -> WeakExpr :=

-  fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) :=
+  fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=

   match cvl with
     | nil      => me
     | cv::cvl' => WELam cv (closeExpression me cvl')
   end) me (getWeakExprFreeVars me).
 
 (* messy first-order capture-avoiding substitution on CoreType's *)
   match cvl with
     | nil      => me
     | cv::cvl' => WELam cv (closeExpression me cvl')
   end) me (getWeakExprFreeVars me).
 
 (* messy first-order capture-avoiding substitution on CoreType's *)

-Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) :=
+Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType :=

   match te with
     | TyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
   match te with
     | TyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te

-    | AppTy    t1 t2          => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
+    | AppTy  t1 t2            => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)

     | FunTy    t1 t2          => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
     | FunTy    t1 t2          => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)

-    | ForAllTy tv' t          => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
+    | ForAllTy  tv' t         => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)

     | PredTy (EqPred t1 t2)   => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
     | PredTy (IParam ip ty)   => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
     | PredTy (ClassP _ c lt)  => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
     | PredTy (EqPred t1 t2)   => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
     | PredTy (IParam ip ty)   => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
     | PredTy (ClassP _ c lt)  => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=

@@ -106,64 +115,48 @@ Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) :=
 (* calculate the CoreType of a WeakExpr *)
 Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
   match ce with
 (* calculate the CoreType of a WeakExpr *)
 Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
   match ce with

-    | WEVar   v     => match coreVarSort v with
-                         | CoreExprVar t => OK t
-                         | CoreTypeVar _ => Error "found tyvar in expression"
-                         | CoreCoerVar _ => Error "found coercion variable in expression"
-                       end
+    | WEVar   (weakExprVar v t) => OK t

     | WELit   lit   => OK (haskLiteralToCoreType lit)
     | WEApp   e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
                        match t' with
     | WELit   lit   => OK (haskLiteralToCoreType lit)
     | WEApp   e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
                        match t' with

-                         | FunTy t1 t2 => OK t2

                          | (TyConApp 2 tc (t1::t2::nil)) =>
                            if (tyCon_eq tc ArrowTyCon)
                              then OK t2
                          | (TyConApp 2 tc (t1::t2::nil)) =>
                            if (tyCon_eq tc ArrowTyCon)
                              then OK t2

-                             else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
-                         | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
+                             else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
+                         | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")

                        end
     | WETyApp e t    => coreTypeOfWeakExpr e >>= fun te =>
                         match te with
                        end
     | WETyApp e t    => coreTypeOfWeakExpr e >>= fun te =>
                         match te with

-                          | ForAllTy v ct => match coreVarSort v with
-                                               | CoreExprVar _ => Error "found an expression variable inside an forall-type!"
-                                               | CoreTypeVar _ => OK (replaceCoreVar ct v t)
-                                               | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!"
-                                             end
-                          | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp")
+                          | ForAllTy v ct => OK (replaceCoreVar ct v t)
+                          | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")

                         end
     | WECoApp e co   => coreTypeOfWeakExpr e >>= fun te =>
                         match te with
                         end
     | WECoApp e co   => coreTypeOfWeakExpr e >>= fun te =>
                         match te with

-                          | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3

                           | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
                             if (tyCon_eq tc ArrowTyCon)
                               then OK t3
                           | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
                             if (tyCon_eq tc ArrowTyCon)
                               then OK t3

-                              else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
-                          | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
+                              else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
+                          | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")

                         end
                         end

-    | WELam   ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with
-                                               | CoreExprVar vt => OK (FunTy vt t')
-                                               | CoreTypeVar _  => Error "found a type variable in a WELam!"
-                                               | CoreCoerVar _  => Error "found a coercion variable in a WELam!"
-                                             end
-    | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t')
-    | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with
-                                               | CoreExprVar vt => Error "found an expression variable in a WECoLam!"
-                                               | CoreTypeVar _  => Error "found a type variable in a WECoLam!"
-                                               | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t')
-                                             end
+    | WELam   (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil))
+    | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end
+    | WECoLam (weakCoerVar cv φ₁ φ₂) e =>
+      coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil))

     | WELet   ev ve e            => coreTypeOfWeakExpr e
     | WELetRec rb e              => coreTypeOfWeakExpr e
     | WENote  n e                => coreTypeOfWeakExpr e
     | WELet   ev ve e            => coreTypeOfWeakExpr e
     | WELetRec rb e              => coreTypeOfWeakExpr e
     | WENote  n e                => coreTypeOfWeakExpr e

-    | WECast  e co               => OK (snd (coreCoercionKind co))
+    | WECast  e (weakCoercion t1 t2 _) => OK t2

     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches

-    | WEBrak  ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil))
-    | WEEsc   ec e => coreTypeOfWeakExpr e >>= fun t' =>
+    | WEBrak  ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+                                                           OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
+    | WEEsc   ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>

       match t' with
         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
           if (tyCon_eq tc hetMetCodeTypeTyCon)
       match t' with
         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
           if (tyCon_eq tc hetMetCodeTypeTyCon)

-          then if eqd_dec ec ec' then OK t''
+          then if eqd_dec ecc ec' then OK t''

             else Error "level mismatch in escapification"
           else Error "ill-typed escapification"
         | _ => Error "ill-typed escapification"
             else Error "level mismatch in escapification"
           else Error "ill-typed escapification"
         | _ => Error "ill-typed escapification"

-      end
+      end end

   end.
 
   end.
 

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
new file mode 100644 (file)
index 0000000..c43842f
--- /dev/null
+++ b/src/HaskWeakVars.v
@@ -0,0 +1,88 @@
+(*********************************************************************************************************************************)
+(* HaskWeakVars: types and variables for HaskWeak                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+
+Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind     -> WeakTypeVar.
+
+Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion.
+
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar.
+
+Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar.
+
+Inductive WeakVar : Type :=
+| WExprVar : WeakExprVar -> WeakVar
+| WTypeVar : WeakTypeVar -> WeakVar
+| WCoerVar : WeakCoerVar -> WeakVar.
+
+Definition haskLiteralToCoreType lit : CoreType :=
+  TyConApp (haskLiteralToTyCon lit) nil.
+
+Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
+
+Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType.
+
+(* EqDecidable instances for all of the above *)
+Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.
+  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 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.
+
+
+
+

diff --git a/src/Main.v b/src/Main.v
index 300dfb8..9188e5d 100644 (file)
--- a/src/Main.v
+++ b/src/Main.v
@@ -9,6 +9,7 @@ Require Import HaskLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.

+Require Import HaskWeakVars.

 Require Import HaskWeak.
 Require Import HaskCoreToWeak.
 Require Import HaskStrongTypes.
 Require Import HaskWeak.
 Require Import HaskCoreToWeak.
 Require Import HaskStrongTypes.