CoreMonad: add lookupOrigCoreM, modeled after IfaceEnv.lookupOrig
[ghc-hetmet.git] / compiler / deSugar / Desugar.lhs
index 37a3cf9..8ac2819 100644 (file)
@@ -14,10 +14,14 @@ import HscTypes
 import HsSyn
 import TcRnTypes
 import MkIface
+import IfaceEnv
 import Id
+import Pair
 import Name
+import FastString
 import CoreSyn
 import CoreSubst
+import CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 import PprCore
 import DsMonad
 import DsExpr
@@ -40,6 +44,12 @@ import MonadUtils
 import OrdList
 import Data.List
 import Data.IORef
+import PrelNames
+import UniqSupply
+import UniqFM
+import CoreFVs
+import Type
+import Coercion
 \end{code}
 
 %************************************************************************
@@ -49,6 +59,7 @@ import Data.IORef
 %************************************************************************
 
 \begin{code}
+
 -- | Main entry point to the desugarer.
 deSugar :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts)
 -- Can modify PCS by faulting in more declarations
@@ -89,7 +100,7 @@ deSugar hsc_env
               <- case target of
                   HscNothing ->
                        return (emptyMessages,
-                               Just ([], nilOL, [], [], NoStubs, hpcInfo, emptyModBreaks))
+                               Just ([], nilOL, [], [], NoStubs, hpcInfo, emptyModBreaks, undefined))
                    _        -> do
                      (binds_cvr,ds_hpc_info, modBreaks)
                         <- if (opt_Hpc
@@ -98,6 +109,7 @@ deSugar hsc_env
                               then addCoverageTicksToBinds dflags mod mod_loc
                                                            (typeEnvTyCons type_env) binds 
                               else return (binds, hpcInfo, emptyModBreaks)
+
                      initDs hsc_env mod rdr_env type_env $ do
                        do { ds_ev_binds <- dsEvBinds ev_binds
                           ; core_prs <- dsTopLHsBinds auto_scc binds_cvr
@@ -105,6 +117,93 @@ deSugar hsc_env
                           ; (ds_fords, foreign_prs) <- dsForeigns fords
                           ; ds_rules <- mapMaybeM dsRule rules
                           ; ds_vects <- mapM dsVect vects
+                          ; junk <- if dopt Opt_F_coqpass dflags
+                                    then do { hetmet_brak_name <- lookupOrig gHC_HETMET_CODETYPES (mkOccNameFS varName (fsLit "hetmet_brak"))
+                                            ; hetmet_brak <- dsLookupGlobalId hetmet_brak_name
+                                            ; hetmet_esc_name <- lookupOrig gHC_HETMET_CODETYPES (mkOccNameFS varName (fsLit "hetmet_esc"))
+                                            ; hetmet_esc  <- dsLookupGlobalId hetmet_esc_name 
+                                            ; hetmet_flatten_name <- lookupOrig gHC_HETMET_CODETYPES (mkOccNameFS varName (fsLit "hetmet_flatten"))
+                                            ; hetmet_flatten <- dsLookupGlobalId hetmet_flatten_name
+                                            ; hetmet_unflatten_name <- lookupOrig gHC_HETMET_CODETYPES (mkOccNameFS varName (fsLit "pga_unflatten"))
+                                            ; hetmet_unflatten <- dsLookupGlobalId hetmet_unflatten_name
+                                            ; hetmet_flattened_id_name <- lookupOrig gHC_HETMET_CODETYPES (mkOccNameFS varName (fsLit "pga_flattened_id"))
+                                            ; hetmet_flattened_id <- dsLookupGlobalId hetmet_flattened_id_name
+                                            ; hetmet_PGArrow_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS tcName (fsLit "PGArrow"))
+                                            ; hetmet_PGArrow <- dsLookupTyCon hetmet_PGArrow_name
+                                            ; hetmet_PGArrow_unit_name <- lookupOrig gHC_HETMET_GARROW (mkOccNameFS tcName (fsLit "GArrowUnit"))
+                                            ; hetmet_PGArrow_unit <- dsLookupTyCon hetmet_PGArrow_unit_name
+                                            ; hetmet_PGArrow_tensor_name <- lookupOrig gHC_HETMET_GARROW (mkOccNameFS tcName (fsLit "GArrowTensor"))
+                                            ; hetmet_PGArrow_tensor <- dsLookupTyCon hetmet_PGArrow_tensor_name
+                                            ; hetmet_PGArrow_exponent_name <- lookupOrig gHC_HETMET_GARROW (mkOccNameFS tcName (fsLit "GArrowExponent"))
+                                            ; hetmet_PGArrow_exponent <- dsLookupTyCon hetmet_PGArrow_exponent_name
+                                            ; hetmet_pga_id_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_id"))
+                                            ; hetmet_pga_id <- dsLookupGlobalId hetmet_pga_id_name
+                                            ; hetmet_pga_comp_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_comp"))
+                                            ; hetmet_pga_comp <- dsLookupGlobalId hetmet_pga_comp_name
+                                            ; hetmet_pga_first_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_first"))
+                                            ; hetmet_pga_first <- dsLookupGlobalId hetmet_pga_first_name
+                                            ; hetmet_pga_second_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_second"))
+                                            ; hetmet_pga_second <- dsLookupGlobalId hetmet_pga_second_name
+                                            ; hetmet_pga_cancell_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_cancell"))
+                                            ; hetmet_pga_cancell <- dsLookupGlobalId hetmet_pga_cancell_name
+                                            ; hetmet_pga_cancelr_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_cancelr"))
+                                            ; hetmet_pga_cancelr <- dsLookupGlobalId hetmet_pga_cancelr_name
+                                            ; hetmet_pga_uncancell_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_uncancell"))
+                                            ; hetmet_pga_uncancell <- dsLookupGlobalId hetmet_pga_uncancell_name
+                                            ; hetmet_pga_uncancelr_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_uncancelr"))
+                                            ; hetmet_pga_uncancelr <- dsLookupGlobalId hetmet_pga_uncancelr_name
+                                            ; hetmet_pga_assoc_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_assoc"))
+                                            ; hetmet_pga_assoc <- dsLookupGlobalId hetmet_pga_assoc_name
+                                            ; hetmet_pga_unassoc_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_unassoc"))
+                                            ; hetmet_pga_unassoc <- dsLookupGlobalId hetmet_pga_unassoc_name
+                                            ; hetmet_pga_copy_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_copy"))
+                                            ; hetmet_pga_copy <- dsLookupGlobalId hetmet_pga_copy_name
+                                            ; hetmet_pga_drop_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_drop"))
+                                            ; hetmet_pga_drop <- dsLookupGlobalId hetmet_pga_drop_name
+                                            ; hetmet_pga_swap_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_swap"))
+                                            ; hetmet_pga_swap <- dsLookupGlobalId hetmet_pga_swap_name
+                                            ; hetmet_pga_applyl_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_applyl"))
+                                            ; hetmet_pga_applyl <- dsLookupGlobalId hetmet_pga_applyl_name
+                                            ; hetmet_pga_applyr_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_applyr"))
+                                            ; hetmet_pga_applyr <- dsLookupGlobalId hetmet_pga_applyr_name
+                                            ; hetmet_pga_curryl_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_curryl"))
+                                            ; hetmet_pga_curryl <- dsLookupGlobalId hetmet_pga_curryl_name
+                                            ; hetmet_pga_curryr_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_curryr"))
+                                            ; hetmet_pga_curryr <- dsLookupGlobalId hetmet_pga_curryr_name
+                                            ; hetmet_pga_loopl_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_loopl"))
+                                            ; hetmet_pga_loopl <- dsLookupGlobalId hetmet_pga_loopl_name
+                                            ; hetmet_pga_loopr_name <- lookupOrig gHC_HETMET_PRIVATE (mkOccNameFS varName (fsLit "pga_loopr"))
+                                            ; hetmet_pga_loopr <- dsLookupGlobalId hetmet_pga_loopr_name
+                                            ; return ( hetmet_brak
+                                                     , hetmet_esc
+                                                     , hetmet_flatten
+                                                     , hetmet_unflatten
+                                                     , hetmet_flattened_id
+                                                     , hetmet_PGArrow
+                                                     , hetmet_PGArrow_unit
+                                                     , hetmet_PGArrow_tensor
+                                                     , hetmet_PGArrow_exponent
+                                                     , 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
+                                                     , hetmet_pga_loopl
+                                                     , hetmet_pga_loopr )
+                                            }
+                                    else return undefined
                           ; let hpc_init
                                   | opt_Hpc   = hpcInitCode mod ds_hpc_info
                                   | otherwise = empty
@@ -112,39 +211,125 @@ 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) }
+                                   , ds_hpc_info, modBreaks, junk)
+                                   }
 
         ; case mb_res of {
            Nothing -> return (msgs, Nothing) ;
-           Just (ds_ev_binds, all_prs, all_rules, ds_vects, ds_fords,ds_hpc_info, modBreaks) -> do
+           Just (ds_ev_binds, all_prs, all_rules, vects0, ds_fords, ds_hpc_info, modBreaks, junk) -> do
 
-       {       -- Add export flags to bindings
-         keep_alive <- readIORef keep_var
-       ; let (rules_for_locals, rules_for_imps) 
+        {       -- Add export flags to bindings
+          keep_alive <- readIORef keep_var
+        ; let (rules_for_locals, rules_for_imps) 
                    = partition isLocalRule all_rules
               final_prs = addExportFlagsAndRules target
-                             export_set keep_alive rules_for_locals (fromOL all_prs)
+                              export_set keep_alive rules_for_locals (fromOL all_prs)
+
+              final_pgm = let comb = combineEvBinds ds_ev_binds final_prs
+                          in if dopt Opt_F_simpleopt_before_flatten dflags
+                             then comb
+                             else simplifyBinds comb
+        -- Notice that we put the whole lot in a big Rec, even the foreign binds
+        -- When compiling PrelFloat, which defines data Float = F# Float#
+        -- we want F# to be in scope in the foreign marshalling code!
+        -- You might think it doesn't matter, but the simplifier brings all top-level
+        -- things into the in-scope set before simplifying; so we get no unfolding for F#!
+
+       ; (final_pgm1, rules_for_imps1, ds_vects1) <- if dopt Opt_F_simpleopt_before_flatten dflags
+                                                      then simpleOptPgm dflags final_pgm rules_for_imps vects0
+                                                      else return (final_pgm, rules_for_imps, vects0)
+
+        ; ds_binds1 <- 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
+                               ; (case junk of {
+                                     ( hetmet_brak ,
+                                       hetmet_esc ,
+                                       hetmet_flatten ,
+                                       hetmet_unflatten ,
+                                       hetmet_flattened_id ,
+                                       hetmet_PGArrow ,
+                                       hetmet_PGArrow_unit ,
+                                       hetmet_PGArrow_tensor ,
+                                       hetmet_PGArrow_exponent ,
+                                       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 ,
+                                       hetmet_pga_loopl ,
+                                       hetmet_pga_loopr ) ->
+                                           return (coqPassCoreToCore
+                                                     do_flatten
+                                                     do_skolemize
+                                                     hetmet_brak
+                                                     hetmet_esc
+                                                     hetmet_flatten
+                                                     hetmet_unflatten
+                                                     hetmet_flattened_id
+                                                     us
+                                                     final_pgm1
+                                                     hetmet_PGArrow
+                                                     hetmet_PGArrow_unit
+                                                     hetmet_PGArrow_tensor
+                                                     hetmet_PGArrow_exponent
+                                                     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
+                                                     hetmet_pga_loopl
+                                                     hetmet_pga_loopr
+                                        )
+                                            }
+                                 )
+                               }
+                       else return final_pgm
+
+       ; (ds_binds2, ds_rules_for_imps2, ds_vects2) <- if dopt Opt_F_simpleopt_before_flatten dflags
+                                                        then return (ds_binds1, rules_for_imps1, ds_vects1)
+                                                        else simpleOptPgm dflags ds_binds1 rules_for_imps1 ds_vects1
+                        -- The simpleOptPgm gets rid of type 
+                        -- bindings plus any stupid dead code
 
-              final_pgm = combineEvBinds ds_ev_binds final_prs
-       -- Notice that we put the whole lot in a big Rec, even the foreign binds
-       -- When compiling PrelFloat, which defines data Float = F# Float#
-       -- we want F# to be in scope in the foreign marshalling code!
-       -- You might think it doesn't matter, but the simplifier brings all top-level
-       -- things into the in-scope set before simplifying; so we get no unfolding for F#!
+        ; dumpIfSet_dyn dflags Opt_D_dump_proofs "Coq Pass Output" $ text $ coqPassCoreToString ds_binds1
 
-       -- Lint result if necessary, and print
-        ; dumpIfSet_dyn dflags Opt_D_dump_ds "Desugared, before opt" $
-               (vcat [ pprCoreBindings final_pgm
-                     , pprRules rules_for_imps ])
+        ; dumpIfSet_dyn dflags Opt_D_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds1)
 
-       ; (ds_binds, ds_rules_for_imps) <- simpleOptPgm dflags final_pgm rules_for_imps
-                        -- The simpleOptPgm gets rid of type 
-                        -- bindings plus any stupid dead code
+        ; (ds_binds3, ds_rules_for_imps3, ds_vects3) 
+            <- simpleOptPgm dflags ds_binds2 ds_rules_for_imps2 ds_vects2
+                         -- The simpleOptPgm gets rid of type 
+                         -- bindings plus any stupid dead code
 
-       ; endPass dflags CoreDesugar ds_binds ds_rules_for_imps
+        ; endPass dflags CoreDesugar ds_binds3 ds_rules_for_imps3
 
         ; let used_names = mkUsedNames tcg_env
-       ; deps <- mkDependencies tcg_env
+        ; deps <- mkDependencies tcg_env
 
         ; let mod_guts = ModGuts {     
                mg_module       = mod,
@@ -162,12 +347,12 @@ deSugar hsc_env
                mg_fam_insts    = fam_insts,
                mg_inst_env     = inst_env,
                mg_fam_inst_env = fam_inst_env,
-               mg_rules        = ds_rules_for_imps,
-               mg_binds        = ds_binds,
+               mg_rules        = ds_rules_for_imps3,
+               mg_binds        = ds_binds3,
                mg_foreign      = ds_fords,
                mg_hpc_info     = ds_hpc_info,
                 mg_modBreaks    = modBreaks,
-                mg_vect_decls   = ds_vects,
+                mg_vect_decls   = ds_vects2,
                 mg_vect_info    = noVectInfo
               }
         ; return (msgs, Just mod_guts)
@@ -378,6 +563,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 #-}
@@ -391,16 +578,44 @@ the rule is precisly to optimise them:
 
 \begin{code}
 dsVect :: LVectDecl Id -> DsM CoreVect
-dsVect (L loc (HsVect v rhs))
+dsVect (L loc (HsVect (L _ v) rhs))
   = putSrcSpanDs loc $ 
     do { rhs' <- fmapMaybeM dsLExpr rhs
-       ; return $ Vect (unLoc v) rhs'
+       ; return $ Vect v rhs'
           }
--- dsVect (L loc (HsVect v Nothing))
---   = return $ Vect v Nothing
--- dsVect (L loc (HsVect v (Just rhs)))
---   = putSrcSpanDs loc $ 
---     do { rhs' <- dsLExpr rhs
---        ; return $ Vect v (Just rhs')
---       }
+dsVect (L _loc (HsNoVect (L _ v)))
+  = return $ NoVect v
+\end{code}
+
+
+
+\begin{code}
+--
+-- Simplification routines run before the flattener.  We can't use
+-- simpleOptPgm -- it doesn't preserve the order of subexpressions or
+-- let-binding groups.
+--
+simplify :: Expr CoreBndr -> Expr CoreBndr
+simplify (Var v)                 = Var v
+simplify (App e1 e2)             = App (simplify e1) (simplify e2)
+simplify (Lit lit)               = Lit lit
+simplify (Note note e)           = Note note (simplify e)
+simplify (Cast e co)             = if eqType (fst $ unPair $ coercionKind co) (snd $ unPair $ coercionKind co)
+                                       then simplify e
+                                       else Cast (simplify e) co
+simplify (Lam v e)               = Lam v (simplify e)
+simplify (Case e b ty as)        = Case (simplify e) b ty (map (\(a,b,e) -> (a,b,simplify e)) as)
+simplify (Let bind body)         = foldr Let (simplify body) (simplifyBind bind)
+simplify (Type t)                = Type t
+simplify (Coercion co)           = Coercion co
+
+simplifyBind :: Bind CoreBndr -> [Bind CoreBndr]
+simplifyBind (NonRec b e)             = [NonRec b (simplify e)]
+simplifyBind (Rec [])                 = []
+simplifyBind (Rec (rbs@((b,e):rbs'))) =
+    if or $ map (\x -> elemUFM x (exprFreeIds e)) (map fst rbs)
+    then [Rec (map (\(v,e) -> (v,simplify e)) rbs)]
+    else (NonRec b (simplify e)):(simplifyBind $ Rec rbs')
+
+simplifyBinds = concatMap simplifyBind
 \end{code}