add -fflatten and -funsafe-skolemize flags

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index 374c13b..f219c01 100644 (file)
--- a/compiler/deSugar/Desugar.lhs
+++ b/compiler/deSugar/Desugar.lhs
@@ -248,7 +248,11 @@ deSugar hsc_env
 
         ; ds_binds <- if dopt Opt_F_coqpass dflags
                        then do { us <- mkSplitUniqSupply '~'
 
         ; 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
                                ; return (coqPassCoreToCore

+                                             do_flatten
+                                             do_skolemize

                                              hetmet_brak
                                              hetmet_esc
                                              hetmet_flatten
                                              hetmet_brak
                                              hetmet_esc
                                              hetmet_flatten

@@ -284,9 +288,9 @@ deSugar hsc_env
                         -- The simpleOptPgm gets rid of type 
                         -- bindings plus any stupid dead code
 
                         -- 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
 
 
        ; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps
 

diff --git a/compiler/hetmet b/compiler/hetmet
index a45824c..a663de9 160000 (submodule)
--- a/compiler/hetmet
+++ b/compiler/hetmet
@@ -1 +1 @@
-Subproject commit a45824c7d03fcf797e22d2919187a7e97fb567cc
+Subproject commit a663de9a349ffe83a6c4fc10f1259f2fa6a915ed

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index e292722..6ff7924 100644 (file)
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -190,9 +190,11 @@ data DynFlag
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
 
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
 

-   | Opt_F_coqpass                      -- run the core-to-core   coqPass (does whatever CoqPass.hs says)
+   | 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_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
    | Opt_D_coqpass                      -- run the core-to-string coqPass and dumps the result

-   | Opt_D_dump_coqpass                 -- dumps the output of the core-to-core coqPass

 
    | Opt_WarnIsError                    -- -Werror; makes warnings fatal
    | Opt_WarnDuplicateExports
 
    | Opt_WarnIsError                    -- -Werror; makes warnings fatal
    | Opt_WarnDuplicateExports

@@ -1334,9 +1336,11 @@ dynamic_flags = [
   , Flag "dfaststring-stats"       (NoArg (setDynFlag Opt_D_faststring_stats))
 
         ------ Coq-in-GHC ---------------------------
   , Flag "dfaststring-stats"       (NoArg (setDynFlag Opt_D_faststring_stats))
 
         ------ Coq-in-GHC ---------------------------

-  , Flag "dcoqpass"                (NoArg (setDynFlag Opt_D_coqpass))
-  , Flag "ddump-coqpass"           (NoArg (setDynFlag Opt_D_dump_coqpass))
+  , 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 "fcoqpass"                (NoArg (setDynFlag Opt_F_coqpass))

+  , 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 }))

 
         ------ Machine dependant (-m<blah>) stuff ---------------------------
 
 
         ------ Machine dependant (-m<blah>) stuff ---------------------------
 

diff --git a/libraries/base b/libraries/base
index b64a0d3..696df0c 160000 (submodule)
--- a/libraries/base
+++ b/libraries/base
@@ -1 +1 @@
-Subproject commit b64a0d3816bd3f2586a2544f99e9b42d9a24e7ee
+Subproject commit 696df0cbdfe203a618c325e25c2ed60408ee54b9