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 Variable tyConToCoreTyCon : TyCon -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
  17 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
  18 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
  19 Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
  20
  21 Instance TyConToString : ToString TyCon := { toString := tyConToString }.
  22 Instance TyFunToString : ToString TyFun := { toString := tyConToString }.
  23
  24 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
  25 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
  26
  27 (*
  28  * WeakType is much like CoreType, but:
  29  *   1. avoids mutually-inductive definitions
  30  *   2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
  31  *   3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
  32  *)
  33 Inductive WeakType :=
  34 | WTyVarTy  : WeakTypeVar                                      -> WeakType
  35 | WAppTy    : WeakType            ->                  WeakType -> WeakType
  36 | WTyFunApp : TyFun               ->             list WeakType -> WeakType
  37 | WTyCon    : TyCon                                            -> WeakType
  38 | WFunTyCon :                                                     WeakType    (* never use (WTyCon ArrowCon);    always use this! *)
  39 | WCodeTy   : WeakTypeVar         ->                  WeakType -> WeakType    (* never use the raw tycon *)
  40 | WCoFunTy  : WeakType            -> WeakType      -> WeakType -> WeakType
  41 | WForAllTy : WeakTypeVar         ->                  WeakType -> WeakType
  42 | WClassP   : Class_              ->             list WeakType -> WeakType
  43 | WIParam   : CoreIPName CoreName ->                  WeakType -> WeakType.
  44
  45 (* EqDecidable instances for WeakType *)
  46 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
  47   apply Build_EqDecidable.
  48   intros.
  49   destruct v1 as [cv1 k1].
  50   destruct v2 as [cv2 k2].
  51   destruct (eqd_dec cv1 cv2); subst.
  52     destruct (eqd_dec k1 k2); subst.
  53     left; auto.
  54     right; intro; apply n; inversion H; subst; auto.
  55     right; intro; apply n; inversion H; subst; auto.
  56     Defined.
  57
  58 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
  59 Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
  60
  61 Inductive WeakCoercion : Type :=
  62 | WCoVar          : WeakCoerVar                                   -> WeakCoercion (* g      *)
  63 | WCoType         : WeakType                                      -> WeakCoercion (* τ      *)
  64 | WCoApp          : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* γ γ    *)
  65 | WCoAppT         : WeakCoercion -> WeakType                      -> WeakCoercion (* γ@v    *)
  66 | WCoAll          : Kind  -> (WeakTypeVar -> WeakCoercion)        -> WeakCoercion (* ∀a:κ.γ *)
  67 | WCoSym          : WeakCoercion                                  -> WeakCoercion (* sym    *)
  68 | WCoComp         : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* ◯      *)
  69 | WCoLeft         : WeakCoercion                                  -> WeakCoercion (* left   *)
  70 | WCoRight        : WeakCoercion                                  -> WeakCoercion (* right  *)
  71 | WCoUnsafe       : WeakType -> WeakType                          -> WeakCoercion (* unsafe *)
  72 (*| WCoCFApp        : ∀ n, CoFunConst n -> vec WeakCoercion n       -> WeakCoercion (* C   γⁿ *)*)
  73 (*| WCoTFApp        : ∀ n, TyFunConst n -> vec WeakCoercion n       -> WeakCoercion (* S_n γⁿ *)*)
  74 .
  75
  76 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
  77 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
  78 match wc with
  79 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
  80 | WCoType    t                       => Prelude_error "FIXME WCoType"
  81 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
  82 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
  83 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
  84 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
  85 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
  86 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
  87 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
  88 | WCoUnsafe  t1 t2                   => (t1,t2)
  89 end.
  90
  91 (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)
  92 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
  93 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
  94
  95 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
  96 Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) :=
  97   match wt with
  98     | WTyCon tc    => Some (tc,acc)
  99     | WAppTy t1 t2 => isTyConApp t1 (t2::acc)
 100     | _            => None
 101   end.
 102
 103 (* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *)
 104 Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
 105
 106 Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
 107   match wt with
 108     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
 109     | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
 110     | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
 111                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
 112                                            | t1'             => AppTy t1' (weakTypeToCoreType' t2)
 113                                          end
 114     | WTyCon    tc                    => TyConApp tc nil
 115     | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType' lt)
 116     | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType' lt))
 117     | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType' ty))
 118     | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t)
 119     | WFunTyCon                       => TyConApp ArrowTyCon nil
 120     | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil)
 121     | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)))
 122                                             (weakTypeToCoreType' t3)
 123   end.
 124
 125 Definition weakTypeToCoreType (wt:WeakType) :=
 126   weakTypeToCoreType' (normalizeWeakType wt).
 127
 128 Definition compare_weakTypes (w1 w2:WeakType) :=
 129   if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
 130     then true
 131     else false.
 132
 133 (*
 134 Instance EqDecidableWeakType : EqDecidable WeakType.
 135   apply Build_EqDecidable.
 136   intros.
 137   set (compare_weakTypes_axiom v1 v2) as x.
 138   set (compare_weakTypes v1 v2) as y.
 139   assert (y=compare_weakTypes v1 v2). reflexivity.
 140   destruct y; rewrite <- H in x.
 141   left; auto.
 142   right; auto.
 143   Defined.
 144 *)
 145
 146 Instance WeakTypeToString : ToString WeakType :=
 147   { toString := coreTypeToString ○ weakTypeToCoreType }.
 148