X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2FdeSugar%2FDesugar.lhs;h=b2131ca4f2a2cf6d2cbf6dfd6f59aa5e7458e974;hp=374c13b6260cb952872408cf0f9a0834a2ca0699;hb=b2524b3960999fffdb3767900f58825903f6560f;hpb=095c02ee7fbadae65d65a78f558147365190c636

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index 374c13b..b2131ca 100644
--- a/compiler/deSugar/Desugar.lhs
+++ b/compiler/deSugar/Desugar.lhs
@@ -246,16 +246,24 @@ 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
+                               ; let do_skolemize = dopt Opt_F_skolemize dflags
                                ; return (coqPassCoreToCore
+                                             do_flatten
+                                             do_skolemize
                                              hetmet_brak
                                              hetmet_esc
                                              hetmet_flatten
                                              hetmet_unflatten
                                              hetmet_flattened_id
                                              us
-                                             final_pgm
+                                             final_pgm'
                                              hetmet_PGArrow
                                              hetmet_PGArrow_unit
                                              hetmet_PGArrow_tensor
@@ -280,13 +288,15 @@ 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
 
-        ; dumpIfSet_dyn dflags Opt_D_coqpass "Coq Pass Output" $ text $ coqPassCoreToString ds_binds'
+        ; dumpIfSet_dyn dflags Opt_D_dump_proofs "Coq Pass Output" $ text $ coqPassCoreToString ds_binds'
 
-        ; dumpIfSet_dyn dflags Opt_D_dump_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
+        ; dumpIfSet_dyn dflags Opt_D_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
 
 	; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps
 
@@ -525,6 +535,8 @@ switching off EnableRewriteRules.  See DsExpr.dsExplicitList.
 
 That keeps the desugaring of list comprehensions simple too.
 
+
+
 Nor do we want to warn of conversion identities on the LHS;
 the rule is precisly to optimise them:
   {-# RULES "fromRational/id" fromRational = id :: Rational -> Rational #-}
@@ -582,4 +594,4 @@ simplifyBind (Rec (rbs@((b,e):rbs'))) =
     else (NonRec b (simplify e)):(simplifyBind $ Rec rbs')
 
 simplifyBinds = concatMap simplifyBind
-\end{code}
\ No newline at end of file
+\end{code}