-
-(* A "tag" is something that distinguishes one case branch from another; it's a lot like Core's AltCon *)
-Inductive Tag {n:nat}(tc:TyCon n) : Type :=
-| TagDefault : Tag tc
-| TagLiteral : forall lit:HaskLiteral , Tag tc (* FIXME: solution is a new StrongLiteral indexed by a tycon *)
-| TagDataCon : forall m q z, DataCon tc m q z -> Tag tc.
-
-(* the number of value variables bound in branches with the given tag *)
-Definition tagNumValVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
- match tag with
- | TagDefault => 0
- | TagLiteral lit => 0
- | TagDataCon m q z dc => z
- end.
-
-(* the number of existential type variables bound in branches with the given tag *)
-Definition tagNumExVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
- match tag with
- | TagDefault => 0
- | TagLiteral lit => 0
- | TagDataCon m q z dc => m
- end.
-
-(* the number of coercion variables bound in branches with the given tag *)
-Definition tagNumCoVars {n}{tc:TyCon n}(tag:Tag tc) : nat :=
- match tag with
- | TagDefault => 0
- | TagLiteral lit => 0
- | TagDataCon m q z dc => q
- end.
+(* like a GHC DataCon, but using PHOAS representation for types and coercions *)
+Record StrongAltConInfo {n}{tc:TyCon n} :=
+{ saci_numExTyVars : nat
+; saci_numCoerVars : nat
+; saci_numExprVars : nat
+; saci_akinds : vec Kind n
+; saci_ekinds : vec Kind saci_numExTyVars
+; saci_kinds := app (vec2list saci_akinds) (vec2list saci_ekinds)
+; saci_coercions : vec (HaskType saci_kinds * HaskType saci_kinds) saci_numCoerVars
+; saci_types : vec (HaskType saci_kinds) saci_numExprVars
+}.
+Implicit Arguments StrongAltConInfo [[n]].