thread wired-in names of GHC.HetMet.Private.* through to Coq code
[ghc-hetmet.git] / compiler / deSugar / Desugar.lhs
index 603c858..4276414 100644 (file)
@@ -92,7 +92,26 @@ deSugar hsc_env
               <- case target of
                   HscNothing ->
                        return (emptyMessages,
-                               Just ([], nilOL, [], [], NoStubs, hpcInfo, emptyModBreaks, undefined, undefined))
+                               Just ([], nilOL, [], [], NoStubs, hpcInfo, emptyModBreaks, undefined, undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                                    , undefined
+                               ))
                    _        -> do
                      (binds_cvr,ds_hpc_info, modBreaks)
                         <- if (opt_Hpc
@@ -110,6 +129,24 @@ deSugar hsc_env
                           ; ds_vects <- mapM dsVect vects
                           ; hetmet_brak <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_brak_name else return undefined
                           ; hetmet_esc  <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_esc_name  else return undefined
+                          ; hetmet_PGArrow <- if dopt Opt_F_coqpass dflags then dsLookupTyCon hetmet_PGArrow_name else return undefined
+                          ; hetmet_pga_id <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_id_name else return undefined
+                          ; hetmet_pga_comp <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_comp_name else return undefined
+                          ; hetmet_pga_first <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_first_name else return undefined
+                          ; hetmet_pga_second <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_second_name else return undefined
+                          ; hetmet_pga_cancell <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_cancell_name else return undefined
+                          ; hetmet_pga_cancelr <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_cancelr_name else return undefined
+                          ; hetmet_pga_uncancell <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_uncancell_name else return undefined
+                          ; hetmet_pga_uncancelr <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_uncancelr_name else return undefined
+                          ; hetmet_pga_assoc <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_assoc_name else return undefined
+                          ; hetmet_pga_unassoc <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_unassoc_name else return undefined
+                          ; hetmet_pga_copy <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_copy_name else return undefined
+                          ; hetmet_pga_drop <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_drop_name else return undefined
+                          ; hetmet_pga_swap <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_swap_name else return undefined
+                          ; hetmet_pga_applyl <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_applyl_name else return undefined
+                          ; hetmet_pga_applyr <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_applyr_name else return undefined
+                          ; hetmet_pga_curryl <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_curryl_name else return undefined
+                          ; hetmet_pga_curryr <- if dopt Opt_F_coqpass dflags then dsLookupGlobalId hetmet_pga_curryr_name else return undefined
                           ; let hpc_init
                                   | opt_Hpc   = hpcInitCode mod ds_hpc_info
                                   | otherwise = empty
@@ -117,11 +154,48 @@ deSugar hsc_env
                                    , foreign_prs `appOL` core_prs `appOL` spec_prs
                                    , spec_rules ++ ds_rules, ds_vects
                                    , ds_fords `appendStubC` hpc_init
-                                   , ds_hpc_info, modBreaks, hetmet_brak, hetmet_esc) }
+                                   , ds_hpc_info, modBreaks, hetmet_brak, hetmet_esc
+                                   , hetmet_PGArrow
+                                   , hetmet_pga_id
+                                   , hetmet_pga_comp
+                                   , hetmet_pga_first
+                                   , hetmet_pga_second
+                                   , hetmet_pga_cancell
+                                   , hetmet_pga_cancelr
+                                   , hetmet_pga_uncancell
+                                   , hetmet_pga_uncancelr
+                                   , hetmet_pga_assoc
+                                   , hetmet_pga_unassoc
+                                   , hetmet_pga_copy
+                                   , hetmet_pga_drop
+                                   , hetmet_pga_swap
+                                   , hetmet_pga_applyl
+                                   , hetmet_pga_applyr
+                                   , hetmet_pga_curryl
+                                   , hetmet_pga_curryr
+                                   ) }
 
         ; case mb_res of {
            Nothing -> return (msgs, Nothing) ;
-           Just (ds_ev_binds, all_prs, all_rules, ds_vects, ds_fords,ds_hpc_info, modBreaks, hetmet_brak, hetmet_esc) -> do
+           Just (ds_ev_binds, all_prs, all_rules, ds_vects, ds_fords,ds_hpc_info, modBreaks, hetmet_brak, hetmet_esc
+                                   , hetmet_PGArrow
+                                   , hetmet_pga_id
+                                   , hetmet_pga_comp
+                                   , hetmet_pga_first
+                                   , hetmet_pga_second
+                                   , hetmet_pga_cancell
+                                   , hetmet_pga_cancelr
+                                   , hetmet_pga_uncancell
+                                   , hetmet_pga_uncancelr
+                                   , hetmet_pga_assoc
+                                   , hetmet_pga_unassoc
+                                   , hetmet_pga_copy
+                                   , hetmet_pga_drop
+                                   , hetmet_pga_swap
+                                   , hetmet_pga_applyl
+                                   , hetmet_pga_applyr
+                                   , hetmet_pga_curryl
+                                   , hetmet_pga_curryr) -> do
 
        {       -- Add export flags to bindings
          keep_alive <- readIORef keep_var
@@ -146,14 +220,36 @@ deSugar hsc_env
                         -- 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
-
         ; ds_binds' <- if dopt Opt_F_coqpass dflags
                        then do { us <- mkSplitUniqSupply '~'
-                               ; return $ coqPassCoreToCore hetmet_brak hetmet_esc us ds_binds
+                               ; return (coqPassCoreToCore
+                                             hetmet_brak
+                                             hetmet_esc
+                                             us
+                                             ds_binds
+                                             hetmet_PGArrow
+                                             hetmet_pga_id
+                                             hetmet_pga_comp
+                                             hetmet_pga_first
+                                             hetmet_pga_second
+                                             hetmet_pga_cancell
+                                             hetmet_pga_cancelr
+                                             hetmet_pga_uncancell
+                                             hetmet_pga_uncancelr
+                                             hetmet_pga_assoc
+                                             hetmet_pga_unassoc
+                                             hetmet_pga_copy
+                                             hetmet_pga_drop
+                                             hetmet_pga_swap
+                                             hetmet_pga_applyl
+                                             hetmet_pga_applyr
+                                             hetmet_pga_curryl
+                                             hetmet_pga_curryr)
                                }
                        else return ds_binds
 
+        ; dumpIfSet_dyn dflags Opt_D_coqpass "Coq Pass Output" $ text $ coqPassCoreToString ds_binds'
+
         ; dumpIfSet_dyn dflags Opt_D_dump_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
 
        ; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps