Require Import HaskStrong.
Require Import HaskCoreVars.
-(* can remove *)
-Require Import HaskStrongToWeak.
-
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
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 " +++ t)
+ 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 _
| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
| WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
| 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' => φ (@fixkind ★ ec) >>= fun ec' => _
+ | 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
) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
end ); clear weakTypeToType.
+ apply ConcatenableString.
destruct case_WTyVarTy.
apply (addErrorMessage "case_WTyVarTy").
apply (addErrorMessage "case_WAppTy").
destruct t1' as [k1' t1'].
destruct t2' as [k2' t2'].
- set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
+ 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 OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
- apply TyFunApp.
+ apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
apply lt'.
apply X.
apply h.
Defined.
-
-Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
-
(* 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).
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:CoreDataCon))) ]; 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 *.
destruct τ' as [τ' l'].
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 haskTyVarToType l) "")+++eol+++
- " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
+ " 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: " +++τ+++eol+++
- " wanted: "+++τ'
+ " got: " +++toString τ+++eol+++
+ " wanted: "+++toString τ'
)) ].
subst.
apply OK.
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 Γ)
(τ:HaskType Γ ★)
(lev:HaskLevel Γ)
(we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
- addErrorMessage ("in weakExprToStrongExpr " +++ we)
+ addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
match we with
| WEVar v => if ig v
- then OK (EGlobal Γ Δ ξ (τ@@lev) v)
- else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+ then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
+ else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
- | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+ | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
| WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr ebody >>= fun tbody =>
weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
- let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
+ let ξ' := update_ξ ξ 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')
| WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
- weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil))
+ weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
(update_ig ig ((v:CoreVar)::nil)) τ lev ebody
>>= fun ebody' =>
OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
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 "+++te)
+ | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
end
| WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
OK (ECoApp Γ Δ κ t1'' t2''
(weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
end
- | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
end
| WECoLam cv e => let (_,_,t1,t2) := cv in
(ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
| WELetRec rb e =>
- let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in
+ let ξ' := update_ξ ξ 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))
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')
+ OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
| WECase vscrut escrut tbranches tc avars alts =>
weakTypeOfWeakExpr escrut >>= fun tscrut =>
weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
-(*
- let ξ' := update_ξ ξ (((vscrut:CoreVar),tscrut'@@lev)::nil) in
- let ig' := update_ig ig ((vscrut:CoreVar)::nil) in
-*)
- let ξ' := ξ in
- let ig' := ig in
- mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ 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
- ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
- Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
+ ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
+ Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ 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 scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
- weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+ (let case_pf := tt in _) >>= fun pf =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
+ weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
(sacpj_ψ sac _ _ avars' ψ)
- (scbwv_ξ scb ξ' lev)
- (update_ig ig' (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
+ (scbwv_ξ 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 =>
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)
-(*
- weakExprToStrongExpr Γ Δ φ ψ ξ ig tscrut' lev escrut >>= fun escrut' =>
- castExpr we "ECaseScrut" (caseType tc avars' @@ lev) (EVar Γ Δ ξ' vscrut) >>= fun evscrut' =>
- castExpr we "ECase" (τ@@lev)
- (ELet Γ Δ ξ tscrut' tbranches' lev (vscrut:CoreVar) escrut'
- (ECase Γ Δ ξ' lev tc tbranches' avars' evscrut' tree))
-*)
- end)).
-
+ 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 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'.
projects / coq-hetmet.git / blobdiff