src/HaskWeakVars.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakVars: types and variables for HaskWeak                                                                               *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import Coq.Strings.String.
   8 Require Import Coq.Lists.List.
   9 Require Import General.
  10 Require Import HaskKinds.
  11 Require Import HaskLiterals.
  12 Require Import HaskTyCons.
  13 Require Import HaskCoreVars.
  14 Require Import HaskCoreTypes.
  15 Require Import HaskWeakTypes.
  16
  17 Inductive CoreVarToWeakVarResult : Type :=
  18 | CVTWVR_EVar  : CoreType ->             CoreVarToWeakVarResult
  19 | CVTWVR_TyVar : Kind     ->             CoreVarToWeakVarResult
  20 | CVTWVR_CoVar : CoreType -> CoreType -> CoreVarToWeakVarResult.
  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     -> CoreVarToWeakVarResult. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
  51 Variable getTyConTyVars_   : CoreTyCon   -> list CoreVar.           Extract Inlined Constant getTyConTyVars_  => "getTyConTyVars".
  52
  53 Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".
  54
  55 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
  56   rawTyFunKind tc.
  57
  58 Instance WeakVarToString : ToString WeakVar :=
  59   { toString := fun x => toString (weakVarToCoreVar x) }.