src/HaskWeakVars.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakVars: types and variables for HaskWeak                                                                               *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import Coq.Lists.List.
  10 Require Import HaskKinds.
  11 Require Import HaskCoreLiterals.
  12 Require Import HaskCoreVars.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskWeakTypes.
  15
  16 (* TO DO: finish this *)
  17 Inductive WeakCoercion : Type := weakCoercion : WeakType -> WeakType -> CoreCoercion -> WeakCoercion.
  18
  19 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
  20 Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
  21
  22 (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
  23 Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.
  24
  25 (* a WeakVar is one of the three sorts *)
  26 Inductive WeakVar : Type :=
  27 | WExprVar : WeakExprVar -> WeakVar
  28 | WTypeVar : WeakTypeVar -> WeakVar
  29 | WCoerVar : WeakCoerVar -> WeakVar.
  30   Coercion WExprVar : WeakExprVar >-> WeakVar.
  31   Coercion WTypeVar : WeakTypeVar >-> WeakVar.
  32   Coercion WCoerVar : WeakCoerVar >-> WeakVar.
  33
  34 Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind :=
  35   match tv with weakTypeVar _ k => k end.
  36   Coercion weakTypeVarToKind : WeakTypeVar >-> Kind.
  37
  38 Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
  39   match wv with
  40   | WExprVar (weakExprVar v _   ) => v
  41   | WTypeVar (weakTypeVar v _   ) => v
  42   | WCoerVar (weakCoerVar v _ _ ) => v
  43  end.
  44  Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
  45
  46 Definition haskLiteralToWeakType lit : WeakType :=
  47   WTyCon (haskLiteralToTyCon lit).
  48   Coercion haskLiteralToWeakType : HaskLiteral >-> WeakType.
  49
  50 (* EqDecidable instances for all of the above *)
  51 Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
  52   apply Build_EqDecidable.
  53   intros.
  54   destruct v1 as [cv1 t1a t1b].
  55   destruct v2 as [cv2 t2a t2b].
  56   destruct (eqd_dec cv1 cv2); subst.
  57     destruct (eqd_dec t1a t2a); subst.
  58     destruct (eqd_dec t1b t2b); subst.
  59     left; auto.
  60     right; intro; apply n; inversion H; subst; auto.
  61     right; intro; apply n; inversion H; subst; auto.
  62     right; intro; apply n; inversion H; subst; auto.
  63     Defined.
  64
  65 Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
  66   apply Build_EqDecidable.
  67   intros.
  68   destruct v1 as [cv1 k1].
  69   destruct v2 as [cv2 k2].
  70   destruct (eqd_dec cv1 cv2); subst.
  71     destruct (eqd_dec k1 k2); subst.
  72     left; auto.
  73     right; intro; apply n; inversion H; subst; auto.
  74     right; intro; apply n; inversion H; subst; auto.
  75     Defined.
  76
  77 Instance WeakVarEqDecidable : EqDecidable WeakVar.
  78   apply Build_EqDecidable.
  79   induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
  80      destruct (eqd_dec w w0); subst.
  81      left; auto.
  82      right; intro X; apply n; inversion X; auto.
  83      left; auto.
  84      right; intro X; apply n; inversion X; auto.
  85      left; auto.
  86      right; intro X; apply n; inversion X; auto.
  87   Defined.