src/HaskWeakTypes.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakTypes: types 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
  15 (* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *)
  16
  17 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
  18 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
  19
  20 (*
  21  * WeakType is much like CoreType, but:
  22  *   1. avoids mutually-inductive definitions
  23  *   2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
  24  *   3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
  25  *)
  26 Inductive WeakType :=
  27 | WTyVarTy  : WeakTypeVar                                      -> WeakType
  28 | WAppTy    : WeakType            ->                  WeakType -> WeakType
  29 | WTyFunApp : TyCon               ->             list WeakType -> WeakType
  30 | WTyCon    : TyCon                                            -> WeakType
  31 | WFunTyCon :                                                     WeakType    (* never use (WTyCon ArrowCon);    always use this! *)
  32 | WCodeTy   : WeakTypeVar         ->                  WeakType -> WeakType    (* never use the raw tycon *)
  33 | WCoFunTy  : WeakType            -> WeakType      -> WeakType -> WeakType
  34 | WForAllTy : WeakTypeVar         ->                  WeakType -> WeakType
  35 | WClassP   : Class_              ->             list WeakType -> WeakType
  36 | WIParam   : CoreIPName CoreName ->                  WeakType -> WeakType.
  37
  38 (* EqDecidable instances for WeakType *)
  39 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
  40   apply Build_EqDecidable.
  41   intros.
  42   destruct v1 as [cv1 k1].
  43   destruct v2 as [cv2 k2].
  44   destruct (eqd_dec cv1 cv2); subst.
  45     destruct (eqd_dec k1 k2); subst.
  46     left; auto.
  47     right; intro; apply n; inversion H; subst; auto.
  48     right; intro; apply n; inversion H; subst; auto.
  49     Defined.
  50
  51 (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)
  52 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
  53 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
  54
  55 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
  56 Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) :=
  57   match wt with
  58     | WTyCon tc    => Some (tc,acc)
  59     | WAppTy t1 t2 => isTyConApp t1 (t2::acc)
  60     | _            => None
  61   end.
  62
  63 (* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *)
  64 Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType :=
  65   match te with
  66     | WTyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
  67     | WAppTy  t1 t2            => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst)
  68     | WForAllTy  tv' t         => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst)
  69     | WCoFunTy t1 t2 t         => WCoFunTy (replaceWeakTypeVar t1 tv tsubst)
  70                                       (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst)
  71     | WIParam ip ty  => WIParam ip (replaceWeakTypeVar ty tv tsubst)
  72     | WClassP  c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) :=
  73       match lt with
  74         | nil => nil
  75         | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
  76       end) lt)
  77     | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) :=
  78       match lt with
  79         | nil => nil
  80         | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
  81       end) lt)
  82     | WTyCon tc                => WTyCon tc
  83     | WFunTyCon                => WFunTyCon
  84     | WModalBoxTyCon           => WModalBoxTyCon
  85   end.
  86
  87 (* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *)
  88 Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
  89
  90 Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
  91   match wt with
  92     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
  93     | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
  94                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
  95                                            | t1'             => AppTy t1' (weakTypeToCoreType' t2)
  96                                          end
  97     | WTyCon    tc                    => TyConApp tc nil
  98     | WTyFunApp tc lt                 => TyConApp tc (map weakTypeToCoreType' lt)
  99     | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType' lt))
 100     | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType' ty))
 101     | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t)
 102     | WFunTyCon                       => TyConApp ArrowTyCon nil
 103     | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil)
 104     | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)))
 105                                             (weakTypeToCoreType' t3)
 106   end.
 107
 108 Definition weakTypeToCoreType (wt:WeakType) :=
 109   weakTypeToCoreType' (normalizeWeakType wt).
 110
 111 Definition compare_weakTypes (w1 w2:WeakType) :=
 112   if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
 113     then true
 114     else false.
 115
 116 (* Coq's "decide equality" can't cope here; we have to cheat for now *)
 117 Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2).
 118
 119 Instance EqDecidableWeakType : EqDecidable WeakType.
 120   apply Build_EqDecidable.
 121   intros.
 122   set (compare_weakTypes_axiom v1 v2) as x.
 123   set (compare_weakTypes v1 v2) as y.
 124   assert (y=compare_weakTypes v1 v2). reflexivity.
 125   destruct y; rewrite <- H in x.
 126   left; auto.
 127   right; auto.
 128   Defined.
 129
 130 Definition weakTypeToString : WeakType -> string :=
 131   coreTypeToString ○ weakTypeToCoreType.
 132