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 Variable coreVarToWeakVar  : CoreVar  -> WeakVar.   Extract Inlined Constant coreVarToWeakVar    => "coreVarToWeakVar".
  51 Variable getTyConTyVars_   : CoreTyCon   -> list CoreVar.  Extract Inlined Constant getTyConTyVars_   => "getTyConTyVars".
  52 Definition tyConTyVars (tc:CoreTyCon) :=
  53   General.filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)).
  54   Opaque tyConTyVars.
  55 Definition tyConKind (tc:TyCon) : list Kind :=
  56   map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
  57 Variable tyFunResultKind : CoreTyCon -> Kind. Extract Inlined Constant tyFunResultKind => "tyFunResultKind".
  58 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
  59   ((map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc)) , (tyFunResultKind tc)).
  60
  61 (* EqDecidable instances for all of the above *)
  62 Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
  63   apply Build_EqDecidable.
  64   intros.
  65   destruct v1 as [cv1 t1a t1b].
  66   destruct v2 as [cv2 t2a t2b].
  67   destruct (eqd_dec cv1 cv2); subst.
  68     destruct (eqd_dec t1a t2a); subst.
  69     destruct (eqd_dec t1b t2b); subst.
  70     left; auto.
  71     right; intro; apply n; inversion H; subst; auto.
  72     right; intro; apply n; inversion H; subst; auto.
  73     right; intro; apply n; inversion H; subst; auto.
  74     Defined.
  75
  76 Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
  77   apply Build_EqDecidable.
  78   intros.
  79   destruct v1 as [cv1 k1].
  80   destruct v2 as [cv2 k2].
  81   destruct (eqd_dec cv1 cv2); subst.
  82     destruct (eqd_dec k1 k2); subst.
  83     left; auto.
  84     right; intro; apply n; inversion H; subst; auto.
  85     right; intro; apply n; inversion H; subst; auto.
  86     Defined.
  87
  88 Instance WeakVarEqDecidable : EqDecidable WeakVar.
  89   apply Build_EqDecidable.
  90   induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
  91      destruct (eqd_dec w w0); subst.
  92      left; auto.
  93      right; intro X; apply n; inversion X; auto.
  94      left; auto.
  95      right; intro X; apply n; inversion X; auto.
  96      left; auto.
  97      right; intro X; apply n; inversion X; auto.
  98   Defined.
  99
 100
 101
 102 Instance WeakVarToString : ToString WeakVar :=
 103   { toString := fun x => toString (weakVarToCoreVar x) }.