From a663de9a349ffe83a6c4fc10f1259f2fa6a915ed Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 29 May 2011 17:01:32 -0700 Subject: [PATCH] add -fflatten and -funsafe-skolemize flags --- examples/Demo.hs | 2 +- examples/Makefile | 2 +- src/ExtractionMain.v | 53 ++++++++++++++++++++++++++++++++++++++------------ src/HaskFlattener.v | 11 +++++++++-- 4 files changed, 52 insertions(+), 16 deletions(-) diff --git a/examples/Demo.hs b/examples/Demo.hs index 4c53aa5..6d0e69d 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XModalTypes -fcoqpass -dcore-lint #-} +{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint #-} module Demo (demo) where diff --git a/examples/Makefile b/examples/Makefile index c89fb10..17d92e8 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -4,7 +4,7 @@ open: make demo open .build/test.pdf -all: +sanity: ../../../inplace/bin/ghc-stage2 -dcore-lint -fforce-recomp -fcoqpass -ddump-coqpass -ddump-to-file \ `ls *.hs | grep -v Regex | grep -v Unify.hs | grep -v GArrowTikZ.hs ` +RTS -K500M ../../../inplace/bin/ghc-stage2 -dcore-lint -fforce-recomp \ diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index df7896b..4926bff 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -275,6 +275,8 @@ Section core2proof. Section coqPassCoreToCore. Context + (do_flatten : bool) + (do_skolemize : bool) (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) (hetmet_flatten : CoreVar) @@ -432,18 +434,41 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten' - hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e) - in (* insert HaskProof-to-HaskProof manipulations here *) - OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) - >>= fun e' => - (snd e') >>= fun e'' => - strongExprToWeakExpr hetmet_brak' hetmet_esc' - mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply - (projT2 e'') INil - >>= fun q => - OK (weakExprToCoreExpr q) - )))))))))). + (if do_skolemize + then + (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten' + hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e) + in (* insert HaskProof-to-HaskProof manipulations here *) + OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ + (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak' hetmet_esc' + mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => OK (weakExprToCoreExpr q)) + else (if do_flatten + then + (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 _ _ τ nil _ + (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak' hetmet_esc' + mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => OK (weakExprToCoreExpr q)) + else + (let haskProof := @expr2proof _ _ _ _ _ _ _ e + in (* insert HaskProof-to-HaskProof manipulations here *) + OK ((@proof2expr nat _ FreshNat _ _ τ nil _ + (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak' hetmet_esc' + mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => OK (weakExprToCoreExpr q)))) + ))))))))). Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) := match coreToCoreExpr' ce with @@ -473,6 +498,8 @@ Section core2proof. End coqPassCoreToCore. Definition coqPassCoreToCore + (do_flatten : bool) + (do_skolemize : bool) (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) (hetmet_flatten : CoreVar) @@ -502,6 +529,8 @@ Section core2proof. (hetmet_pga_curryl : CoreVar) (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) := coqPassCoreToCore' + do_flatten + do_skolemize hetmet_brak hetmet_esc hetmet_flatten diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index c5587c1..d805de4 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -799,7 +799,7 @@ Section HaskFlattener. reflexivity. Qed. - Definition flatten_proof : + Definition flatten_skolemized_proof : forall {h}{c}, ND SRule h c -> ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). @@ -1315,6 +1315,13 @@ Section HaskFlattener. apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). Defined. + Definition flatten_proof : + forall {h}{c}, + ND Rule h c -> + ND Rule h c. + apply (Prelude_error "sorry, non-skolemized flattening isn't implemented"). + Defined. + Definition skolemize_and_flatten_proof : forall {h}{c}, ND Rule h c -> @@ -1324,7 +1331,7 @@ Section HaskFlattener. intros. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. - apply flatten_proof. + apply flatten_skolemized_proof. apply skolemize_proof. apply X. Defined. -- 1.7.10.4