[ compilers ] removed (unused) smashing code

- command line option - pragma - dead code We do smashing in treeless now, and it makes little sense to turn it off.
agda · Aug 17, 2016 · ee35abc · ee35abc
1 parent 1524615
commit ee35abc
Show file tree

Hide file tree

Showing 20 changed files with 11 additions and 223 deletions.
diff --git a/Agda.cabal b/Agda.cabal
@@ -243,7 +243,6 @@ library
                     Agda.Compiler.UHC.Pragmas.Base
                     Agda.Compiler.UHC.Pragmas.Parse
                     Agda.Compiler.UHC.Primitives
-                    Agda.Compiler.UHC.Smashing
                     Agda.ImpossibleTest
                     Agda.Interaction.BasicOps
                     Agda.Interaction.SearchAbout

diff --git a/src/full/Agda/Compiler/UHC/Smashing.hs b/src/full/Agda/Compiler/UHC/Smashing.hs
diff --git a/src/full/Agda/Interaction/Options.hs b/src/full/Agda/Interaction/Options.hs
@@ -500,9 +500,6 @@ uhcTraceLevelFlag i o = return $ o { optUHCTraceLevel = read i }
 uhcFlagsFlag :: String -> Flag CommandLineOptions
 uhcFlagsFlag s o = return $ o { optUHCFlags = optUHCFlags o ++ [s] }
 
-optimNoSmashing :: Flag CommandLineOptions
-optimNoSmashing o = return $ o {optOptimSmashing = False }
-
 htmlFlag :: Flag CommandLineOptions
 htmlFlag o = return $ o { optGenerateHTML = True }
 
@@ -583,7 +580,6 @@ standardOptions =
     , Option []     ["uhc-gen-trace"] (ReqArg uhcTraceLevelFlag "TRACE") "Add tracing code to generated executable."
     , Option []     ["uhc-flag"] (ReqArg uhcFlagsFlag "UHC-FLAG")
                     "give the flag UHC-FLAG to UHC when compiling using the UHC backend"
-    , Option []     ["no-smashing"] (NoArg optimNoSmashing) "Don't apply the smashing optimization."
     , Option []     ["compile-dir"] (ReqArg compileDirFlag "DIR")
                     ("directory for compiler output (default: the project root)")
 

diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs
@@ -186,7 +186,6 @@ data Pragma
   | CompiledJSPragma QName String
   | CompiledUHCPragma QName String
   | CompiledDataUHCPragma QName String [String]
-  | NoSmashingPragma QName
   | StaticPragma QName
   | InlinePragma QName
   | DisplayPragma QName [NamedArg Pattern] Expr

diff --git a/src/full/Agda/Syntax/Abstract/Views.hs b/src/full/Agda/Syntax/Abstract/Views.hs
@@ -344,7 +344,6 @@ instance ExprLike Pragma where
       CompiledJSPragma{}          -> pure p
       CompiledUHCPragma{}         -> pure p
       CompiledDataUHCPragma{}     -> pure p
-      NoSmashingPragma{}          -> pure p
       StaticPragma{}              -> pure p
       InlinePragma{}              -> pure p
       DisplayPragma f xs e        -> DisplayPragma f <$> rec xs <*> rec e

diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
@@ -386,7 +386,6 @@ data Pragma
   | CompiledUHCPragma         Range QName String
   | CompiledDataUHCPragma     Range QName String [String]
   | HaskellCodePragma         Range String
-  | NoSmashingPragma          Range QName
   | StaticPragma              Range QName
   | InlinePragma              Range QName
   | ImportPragma              Range String
@@ -655,7 +654,6 @@ instance HasRange Pragma where
   getRange (CompiledUHCPragma r _ _)         = r
   getRange (CompiledDataUHCPragma r _ _ _)   = r
   getRange (HaskellCodePragma r _)           = r
-  getRange (NoSmashingPragma r _)            = r
   getRange (StaticPragma r _)                = r
   getRange (InlinePragma r _)                = r
   getRange (ImportPragma r _)                = r
@@ -832,7 +830,6 @@ instance KillRange Pragma where
   killRange (CompiledUHCPragma _ q s)         = killRange1 (\q -> CompiledUHCPragma noRange q s) q
   killRange (CompiledDataUHCPragma _ q s ss)  = killRange1 (\q -> CompiledDataUHCPragma noRange q s ss) q
   killRange (HaskellCodePragma _ s)           = HaskellCodePragma noRange s
-  killRange (NoSmashingPragma _ q)            = killRange1 (NoSmashingPragma noRange) q
   killRange (StaticPragma _ q)                = killRange1 (StaticPragma noRange) q
   killRange (InlinePragma _ q)                = killRange1 (InlinePragma noRange) q
   killRange (ImportPragma _ s)                = ImportPragma noRange s
