Require Import HaskCoreToWeak.
Require Import HaskWeakToStrong.
Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
+(*Require Import HaskProofToStrong.*)
Require Import HaskProofToLatex.
Require Import HaskStrongToWeak.
Require Import HaskWeakToCore.
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).
| 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+++
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 =>
(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.
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
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 Γ Δ).
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) ).
(φ: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)
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)
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'')
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
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.
projects / coq-hetmet.git / commitdiff