From: Adam Megacz Date: Wed, 16 Mar 2011 08:54:16 +0000 (-0700) Subject: major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=f7a6e08c97cae1c1b278c18a1904eadec4e5f010 major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial --- diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index b144116..3dec80f 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -1,11 +1,14 @@ {-# OPTIONS_GHC -fno-warn-unused-binds #-} module CoqPass ( coqPassCoreToString, coqPassCoreToCore ) where +import qualified Unique +import qualified UniqSupply import qualified MkCore import qualified TysWiredIn import qualified TysPrim import qualified Outputable import qualified PrelNames +import qualified OccName import qualified Name import qualified Literal import qualified Type @@ -82,6 +85,11 @@ sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x) sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x) sanitizeForLatex (c:x) = c:(sanitizeForLatex x) +kindToCoreKind :: Kind -> TypeRep.Kind +kindToCoreKind KindStar = TypeRep.liftedTypeKind +kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) +kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that" + coreKindToKind :: TypeRep.Kind -> Kind coreKindToKind k = case Coercion.splitKindFunTy_maybe k of diff --git a/src/Extraction.v b/src/Extraction.v index 53b1185..66a69da 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -25,7 +25,7 @@ Require Import HaskProof. Require Import HaskCoreToWeak. Require Import HaskWeakToStrong. Require Import HaskStrongToProof. -Require Import HaskProofToStrong. +(*Require Import HaskProofToStrong.*) Require Import HaskProofToLatex. Require Import HaskStrongToWeak. Require Import HaskWeakToCore. @@ -58,6 +58,17 @@ Extract Constant shift => "shiftAscii". Unset Extraction Optimize. Unset Extraction AutoInline. + +Variable Name : Type. Extract Inlined Constant Name => "Name.Name". +Variable mkSystemName : Unique -> string -> nat -> Name. + Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))". +Variable mkTyVar : Name -> Kind -> CoreVar. + Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))". +Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. + Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))". +Variable mkExVar : Name -> CoreType -> CoreVar. + Extract Inlined Constant mkExVar => "Id.mkLocalId". + Section core2proof. Context (ce:@CoreExpr CoreVar). @@ -84,6 +95,9 @@ Section core2proof. | WCoerVar _ => Prelude_error "top-level xi got a coercion variable" end. + + (* core-to-string (-dcoqpass) *) + Definition header : string := "\documentclass[9pt]{article}"+++eol+++ "\usepackage{amsmath}"+++eol+++ @@ -102,7 +116,7 @@ Section core2proof. eol+++"\end{document}"+++ eol. - Definition handleExpr' (ce:@CoreExpr CoreVar) : ???string := + Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := addErrorMessage ("input CoreSyn: " +++ ce) (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( coreExprToWeakExpr ce >>= fun we => @@ -112,29 +126,90 @@ Section core2proof. (addErrorMessage ("WeakType: " +++ t) ((weakTypeToTypeOfKind φ t ★) >>= fun τ => addErrorMessage ("HaskType: " +++ τ) - ((weakExprToStrongExpr Γ Δ φ ψ ξ τ nil we) >>= fun e => + ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol) )))))))). - Definition handleExpr (ce:@CoreExpr CoreVar) : string := - match handleExpr' ce with + Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string := + match coreToStringExpr' ce with | OK x => x | Error s => Prelude_error s end. - Definition handleBind (bind:@CoreBind CoreVar) : string := - match bind with - | CoreNonRec _ e => handleExpr e - | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) "" + Definition coreToStringBind (binds:@CoreBind CoreVar) : string := + match binds with + | CoreNonRec _ e => coreToStringExpr e + | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) "" end. Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string := header +++ - (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "") + (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "") +++ footer. - Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := - lbinds. + + (* core-to-core (-fcoqpass) *) + Section CoreToCore. + + Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar := + weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k. + Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar := + weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2. + Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar := + weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t. + + Context (hetmet_brak : WeakExprVar). + Context (hetmet_esc : WeakExprVar). + Context (uniqueSupply : UniqSupply). + + Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := + addErrorMessage ("input CoreSyn: " +++ ce) + (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( + coreExprToWeakExpr ce >>= fun we => + addErrorMessage ("WeakExpr: " +++ we) + ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we)) + ((weakTypeOfWeakExpr we) >>= fun t => + (addErrorMessage ("WeakType: " +++ t) + ((weakTypeToTypeOfKind φ t ★) >>= fun τ => + + ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => + (* insert HaskStrong-to-HaskStrong manipulations here *) + strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil + >>= fun q => OK (weakExprToCoreExpr q) +(* + OK (weakExprToCoreExpr we) +*) + )))))))). + + Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) := + match coreToCoreExpr' ce with + | OK x => x + | Error s => Prelude_error s + end. + + Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar := + match binds with + | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e) + | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe) + end. + + Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := + map coreToCoreBind lbinds. + + End CoreToCore. + + Definition coqPassCoreToCore + (hetmet_brak : CoreVar) + (hetmet_esc : CoreVar) + (uniqueSupply : UniqSupply) + (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := + match coreVarToWeakVar hetmet_brak with + | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with + | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds + | _ => Prelude_error "IMPOSSIBLE" + end + | _ => Prelude_error "IMPOSSIBLE" + end. End core2proof. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index b4b0caa..e86e544 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -14,136 +14,234 @@ Require Import HaskLiteralsAndTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. +Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. -Require Import HaskCoreVars. - -Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ) - : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) := - match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) * - (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with - | nil => (f,(vec_nil,ite)) - | k::lk' => - let (f',varsite') := mfresh f lk' ite - in let (vars,ite') := varsite' - in let (v,f'') := next _ _ f' k - in (f'',((v:::vars),v::::ite')) - end. -Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) - {struct rht} : WeakType := -match rht with - | TVar _ v => WTyVarTy v - | TCon tc => WTyCon tc - | TCoerc _ t1 t2 t3 => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3) - | TArrow => WFunTyCon - | TApp _ _ t1 t2 => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) - | TAll k rht' => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv)) - | TCode t1 t2 => - match (rawHaskTypeToWeakType f t1) with - | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2) - | impossible => impossible (* TODO: find a way to convince Coq this can't happen *) - end - | TyFunApp tfc tls => WTyFunApp tfc (rawHaskTypeListToWeakType f tls) -end -with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) := -match rht with - | TyFunApp_nil => nil - | TyFunApp_cons κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl') -end. - -Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)) - {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType := - rawHaskTypeToWeakType f (τ _ φ). - -(* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's - * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *) -(* -Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH} - {Γ}{Δ}{ξ}{lev}(exp:@Expr VV eqVV Γ Δ ξ lev) : { ξ' : HH -> LeveledHaskType Γ & @Expr HH eqHH Γ Δ ξ' lev }. - Defined. - *) - -Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) - := tv::::ite. - -Definition coercionToWeakCoercion Γ Δ κ t1 t2 ftv ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)) : WeakCoercion := - WCoUnsafe (@typeToWeakType ftv Γ κ t1 ite) (@typeToWeakType ftv Γ κ t2 ite). - -Section strongExprToWeakExpr. +(* Uniques *) +Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply". +Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique". +Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply". +Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply. + Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply". + +Inductive UniqM {T:Type} : Type := + | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM. + Implicit Arguments UniqM [ ]. + +Instance UniqMonad : Monad UniqM := +{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x)) +; bindM := fun a b (x:UniqM a) (f:a->UniqM b) => + uniqM (fun u => + match x with + | uniqM fa => + match fa u with + | Error s => Error s + | OK (u',va) => match f va with + | uniqM fb => fb u' + end + end + end) +}. + +Definition getU : UniqM Unique := + uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))). + +Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity). +Notation "'return' x" := (returnM x) (at level 100). +Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100). + +Section HaskStrongToWeak. Context (hetmet_brak : WeakExprVar). Context (hetmet_esc : WeakExprVar). - Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ} - (ftv:Fresh Kind (fun _ => WeakTypeVar)) - (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) - (fev:Fresh WeakType (fun _ => WeakExprVar)) - (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ) - : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr := - match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with - | EVar Γ' _ ξ' ev => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★ (unlev (ξ' ev)) ite)) - | ELit _ _ _ lit _ => fun ite => WELit lit - | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite) - | ELam Γ' _ _ _ t _ cv e => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e ite) - | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite) - | EEsc Γ' _ _ ec t _ e => fun ite => WEEsc hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite) - | EBrak Γ' _ _ ec t _ e => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite) - | ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv fev e ite) - | ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv τ ite) - | ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv fev elrb ite)(strongExprToWeakExpr ftv fcv fev e ite) - | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv fev e ite) - (coercionToWeakCoercion _ _ _ _ _ ftv ite γ) - | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite) - (coercionToWeakCoercion _ _ _ _ _ ftv ite γ) - | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite => - let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in - WECase - ev - (strongExprToWeakExpr ftv fcv fev' e ite) - (@typeToWeakType ftv Γ _ tbranches ite) - tc - (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes)) - ((fix caseBranches - (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) - (update_ξ (weakLT'○ξ) (vec2list (vec_map - (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb)))) - (weakLT' (tbranches@@l)) }) - : Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) := - match tree with - | T_Leaf None => [] - | T_Leaf (Some x) => let (scb,e) := x in - let (ftv',evarsite') := mfresh ftv _ ite in - let fcv' := fcv in - let (evars,ite') := evarsite' in - [(sac_altcon scb, - vec2list evars, - nil (*FIXME*), - map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)), - strongExprToWeakExpr ftv' fcv' fev' e ite' - )] - | T_Branch b1 b2 => (caseBranches b1),,(caseBranches b2) - end - ) alts) - | ETyLam _ _ _ k _ _ e => fun ite => - let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv fev e (updateITE tv ite)) - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => - let t1' := typeToWeakType ftv σ₁ ite in - let t2' := typeToWeakType ftv σ₂ ite in - let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' fev e ite) + Context (mkWeakTypeVar_ : Unique -> Kind -> WeakTypeVar). + Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar). + Context (mkWeakExprVar_ : Unique -> WeakType -> WeakExprVar). + + Definition mkWeakTypeVar (k:Kind) : UniqM WeakTypeVar := bind u = getU ; return mkWeakTypeVar_ u k. + Definition mkWeakCoerVar (k:Kind)(t1 t2:WeakType) : UniqM WeakCoerVar := bind u = getU ; return mkWeakCoerVar_ u k t1 t2. + Definition mkWeakExprVar (t:WeakType) : UniqM WeakExprVar := bind u = getU ; return mkWeakExprVar_ u t. + + Fixpoint mfresh (lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ) + : UniqM (((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ)))) := + match lk as LK return UniqM ((vec WeakTypeVar (length LK)) * (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with + | nil => return (vec_nil,ite) + | k::lk' => bind v = mkWeakTypeVar k + ; bind vars_ite' = mfresh lk' ite + ; return ((v:::(fst vars_ite')),v::::(snd vars_ite')) + end. + + Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType := + match rht with + | TVar _ v => return WTyVarTy v + | TCon tc => return WTyCon tc + | TCoerc _ t1 t2 t3 => bind t1' = rawHaskTypeToWeakType t1 + ; bind t2' = rawHaskTypeToWeakType t2 + ; bind t3' = rawHaskTypeToWeakType t3 + ; return WCoFunTy t1' t2' t3' + | TArrow => return WFunTyCon + | TApp _ _ t1 t2 => bind t1' = rawHaskTypeToWeakType t1 + ; bind t2' = rawHaskTypeToWeakType t2 + ; return WAppTy t1' t2' + | TAll k rht' => bind tv = mkWeakTypeVar k + ; bind t' = rawHaskTypeToWeakType (rht' tv) + ; return WForAllTy tv t' + | TCode t1 t2 => bind t1' = rawHaskTypeToWeakType t1 + ; bind t2' = rawHaskTypeToWeakType t2 + ; match t1' with + | WTyVarTy ec => return WCodeTy ec t2' + | _ => failM "impossible" + end + | TyFunApp tfc tls => bind tls' = rawHaskTypeListToWeakType tls + ; return WTyFunApp tfc tls' end - with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars} - (ftv:Fresh Kind (fun _ => WeakTypeVar)) - (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) - (fev:Fresh WeakType (fun _ => WeakExprVar)) - (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars) - : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) := - match elrb as E in ELetRecBindings G D X L V - return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with - | ELR_nil _ _ _ _ => fun ite => [] - | ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))] - | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite) + with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) := + match rht with + | TyFunApp_nil => return nil + | TyFunApp_cons κ kl rht' rhtl' => bind t = rawHaskTypeToWeakType rht' + ; bind tl = rawHaskTypeListToWeakType rhtl' + ; return t::tl + end. + + Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType := + rawHaskTypeToWeakType (τ _ φ). + + Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) + := tv::::ite. + + Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)) + : UniqM WeakCoercion + := bind t1' = @typeToWeakType Γ κ t1 ite + ; bind t2' = @typeToWeakType Γ κ t2 ite + ; return WCoUnsafe t1' t2'. + + Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) := + match l with + | nil => return nil + | x::y => bind x' = x + ; bind y' = seqM y + ; return x'::y' + end. + + Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}. + + Definition update_χ (χ: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 := + match varsexprs with + | nil => χ + | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev + end. + + Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ) + : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ + -> 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 + | EGlobal Γ' _ ξ' t wev => fun ite => return WEVar wev + | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite + ; bind ev' = mkWeakExprVar tv' + ; bind e' = exprToWeakExpr (update_χ χ 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 + ; return WELet ev' e1' e2' + | ELit _ _ _ lit _ => fun ite => return WELit lit + | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite + ; bind e2' = exprToWeakExpr χ e2 ite + ; return WEApp e1' e2' + | EEsc Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite + ; bind e' = exprToWeakExpr χ e ite + ; return WEEsc hetmet_esc (ec _ ite) e' t' + | 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 + ; return WENote n e' + | ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite + ; bind e' = exprToWeakExpr χ e ite + ; return WETyApp e' t' + | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => bind e' = exprToWeakExpr χ e ite + ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ + ; return WECoApp e' c' + | 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) + ; return WETyLam tv e' + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite + ; bind t2' = typeToWeakType σ₂ ite + ; bind cv = mkWeakCoerVar κ t1' t2' + ; bind e' = exprToWeakExpr χ e ite + ; return WECoLam cv e' + | ECase Γ Δ ξ l tc tbranches atypes escrut alts => + fun ite => bind tscrut' = typeToWeakType (caseType tc atypes) ite + ; bind vscrut' = mkWeakExprVar tscrut' + ; bind tbranches' = @typeToWeakType Γ _ tbranches ite + ; bind escrut' = exprToWeakExpr χ escrut ite + ; bind branches' = + ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & 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 + let varstypes := vec2list (scbwv_varstypes scb) in + bind evars_ite = mfresh _ ite + ; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★ + => bind tleaf = typeToWeakType (snd vt) (snd evars_ite) + ; bind v' = mkWeakExprVar tleaf + ; return ((fst vt),v')) + varstypes) + ; let χ' := update_χ' χ exprvars in + bind e'' = exprToWeakExpr χ' e (snd evars_ite) + ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] + | T_Branch b1 b2 => bind b1' = caseBranches b1 + ; bind b2' = caseBranches b2 + ; return (b1',,b2') + end) alts) + ; bind tys = seqM (ilist_to_list (@ilmap _ _ + (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 _ ★ + => bind tleaf = typeToWeakType (snd vt) ite + ; bind v' = mkWeakExprVar tleaf + ; return ((fst vt),v')) + (leaves vars)) + ; let χ' := update_χ' χ vars' in + bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite + ; bind e' = exprToWeakExpr χ' e ite + ; return WELetRec elrb' e' + end + with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars) + : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) := + 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 + ; bind e' = exprToWeakExpr χ e ite + ; bind v' = match χ v with Error s => failM s | OK y => return y end + ; return [(v',e')] + | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite + ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite + ; return b1',,b2' end. -End strongExprToWeakExpr. + + + Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ) + (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) + : ???WeakExpr := + match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with + uniqM f => f us >>= fun x => OK (snd x) + end. + +End HaskStrongToWeak. \ No newline at end of file diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 2593a5c..38a4304 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,6 +19,9 @@ Require Import HaskStrongTypes. 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 Γ Δ). @@ -454,12 +457,23 @@ match lk as LK return ???(IList Kind (HaskType Γ) LK) with end end. +Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool := + match vars with + | nil => ig + | v::vars' => + fun v' => + if eqd_dec v v' + then false + else update_ig ig vars' v' + end. + Definition weakExprToStrongExpr : forall (Γ:TypeEnv) (Δ:CoercionEnv Γ) (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ), WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ). @@ -470,13 +484,16 @@ Definition weakExprToStrongExpr : forall (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ) (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := addErrorMessage ("in weakExprToStrongExpr " +++ we) match we with - | WEVar v => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) + | WEVar v => if ig v + then OK (EGlobal Γ Δ ξ (τ@@lev) v) + else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev) @@ -484,53 +501,53 @@ Definition weakExprToStrongExpr : forall weakTypeOfWeakExpr ebody >>= fun tbody => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in - weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' => + 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') | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => - weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' => castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e') | WEEsc _ ec e tbody => φ ec >>= fun ec'' => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => match lev with | nil => Error "ill-leveled escapification" - | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e + | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e') end | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage" - | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => - weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody + weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) + (update_ig ig ((v:CoreVar)::nil)) τ lev ebody >>= fun ebody' => OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 => weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => - weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' => - weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' => OK (EApp _ _ _ _ _ _ e1' e2') | WETyLam tv e => let φ' := upφ tv φ in weakTypeOfWeakExpr e >>= fun te => weakTypeToTypeOfKind φ' te ★ >>= fun τ' => weakExprToStrongExpr _ (weakCE Δ) φ' - (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e - >>= fun e' => - castExpr we "WETyLam1" _ e' >>= fun e'' => - castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'') + (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e + >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e') | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with | WForAllTy wtv te' => let φ' := upφ wtv φ in weakTypeToTypeOfKind φ' te' ★ >>= fun te'' => - weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' => + 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) @@ -544,7 +561,7 @@ Definition weakExprToStrongExpr : forall haskTypeOfSomeKind κ t1'' => weakTypeToTypeOfKind φ t2 κ >>= fun t2'' => weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' => - weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => castExpr we "WECoApp" _ e' >>= fun e'' => OK (ECoApp Γ Δ κ t1'' t2'' (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'') @@ -557,37 +574,43 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ te ★ >>= fun te' => weakTypeToTypeOfKind φ t1 cv >>= fun t1' => weakTypeToTypeOfKind φ t2 cv >>= fun t2' => - weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' => + weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' => castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') | WECast e co => let (t1,t2) := weakCoercionTypes co in weakTypeToTypeOfKind φ t1 ★ >>= fun t1' => weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => - weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' => castExpr we "WECast" _ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => - let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) - in let binds := + let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ 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)) : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) := match t with | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _) - | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e) + | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e) | T_Branch b1 b2 => binds b1 >>= fun b1' => binds b2 >>= fun b2' => OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2') end) rb in binds >>= fun binds' => - weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' => + weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' => OK (ELetRec Γ Δ ξ lev τ _ binds' e') - | WECase vscrut ve tbranches tc avars alts => - weakTypeToTypeOfKind φ (vscrut:WeakType) ★ >>= fun tv => - weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' => - let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in + | 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' => weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree @@ -602,19 +625,25 @@ Definition weakExprToStrongExpr : forall let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => + (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 => mkTree b1 >>= fun b1' => mkTree b2 >>= fun b2' => OK (b1',,b2') end) alts >>= fun tree => - castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut => - castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree) - >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase') - - + 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)). destruct case_some.