X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=deb7adc20b2b1bb7dfd4edf42c319d1cfad65240;hp=dacdcae45f240a7aef6e0d3c30d4aa04f8cad629;hb=3def45d67899c421a3eabaf0c5238d4469ad10d7;hpb=539d675a181f178e24c15b2a6ad3c990492eed79 diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index dacdcae..deb7adc 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -10,7 +10,8 @@ Require Import Coq.Strings.String. 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. @@ -61,7 +62,7 @@ Section HaskStrongToWeak. | 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) := @@ -94,32 +95,33 @@ Section HaskStrongToWeak. 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 @@ -131,7 +133,7 @@ Section HaskStrongToWeak. | 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 @@ -156,11 +158,13 @@ Section HaskStrongToWeak. ; 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 _ ★ @@ -168,9 +172,9 @@ Section HaskStrongToWeak. ; 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') @@ -179,12 +183,12 @@ Section HaskStrongToWeak. (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' @@ -204,11 +208,11 @@ Section HaskStrongToWeak. 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.