[ GHC backend ] Tried to fix #5421.

agda · May 31, 2021 · 498122f · 498122f
1 parent a605972
commit 498122f
Show file tree

Hide file tree

Showing 4 changed files with 106 additions and 29 deletions.
diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
@@ -7,6 +7,7 @@ import Control.Monad.Except (throwError)
 import Control.Monad.Reader
 import Control.Monad.Writer hiding ((<>))
 
+import qualified Data.HashSet as HashSet
 import qualified Data.List as List
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -223,36 +224,77 @@ ghcPreCompile flags = do
   mid         <- getBuiltinName builtinId
   mconid      <- getBuiltinName builtinConId
 
+  istcbuiltin <- do
+    builtins <- mapM getBuiltinName
+      [ builtinAgdaTCMReturn
+      , builtinAgdaTCMBind
+      , builtinAgdaTCMUnify
+      , builtinAgdaTCMTypeError
+      , builtinAgdaTCMInferType
+      , builtinAgdaTCMCheckType
+      , builtinAgdaTCMNormalise
+      , builtinAgdaTCMReduce
+      , builtinAgdaTCMCatchError
+      , builtinAgdaTCMQuoteTerm
+      , builtinAgdaTCMUnquoteTerm
+      , builtinAgdaTCMQuoteOmegaTerm
+      , builtinAgdaTCMGetContext
+      , builtinAgdaTCMExtendContext
+      , builtinAgdaTCMInContext
+      , builtinAgdaTCMFreshName
+      , builtinAgdaTCMDeclareDef
+      , builtinAgdaTCMDeclarePostulate
+      , builtinAgdaTCMDefineFun
+      , builtinAgdaTCMGetType
+      , builtinAgdaTCMGetDefinition
+      , builtinAgdaTCMBlockOnMeta
+      , builtinAgdaTCMCommit
+      , builtinAgdaTCMIsMacro
+      , builtinAgdaTCMWithNormalisation
+      , builtinAgdaTCMWithReconsParams
+      , builtinAgdaTCMDebugPrint
+      , builtinAgdaTCMOnlyReduceDefs
+      , builtinAgdaTCMDontReduceDefs
+      , builtinAgdaTCMNoConstraints
+      , builtinAgdaTCMRunSpeculative
+      , builtinAgdaTCMExec
+      ]
+    return $
+      flip HashSet.member $
+      HashSet.fromList $
+      catMaybes builtins
+
   return $ GHCEnv
-    { ghcEnvOpts       = ghcOpts
-    , ghcEnvBool       = mbool
-    , ghcEnvTrue       = mtrue
-    , ghcEnvFalse      = mfalse
-    , ghcEnvMaybe      = mmaybe
-    , ghcEnvNothing    = mnothing
-    , ghcEnvJust       = mjust
-    , ghcEnvList       = mlist
-    , ghcEnvNil        = mnil
-    , ghcEnvCons       = mcons
-    , ghcEnvNat        = mnat
-    , ghcEnvInteger    = minteger
-    , ghcEnvWord64     = mword64
-    , ghcEnvInf        = minf
-    , ghcEnvSharp      = msharp
-    , ghcEnvFlat       = mflat
-    , ghcEnvInterval   = minterval
-    , ghcEnvIZero      = mizero
-    , ghcEnvIOne       = mione
-    , ghcEnvIsOne      = misone
-    , ghcEnvItIsOne    = mitisone
-    , ghcEnvIsOne1     = misone1
-    , ghcEnvIsOne2     = misone2
-    , ghcEnvIsOneEmpty = misoneempty
-    , ghcEnvPathP      = mpathp
-    , ghcEnvSub        = msub
-    , ghcEnvSubIn      = msubin
-    , ghcEnvId         = mid
-    , ghcEnvConId      = mconid
+    { ghcEnvOpts        = ghcOpts
+    , ghcEnvBool        = mbool
+    , ghcEnvTrue        = mtrue
+    , ghcEnvFalse       = mfalse
+    , ghcEnvMaybe       = mmaybe
+    , ghcEnvNothing     = mnothing
+    , ghcEnvJust        = mjust
+    , ghcEnvList        = mlist
+    , ghcEnvNil         = mnil
+    , ghcEnvCons        = mcons
+    , ghcEnvNat         = mnat
+    , ghcEnvInteger     = minteger
+    , ghcEnvWord64      = mword64
+    , ghcEnvInf         = minf
+    , ghcEnvSharp       = msharp
+    , ghcEnvFlat        = mflat
+    , ghcEnvInterval    = minterval
+    , ghcEnvIZero       = mizero
+    , ghcEnvIOne        = mione
+    , ghcEnvIsOne       = misone
+    , ghcEnvItIsOne     = mitisone
+    , ghcEnvIsOne1      = misone1
+    , ghcEnvIsOne2      = misone2
+    , ghcEnvIsOneEmpty  = misoneempty
+    , ghcEnvPathP       = mpathp
+    , ghcEnvSub         = msub
+    , ghcEnvSubIn       = msubin
+    , ghcEnvId          = mid
+    , ghcEnvConId       = mconid
+    , ghcEnvIsTCBuiltin = istcbuiltin
     }
 
 ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
@@ -616,6 +658,16 @@ definition def@Defn{defName = q, defType = ty, theDef = d} = do
                  emptyBinds]
           ]
 
+      -- TC builtins are compiled to erased, which is an ∞-ary
+      -- function.
+      Axiom{} | ghcEnvIsTCBuiltin env q -> do
+        retDecls $
+          [ HS.FunBind
+              [HS.Match (dname q) []
+                 (HS.UnGuardedRhs (HS.FakeExp mazErasedName))
+                 emptyBinds]
+          ]
+
       DataOrRecSig{} -> __IMPOSSIBLE__
 
       Axiom{} -> do

diff --git a/src/full/Agda/Compiler/MAlonzo/Misc.hs b/src/full/Agda/Compiler/MAlonzo/Misc.hs
@@ -93,6 +93,8 @@ data GHCEnv = GHCEnv
   , ghcEnvConId
     :: Maybe QName
     -- Various (possibly) builtin names.
+  , ghcEnvIsTCBuiltin :: QName -> Bool
+    -- ^ Is the given name a @TC@ builtin (except for @TC@ itself)?
   }
 
 -- | Module compilation environment, bundling the overall

diff --git a/test/Compiler/simple/Issue5421.agda b/test/Compiler/simple/Issue5421.agda
@@ -0,0 +1,18 @@
+open import Agda.Builtin.IO
+open import Agda.Builtin.Reflection
+open import Agda.Builtin.Strict
+open import Agda.Builtin.String
+open import Agda.Builtin.Unit
+
+postulate
+  putStr : String → IO ⊤
+
+{-# FOREIGN GHC import qualified Data.Text.IO #-}
+{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
+{-# COMPILE JS putStr =
+    function (x) {
+      return function(cb) {
+        process.stdout.write(x); cb(0); }; } #-}
+
+main : IO ⊤
+main = primForce commitTC λ _ → putStr "Success\n"
diff --git a/test/Compiler/simple/Issue5421.out b/test/Compiler/simple/Issue5421.out
@@ -0,0 +1,5 @@
+EXECUTED_PROGRAM
+
+ret > ExitSuccess
+out > Success
+out >