Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
-Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
+Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta".
Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
Definition dataConExTyVars cdc :=
- filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+ filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
Opaque dataConExTyVars.
Definition dataConCoerKinds cdc :=
filter (map (fun x => match x with EqPred t1 t2 =>
Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
+Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
+
Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
match lht with t@@l => t end.
(* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
-Definition take_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), list (RawHaskType TV κ).
-refine (fix take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
- match exp as E in RawHaskType _ K return κ=K -> list (RawHaskType _ K) with
- | TApp κ₁ κ₂ x y =>
- fun eqpf =>
- ((fun q:list (RawHaskType TV κ₂) =>
- match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> list (RawHaskType _ _) with
- | TApp κ₁' κ₂' x' y' =>
- fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
- | TArrow => fun eqpf'' => _
- | _ => fun _ => nil
- end (refl_equal _)
- | _ => fun _ => nil
- end (refl_equal _))
- (take_arg_types TV _ y))
- | _ => fun _ => nil
- end (refl_equal _)).
- subst; inversion eqpf''; subst.
- apply (y'::q).
- Defined.
+Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
+ match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
+ | KindStar => fun x' =>
+ match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
+ list (RawHaskType _ KindStar) with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => a::b
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end x''
+ | _ => fun _ => nil
+ end
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end) x (take_arg_types y)
+ | _ => nil
+ end.
+
+Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
+ match exp as E in RawHaskType _ K return nat with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
+ | KindStar => fun x' =>
+ match x' return nat -> nat with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => S b
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end x''
+ | _ => fun _ => 0
+ end
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end) x (count_arg_types y)
+ | _ => 0
+ end.
+
+ Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+ intros.
+ induction Γ.
+ apply INil.
+ apply ICons; auto.
+ apply tt.
+ Defined.
+
+Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
+ fun pf =>
+ fun TV ite =>
+ match take_arg_types (ht TV ite) with
+ | nil => Prelude_error "impossible"
+ | x::y => x
+ end.
(* From (t1->(t2->(t3-> ... t))), return t *)
(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
-Definition drop_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), RawHaskType TV κ.
-refine (fix drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : RawHaskType TV κ :=
- match exp as E in RawHaskType _ K return κ=K -> RawHaskType _ K with
- | TApp κ₁ κ₂ x y =>
- fun eqpf =>
- ((fun q:RawHaskType TV κ₂ =>
- match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> RawHaskType _ _ with
- | TApp κ₁' κ₂' x' y' =>
- fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
- | TArrow => fun eqpf'' => _
- | z => fun _ => TApp x y
- end (refl_equal _)
- | z => fun _ => TApp x y
- end (refl_equal _))
- (drop_arg_types TV _ y))
- | z => fun _ => z
- end (refl_equal _)).
- subst; inversion eqpf''; subst.
- apply q.
- Defined.
+Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+ match exp as E in RawHaskType _ K return RawHaskType _ K with
+ | TApp κ₁ κ₂ x y =>
+ let q :=
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
+ | KindStar => fun x' =>
+ match x' return (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun _ b => Some b
+ | _ => fun _ b => None
+ end
+ | _ => fun _ b => None
+ end x''
+ | _ => fun _ => None
+ end
+ | _ => fun _ _ => None
+ end
+ | _ => fun _ _ => None
+ end) x (drop_arg_types y)
+ in match q with
+ | None => TApp x y
+ | Some y => y
+ end
+ | b => b
+ end.
; sac_numExprVars : nat
; sac_ekinds : vec Kind sac_numExTyVars
; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
-; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
-; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
-; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
+; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ
+; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
+; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
+; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
}.
Coercion sac_tc : StrongAltCon >-> TyCon.
Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
-Fixpoint update_ξ
+Fixpoint update_xi
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
(lev:HaskLevel Γ)
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
- | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
end.
-Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
not (In v (map (@fst _ _) varstypes)) ->
- (update_ξ ξ lev varstypes) v = ξ v.
+ (update_xi ξ lev varstypes) v = ξ v.
intros.
induction varstypes.
reflexivity.
projects / coq-hetmet.git / blobdiff