Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
+Require Import HaskWeakToCore.
Require Import HaskStrongTypes.
Require Import HaskStrong.
-Require Import HaskCoreTypes.
Require Import HaskCoreVars.
+Require Import HaskCoreToWeak.
+Require Import HaskCoreTypes.
Open Scope string_scope.
-Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt.
-Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ.
+Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
+Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
+
+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
+ rewrite <- ass_app in lt.
+ exact lt.
+ Defined.
-Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
+Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
unfold TyVarResolver.
refine (fun tv' =>
if eqd_dec tv tv'
- then let fresh := @FreshHaskTyVar Γ tv in _
- else fun TV ite => φ tv' TV (weakITE ite)).
+ then let fresh := @FreshHaskTyVar Γ tv in OK _
+ else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
rewrite <- _H; apply fresh.
Defined.
-Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
+Definition upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
: (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
induction tvs.
apply φ.
simpl.
- apply upφ.
+ apply upPhi.
apply IHtvs.
Defined.
apply X.
Defined.
-Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
+Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
induction lk.
intro q; apply q.
simpl.
(* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
Record StrongAltConPlusJunk {tc:TyCon} :=
{ sacpj_sac : @StrongAltCon tc
-; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
-; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
- (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
+; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ))
+; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ))
}.
Implicit Arguments StrongAltConPlusJunk [ ].
Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
Definition mkPhi (lv:list WeakTypeVar)
: (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
- set (upφ'(Γ:=nil) lv emptyφ) as φ'.
- rewrite <- app_nil_end in φ'.
- apply φ'.
+ set (upPhi2(Γ:=nil) lv emptyφ) as φ2.
+ rewrite <- app_nil_end in φ2.
+ apply φ2.
Defined.
Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
Ltac matchThings T1 T2 S :=
destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
- [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
+ [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
intros.
Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
+ addErrorMessage ("weakTypeToType " +++ toString t)
match t with
| WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
| WTyCon tc => let case_WTyCon := tt in _
| WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
| WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
- | WTyVarTy v => let case_WTyVarTy := tt in _
- | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
- | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => _
+ | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
+ | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _
+ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
+ >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
| WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
weakTypeToType _ φ t1 >>= fun t1' =>
weakTypeToType _ φ t2 >>= fun t2' =>
end
| tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
- | nil => Error "WTyFunApp applied to too many types"
+ | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
+ " tyCon= " +++ toString tc +++ eol +++
+ " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
+ " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
+ " types= " +++ toString lt +++ eol*))
| k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
let case_weakTypeListToTypeList := tt in _
end
end
) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
end ); clear weakTypeToType.
+ apply ConcatenableString.
destruct case_WTyVarTy.
+ apply (addErrorMessage "case_WTyVarTy").
apply OK.
- exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))).
+ exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
destruct case_WAppTy.
+ apply (addErrorMessage "case_WAppTy").
destruct t1' as [k1' t1'].
destruct t2' as [k2' t2'].
+ set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
+ toString t2'+++" of kind "+++toString k2') as err.
destruct k1';
try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
- apply (Error "Kind mismatch in WAppTy:: ").
-
+ apply (Error ("Kind mismatch in WAppTy: "+++err)).
+
destruct case_weakTypeListToTypeList.
+ apply (addErrorMessage "case_weakTypeListToTypeList").
destruct t' as [ k' t' ].
matchThings k k' "Kind mismatch in weakTypeListToTypeList".
subst.
apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
destruct case_WTyFunApp.
+ apply (addErrorMessage "case_WTyFunApp").
apply OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
- apply TyFunApp.
+ apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
apply lt'.
apply X.
destruct case_WTyCon.
+ apply (addErrorMessage "case_WTyCon").
apply OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
apply (TCon tc).
destruct case_WCodeTy.
+ apply (addErrorMessage "case_WCodeTy").
destruct tbody'.
matchThings κ ★ "Kind mismatch in WCodeTy: ".
apply OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
apply TCode.
- apply (TVar (φ (@fixkind ★ ec) TV X)).
+ apply (TVar (ec' TV X)).
subst.
apply h.
apply X.
destruct case_WCoFunTy.
+ apply (addErrorMessage "case_WCoFunTy").
destruct t1' as [ k1' t1' ].
destruct t2' as [ k2' t2' ].
destruct t3' as [ k3' t3' ].
apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
destruct case_WForAllTy.
+ apply (addErrorMessage "case_WForAllTy").
destruct t1.
matchThings ★ κ "Kind mismatch in WForAllTy: ".
subst.
apply h.
Defined.
-
-
(* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
Section StrongAltCon.
Context (tc : TyCon)(dc:DataCon tc).
-(*
-Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
+
+Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
+ -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
intro avars.
intro ct.
- set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
- set (@substφ _ _ avars') as q.
- set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
- set (@weakTypeToType _ φ' ct) as t.
- set (@weakT'' _ Γ t) as t'.
- set (@lamer _ _ _ t') as t''.
+ apply (addErrorMessage "weakTypeToType'").
+ set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
+ set (@substphi _ _ avars') as q.
+ set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2.
+ set (@weakTypeToType _ φ2 ct) as t.
+ destruct t as [|t]; try apply (Error error_message).
+ destruct t as [tk t].
+ matchThings tk ★ "weakTypeToType'".
+ subst.
+ apply OK.
+ set (@weakT'' _ Γ _ t) as t'.
+ set (@lamer _ _ _ _ t') as t''.
fold (tyConKinds tc) in t''.
fold (dataConExKinds dc) in t''.
- apply (q (tyConKinds tc)).
+ apply q.
+ clear q.
unfold tyConKinds.
unfold dataConExKinds.
rewrite <- vec2list_map_list2vec.
Definition mkStrongAltCon : @StrongAltCon tc.
refine
- {| sac_altcon := DataAlt dc
+ {| sac_altcon := WeakDataAlt dc
; sac_numCoerVars := length (dataConCoerKinds dc)
; sac_numExprVars := length (dataConFieldTypes dc)
- ; sac_akinds := tyConKinds tc
; sac_ekinds := dataConExKinds dc
; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
; sac_types := fun Γ avars => let case_sac_types := tt in _
refine (vec_map _ (list2vec (dataConCoerKinds dc))).
intro.
destruct X.
- apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ apply (
+ match
+ q avars w >>= fun t1 =>
+ q avars w0 >>= fun t2 =>
+ OK (mkHaskCoercionKind t1 t2)
+ with
+ | Error s => Prelude_error s
+ | OK y => y
+ end).
destruct case_sac_types.
refine (vec_map _ (list2vec (dataConFieldTypes dc))).
intro X.
- apply (weakTypeToType' avars).
- apply X.
+ unfold tyConKind in avars.
+ set (@weakTypeToType' Γ) as q.
+ unfold tyConKinds in q.
+ rewrite <- vec2list_map_list2vec in q.
+ rewrite vec2list_list2vec in q.
+ set (q avars X) as y.
+ apply (match y with
+ | Error s =>Prelude_error s
+ | OK y' => y'
+ end).
Defined.
-
+
+
Lemma weakCV' : forall {Γ}{Δ} Γ',
HaskCoVar Γ Δ
-> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
intros.
unfold HaskCoVar in *.
intros; apply (X TV CV).
- apply vec_chop' in env; auto.
+ apply ilist_chop' in env; auto.
unfold InstantiatedCoercionEnv in *.
unfold weakCK'' in cenv.
destruct Γ'.
+ rewrite <- map_preserves_length in cenv.
apply cenv.
rewrite <- map_preserves_length in cenv.
apply cenv.
Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
refine
{| sacpj_sac := mkStrongAltCon
- ; sacpj_φ := fun Γ φ => (fun htv => weakV' (φ htv))
- ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
+ ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
+ ; sacpj_psi :=
+ fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
|}.
intro.
- unfold sac_Γ.
+ unfold sac_gamma.
unfold HaskCoVar in *.
intros.
apply (x TV CV env).
simpl in cenv.
- unfold sac_Δ in *.
+ unfold sac_delta in *.
unfold InstantiatedCoercionEnv in *.
apply vec_chop' in cenv.
apply cenv.
Defined.
-*)
+
+ Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
+ intros.
+ induction Δ.
+ reflexivity.
+ simpl.
+ rewrite IHΔ.
+ reflexivity.
+ Qed.
+
End StrongAltCon.
-(*
-Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
+
+Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
destruct alt.
set (c:DataCon _) as dc.
set ((dataConTyCon c):TyCon) as tc' in *.
set (eqd_dec tc tc') as eqpf; destruct eqpf;
[ idtac
- | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst.
+ | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
apply OK.
eapply mkStrongAltConPlusJunk.
simpl in *.
apply dc.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
- ; sac_altcon := LitAlt h
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ ; sac_altcon := WeakLitAlt h
|} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
- apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
- ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
- ; sac_altcon := DEFAULT |} |}.
+ intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
+ apply OK; refine {| sacpj_sac := {|
+ sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
+ ; sac_altcon := WeakDEFAULT |} |}.
intro; intro φ; apply φ.
- intro; intro; intro; intro ψ; apply ψ.
+ intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
+ rewrite weakCK'_nil_inert. apply ψ.
Defined.
-Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) :=
- match mlr with
- | T_Leaf None => []
- | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
- | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
- end.
-*)
-
Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
fun wev => match wev with weakExprVar _ t => t end.
Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
-(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*)
+Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
-Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
- WeakCoerVar -> HaskCoVar Γ (κ::Δ).
+Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
+ WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
intros.
+ refine (ψ X >>= _).
unfold HaskCoVar.
intros.
- apply (ψ X TV CV env).
+ apply OK.
+ intros.
inversion cenv; auto.
Defined.
(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
-Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ)
- : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ').
+Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l)
+ : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l').
+ apply (addErrorMessage ("castExpr " +++ err_msg)).
intros.
- destruct τ as [τ l].
- destruct τ' as [τ' l'].
- destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
- destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
+ destruct (eqd_dec l l'); [ idtac
+ | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
+ " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
+ " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
+ )) ].
+ destruct (eqd_dec τ τ'); [ idtac
+ | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
+ " got: " +++toString τ+++eol+++
+ " wanted: "+++toString τ'
+ )) ].
subst.
apply OK.
apply e.
Defined.
-Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
+Definition coVarKind (wcv:WeakCoerVar) : Kind :=
+ match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
+ Coercion coVarKind : WeakCoerVar >-> Kind.
+
+Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
intros.
set (weakTypeToType φ t) as wt.
destruct wt; try apply (Error error_message).
destruct h.
- matchThings κ κ0 "Kind mismatch in weakTypeToType': ".
+ matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
subst.
apply OK.
apply h.
Defined.
+Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
+ match t with
+ | T_Leaf None => []
+ | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
+ | OK t' => [((wev:CoreVar),t')]
+ | _ => []
+ end
+ | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
+ end.
+
+Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
+match lk as LK return ???(IList Kind (HaskType Γ) LK) with
+ | nil => match wtl with
+ | nil => OK INil
+ | _ => Error "length mismatch in mkAvars"
+ end
+ | k::lk' => match wtl with
+ | nil => Error "length mismatch in mkAvars"
+ | wt::wtl' =>
+ weakTypeToTypeOfKind φ wt k >>= fun t =>
+ mkAvars wtl' lk' φ >>= fun rest =>
+ OK (ICons _ _ t rest)
+ end
+end.
+
+Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
+ match vars with
+ | nil => ig
+ | v::vars' =>
+ fun v' =>
+ if eqd_dec v v'
+ then false
+ else update_ig ig vars' v'
+ end.
+
+(* does the specified variable occur free in the expression? *)
+Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
+ match me with
+ | WELit _ => false
+ | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
+ | WECast e co => doesWeakVarOccur wev e
+ | WENote n e => doesWeakVarOccur wev e
+ | WETyApp e t => doesWeakVarOccur wev e
+ | WECoApp e co => doesWeakVarOccur wev e
+ | WEBrak _ ec e _ => doesWeakVarOccur wev e
+ | WEEsc _ ec e _ => doesWeakVarOccur wev e
+ | WECSP _ ec e _ => doesWeakVarOccur wev e
+ | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
+ | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+ | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+ | WETyLam cv e => doesWeakVarOccur wev e
+ | WECoLam cv e => doesWeakVarOccur wev e
+ | WECase vscrut escrut tbranches tc avars alts =>
+ doesWeakVarOccur wev escrut ||
+ if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
+ ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
+ match alts with
+ | T_Leaf None => false
+ | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
+ | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
+ | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
+ | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
+ end) alts)
+ | WELetRec mlr e =>
+ doesWeakVarOccur wev e ||
+ (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
+ match mlr with
+ | T_Leaf None => false
+ | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+ | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
+ end) mlr
+ end.
+Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
+ (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
+ match alts with
+ | T_Leaf None => false
+ | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
+ | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
+ | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
+ | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
+ end.
+
+Definition checkDistinct :
+ forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+ intros.
+ set (distinct_decidable lv) as q.
+ destruct q.
+ exact (OK d).
+ exact (Error "checkDistinct failed").
+ Defined.
+
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+ refine {| glob_kinds := nil |}.
+ apply wev.
+ intros.
+ apply τ.
+ Defined.
+
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
(Δ:CoercionEnv Γ)
(φ:TyVarResolver Γ)
(ψ:CoVarResolver Γ Δ)
- (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
+ (ig:CoreVar -> bool)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ),
- WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ).
+ WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ).
refine ((
fix weakExprToStrongExpr
(Γ:TypeEnv)
(Δ:CoercionEnv Γ)
(φ:TyVarResolver Γ)
(ψ:CoVarResolver Γ Δ)
- (ξ:WeakExprVar -> LeveledHaskType Γ ★)
+ (ξ:CoreVar -> LeveledHaskType Γ ★)
+ (ig:CoreVar -> bool)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ)
- (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
+ (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) :=
+ addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
match we with
- | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
+ | WEVar v => if ig v
+ then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev)
+ else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v)
- | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
+ | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev)
- | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv =>
- weakTypeOfWeakExpr e >>= fun t =>
- weakTypeToType' φ t ★ >>= fun τ' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' =>
- castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
+ | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
+ weakTypeOfWeakExpr ebody >>= fun tbody =>
+ weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
+ let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in
+ let ig' := update_ig ig ((ev:CoreVar)::nil) in
+ weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
+ castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody')
- | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
- castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
+ | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
+ weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
+ castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e')
- | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' =>
+ | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
+ weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
match lev with
| nil => Error "ill-leveled escapification"
- | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
- >>= fun e' =>
- castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
+ | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
+ >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e')
end
- | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
- | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv =>
- weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody
+ | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
+
+ | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e')
+
+ | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
+ weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil))
+ (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
>>= fun ebody' =>
- OK (ELet _ _ _ tv _ lev v ve' ebody')
+ OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
| WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
- weakTypeToType' φ t2 ★ >>= fun t2' =>
- weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
- weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
+ weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
OK (EApp _ _ _ _ _ _ e1' e2')
- | WETyLam tv e => let φ' := upφ tv φ in
+ | WETyLam tv e => let φ2 := upPhi tv φ in
weakTypeOfWeakExpr e >>= fun te =>
- weakTypeToType' φ' te ★ >>= fun τ' =>
- weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
- >>= fun e' =>
- castExpr "WETyLam1" _ e' >>= fun e'' =>
- castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
+ weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
+ weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+ (fun x => (ψ x) >>= fun y =>
+ OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+ >>= fun e' => castExpr we "WETyLam2" _ _
+ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')
| WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
match te with
| WForAllTy wtv te' =>
- let φ' := upφ wtv φ in
- weakTypeToType' φ' te' ★ >>= fun te'' =>
- weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
- weakTypeToType' φ t wtv >>= fun t' =>
- castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
- | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
+ let φ2 := upPhi wtv φ in
+ weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
+ weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
+ castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
+ | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
end
- (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
- * to get them back working again *)
- | WECoApp e t => Error "weakExprToStrongExpr: WECoApp not yet implemented"
- | WECoLam cv e => Error "weakExprToStrongExpr: WECoLam not yet implemented"
- | WECast e co => Error "weakExprToStrongExpr: WECast not yet implemented"
- | WELetRec rb e => Error "weakExprToStrongExpr: WELetRec not yet implemented"
- | WECase e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase not yet implemented"
- end)).
+ | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | WCoFunTy t1 t2 t3 =>
+ weakTypeToType φ t1 >>= fun t1' =>
+ match t1' with
+ haskTypeOfSomeKind κ t1'' =>
+ weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
+ weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
+ castExpr we "WECoApp" _ _ e' >>= fun e'' =>
+ OK (ECoApp Γ Δ κ t1'' t2''
+ (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
+ end
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
+ end
+
+ | WECoLam cv e => let (_,t1,t2) := cv in
+ weakTypeOfWeakExpr e >>= fun te =>
+ weakTypeToTypeOfKind φ te ★ >>= fun te' =>
+ weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
+ weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
+ weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' =>
+ castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+
+ | WECast e co => let (t1,t2) := weakCoercionTypes co in
+ weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
+ weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
+ castExpr we "WECast" _ _
+ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
+
+ | WELetRec rb e =>
+ let ξ' := update_xi ξ lev _ in
+ let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
+ let binds :=
+ (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
+ : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
+ match t with
+ | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
+ | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
+ | T_Branch b1 b2 =>
+ binds b1 >>= fun b1' =>
+ binds b2 >>= fun b2' =>
+ OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
+ end) rb
+ in binds >>= fun binds' =>
+ checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
+ OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
+
+ | WECase vscrut escrut tbranches tc avars alts =>
+ weakTypeOfWeakExpr escrut >>= fun tscrut =>
+ weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
+ if doesWeakVarOccurAlts vscrut alts
+ then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
+ else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
+ (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+ ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
+ Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) :=
+ match t with
+ | T_Leaf None => OK []
+ | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
+ mkStrongAltConPlusJunk' tc ac >>= fun sac =>
+ list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
+ >>= fun exprvars' =>
+ (let case_pf := tt in _) >>= fun pf =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
+ weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ)
+ (sacpj_psi sac _ _ avars' ψ)
+ (scbwv_xi scb ξ lev)
+ (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
+ (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+ let case_case := tt in OK [ _ ]
+ | T_Branch b1 b2 =>
+ mkTree b1 >>= fun b1' =>
+ mkTree b2 >>= fun b2' =>
+ OK (b1',,b2')
+ end) alts >>= fun tree =>
+
+ weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
+ castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
+ end)); try clear binds; try apply ConcatenableString.
+
+ destruct case_some.
+ apply (addErrorMessage "case_some").
+ simpl.
+ destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
+ matchThings h (unlev (ξ' wev)) "LetRec".
+ destruct wev.
+ rewrite matchTypeVars_pf.
+ clear matchTypeVars_pf.
+ set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
+ destruct e''; try apply (Error error_message).
+ apply OK.
+ apply ELR_leaf.
+ unfold ξ'.
+ simpl.
+ induction (leaves (varsTypes rb φ)).
+ simpl; auto.
+ destruct (ξ c).
+ simpl.
+ apply e1.
+ rewrite mapleaves.
+ apply rb_distinct.
+
+ destruct case_pf.
+ set (distinct_decidable (vec2list exprvars')) as dec.
+ destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
+ apply OK; auto.
+
+ destruct case_case.
+ exists sac.
+ exists scb.
+ apply ebranch'.
+
Defined.
projects / coq-hetmet.git / blobdiff