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