Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
; return WTyFunApp tfc tls'
end
with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
; return WTyFunApp tfc tls'
end
with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
-> UniqM WeakExpr :=
match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
| EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
-> UniqM WeakExpr :=
match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
| EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
; return WELam ev' e'
| ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite
; bind e1' = exprToWeakExpr χ e1 ite
; bind ev' = mkWeakExprVar tv'
; return WELam ev' e'
| ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite
; bind e1' = exprToWeakExpr χ e1 ite
; bind ev' = mkWeakExprVar tv'
; return WELet ev' e1' e2'
| ELit _ _ _ lit _ => fun ite => return WELit lit
| EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
; return WELet ev' e1' e2'
| ELit _ _ _ lit _ => fun ite => return WELit lit
| EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
: UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match tree with
| T_Leaf None => return []
: UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match tree with
| T_Leaf None => return []
let varstypes := vec2list (scbwv_varstypes scb) in
bind evars_ite = mfresh _ ite
; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
let varstypes := vec2list (scbwv_varstypes scb) in
bind evars_ite = mfresh _ ite
; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
- ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+ ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
(fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
; return WECase vscrut' escrut' tbranches' tc tys branches'
(fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
; return WECase vscrut' escrut' tbranches' tc tys branches'
bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
; bind e' = exprToWeakExpr χ' e ite
; return WELetRec elrb' e'
bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
; bind e' = exprToWeakExpr χ' e ite
; return WELetRec elrb' e'
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=