prevent compilation of primitives

Author: flupe

src/Agda2Lambox/Compile.hs

@@ -85,13 +85,18 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
       reportSDoc "agda2lambox.compile" 5 $
         "Found primitive: " <> prettyTCM defName
 
-      getBuiltinThing (PrimitiveName primName) >>= \case
-
-        -- if it's a primitive with an actual implementation
-        -- we try to convert it to a function, manually
-        Just (Prim (PrimFun{})) -> do
+      -- It's a primitive with no Agda definition
+      if null primClauses then do
+        -- we compile it as an axiom
+        reportSDoc "agda2lambox.compile" 5 "Compiling it to an axiom."
+        typ <- whenTyped target $ compileTopLevelType defType
+        pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+
+      -- otherwise, we attempt compiling it as a regular Agda function
+      else do
           reportSDoc "agda2lambox.compile" 5 $
             "It's a builtin, converting it to a function."
+          reportSDoc "agda2lambox.compile" 5 $ prettyTCM primClauses
           let
             defn' = defn
               { theDef = Function
@@ -117,10 +122,5 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
           -- and then we compile it as a regular function
           compileFunction target defn'
 
-        -- otherwise, compiling it as an axiom
-        _ -> do
-          reportSDoc "agda2lambox.compile" 5 $ "Compiling it to an axiom."
-          typ <- whenTyped target $ compileTopLevelType defType
-          pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
     _ -> genericError $ "Cannot compile: " <> prettyShow defName