@@ -964,7 +961,6 @@ instance NFData Pragma where
   rnf (CompiledUHCPragma _ a b)         = rnf a `seq` rnf b
   rnf (CompiledDataUHCPragma _ a b c)   = rnf a `seq` rnf b `seq` rnf c
   rnf (HaskellCodePragma _ s)           = rnf s
-  rnf (NoSmashingPragma _ a)            = rnf a
   rnf (StaticPragma _ a)                = rnf a
   rnf (InlinePragma _ a)                = rnf a
   rnf (ImportPragma _ a)                = rnf a

diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -449,8 +449,6 @@ instance Pretty Pragma where
       hsep $ [ text "COMPILED_DATA_UHC", pretty x] ++ map text (crd : crcs)
     pretty (HaskellCodePragma _ s) =
       vcat (text "HASKELL" : map text (lines s))
-    pretty (NoSmashingPragma _ i) =
-      hsep $ [text "NO_SMASHING", pretty i]
     pretty (StaticPragma _ i) =
       hsep $ [text "STATIC", pretty i]
     pretty (InlinePragma _ i) =

diff --git a/src/full/Agda/Syntax/Parser/Lexer.x b/src/full/Agda/Syntax/Parser/Lexer.x
@@ -95,7 +95,6 @@ tokens :-
 <pragma_>   "LINE"                     { keyword KwLINE }
 <pragma_>   "MEASURE"                  { keyword KwMEASURE }
 <pragma_>   "NO_POSITIVITY_CHECK"      { keyword KwNO_POSITIVITY_CHECK }
-<pragma_>   "NO_SMASHING"              { keyword KwNO_SMASHING }
 <pragma_>   "NO_TERMINATION_CHECK"     { keyword KwNO_TERMINATION_CHECK }
 <pragma_>   "NON_TERMINATING"          { keyword KwNON_TERMINATING }
 <pragma_>   "OPTIONS"                  { keyword KwOPTIONS }

diff --git a/src/full/Agda/Syntax/Parser/Parser.y b/src/full/Agda/Syntax/Parser/Parser.y
@@ -145,7 +145,6 @@ import Agda.Utils.Impossible
     'IMPOSSIBLE'              { TokKeyword KwIMPOSSIBLE $$ }
     'INLINE'                  { TokKeyword KwINLINE $$ }
     'MEASURE'                 { TokKeyword KwMEASURE $$ }
-    'NO_SMASHING'             { TokKeyword KwNO_SMASHING $$ }
     'NO_TERMINATION_CHECK'    { TokKeyword KwNO_TERMINATION_CHECK $$ }
     'NO_POSITIVITY_CHECK'     { TokKeyword KwNO_POSITIVITY_CHECK $$ }
     'NON_TERMINATING'         { TokKeyword KwNON_TERMINATING $$ }
@@ -275,7 +274,6 @@ Token
     | 'IMPOSSIBLE'              { TokKeyword KwIMPOSSIBLE $1 }
     | 'INLINE'                  { TokKeyword KwINLINE $1 }
     | 'MEASURE'                 { TokKeyword KwMEASURE $1 }
-    | 'NO_SMASHING'             { TokKeyword KwNO_SMASHING $1 }
     | 'NO_TERMINATION_CHECK'    { TokKeyword KwNO_TERMINATION_CHECK $1 }
     | 'NO_POSITIVITY_CHECK'     { TokKeyword KwNO_POSITIVITY_CHECK $1 }
     | 'NON_TERMINATING'         { TokKeyword KwNON_TERMINATING $1 }
@@ -1376,7 +1374,6 @@ DeclarationPragma
   | CompiledUHCPragma        { $1 }
   | CompiledDataUHCPragma    { $1 }
   | HaskellPragma            { $1 }
-  | NoSmashingPragma         { $1 }
   | StaticPragma             { $1 }
   | InlinePragma             { $1 }
   | ImportPragma             { $1 }
@@ -1460,11 +1457,6 @@ HaskellPragma :: { Pragma }
 HaskellPragma
   : '{-#' 'HASKELL' Strings '#-}' { HaskellCodePragma (getRange ($1, $2, $4)) (recoverLayout $3) }
 
-NoSmashingPragma :: { Pragma }
-NoSmashingPragma
-  : '{-#' 'NO_SMASHING' PragmaQName '#-}'
-    { NoSmashingPragma (getRange ($1,$2,$3,$4)) $3 }
-
 StaticPragma :: { Pragma }
 StaticPragma
   : '{-#' 'STATIC' PragmaQName '#-}'

diff --git a/src/full/Agda/Syntax/Parser/Tokens.hs b/src/full/Agda/Syntax/Parser/Tokens.hs
@@ -21,7 +21,7 @@ data Keyword
         | KwCOMPILED_DATA | KwCOMPILED_DECLARE_DATA | KwCOMPILED_TYPE | KwCOMPILED | KwCOMPILED_EXPORT
         | KwHASKELL
         | KwCOMPILED_EPIC | KwCOMPILED_JS | KwCOMPILED_UHC | KwCOMPILED_DATA_UHC
