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 Coercion WExprVar : WeakExprVar >-> WeakVar.
  28 Coercion WTypeVar : WeakTypeVar >-> WeakVar.
  29 Coercion WCoerVar : WeakCoerVar >-> WeakVar.
  30
  31
  32 Definition haskLiteralToCoreType lit : CoreType :=
  33   TyConApp (haskLiteralToTyCon lit) nil.
  34
  35 Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
  36
  37 Definition weakTypeToString : CoreType -> string :=
  38   coreTypeToString ○ weakTypeToCoreType.
  39
  40 (* EqDecidable instances for all of the above *)
  41 Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.
  42   apply Build_EqDecidable.
  43   intros.
  44   destruct v1 as [cv1 k1].
  45   destruct v2 as [cv2 k2].
  46   destruct (eqd_dec cv1 cv2); subst.
  47     destruct (eqd_dec k1 k2); subst.
  48     left; auto.
  49     right; intro; apply n; inversion H; subst; auto.
  50     right; intro; apply n; inversion H; subst; auto.
  51     Defined.
  52
  53 Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
  54   apply Build_EqDecidable.
  55   intros.
  56   destruct v1 as [cv1 t1a t1b].
  57   destruct v2 as [cv2 t2a t2b].
  58   destruct (eqd_dec cv1 cv2); subst.
  59     destruct (eqd_dec t1a t2a); subst.
  60     destruct (eqd_dec t1b t2b); subst.
  61     left; auto.
  62     right; intro; apply n; inversion H; subst; auto.
  63     right; intro; apply n; inversion H; subst; auto.
  64     right; intro; apply n; inversion H; subst; auto.
  65     Defined.
  66
  67 Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
  68   apply Build_EqDecidable.
  69   intros.
  70   destruct v1 as [cv1 k1].
  71   destruct v2 as [cv2 k2].
  72   destruct (eqd_dec cv1 cv2); subst.
  73     destruct (eqd_dec k1 k2); subst.
  74     left; auto.
  75     right; intro; apply n; inversion H; subst; auto.
  76     right; intro; apply n; inversion H; subst; auto.
  77     Defined.
  78
  79 Instance WeakVarEqDecidable : EqDecidable WeakVar.
  80   apply Build_EqDecidable.
  81   induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
  82      destruct (eqd_dec w w0); subst.
  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      left; auto.
  88      right; intro X; apply n; inversion X; auto.
  89   Defined.
  90
  91
  92
  93