add -fsimpleopt-before-flatten

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index f219c01..0e7c032 100644 (file)
--- 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 (submodule)
--- 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 (file)
--- 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 }))