From 16b9e80dc14db24509f051f294b5b51943285090 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 30 May 2011 17:41:34 -0700 Subject: [PATCH] add -fsimpleopt-before-flatten --- compiler/deSugar/Desugar.lhs | 10 ++++++++-- compiler/hetmet | 2 +- compiler/main/DynFlags.hs | 2 ++ 3 files changed, 11 insertions(+), 3 deletions(-) diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs index f219c01..0e7c032 100644 --- a/compiler/deSugar/Desugar.lhs +++ b/compiler/deSugar/Desugar.lhs @@ -246,6 +246,10 @@ deSugar hsc_env (vcat [ pprCoreBindings final_pgm , pprRules rules_for_imps ]) + ; (final_pgm', rules_for_imps') <- if dopt Opt_F_simpleopt_before_flatten dflags + then simpleOptPgm dflags final_pgm rules_for_imps + else return (final_pgm, rules_for_imps) + ; ds_binds <- if dopt Opt_F_coqpass dflags then do { us <- mkSplitUniqSupply '~' ; let do_flatten = dopt Opt_F_flatten dflags @@ -259,7 +263,7 @@ deSugar hsc_env hetmet_unflatten hetmet_flattened_id us - final_pgm + final_pgm' hetmet_PGArrow hetmet_PGArrow_unit hetmet_PGArrow_tensor @@ -284,7 +288,9 @@ deSugar hsc_env } else return final_pgm - ; (ds_binds', ds_rules_for_imps) <- simpleOptPgm dflags ds_binds rules_for_imps + ; (ds_binds', ds_rules_for_imps) <- if dopt Opt_F_simpleopt_before_flatten dflags + then return (ds_binds, rules_for_imps') + else simpleOptPgm dflags ds_binds rules_for_imps' -- The simpleOptPgm gets rid of type -- bindings plus any stupid dead code diff --git a/compiler/hetmet b/compiler/hetmet index 8064e50..d9117c5 160000 --- a/compiler/hetmet +++ b/compiler/hetmet @@ -1 +1 @@ -Subproject commit 8064e50e47f40228631f8a96ba28cbfb570c76ff +Subproject commit d9117c50c1e7d287651720b5cda988c8821b8d62 diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 6ff7924..6fe6708 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -193,6 +193,7 @@ data DynFlag | Opt_F_coqpass -- run the core-to-core coqPass, but don't change anything (just "parse/unparse") | Opt_F_skolemize -- run the core-to-core coqPass, skolemizing the proof | Opt_F_flatten -- run the core-to-core coqPass, flattening the proof + | Opt_F_simpleopt_before_flatten -- run the "simplPgmOpt" before the coqPass | Opt_D_dump_proofs -- dump natural deduction typing proof of the coqpass input | Opt_D_coqpass -- run the core-to-string coqPass and dumps the result @@ -1339,6 +1340,7 @@ dynamic_flags = [ , Flag "ddump-proofs" (NoArg (setDynFlag Opt_D_dump_proofs)) , Flag "ddump-coqpass" (NoArg (setDynFlag Opt_D_coqpass)) , Flag "fcoqpass" (NoArg (setDynFlag Opt_F_coqpass)) + , Flag "fsimpleopt-before-flatten" (NoArg (setDynFlag Opt_F_simpleopt_before_flatten)) , Flag "fflatten" (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten })) , Flag "funsafe-skolemize" (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten ; setDynFlag Opt_F_skolemize })) -- 1.7.10.4