Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
(*Opaque DataCon.*)
-Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
- intros.
- destruct dc1.
- destruct dc2.
- exact (if eqd_dec cdc cdc0 then true else false).
- Defined.
-
-Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
-
-Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
- intros.
- apply Build_EqDecidable.
- intros.
- set (trust_compare_datacons _ v1 v2) as x.
- set (compare_datacons tc v1 v2) as y.
- assert (y=compare_datacons tc v1 v2). reflexivity.
- destruct y; rewrite <- H in x.
- left; auto.
- right; auto.
- Defined.
-
Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
(* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
(* ToString instance for PHOAS types *)
Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
match t with
- | TVar _ v => "tv" +++ v
+ | TVar _ v => "tv" +++ toString v
| TCon tc => toString tc
| TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
+++typeToString' false n t2+++")=>"
else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
end
| TArrow => "(->)"
- | TAll k f => let alpha := "tv"+++n
- in "(forall "+++ alpha +++ ":"+++ k +++")"+++
+ | TAll k f => let alpha := "tv"+++ toString n
+ in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
typeToString' false (S n) (f n)
| TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
- | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
+ | TyFunApp tfc lt => toString tfc+++ "_" +++ toString n+++" ["+++
+ (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
end
with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
match t with