-        | KwIMPORT | KwIMPORT_UHC | KwIMPOSSIBLE | KwSTATIC | KwINLINE | KwNO_SMASHING
+        | KwIMPORT | KwIMPORT_UHC | KwIMPOSSIBLE | KwSTATIC | KwINLINE
         | KwNO_TERMINATION_CHECK | KwTERMINATING | KwNON_TERMINATING
         | KwMEASURE | KwDISPLAY
         | KwREWRITE

diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -838,7 +838,6 @@ instance ToConcrete RangeAndPragma C.Pragma where
     A.CompiledDataUHCPragma x crd crcs -> do
       x <- toConcrete x
       return $ C.CompiledDataUHCPragma r x crd crcs
-    A.NoSmashingPragma x -> C.NoSmashingPragma r <$> toConcrete x
     A.StaticPragma x -> C.StaticPragma r <$> toConcrete x
     A.InlinePragma x -> C.InlinePragma r <$> toConcrete x
     A.DisplayPragma f ps rhs ->

diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -1718,15 +1718,6 @@ instance ToAbstract C.Pragma [A.Pragma] where
     case e of
       A.Def x -> return [ A.CompiledDataUHCPragma x crd crcs ]
       _       -> fail $ "Bad compiled type: " ++ show x  -- TODO: error message
-  toAbstract (C.NoSmashingPragma _ x) = do
-      e <- toAbstract $ OldQName x Nothing
-      y <- case e of
-          A.Def  x -> return x
-          A.Proj _ (AmbQ [x]) -> return x
-          A.Proj _ x -> genericError $
-            "NO_SMASHING used on ambiguous name " ++ prettyShow x
-          _        -> genericError "Target of NO_SMASHING pragma should be a function"
-      return [ A.NoSmashingPragma y ]
   toAbstract (C.StaticPragma _ x) = do
       e <- toAbstract $ OldQName x Nothing
       y <- case e of

diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -1389,7 +1389,6 @@ setEtaEquality _ b = Inferred b
 
 data FunctionFlag = FunStatic       -- ^ Should calls to this function be normalised at compile-time?
                   | FunInline       -- ^ Should calls to this function be inlined by the compiler?
-                  | FunSmashable    -- ^ Are we allowed to smash this function?
                   | FunMacro        -- ^ Is this function a macro?
   deriving (Typeable, Eq, Ord, Enum, Show)
 
@@ -1493,7 +1492,7 @@ emptyFunction = Function
   , funAbstr       = ConcreteDef
   , funDelayed     = NotDelayed
   , funProjection  = Nothing
-  , funFlags       = Set.singleton FunSmashable
+  , funFlags       = Set.empty
   , funTerminates  = Nothing
   , funExtLam      = Nothing
   , funWith        = Nothing
@@ -1506,10 +1505,9 @@ funFlag flag f def@Function{ funFlags = flags } =
   \ b -> def{ funFlags = (if b then Set.insert else Set.delete) flag flags }
 funFlag _ f def = f False <&> const def
 
-funStatic, funInline, funSmashable, funMacro :: Lens' Bool Defn
+funStatic, funInline, funMacro :: Lens' Bool Defn
 funStatic       = funFlag FunStatic
 funInline       = funFlag FunInline
-funSmashable    = funFlag FunSmashable
 funMacro        = funFlag FunMacro
 
 isMacro :: Defn -> Bool

diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs
@@ -169,9 +169,6 @@ setFunctionFlag flag val q =
   modifySignature $ updateDefinition q $
   set (theDefLens . funFlag flag) val
 
-markNoSmashing :: QName -> TCM ()
-markNoSmashing = setFunctionFlag FunSmashable False
-
 markStatic :: QName -> TCM ()
 markStatic = setFunctionFlag FunStatic True
 
@@ -450,9 +447,7 @@ applySection' new ptel old ts rd rm = do
                         , funMutual         = mutual
                         , funAbstr          = ConcreteDef -- OR: abstr -- ?!
                         , funProjection     = proj
-                        , funFlags          = Set.fromList $
-                                                [ FunSmashable ] ++
-                                                [ FunMacro | isMacro oldDef ]
+                        , funFlags          = Set.fromList [ FunMacro | isMacro oldDef ]
                         , funTerminates     = Just True
                         , funExtLam         = extlam
                         , funWith           = with

diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs
@@ -700,11 +700,6 @@ checkPragma r p =
                 addCoreType x dt'
                 sequence_ $ zipWith addCoreConstr cs cons'
             _ -> typeError $ GenericError "COMPILED_DATA_UHC on non datatype"
-        A.NoSmashingPragma x -> do
-          def <- getConstInfo x
-          case theDef def of
-            Function{} -> markNoSmashing x
-            _          -> typeError $ GenericError "NO_SMASHING directive only works on functions"
         A.StaticPragma x -> do
           def <- getConstInfo x
           case theDef def of