X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=8bb52e12f6ee81c217dd02d4ccc323519f395be2;hp=e956dd659394f4eb9c9a3853f214ac67a8ce8f7b;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index e956dd6..8bb52e1 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) := @@ -78,6 +79,18 @@ Section HaskStrongToWeak. 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 @@ -94,32 +107,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 +145,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 @@ -142,8 +156,8 @@ Section HaskStrongToWeak. | 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 @@ -156,7 +170,7 @@ Section HaskStrongToWeak. ; bind tbranches' = @typeToWeakType Γ _ tbranches ite ; bind escrut' = exprToWeakExpr χ escrut ite ; bind branches' = - ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & 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 [] @@ -170,7 +184,7 @@ 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 sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] | T_Branch b1 b2 => bind b1' = caseBranches b1 @@ -181,12 +195,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' @@ -206,7 +220,7 @@ 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 " +++ toString v)) exp ite with