; 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
-- 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
| 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_dump_coqpass -- dumps the output of the core-to-core coqPass
| Opt_WarnIsError -- -Werror; makes warnings fatal
| Opt_WarnDuplicateExports
, 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 "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 ---------------------------