Break up the builder script and add the math shell

This commit is contained in:
Sameer Rahmani 2024-01-26 20:20:46 +00:00
parent 99586477e0
commit 9b377a0a3a
Signed by: lxsameer
GPG Key ID: B0A4AF28AB9FD90B
8 changed files with 441 additions and 286 deletions

View File

@ -26,7 +26,7 @@
let
# Out zsh configuration directory. mkShell will pick up the .zshrc
# from this directory.
zshDir = ./scripts/zsh;
zshDir = ./scripts;
# Most of these overlays are do to bugs and problems
# in upstream nixpkgs. But thanks to their design
@ -89,7 +89,7 @@
else [];
});
libbsd = prev.libbsd.overrideAttrs (old: { #old.NIX_LDFLAGS ++
libbsd = prev.libbsd.overrideAttrs (old: { #old.NIX_LDFLAGS ++
NIX_LDFLAGS = if prev.stdenv.cc.isClang
then [ "--undefined-version" ]
else [];
@ -125,6 +125,8 @@
# Create a package set based on the build system
pkgs = utils.get_pkgs system overlays;
nativePkgs = import nixpkgs { inherit system overlays; };
# Create a stdenv based on LLVM 17
stdenv = pkgs.stdenvAdapters.overrideCC pkgs.stdenv pkgs.llvmPackages_17.clangUseLLVM;
@ -174,16 +176,19 @@
iwyu
]);
buildDevToolsDeps = (with pkgs; [
ccache
git'
python3
shellTools = (with pkgs; [
zsh
zsh-autosuggestions
zsh-autocomplete
zsh-syntax-highlighting
]);
buildDevToolsDeps = (with pkgs; [
ccache
git'
python3
]);
buildDeps = (with pkgs; [
gc
zlib'
@ -195,16 +200,37 @@
testDeps = (with pkgs; [
gtest
gmock
gbenchmark
]);
mathDeps = (with nativePkgs; [
idris2
agda
git
zsh
zsh-autosuggestions
zsh-autocomplete
zsh-syntax-highlighting
]);
in {
inherit pkgs;
devShells.default = (pkgs.mkShell.override { stdenv = stdenv';}) {
nativeBuildInputs = buildDevToolsDeps ++ buildToolsDeps;
nativeBuildInputs = buildDevToolsDeps ++ buildToolsDeps ++ shellTools;
buildInputs = buildDeps ++ testDeps;
shellHook =
''
ZDOTDIR=${zshDir} zsh -d && exit
BUILDER= ZDOTDIR=${zshDir} zsh -d && exit
'';
};
# This shell is gcc based and we use it only
# for the mathematics side of our design
devShells.math = nativePkgs.mkShell {
nativeBuildInputs = mathDeps;
shellHook =
''
BUILDER=math ZDOTDIR=${zshDir} zsh -d -i && exit
'';
};

92
scripts/.zshrc Normal file
View File

@ -0,0 +1,92 @@
#! /bin/zsh
# shellcheck disable=all
# Serene Programming Language
#
# Copyright (c) 2019-2024 Sameer Rahmani <lxsameer@gnu.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
mkdir -p "$HOME/.config/serene/"
export HISTFILE="$HOME/.config/serene/.zsh_history"
export HISTFILESIZE=500
export SAVEHIST=500
export HISTSIZE=500
setopt HIST_IGNORE_DUPS
setopt NO_HIST_BEEP
setopt PROMPT_SUBST
setopt NO_BEEP
setopt AUTO_CD
setopt CORRECT
setopt SHARE_HISTORY
setopt HIST_IGNORE_ALL_DUPS
setopt NO_ERR_EXIT
function user_prompt () {
if [ $UID != 0 ]; then
echo "%F{028}%F{002}> "
else
echo "%F{001}# "
fi
}
autoload -U colors && colors
autoload -Uz compinit
compinit
zstyle ':completion:*' auto-description 'specify: %d'
zstyle ':completion:*' completer _expand _complete _correct _approximate
zstyle ':completion:*' format 'Completing %d'
zstyle ':completion:*' group-name ''
if [ "$(uname 2> /dev/null)" = "Linux" ]; then
zstyle ':completion:*' menu select=2 eval "$(dircolors -b)"
fi
zstyle ':completion:*:default' list-colors ${(s.:.)LS_COLORS}
zstyle ':completion:*' list-colors ''
zstyle ':completion:*' list-prompt %SAt %p: Hit TAB for more, or the character to insert%s
zstyle ':completion:*' matcher-list '' 'm:{a-z}={A-Z}' 'm:{a-zA-Z}={A-Za-z}' 'r:|[._-]=* r:|=* l:|=*'
zstyle ':completion:*' menu select=long
zstyle ':completion:*' select-prompt %SScrolling active: current selection at %p%s
zstyle ':completion:*' use-compctl false
zstyle ':completion:*' verbose true
zstyle ':completion:*:*:kill:*:processes' list-colors '=(#b) #([0-9]#)*=0=01;31'
zstyle ':completion:*:kill:*' command 'ps -u $USER -o pid,%cpu,tty,cputime,cmd'
echo "Welcome to serene's development environment"
PROMPT='
%F{015}[%F{099}SERENE%F{015}][%F{198}$(git branch --show-current)%F{015}]
%F{005}%~%F{003} $(user_prompt)%f'
echo -e "\nSerene Development Shell $VERSION"
echo -e "\nCopyright (C) 2019-2024"
echo -e "Sameer Rahmani <lxsameer@gnu.org>"
echo -e "Serene comes with ABSOLUTELY NO WARRANTY;"
echo -e "This is free software, and you are welcome"
echo -e "to redistribute it under certain conditions;"
echo -e "for details take a look at the LICENSE file.\n"
echo -e "\nUse the 'help' command to view a list of helpers.\n"
ME=$(cd "$(dirname "$0")/." >/dev/null 2>&1 ; pwd -P)
export ME
VERSION="0.9.0"
. "$ME/scripts/${BUILDER}functions.sh"
export PROMPT

View File

@ -1,142 +0,0 @@
#! /bin/bash
# Serene Programming Language
#
# Copyright (c) 2019-2024 Sameer Rahmani <lxsameer@gnu.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# -----------------------------------------------------------------------------
# Commentary
# -----------------------------------------------------------------------------
# This file installs all the dependencies on the guest container during the
# devfs initialization.
set -e
# shellcheck source=/dev/null
source /serene/scripts/utils.sh
function install_llvm() {
wget https://apt.llvm.org/llvm.sh -O /root/llvm.sh
chmod +x llvm.sh
/root/llvm.sh "${LLVM_VERSION}" all
apt-get update --fix-missing
apt-get install -y --no-install-recommends \
mlir-"${LLVM_VERSION}"-tools \
libmlir-"${LLVM_VERSION}"-dev \
libmlir-"${LLVM_VERSION}" \
libmlir-"${LLVM_VERSION}"-dbgsym \
liblld-"${LLVM_VERSION}" \
liblld-"${LLVM_VERSION}"-dev \
clang-format-"${LLVM_VERSION}" \
clang-tidy-"${LLVM_VERSION}"
ln -s "$(which lld-"${LLVM_VERSION}")" /usr/bin/lld
ln -s "$(which clang-"${LLVM_VERSION}")" /usr/bin/clang
ln -s "$(which clang++-"${LLVM_VERSION}")" /usr/bin/clang++
ln -s "$(which clang-format-"${LLVM_VERSION}")" /usr/bin/clang-format
ln -s "$(which clang-tidy-"${LLVM_VERSION}")" /usr/bin/clang-tidy
ln -s "$(which mlir-tblgen-"${LLVM_VERSION}")" /usr/bin/mlir-tblgen
MLIR_DIR="/usr/lib/llvm-${LLVM_VERSION}"
CMAKE_PREFIX_PATH="/usr/lib/llvm-${LLVM_VERSION}"
LD_LIBRARY_PATH="/usr/lib/llvm-${LLVM_VERSION}/lib/clang/${LLVM_VERSION}.0.0/lib/linux/"
CC=/usr/bin/clang
CXX=/usr/bin/clang++
}
function install_iwuy() {
mkdir -p /opt/iwuy
pushd /opt/iwuy
git clone https://github.com/include-what-you-use/include-what-you-use.git --depth 1
mkdir build
pushd build
cmake -G Ninja -DCMAKE_PREFIX_PATH="/usr/lib/llvm-${LLVM_VERSION}" ../include-what-you-use
cmake --build .
cmake -P cmake_install.cmake
popd
popd
rm -rf /opt/iwuy
}
function install_boehm() {
mkdir -p /opt/boehm
pushd /opt/boehm
git clone https://github.com/ivmai/bdwgc.git --depth 1 --branch v8.2.0
mkdir build
pushd build
cmake -G Ninja -DBUILD_SHARED_LIBS=OFF -Denable_cplusplus=ON -Denable_threads=ON \
-Denable_gcj_support=OFF -Dinstall_headers=ON \
-DCMAKE_POSITION_INDEPENDENT_CODE=ON ../bdwgc
cmake --build . --config Release
cmake -P cmake_install.cmake
popd
popd
rm -rf /opt/boehm
}
function main() {
pushd "/root"
apt-get update
apt-get install --no-install-recommends -y \
gnupg \
cmake \
ccache \
git \
ninja-build \
binutils \
lsb-release \
wget \
software-properties-common \
zlib1g \
cppcheck \
sudo \
shellcheck \
zlib1g-dev
install_llvm
install_iwuy
install_boehm
popd
info "Enabling passwordless sudo"
sed 's/%sudo.*/%sudo ALL=(ALL) NOPASSWD:ALL/' -i /etc/sudoers
apt-get autoremove -y
apt-get clean
}
if [ ! -f "/etc/llvm_version" ]; then
error "Can't find '/etc/llvm_version' on the container"
exit 1
fi
export LANG=C.UTF-8
export LLVM_VERSION
export MLIR_DIR
export CMAKE_PREFIX_PATH
export LD_LIBRARY_PATH
export CC
export CXX
LLVM_VERSION=$(cat /etc/llvm_version)
main

253
scripts/functions.sh Normal file
View File

@ -0,0 +1,253 @@
#! /bin/sh
# shellcheck disable=all
# Serene Programming Language
#
# Copyright (c) 2019-2024 Sameer Rahmani <lxsameer@gnu.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
#
# -----------------------------------------------------------------------------
# Commentary
# -----------------------------------------------------------------------------
# This is the builder script for the Serene project. It makes it easier to
# interact with the CMake build scripts.
#
# In order to define a subcommand all you need to do is to define a function
# with the following syntax:
#
# function subcommand-name() { ## DESCRIPTION
# .. subcommand body ..
# }
#
# Make sure to provid one line of DESCRIPTION for the subcommand and use two "#"
# characters to start the description following by a space. Otherwise, your
# subcommand won't be registered
#
# shellcheck source=./utils.sh
source "$ME/scripts/utils.sh"
# -----------------------------------------------------------------------------
# CONFIG VARS
# -----------------------------------------------------------------------------
# By default Clang is the compiler that we use and support. But you may use
# whatever you want. But just be aware of the fact that we might not be able
# to help you in case of any issue.
if [[ "$CC" = "" ]]; then
CC=$(which clang || echo "Clang_not_found")
export CC
fi
if [[ "$CXX" = "" ]]; then
CXX=$(which clang++ || echo "Clang++_not_found")
export CXX
fi
BUILD_DIR_NAME="build"
export BUILD_DIR_NAME
BUILD_DIR="$ME/$BUILD_DIR_NAME"
export BUILD_DIR
SERENE_HOME_DIR="$HOME/.serene"
export SERENE_HOME_DIR
# Serene subprojects. We use this array to run common tasks on all the projects
# like running the test cases
PROJECTS=(libserene serenec serene-repl serene-tblgen)
# TODO: Add sloppiness to the cmake list file as well
CCACHE_SLOPPINESS="pch_defines,time_macros"
export CCACHE_SLOPPINESS
ASAN_OPTIONS=check_initialization_order=1
export ASAN_OPTIONS
LSAN_OPTIONS=suppressions="$ME/.ignore_sanitize"
export LSAN_OPTIONS
# -----------------------------------------------------------------------------
# Helper functions
# -----------------------------------------------------------------------------
function gen_precompile_header_index() {
{
echo "// DO NOT EDIT THIS FILE: It is aute generated by './builder gen_precompile_index'"
echo "#ifndef SERENE_PRECOMPIL_H"
echo "#define SERENE_PRECOMPIL_H"
grep -oP "#include .llvm/.*" . -R|cut -d':' -f2|tail +2
grep -oP "#include .mlir/.*" . -R|cut -d':' -f2|tail +2
echo "#endif"
} > ./include/serene_precompiles.h
}
function pushed_build() {
mkdir -p "$BUILD_DIR"
pushd "$BUILD_DIR" > /dev/null || return
}
function popd_build() {
popd > /dev/null || return
}
function build-gen() {
local args
args=(
)
pushed_build
info "Running: "
info "cmake -G Ninja" "${args[@]}" "$ME" "${@:2}"
cmake -G Ninja "${args[@]}" \
"$ME" \
"${@:2}"
popd_build
}
# -----------------------------------------------------------------------------
# Subcomaands
# -----------------------------------------------------------------------------
function compile() { ## Compiles the project using the generated build scripts
pushed_build
cmake --build . --parallel
popd_build
}
function build() { ## Builds the project by regenerating the build scripts
local cpus
rm -rf "$BUILD_DIR"
build-gen "debug" "$@"
pushed_build
cpus=$(nproc)
cmake --build . -j "$cpus"
popd_build
}
function build-20() { ## Builds the project using C++20 (will regenerate the build)
rm -rf "$BUILD_DIR"
pushed_build
build-gen "debug" -DCPP_20_SUPPORT=ON "$@"
cmake --build .
popd_build
}
function build-tidy() { ## Builds the project using clang-tidy (It takes longer than usual)
build "-DSERENE_ENABLE_TIDY=ON" "${@:2}"
}
function build-release() { ## Builds the project in "Release" mode
rm -rf "$BUILD_DIR"
pushed_build
build-gen "release" "$@"
cmake --build . --config Release
popd_build
}
function build-docs() { ## Builds the documentation of Serene
rm -rf "$BUILD_DIR"
pip install -r "$ME/docs/requirements.txt"
pushed_build
build-gen "debug" -DSERENE_ENABLE_DOCS=ON "$@"
cmake --build . --parallel
popd_build
}
function serve-docs() { ## Serve the docs directory from build dir
python -m http.server --directory "$BUILD_DIR/docs/sphinx/"
}
function clean() { ## Cleans up the source dir and removes the build
git clean -dxf
}
function run() { ## Runs `serene` and passes all the given aruguments to it
"$BUILD_DIR"/serene/serene "$@"
}
function lldb-run() { ## Runs `serenec` under lldb
lldb -- "$BUILD_DIR"/serenec/serenec "$@"
}
function repl() { ## Runs `serene-repl` and passes all the given aruguments to it
"$BUILD_DIR"/serene-repl/serene-repl "$@"
}
function memcheck-serene() { ## Runs `valgrind` to check `serenec` birany
export ASAN_FLAG=""
build
pushed_build
valgrind --tool=memcheck --leak-check=yes --trace-children=yes "$BUILD_DIR"/bin/serenec "$@"
popd_build
}
function tests() { ## Runs all the test cases
if [[ "$1" == "all" || "$1" == "" ]]; then
info "Run the entire test suit"
for proj in "${PROJECTS[@]}"; do
local test_file="$BUILD_DIR/$proj/tests/${proj}Tests"
if [[ -f "$test_file" ]]; then
eval "$test_file ${*:2}"
fi
done
else
eval "$BUILD_DIR/$1/tests/$1Tests ${*:2}"
fi
}
function build-tests() { ## Generates and build the project including the test cases
rm -rf "$BUILD_DIR"
pushed_build
build-gen "debug" -DSERENE_BUILD_TESTING=ON "$@"
cmake --build . --parallel
popd_build
}
function setup() { ## Setup the working directory and make it ready for development
local args
if [[ "$SERENE_CI" == "true" ]]; then
args=--break-system-packages
fi
if command -v python3 >/dev/null 2>&1; then
pip install "$args" pre-commit
pre-commit install
else
error "Python is required to setup pre-commit"
fi
}
function scan-build() { ## Runs the `scan-build` utility to analyze the build process
rm -rf "$BUILD_DIR"
build-gen
pushed_build
# The scan-build utility scans the build for bugs checkout the man page
scan-build --force-analyze-debug-code --use-analyzer="$CC" cmake --build .
popd_build
}
function help() { ## Print out this help message
echo "Commands:"
grep -E '^function [a-zA-Z0-9_-]+\(\) \{ ## .*$$' "$ME/scripts/functions.sh" | \
sort | \
sed 's/^function \([a-zA-Z0-9_-]*\)() { ## \(.*\)/\1:\2/' | \
awk 'BEGIN {FS=":"}; {printf "\033[36m%-30s\033[0m %s\n", $1, $2}'
}

49
scripts/mathfunctions.sh Normal file
View File

@ -0,0 +1,49 @@
#! /bin/sh
# shellcheck disable=all
# Serene Programming Language
#
# Copyright (c) 2019-2024 Sameer Rahmani <lxsameer@gnu.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
#
# -----------------------------------------------------------------------------
# Commentary
# -----------------------------------------------------------------------------
# This is the builder script for the Serene project. It makes it easier to
# interact with the CMake build scripts.
#
# In order to define a subcommand all you need to do is to define a function
# with the following syntax:
#
# function subcommand-name() { ## DESCRIPTION
# .. subcommand body ..
# }
#
# Make sure to provid one line of DESCRIPTION for the subcommand and use two "#"
# characters to start the description following by a space. Otherwise, your
# subcommand won't be registered
#
# shellcheck source=./utils.sh
source "$ME/scripts/utils.sh"
function help() { ## Print out this help message
echo "Commands:"
grep -E '^function [a-zA-Z0-9_-]+\(\) \{ ## .*$$' "$ME/scripts/mathfunctions.sh" | \
sort | \
sed 's/^function \([a-zA-Z0-9_-]*\)() { ## \(.*\)/\1:\2/' | \
awk 'BEGIN {FS=":"}; {printf "\033[36m%-30s\033[0m %s\n", $1, $2}'
}

View File

@ -15,7 +15,6 @@
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
set -e
# -----------------------------------------------------------------------------
# Helper functions
@ -71,66 +70,3 @@ function get_version() {
git ls-tree HEAD "$1" | awk '{ print $3 }'
}
function http_push() {
if [[ -z "$DEV_HEROES_TOKEN" ]]; then
error "\$DEV_HEROES_TOKEN is not set."
exit 1
fi
local pkg_name
local version
pkg_name="$1"
version="$2"
curl "$DEV_HEROES/api/packages/serene/generic/$pkg_name/$version/$pkg_name.$version.zstd" \
--upload-file "$pkg_name.$version.zstd" \
--progress-bar \
-H "accept: application/json" \
-H "Authorization: token $DEV_HEROES_TOKEN" \
-H "Content-Type: application/json"
}
function http_pull() {
local pkg_name
local version
local output
local url
pkg_name="$1"
version="$2"
output="$3"
url="$DEV_HEROES/api/packages/serene/generic/$pkg_name/$version/$pkg_name.$version.tar.zstd"
info "Fetching '$url'..."
if curl "$url" --fail --progress-bar -o "$output"; then
return 0
else
return 4
fi
}
function clone_dep() {
local dest
local repo
local version
repo="$1"
version="$2"
dest="$3"
if [[ -d "$dest" ]]; then
return
fi
#mkdir -p "$dest"
#git init -b master
git clone --depth=1 "$repo" "$dest"
_push "$dest"
#git remote add origin "$repo"
git fetch --depth=1 --filter=tree:0 origin "$version"
git reset --hard FETCH_HEAD
_pop
}

View File

@ -1,72 +0,0 @@
#! /bin/zsh
# shellcheck disable=all
# Serene Programming Language
#
# Copyright (c) 2019-2024 Sameer Rahmani <lxsameer@gnu.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, version 2.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
mkdir -p "$HOME/.config/serene/"
export HISTFILE="$HOME/.config/serene/.zsh_history"
export HISTFILESIZE=500
export SAVEHIST=500
export HISTSIZE=500
setopt HIST_IGNORE_DUPS
setopt NO_HIST_BEEP
setopt PROMPT_SUBST
setopt NO_BEEP
setopt AUTO_CD
setopt CORRECT
setopt SHARE_HISTORY
setopt HIST_IGNORE_ALL_DUPS
function user_prompt () {
if [ $UID != 0 ]; then
echo "%F{028}%F{002}> "
else
echo "%F{001}# "
fi
}
autoload -U colors && colors
autoload -Uz compinit
compinit
# zstyle ':completion:*' auto-description 'specify: %d'
# zstyle ':completion:*' completer _expand _complete _correct _approximate
# zstyle ':completion:*' format 'Completing %d'
# zstyle ':completion:*' group-name ''
# if [ "$(uname 2> /dev/null)" = "Linux" ]; then
# zstyle ':completion:*' menu select=2 eval "$(dircolors -b)"
# fi
# zstyle ':completion:*:default' list-colors ${(s.:.)LS_COLORS}
# zstyle ':completion:*' list-colors ''
# zstyle ':completion:*' list-prompt %SAt %p: Hit TAB for more, or the character to insert%s
# zstyle ':completion:*' matcher-list '' 'm:{a-z}={A-Z}' 'm:{a-zA-Z}={A-Za-z}' 'r:|[._-]=* r:|=* l:|=*'
# zstyle ':completion:*' menu select=long
# zstyle ':completion:*' select-prompt %SScrolling active: current selection at %p%s
# zstyle ':completion:*' use-compctl false
# zstyle ':completion:*' verbose true
# zstyle ':completion:*:*:kill:*:processes' list-colors '=(#b) #([0-9]#)*=0=01;31'
# zstyle ':completion:*:kill:*' command 'ps -u $USER -o pid,%cpu,tty,cputime,cmd'
echo "Welcome to serene's development environment"
PROMPT='
%F{015}[%F{099}SERENE%F{015}][%F{198}$(git branch --show-current)%F{015}]
%F{005}%~%F{003} $(user_prompt)%f'
export PROMPT

View File

@ -23,6 +23,19 @@
#include <cstdint>
// Steps for defining a new type:
// 1. Define the type former
// 2. Type constructors
// 3. Type eliminators
// 4. Computation rule (eval rules)
// 5. (optional) A uniqueness principle
// Types to create:
// Universe
// Unit Type
// Dependent Function Type
// Pair (or even better, records)
typedef struct {
const TypeID id;
const char *name;