From 35d3a59796735e5341389fa6a145f62dcea9c3fc Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 9 May 2011 14:10:56 -0700 Subject: [PATCH] add support for hetmet_unflatten --- src/ExtractionMain.v | 8 +++++++- src/HaskFlattener.v | 8 ++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index ebf4e77..ea89cf4 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -167,6 +167,7 @@ Section core2proof. Context (hetmet_brak : WeakExprVar). Context (hetmet_esc : WeakExprVar). Context (hetmet_flatten : WeakExprVar). + Context (hetmet_unflatten : WeakExprVar). Context (hetmet_flattened_id : WeakExprVar). Context (uniqueSupply : UniqSupply). @@ -273,6 +274,7 @@ Section core2proof. (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) (hetmet_flattened_id : CoreVar) (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) @@ -396,6 +398,7 @@ Section core2proof. Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak. Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc. Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten. + Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten. Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id. Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := @@ -411,7 +414,8 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (let haskProof := flatten_proof hetmet_flatten' hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e) + (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten' + hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e) in (* insert HaskProof-to-HaskProof manipulations here *) OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) >>= fun e' => @@ -454,6 +458,7 @@ Section core2proof. (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) (hetmet_flattened_id : CoreVar) (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) @@ -479,6 +484,7 @@ Section core2proof. hetmet_brak hetmet_esc hetmet_flatten + hetmet_unflatten hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 5e16f56..e8aceb1 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -199,6 +199,7 @@ Section HaskFlattener. Set Printing Width 130. Context (hetmet_flatten : WeakExprVar). + Context (hetmet_unflatten : WeakExprVar). Context (hetmet_id : WeakExprVar). Context {unitTy : forall TV, RawHaskType TV ★ }. Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. @@ -914,6 +915,13 @@ Section HaskFlattener. apply nd_rule. apply q. apply INil. + destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)). + set (garrowfy_code_types (g wev)) as t. + set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q. + simpl in q. + apply nd_rule. + apply q. + apply INil. apply nd_rule; rewrite globals_do_not_have_code_types. apply RGlobal. apply (Prelude_error "found RGlobal at depth >0"). -- 1.7.10.4