+(* Decidable equality on PHOAS types *)
+Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
+match t1 with
+| TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
+| TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
+| TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
+| TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
+| TArrow => match t2 with TArrow => true | _ => false end
+| TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
+| TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
+| TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
+end
+with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
+match t1 with
+| TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
+| TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
+end.
+
+Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
+match lk as LK return IList _ _ LK with
+ | nil => INil
+ | h::t => n::::(count' t (S n))
+end.
+
+Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
+ compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
+
+(* The PHOAS axioms
+ *
+ * This is not provable in Coq's logic because the Coq function space
+ * is "too big" - although its only definable inhabitants are Coq
+ * functions, it is not provable in Coq that all function space
+ * inhabitants are definable (i.e. there are no "exotic" inhabitants).
+ * This is actually an important feature of Coq: it lets us reason
+ * about properties of non-computable (non-recursive) functions since
+ * any property proven to hold for the entire function space will hold
+ * even for those functions. However when representing binding
+ * structure using functions we would actually prefer the smaller
+ * function-space of *definable* functions only. These two axioms
+ * assert that. *)
+Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
+ if compareHT Γ κ ht1 ht2
+ then ht1=ht2
+ else ht1≠ht2.
+Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
+ if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
+ then htv1=htv2
+ else htv1≠htv2.
+
+(* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
+Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
+ apply Build_EqDecidable.
+ intros.
+ set (compareHT_decides _ _ v1 v2) as z.
+ set (compareHT Γ κ v1 v2) as q.
+ destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
+ left; auto.
+ right; auto.
+ Defined.
projects / coq-hetmet.git / blobdiff