add support for primitives

Author: flupe

demo/index.html

@@ -46,6 +46,7 @@ <h1>agda2lambox</h1>
   <fieldset>
     <button id="run" disabled>Run</button>
     <button id="reload" disabled>Reload</button>
+    <button id="clear">Clear</button>
     <select id="decoder">
       <option value="nat">Nat</option>
       <option value="bool">Bool</option>
@@ -69,6 +70,7 @@ <h1>agda2lambox</h1>
 on(file,   "change", load)
 on(reload, "click",  load)
 on(run,    "click",  exec)
+on(clear,  "click", () => {output.innerHTML = ""})
 
 async function load() {
   if (file.files.length == 0) return

src/Agda2Lambox/Compile.hs

@@ -15,11 +15,12 @@ import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal ( QName )
-import Agda.Syntax.Common (Arg(..))
+import Agda.Syntax.Common (Arg(..), IsOpaque (TransparentDef))
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.TypeChecking.Pretty
 import Agda.Utils.Monad ( whenM, ifM, unlessM, ifNotM, orM, forM_ )
+import Agda.Utils.SmallSet qualified as SmallSet
 
 import Agda.Utils ( hasPragma, isDataOrRecDef, treeless, isArity )
 
@@ -110,7 +111,33 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
       reportSDoc "agda2lambox.compile" 5 $
         "Found primitive: " <> prettyTCM defName <> ". Compiling it as axiom."
 
-      typ <- whenTyped target $ compileTopLevelType defType
-      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+      getBuiltinThing (PrimitiveName primName) >>= \case
+        -- it's a primitive with an actual implementation
+        -- we try to convert it to a function, manually
+        Just (Prim (PrimFun{})) -> do
+          let def = Function
+                { funClauses    = primClauses
+                , funCompiled   = primCompiled
+                , funSplitTree  = Nothing
+                , funTreeless   = Nothing
+                , funCovering   = []
+                , funInv        = primInv
+                , funMutual     = Just [defName]
+                , funProjection = Left NeverProjection
+                , funFlags      = SmallSet.empty
+                , funTerminates = Just True
+                , funExtLam     = Nothing
+                , funWith       = Nothing
+                , funIsKanOp    = Nothing
+                , funOpaque     = TransparentDef
+                }
+
+          let defn' = defn {theDef = def}
+          liftTCM $ modifyGlobalDefinition defName $ const defn'
+          compileFunction target defn'
+
+        _ -> do
+          typ <- whenTyped target $ compileTopLevelType defType
+          pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
     _ -> genericError $ "Cannot compile: " <> prettyShow defName

src/Main.hs

@@ -104,9 +104,6 @@ agda2lambox = Backend backend
       , mayEraseType          = \ _ -> return True
       }
 
-
-
-
 moduleSetup
   :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath
   -> TCM (Recompile ModuleEnv ModuleRes)
@@ -131,7 +128,6 @@ writeModule Options{..} menv IsMain m defs = do
   let fileName = (outDir </>) . moduleNameToFileName m
       coqMod   = CoqModule env (map qnameToKName programs)
 
-
   liftIO do
     putStrLn $ "Writing " <> fileName ".txt"
     pp coqMod <> "\n" & writeFile (fileName ".txt")

test/BigDemo.agda

@@ -1,5 +1,6 @@
 module _ where
 
