Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
-(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
Definition dataConExTyVars cdc :=
filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
Opaque dataConExTyVars.
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 *)
Inductive RawCoercionKind : Type :=
mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
- Section CV.
-
- (* the PHOAS type which stands for coercion variables of System FC *)
-
-
- (* Figure 7: γ, δ *)
- Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
-(*
- | CoVar : CV -> RawHaskCoer (* g *)
- | CoType : RawHaskType -> RawHaskCoer (* τ *)
- | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
- | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
- | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
- | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
- | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
- | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
- | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
- | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
- | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
-*)
- End CV.
+ (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
+ Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
+ (*
+ * This has been disabled until we manage to reconcile SystemFC's
+ * coercions with what GHC actually implements (they are not the
+ * same!)
+ *
+ | CoVar : CV -> RawHaskCoer (* g *)
+ | CoType : RawHaskType -> RawHaskCoer (* τ *)
+ | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
+ | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
+ | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
+ | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
+ | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
+ | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
+ | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
+ | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
+ | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
+ *)
End Raw.
Implicit Arguments TCon [ [TV] ].
apply weakCK.
apply IHκ.
Defined.
-(*
-Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
- match κ as K return list (HaskCoercionKind (app K Γ)) with
- | nil => hck
- | _ => map weakCK' hck
- end.
-*)
Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
map weakCK' hck.
Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
:= fun TV ite tv => (f TV (weakITE ite) tv).
-(* I keep mixing up left/right folds *)
-(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
-(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
-
Fixpoint caseType0 {Γ}(lk:list Kind) :
IList _ (HaskType Γ) lk ->
HaskType Γ (fold_right KindArrow ★ lk) ->
Fixpoint update_ξ
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
- (vt:list (VV * LeveledHaskType Γ ★))
+ (lev:HaskLevel Γ)
+ (vt:list (VV * HaskType Γ ★))
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
- | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
end.
+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+ not (In v (map (@fst _ _) varstypes)) ->
+ (update_ξ ξ lev varstypes) v = ξ v.
+ intros.
+ induction varstypes.
+ reflexivity.
+ simpl.
+ destruct a.
+ destruct (eqd_dec v0 v).
+ subst.
+ simpl in H.
+ assert False.
+ apply H.
+ auto.
+ inversion H0.
+ apply IHvarstypes.
+ unfold not; intros.
+ apply H.
+ simpl.
+ auto.
+ Defined.
(***************************************************************************************************)
Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
-(* This is not provable in Coq's logic because the Coq function space
+(* 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).
(* 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
projects / coq-hetmet.git / blobdiff