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 HaskGeneral.
  11 Require Import HaskLiterals.
  12 Require Import HaskCoreVars.
  13 Require Import HaskCoreTypes.
  14
  15 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind     -> WeakTypeVar.
  16
  17 Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion.
  18
  19 Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar.
  20
  21 Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar.
  22
  23 Inductive WeakVar : Type :=
  24 | WExprVar : WeakExprVar -> WeakVar
  25 | WTypeVar : WeakTypeVar -> WeakVar
  26 | WCoerVar : WeakCoerVar -> WeakVar.
  27
  28 Definition haskLiteralToCoreType lit : CoreType :=
  29   TyConApp (haskLiteralToTyCon lit) nil.
  30
  31 Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
  32
  33 Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType.
  34
  35 (* EqDecidable instances for all of the above *)
  36 Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.
  37   apply Build_EqDecidable.
  38   intros.
  39   destruct v1 as [cv1 k1].
  40   destruct v2 as [cv2 k2].
  41   destruct (eqd_dec cv1 cv2); subst.
  42     destruct (eqd_dec k1 k2); subst.
  43     left; auto.
  44     right; intro; apply n; inversion H; subst; auto.
  45     right; intro; apply n; inversion H; subst; auto.
  46     Defined.
  47
  48 Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
  49   apply Build_EqDecidable.
  50   intros.
  51   destruct v1 as [cv1 t1a t1b].
  52   destruct v2 as [cv2 t2a t2b].
  53   destruct (eqd_dec cv1 cv2); subst.
  54     destruct (eqd_dec t1a t2a); subst.
  55     destruct (eqd_dec t1b t2b); subst.
  56     left; auto.
  57     right; intro; apply n; inversion H; subst; auto.
  58     right; intro; apply n; inversion H; subst; auto.
  59     right; intro; apply n; inversion H; subst; auto.
  60     Defined.
  61
  62 Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
  63   apply Build_EqDecidable.
  64   intros.
  65   destruct v1 as [cv1 k1].
  66   destruct v2 as [cv2 k2].
  67   destruct (eqd_dec cv1 cv2); subst.
  68     destruct (eqd_dec k1 k2); subst.
  69     left; auto.
  70     right; intro; apply n; inversion H; subst; auto.
  71     right; intro; apply n; inversion H; subst; auto.
  72     Defined.
  73
  74 Instance WeakVarEqDecidable : EqDecidable WeakVar.
  75   apply Build_EqDecidable.
  76   induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
  77      destruct (eqd_dec w w0); subst.
  78      left; auto.
  79      right; intro X; apply n; inversion X; auto.
  80      left; auto.
  81      right; intro X; apply n; inversion X; auto.
  82      left; auto.
  83      right; intro X; apply n; inversion X; auto.
  84   Defined.
  85
  86
  87
  88