added basic support for primitive literals

Author: flupe

src/Agda2Lambox/Compile/Term.hs

@@ -11,6 +11,7 @@ import Control.Monad.Trans
 import Data.List ( elemIndex, foldl', singleton )
 import Data.Maybe ( fromMaybe, listToMaybe )
 import Data.Foldable ( foldrM )
+import Data.Text qualified as Text ( unpack )
 
 import Agda.Compiler.Backend ( MonadTCState, HasOptions, canonicalName )
 import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutual )
@@ -154,16 +155,20 @@ compileTermC = \case
 compileLit :: Literal -> C LBox.Term
 compileLit = \case
 
+  -- TODO(flupe):
+  --   optionally attempt compiling this to an Int63 Primitive
   LitNat i -> do
     qn <- liftTCM $ getBuiltinName_ builtinNat
     qz <- liftTCM $ getBuiltinName_ builtinZero
     qs <- liftTCM $ getBuiltinName_ builtinSuc
     lift do
       requireDef qn
-      iterate (toConApp qs . singleton =<<) 
-              (toConApp qz []) 
+      iterate (toConApp qs . singleton =<<)
+              (toConApp qz [])
         !! fromInteger i
 
+  LitString s -> pure $ LBox.LPrim $ LBox.PString $ Text.unpack s
+
   l -> genericError $ "unsupported literal: " <> prettyShow l
 
 

src/LambdaBox/Term.hs

@@ -2,47 +2,61 @@
 -- | Definition of λ□ terms.
 module LambdaBox.Term where
 
+import Data.Int (Int64)
 import Data.Bifunctor (first)
 import Agda.Syntax.Common.Pretty
 import LambdaBox.Names
 
 
--- | Definition component in a mutual fixpoint.
+-- | Definition component in a mutual fixpoint
 data Def t = Def
   { dName :: Name
   , dBody :: t
   , dArgs :: Int
   }
 
--- | Mutual components of a fixpoint.
+-- | Mutual components of a fixpoint
 type MFixpoint = [Def Term]
 
+-- | 
+data PrimValue
+  = PInt Int64
+      -- NOTE(flupe): ^ Should ensure they are restricted to Int63
+  | PFloat Int64
+  | PString String
+
 -- | λ□ terms
 data Term
-  = LBox          -- ^ Proofs and erased terms
-  | LRel Int      -- ^ Bound variable, with de Bruijn index
-  | LLambda Name Term  -- ^ Lambda abstraction
-  | LLetIn Name Term Term
-      -- ^ Let bindings.
-      --   Unused in the backend, since Agda itself no longer has let bindings
-      --   in the concrete syntac.
+  = LBox                             -- ^ Proofs and erased terms
+  | LRel Int                         -- ^ Bound variable, with de Bruijn index
+  | LLambda Name Term                -- ^ Lambda abstraction
+  | LLetIn Name Term Term            -- ^ Let bindings
   | LApp Term Term                   -- ^ Term application
-  | LConst KerName                   -- ^ Named constant.
-  | LConstruct Inductive Int [Term]  -- ^ Inductive constructor.
-  | LCase              -- ^ Pattern-matching case construct.
-      Inductive        -- ^ Inductive type we cae on.
+  | LConst KerName                   -- ^ Named constant
+  | LConstruct Inductive Int [Term]  -- ^ Inductive constructor
+  | LCase                            -- ^ Pattern-matching case construct
+      Inductive        -- ^ Inductive type we case on
       Int              -- ^ Number of parameters
       Term             -- ^ Discriminee
       [([Name], Term)] -- ^ Branches
-  | LFix        -- ^ Fixpoint combinator.
+  | LFix                             -- ^ Fixpoint combinator
       MFixpoint
-      Int       -- ^ Index of the fixpoint we keep.
+      Int       -- ^ Index of the fixpoint we keep
+  | LPrim PrimValue
+                -- ^ Primitive literal value
 
 
 instance Pretty t => Pretty (Def t) where
   -- prettyPrec _ (Def s _ _) = pretty s
   prettyPrec _ (Def _ t _) = pretty t
 
+
+instance Pretty PrimValue where
+  pretty (PInt i)    = text $ show i
+  pretty (PFloat f)  = text $ show f
+  pretty (PString f) = text $ show f
+
+
 instance Pretty Term where
   prettyPrec p v =
     case v of
@@ -59,7 +73,6 @@ instance Pretty Term where
         in 
         mparens (p > 0) $
         hang ("λ" <+> sep (map pretty (n:ns)) <+> "→") 2 $ pretty t'
-        
 
       LLetIn n e t ->
         mparens (p > 0) $ sep
@@ -85,3 +98,6 @@ instance Pretty Term where
       LFix ds i -> -- FIXME: for mutual recursion
         mparens (p > 0) $
         hang "μ rec ->" 2 $ pretty $ ds !! i
+
+      LPrim p -> pretty p
+        

src/SExpr.hs

@@ -50,6 +50,7 @@ ctor :: Target t -> Text -> [Sexpable t] -> Exp
 ctor t n [] = SAtom (ANode n)
 ctor t n xs = SList () (SAtom (ANode n) : map (toSexp t) xs)
 
+instance ToSexp t Atom         where toSexp _   = SAtom
 instance ToSexp t (Sexp Atom)  where toSexp _ d = d
 instance ToSexp t Int          where toSexp _ s = SAtom (AInt s)
 instance ToSexp t Bool         where toSexp _ s = SAtom (ABool s)
@@ -88,6 +89,20 @@ instance ToSexp t Inductive where
 instance ToSexp t d => ToSexp t (Def d) where
   toSexp t Def{..} = ctor t "def" [S dName, S dBody, S dArgs]
 
+instance ToSexp t PrimValue where
+  toSexp t x = toSexp t (primTag x, primVal x)
+    where 
+      primTag = \case
+        PInt{}    -> ctor t "primInt" []
+        PFloat{}  -> ctor t "primFloat" []
+        PString{} -> ctor t "primString" []
+
+      primVal = \case
+        PInt   i  -> AString (show i)
+        PFloat f  -> AString (show f)
+        PString s -> AString s
+
+
 instance ToSexp t Term where
   toSexp t = \case
     LBox                -> ctor t "tBox"       []
@@ -99,6 +114,7 @@ instance ToSexp t Term where
     LConstruct ind i es -> ctor t "tConstruct" [S ind, S i, S es]
     LCase ind n u bs    -> ctor t "tCase"      [S (ind, n), S u, S bs]
     LFix mf i           -> ctor t "tFix"       [S mf, S i]
+    LPrim p             -> ctor t "tPrim"      [S p]
 
 instance ToSexp t Type where
   toSexp t = \case

test/String.agda

@@ -0,0 +1,5 @@
+open import Agda.Builtin.String
+
+demo : String
+demo = "Hello, World!"
+{-# COMPILE AGDA2LAMBOX demo #-}