1 (*********************************************************************************************************************************)
2 (* HaskWeakVars: types and variables for HaskWeak *)
3 (*********************************************************************************************************************************)
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 HaskGeneral.
11 Require Import HaskLiterals.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
15 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
17 Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion.
19 Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar.
21 Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar.
23 Inductive WeakVar : Type :=
24 | WExprVar : WeakExprVar -> WeakVar
25 | WTypeVar : WeakTypeVar -> WeakVar
26 | WCoerVar : WeakCoerVar -> WeakVar.
28 Definition haskLiteralToCoreType lit : CoreType :=
29 TyConApp (haskLiteralToTyCon lit) nil.
31 Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
33 Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType.
35 (* EqDecidable instances for all of the above *)
36 Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.
37 apply Build_EqDecidable.
39 destruct v1 as [cv1 k1].
40 destruct v2 as [cv2 k2].
41 destruct (eqd_dec cv1 cv2); subst.
42 destruct (eqd_dec k1 k2); subst.
44 right; intro; apply n; inversion H; subst; auto.
45 right; intro; apply n; inversion H; subst; auto.
48 Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
49 apply Build_EqDecidable.
51 destruct v1 as [cv1 t1a t1b].
52 destruct v2 as [cv2 t2a t2b].
53 destruct (eqd_dec cv1 cv2); subst.
54 destruct (eqd_dec t1a t2a); subst.
55 destruct (eqd_dec t1b t2b); subst.
57 right; intro; apply n; inversion H; subst; auto.
58 right; intro; apply n; inversion H; subst; auto.
59 right; intro; apply n; inversion H; subst; auto.
62 Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
63 apply Build_EqDecidable.
65 destruct v1 as [cv1 k1].
66 destruct v2 as [cv2 k2].
67 destruct (eqd_dec cv1 cv2); subst.
68 destruct (eqd_dec k1 k2); subst.
70 right; intro; apply n; inversion H; subst; auto.
71 right; intro; apply n; inversion H; subst; auto.
74 Instance WeakVarEqDecidable : EqDecidable WeakVar.
75 apply Build_EqDecidable.
76 induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
77 destruct (eqd_dec w w0); subst.
79 right; intro X; apply n; inversion X; auto.
81 right; intro X; apply n; inversion X; auto.
83 right; intro X; apply n; inversion X; auto.