Add support for built in types (#192)

* match inductive definitions

* progress towards builtins

* more progress towards builtin types

* add more builtins

* add some errors

* add reverse table to builtins

* Squashed commit of the following:

commit 93333de502d8dd546eb8edf697ca7eef972ea105
Author: Paul Cadman <git@paulcadman.dev>
Date:   Mon Jun 27 18:21:30 2022 +0100

    Use builtin names for match and project functions

    Add an implementation of nat for the standalone backend

commit 868d2098ee57b7acbca84512b6e096650eeeb22d
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Mon Jun 27 18:15:29 2022 +0200

    add builtin information to ClosureInfo

commit 32c78aceb19ee4010d66090a3c4e6025621b5c1f
Author: Paul Cadman <git@paulcadman.dev>
Date:   Mon Jun 27 12:52:10 2022 +0100

    Refactor BuiltinEnum to sum type of each Builtin

commit 55bb72ab12a8fb7d10070c2dee5875482453b7c6
Author: Paul Cadman <git@paulcadman.dev>
Date:   Fri Jun 24 14:44:28 2022 +0100

    Add Builtin information to Mono InfoTable

commit a72368f2e3af20baaf44c5e21fa7e6a469cf1ac5
Author: Paul Cadman <git@paulcadman.dev>
Date:   Fri Jun 24 14:41:51 2022 +0100

    Add Bitraversable to Prelude

commit afa3153d82a9509b0882e7ca99830040fad9ef65
Author: Paul Cadman <git@paulcadman.dev>
Date:   Fri Jun 24 14:41:39 2022 +0100

    Remove unused import

commit ea0b7848fb80970e03a0561be3fb4448486a89a9
Author: Paul Cadman <git@paulcadman.dev>
Date:   Thu Jun 23 13:54:58 2022 +0100

    Use projection functions instead of direct member access

* Avoid shadowing C runtime names in foreign block

* Fix formatting

* Update C names for builtin functions

* Add prim_ prefix to builtin C names

Implement builtins for standalone and libc backends

* Update ormolu action

* ci: run all tests for draft PRs

Co-authored-by: Paul Cadman <git@paulcadman.dev>

.github/workflows/ci.yml

@@ -17,14 +17,6 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  not-a-draft:
-    runs-on: ubuntu-latest
-    if: github.event.pull_request.draft == true
-    steps:
-      - name: Fails in order to indicate that pull request needs to be marked as
-              ready to review.
-        run: exit 1
-
   docs:
     if: github.event.pull_request.merged == true
     runs-on: ubuntu-latest
@@ -55,7 +47,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
-      - uses: mrkkrp/ormolu-action@v5
+      - uses: mrkkrp/ormolu-action@v6
         with:
           extra-args: >-
             --ghc-opt -XDerivingStrategies

app/Commands/Compile.hs

@@ -109,10 +109,13 @@ prepareRuntime projRoot o = do
     libCRuntimeDir :: [(FilePath, BS.ByteString)]
     libCRuntimeDir = $(FE.makeRelativeToProject "minic-runtime/libc" >>= FE.embedDir)
 
+    builtinCRuntimeDir :: [(FilePath, BS.ByteString)]
+    builtinCRuntimeDir = $(FE.makeRelativeToProject "minic-runtime/builtins" >>= FE.embedDir)
+
     runtimeProjectDir :: [(FilePath, BS.ByteString)]
     runtimeProjectDir = case o ^. compileRuntime of
-      RuntimeStandalone -> standaloneRuntimeDir
-      RuntimeLibC -> libCRuntimeDir
+      RuntimeStandalone -> standaloneRuntimeDir <> builtinCRuntimeDir
+      RuntimeLibC -> libCRuntimeDir <> builtinCRuntimeDir
 
     writeRuntime :: (FilePath, BS.ByteString) -> IO ()
     writeRuntime (filePath, contents) =

docs/org/notes/builtins.org

@@ -0,0 +1,70 @@
+#+title: Builtins
+#+author: Jan Mas Rovira
+
+* Overview
+
+The goal is to support builtin types and functions that get compiled to
+efficient primitives. We plan on supporting primitives for the following types
+of definitions:
+
+1. Builtin inductive definitions. For example:
+   #+begin_example
+   builtin natural
+   inductive Nat {
+     zero : Nat;
+     suc : Nat → Nat;
+   };
+   #+end_example
+   We will call this the canonical definition of natural numbers.
+
+2. Builtin function definitions. For example:
+   #+begin_src text
+   inifl 6 +;
+   builtin natural-plus
+   + : Nat → Nat → Nat;
+   + zero b ≔ b;
+   + (suc a) b ≔ suc (a + b);
+   #+end_src
+
+3. Builtin axiom definitions. For example:
+   #+begin_src text
+   builtin natural-print
+   axiom printNat : Nat → Action;
+   #+end_src
+
+** Collecting builtin information
+
+The idea is that builtin definitions are treated normally throughout the
+pipeline except in the backend part. There is one exception to that. We need to
+collect information about the builtins that have been included in the code and
+what are the terms that refer to them. For instance, imagine that we find this
+definitions in a minijuvix module:
+#+begin_src text
+builtin natural
+inductive MyNat {
+    z : MyNat;
+    s : MyNat → MyNat;
+};
+#+end_src
+We need to take care of the following:
+1. Check that the definition =MyInt= is up to renaming equal to the canonical
+   definition that we provide in the compiler.
+2. Rember a map from concrete to canonical names: {MyNat ↦ Nat; z ↦ zero; s ↦ suc};
+3. Rembember that we have a definition for builtin natural numbers. This is
+   necessary if later we attempt to define a builtin function or axiom that
+   depends on natural numbers.
+
+
+In the compiler we need to know the following:
+1. For inductives:
+   1. What is the primitive type that we will target in the backend: E.g. {Nat ↦ int}.
+   2. For constructors:
+      1. What is the primitive constructor function: E.g. {zero ↦ 0; suc ↦ plus_one};
+      2. How to test if a term matches a pattern with that constructor.
+         E.g. {zero ↦ is_zero; suc ↦ is_not_zero};
+      3. How to deconstruct/project each of the constructor arguments. E.g. {zero ↦
+         ∅; suc ↦ minus_one}}. Note that if a constructor takes multiple arguments
+         we will need to have a projection function for each argument.
+2. For functions and axioms:
+   1. What is the primitive function that we will target in the backend: E.g. {+
+      ↦ add}.

