Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
| WTyVarTy ec => return WCodeTy ec t2'
| _ => failM "impossible"
end
- | TyFunApp tfc tls => bind tls' = rawHaskTypeListToWeakType tls
+ | TyFunApp tfc _ _ tls => bind tls' = rawHaskTypeListToWeakType tls
; return WTyFunApp tfc tls'
end
with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
+ Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+ : InstantiatedTypeEnv TV (list_ins n κ Γ).
+ rewrite list_ins_app.
+ rewrite <- (list_take_drop _ Γ n) in ite.
+ apply ilist_app.
+ apply ilist_chop in ite; auto.
+ apply ICons.
+ apply tv.
+ apply ilist_chop' in ite.
+ apply ite.
+ Defined.
+
Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
: UniqM WeakCoercion
:= bind t1' = @typeToWeakType Γ κ t1 ite
Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
- Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
+ Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
fun vv' =>
if eqd_dec vv vv'
then OK ev'
else χ vv'.
- Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
+ Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
match varsexprs with
| nil => χ
- | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
+ | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
end.
- Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
+ Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
: InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
-> UniqM WeakExpr :=
- match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
+ match exp as E in @Expr _ _ G D X T 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
- | EGlobal Γ' _ ξ' t wev => fun ite => return WEVar wev
+ | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
+ ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
- ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite
+ ; bind e' = exprToWeakExpr (update_chi χ cv ev') e ite
; 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'
- ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
+ ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite
; return WELet ev' e1' e2'
| ELit _ _ _ lit _ => fun ite => return WELit lit
| EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
| EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
; bind e' = exprToWeakExpr χ e ite
; return WEBrak hetmet_brak (ec _ ite) e' t'
- | ENote _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
+ | ENote _ _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
; return WENote n e'
| ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite
; bind e' = exprToWeakExpr χ e ite
| ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
; return WECast e' c'
- | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k
- ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
+ | ETyLam _ _ _ k _ _ n e => fun ite => bind tv = mkWeakTypeVar k
+ ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
; return WETyLam tv e'
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
; bind t2' = typeToWeakType σ₂ ite
; bind tbranches' = @typeToWeakType Γ _ tbranches ite
; bind escrut' = exprToWeakExpr χ escrut ite
; bind branches' =
- ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _ })
+ ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
: UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match tree with
| T_Leaf None => return []
- | T_Leaf (Some x) => let (scb,e) := x in
+ | T_Leaf (Some x) =>
+ let (sac,scb_e) := x in
+ let (scb,e) := scb_e in
let varstypes := vec2list (scbwv_varstypes scb) in
bind evars_ite = mfresh _ ite
; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
; bind v' = mkWeakExprVar tleaf
; return ((fst vt),v'))
varstypes)
- ; let χ' := update_χ' χ exprvars in
+ ; let χ' := update_chi' χ exprvars in
bind e'' = exprToWeakExpr χ' e (snd evars_ite)
- ; 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'')]
| T_Branch b1 b2 => bind b1' = caseBranches b1
; bind b2' = caseBranches b2
; return (b1',,b2')
(fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
; return WECase vscrut' escrut' tbranches' tc tys branches'
- | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+ | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
=> bind tleaf = typeToWeakType (snd vt) ite
; bind v' = mkWeakExprVar tleaf
; return ((fst vt),v'))
(leaves vars))
- ; let χ' := update_χ' χ vars' in
+ ; let χ' := update_chi' χ vars' in
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 []
- | ELR_leaf _ _ ξ' cv v e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite
+ | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
end.
- Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
+ Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
- match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+ match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
uniqM f => f us >>= fun x => OK (snd x)
end.
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.
projects / coq-hetmet.git / blobdiff