1 (*********************************************************************************************************************************)
2 (* HaskWeakVars: types and variables for HaskWeak *)
3 (*********************************************************************************************************************************)
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.
17 Inductive CoreVarToWeakVarResult : Type :=
18 | CVTWVR_EVar : CoreType -> CoreVarToWeakVarResult
19 | CVTWVR_TyVar : Kind -> CoreVarToWeakVarResult
20 | CVTWVR_CoVar : CoreType -> CoreType -> CoreVarToWeakVarResult.
22 (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
23 Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.
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.
34 Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind :=
35 match tv with weakTypeVar _ k => k end.
36 Coercion weakTypeVarToKind : WeakTypeVar >-> Kind.
38 Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
40 | WExprVar (weakExprVar v _ ) => v
41 | WTypeVar (weakTypeVar v _ ) => v
42 | WCoerVar (weakCoerVar v _ _) => v
44 Coercion weakVarToCoreVar : WeakVar >-> CoreVar.
46 Definition haskLiteralToWeakType lit : WeakType :=
47 WTyCon (haskLiteralToTyCon lit).
48 Coercion haskLiteralToWeakType : HaskLiteral >-> WeakType.
50 Variable coreVarToWeakVar : CoreVar -> CoreVarToWeakVarResult. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
51 Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars".
53 Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".
55 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
58 Instance WeakVarToString : ToString WeakVar :=
59 { toString := fun x => toString (weakVarToCoreVar x) }.