minic-runtime/builtins/io.h

@@ -0,0 +1,10 @@
+#ifndef IO_H_
+#define IO_H_
+
+typedef int prim_io;
+
+prim_io prim_sequence(prim_io a, prim_io b) {
+    return a + b;
+}
+
+#endif // IO_H_

minic-runtime/builtins/nat.h

@@ -0,0 +1,31 @@
+#ifndef NAT_H_
+#define NAT_H_
+
+#include <stdbool.h>
+
+typedef int prim_nat;
+
+#define prim_zero 0
+
+prim_nat prim_suc(prim_nat n) {
+    return n + 1;
+}
+
+bool is_prim_zero(prim_nat n) {
+    return n == 0;
+}
+
+bool is_prim_suc(prim_nat n) {
+    return n != 0;
+}
+
+prim_nat proj_ca0_prim_suc(prim_nat n) {
+    return n - 1;
+}
+
+prim_nat prim_natplus(prim_nat a, prim_nat b) {
+    return a + b;
+}
+
+
+#endif // NAT_H_

minic-runtime/libc/minic-runtime.h

@@ -5,6 +5,9 @@
 #include <stdio.h>
 #include <string.h>
 
+#include "nat.h"
+#include "io.h"
+
 typedef __UINTPTR_TYPE__ uintptr_t;
 
 typedef struct minijuvix_function {
@@ -90,4 +93,8 @@ int putStrLn(const char* str) {
     return fflush(stdout);
 }
 
+prim_io prim_printNat(prim_nat n) {
+    return putStrLn(intToStr(n));
+}
+
 #endif // MINIC_RUNTIME_H_

minic-runtime/standalone/minic-runtime.h

@@ -1,6 +1,9 @@
 #ifndef MINIC_RUNTIME_H_
 #define MINIC_RUNTIME_H_
 
+#include "nat.h"
+#include "io.h"
+
 typedef __SIZE_TYPE__ size_t;
 typedef __UINT8_TYPE__ uint8_t;
 typedef __UINT16_TYPE__ uint16_t;
@@ -182,6 +185,10 @@ int putStrLn(const char* str) {
     return putStr(str) || putStr("\n");
 }
 
+prim_io prim_printNat(prim_nat n) {
+    return putStrLn(intToStr(n));
+}
+
 // Tries to parse str as a positive integer.
 // Returns -1 if parsing fails.
 int parsePositiveInt(char *str) {

src/MiniJuvix/Builtins.hs

@@ -0,0 +1,10 @@
+module MiniJuvix.Builtins
+  ( module MiniJuvix.Builtins.Effect,
+    module MiniJuvix.Builtins.Natural,
+    module MiniJuvix.Builtins.IO,
+  )
+where
+
+import MiniJuvix.Builtins.Effect
+import MiniJuvix.Builtins.IO
+import MiniJuvix.Builtins.Natural

src/MiniJuvix/Builtins/Base.hs

@@ -0,0 +1,30 @@
+module MiniJuvix.Builtins.Base
+  ( module MiniJuvix.Builtins.Base,
+  )
+where
+
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+
+data BuiltinsEnum
+  = BuiltinsNatural
+  | BuiltinsZero
+  | BuiltinsSuc
+  | BuiltinsNaturalPlus
+  | BuiltinsNaturalPrint
+  | BuiltinsIO
+  | BuiltinsIOSequence
+  deriving stock (Show, Eq, Generic)
+
+instance Hashable BuiltinsEnum
+
+instance Pretty BuiltinsEnum where
+  pretty = \case
+    BuiltinsNatural -> Str.natural
+    BuiltinsZero -> "zero"
+    BuiltinsSuc -> "suc"
+    BuiltinsNaturalPlus -> Str.naturalPlus
+    BuiltinsNaturalPrint -> Str.naturalPrint
+    BuiltinsIO -> Str.io
+    BuiltinsIOSequence -> Str.ioSequence

src/MiniJuvix/Builtins/Effect.hs

@@ -0,0 +1,64 @@
+module MiniJuvix.Builtins.Effect
+  ( module MiniJuvix.Builtins.Effect,
+  )
+where
+
+import MiniJuvix.Builtins.Error
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+
+data Builtins m a where
+  GetBuiltinName' :: Interval -> BuiltinPrim -> Builtins m Name
+  -- GetBuiltin :: Name -> Builtins m (Maybe BuiltinPrims)
+  RegisterBuiltin' :: BuiltinPrim -> Name -> Builtins m ()
+
+makeSem ''Builtins
+
+registerBuiltin :: (IsBuiltin a, Member Builtins r) => a -> Name -> Sem r ()
+registerBuiltin = registerBuiltin' . toBuiltinPrim
+
+getBuiltinName :: (IsBuiltin a, Member Builtins r) => Interval -> a -> Sem r Name
+getBuiltinName i = getBuiltinName' i . toBuiltinPrim
+
+data BuiltinsState = BuiltinsState
+  { _builtinsTable :: HashMap BuiltinPrim Name,
+    _builtinsNameTable :: HashMap Name BuiltinPrim
+  }
+
+makeLenses ''BuiltinsState
+
+iniState :: BuiltinsState
+iniState = BuiltinsState mempty mempty
+
+re :: forall r a. Member (Error MiniJuvixError) r => Sem (Builtins ': r) a -> Sem (State BuiltinsState ': r) a
+re = reinterpret $ \case
+  GetBuiltinName' i b -> fromMaybeM notDefined (gets (^. builtinsTable . at b))
+    where
+      notDefined :: Sem (State BuiltinsState : r) x
+      notDefined =
+        throw $
+          MiniJuvixError
+            NotDefined
+              { _notDefinedBuiltin = b,
+                _notDefinedLoc = i
+              }
+  -- GetBuiltin n -> gets (^. builtinsNameTable . at n)
+  RegisterBuiltin' b n -> do
+    s <- gets (^. builtinsTable . at b)
+    case s of
+      Nothing -> do
+        modify (over builtinsTable (set (at b) (Just n)))
+        modify (over builtinsNameTable (set (at n) (Just b)))
+      Just {} -> alreadyDefined
+    where
+      alreadyDefined :: Sem (State BuiltinsState : r) x
+      alreadyDefined =
+        throw $
+          MiniJuvixError
+            AlreadyDefined
+              { _alreadyDefinedBuiltin = b,
+                _alreadyDefinedLoc = getLoc n
+              }
+
+runBuiltins :: Member (Error MiniJuvixError) r => Sem (Builtins ': r) a -> Sem r a
+runBuiltins = evalState iniState . re

src/MiniJuvix/Builtins/Error.hs

@@ -0,0 +1,45 @@
+module MiniJuvix.Builtins.Error where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+import MiniJuvix.Syntax.Concrete.Builtins
+import MiniJuvix.Termination.Error.Pretty
+
+data AlreadyDefined = AlreadyDefined
+  { _alreadyDefinedBuiltin :: BuiltinPrim,
+    _alreadyDefinedLoc :: Interval
+  }
+
+makeLenses ''AlreadyDefined
+
+hh :: Doc Eann -> Doc Eann
+hh = annotate Highlight
+
+instance ToGenericError AlreadyDefined where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = e ^. alreadyDefinedLoc
+      msg = "The builtin" <+> hh (pretty (e ^. alreadyDefinedBuiltin)) <+> "has already been defined"
+
+data NotDefined = NotDefined
+  { _notDefinedBuiltin :: BuiltinPrim,
+    _notDefinedLoc :: Interval
+  }
+
+makeLenses ''NotDefined
+
+instance ToGenericError NotDefined where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = e ^. notDefinedLoc
+      msg = "The builtin" <+> hh (pretty (e ^. notDefinedBuiltin)) <+> "has not been defined"

src/MiniJuvix/Builtins/IO.hs

@@ -0,0 +1,16 @@
+module MiniJuvix.Builtins.IO where
+
+import MiniJuvix.Builtins.Effect
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+
+registerIO :: Member Builtins r => AxiomDef -> Sem r ()
+registerIO d = do
+  unless (d ^. axiomType === smallUniverse) (error "IO should be in the small universe")
+  registerBuiltin BuiltinIO (d ^. axiomName)
+
+registerIOSequence :: Member Builtins r => AxiomDef -> Sem r ()
+registerIOSequence d = do
+  io <- getBuiltinName (getLoc d) BuiltinIO
+  unless (d ^. axiomType === (io --> io --> io)) (error "IO sequence have type IO → IO")
+  registerBuiltin BuiltinIOSequence (d ^. axiomName)