+{-
 -- - decision procedure (barebones)
 module BAREBONES where
   open import Agda.Primitive using (Level)
@@ -36,48 +37,56 @@ module BAREBONES where
   instance
     HasDecEq-Nat : HasDec (x ≡ y)
     HasDecEq-Nat {x}{y} .dec with x | y
-    ... | zero | zero = yes refl
-    ... | zero | suc n = no λ ()
+    ... | zero  | zero = yes refl
+    ... | zero  | suc n = no λ ()
     ... | suc m | zero = no λ ()
     ... | suc m | suc n with dec
-    ... | yes eq  = yes (cong suc eq)
+    ... | yes eq   = yes (cong suc eq)
     ... | no  m≢n = no λ where refl → m≢n refl
 
   test : Bool
-  test = isYes (dec {A = 42 ≡ 42})
-  -- {-# COMPILE AGDA2LAMBOX test #-}
+  test = isYes (dec {A = 4 ≡ 4})
+  {-# COMPILE AGDA2LAMBOX test #-}
+-- -}
 
+{-
 -- - decision procedure (importing stdlib)
 module STDLIB where
   open import Relation.Nullary using (isYes)
 
   open import Data.Bool using (Bool; true; false)
   open import Data.Bool.Properties using (_≟_)
   test : Bool
-  test = isYes (true ≟ false)
-  -- {-# COMPILE AGDA2LAMBOX test #-}
+  test = isYes (false ≟ true)
+  {-# COMPILE AGDA2LAMBOX test #-}
 
   -- open import Data.Bool using (Bool)
   -- open import Data.Nat.Properties using (_≟_)
   -- test : Bool
   -- test = isYes (42 ≟ 42)
   -- {-# COMPILE AGDA2LAMBOX test #-}
 
+-- -}
+
+-- {-
 -- - sort
 module SORT where
-  open import Data.List.Base using (List; _∷_; [])
-
-  open import Data.Bool.Properties using (≤-decTotalOrder)
-  open import Data.Bool using (Bool; true; false)
-  open import Data.List.Sort ≤-decTotalOrder using (sort)
-  test : List Bool
-  test = sort (true ∷ false ∷ true ∷ false ∷ [])
-  {-# COMPILE AGDA2LAMBOX test #-}
-
-  -- open import Data.Nat.Properties using (≤-decTotalOrder)
-  -- open import Data.Bool using (Bool; true; false)
   -- open import Data.List.Base using (List; _∷_; [])
+  -- open import Data.Bool.Properties using (≤-decTotalOrder)
+  -- open import Data.Bool using (Bool; true; false)
   -- open import Data.List.Sort ≤-decTotalOrder using (sort)
+
   -- test : List Bool
-  -- test = sort (42 ∷ 0 ∷ 5 ∷ 3 ∷ [])
+  -- test = sort (true ∷ false ∷ true ∷ false ∷ [])
   -- {-# COMPILE AGDA2LAMBOX test #-}
+
+  open import Data.Nat.Base
+  open import Data.Nat.Properties using (≤-decTotalOrder)
+  open import Data.List.Base using (List; _∷_; [])
+  open import Data.List.Sort ≤-decTotalOrder using (sort)
+
+  test : List ℕ
+  test = sort (42 ∷ 0 ∷ 5 ∷ 3 ∷ [])
+  {-# COMPILE AGDA2LAMBOX test #-}
+
+-- -}

test/Map.agda

@@ -1,13 +1,17 @@
-open import Agda.Builtin.Nat
+open import Agda.Builtin.Nat using (Nat; suc; zero)
 open import Agda.Builtin.List
 
+double : Nat → Nat
+double zero = zero
+double (suc x) = suc (suc (double x))
+
 xs : List Nat
-xs = zero ∷ []
+xs = 1 ∷ 3 ∷ 5 ∷ []
 
 map : {A B : Set} -> (A → B) → List A → List B
 map f [] = []
 map f (x ∷ xs) = f x ∷ map f xs
 
 ys : List Nat
-ys = map (2 +_) xs
+ys = map double xs
 {-# COMPILE AGDA2LAMBOX ys #-}

test/Nat.agda

@@ -1,21 +1,6 @@
 open import Agda.Builtin.Nat
 
-one : Nat
-one = suc zero
+thing : Nat
+thing = 1 + 2
+{-# COMPILE AGDA2LAMBOX thing #-}
 
-{-
-add : Nat → Nat → Nat
-add zero y = y
-add (suc x) y = suc (add x y)
-
-incr : Nat → Nat
-incr = suc
-
-deux trois : Nat
-deux  = suc (suc zero)
-trois = suc (suc (suc zero))
-
-prog : Nat
-prog = add trois deux
-{-# COMPILE AGDA2LAMBOX prog #-}
--}

test/STLC.agda

@@ -1,58 +1,53 @@
+{-# OPTIONS --erasure #-}
 open import Agda.Builtin.Nat
 
--- we have to redefine addition on builtin nats
--- because the builtin _+_ doesn't compile yet
-add : Nat → Nat → Nat
-add zero y = y
-add (suc x) y = suc (add x y)
-
-variable n : Nat
+variable @0 n : Nat
 
 data Type : Set where
   ℕ   : Type
   _⇒_ : Type → Type → Type
 
-variable α β : Type
+variable @0 α β : Type
 
 infixl 7 _▷_
-data Ctx : Nat → Set where
+data Ctx : @0 Nat → Set where
   []  : Ctx zero
   _▷_ : Ctx n → Type → Ctx (suc n)
 
-variable Γ : Ctx n
+variable @0 Γ : Ctx n
 
 infix 6 _∋_
-data _∋_ : Ctx n → Type → Set where
+data _∋_ : @0 Ctx n → @0 Type → Set where
   here  :          Γ ▷ α ∋ α
   there : Γ ∋ α → Γ ▷ β ∋ α
 
-data Tm (Γ : Ctx n) : Type → Set where
-  var : Γ ∋ α → Tm Γ α
-  lam : Tm (Γ ▷ α) β → Tm Γ (α ⇒ β)
-  app : Tm Γ (α ⇒ β) → Tm Γ α → Tm Γ β
-
-  lit : Nat → Tm Γ ℕ
-  _`+_ : Tm Γ ℕ → Tm Γ ℕ → Tm Γ ℕ
+data _⊢_ (@0 Γ : Ctx n) : @0 Type → Set where
+  var  : Γ ∋ α → Γ ⊢ α
+  lam  : (Γ ▷ α) ⊢ β → Γ ⊢ (α ⇒ β)
+  app  : Γ ⊢ (α ⇒ β) → Γ ⊢ α → Γ ⊢ β
+  lit  : Nat → Γ ⊢ ℕ
+  plus : Γ ⊢ ℕ → Γ ⊢ ℕ → Γ ⊢ ℕ
 
-⟦_⟧ : Type → Set
-⟦ ℕ     ⟧ = Nat
-⟦ α ⇒ β ⟧ = ⟦ α ⟧ → ⟦ β ⟧
+Value : Type → Set
+Value ℕ       = Nat
+Value (α ⇒ β) = Value α → Value β
 
-data Env : Ctx n → Set where
+data Env : @0 Ctx n → Set where
   []  : Env []
-  _▷_ : Env Γ → ⟦ α ⟧ → Env (Γ ▷ α)
+  _▷_ : Env Γ → Value α → Env (Γ ▷ α)
 
-lookupEnv : Env Γ → Γ ∋ α → ⟦ α ⟧
+lookupEnv : Env Γ → Γ ∋ α → Value α
 lookupEnv (env ▷ x) here = x
 lookupEnv (env ▷ _) (there k) = lookupEnv env k
 
-eval : Env Γ → Tm Γ α → ⟦ α ⟧
-eval env (var k)   = lookupEnv env k
-eval env (lam u)   = λ x → eval (env ▷ x) u
-eval env (app u v) = eval env u (eval env v)
-eval env (lit x)   = x
-eval env (u `+ v)   = add (eval env u) (eval env v)
+eval : Env Γ → Γ ⊢ α → Value α
+eval env (var k)    = lookupEnv env k
+eval env (lam u)    = λ x → eval (env ▷ x) u
+eval env (app u v)  = eval env u (eval env v)
+eval env (lit x)    = x
+eval env (plus u v) = eval env u + eval env v
 
+-- (λ x → x + 1) 1
 test : Nat
-test = eval [] (app (lam (lit 1 `+ var here)) (lit 1))
+test = eval [] (app (lam (plus (lit 1) (var here))) (lit 1)) 
 {-# COMPILE AGDA2LAMBOX test #-}