diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | makefile | 23 | ||||
| -rw-r--r-- | readme.md | 38 | ||||
| -rw-r--r-- | src/main.c | 1 | ||||
| -rw-r--r-- | src/parse.c | 3 | ||||
| -rw-r--r-- | src/term.c | 3 |
6 files changed, 55 insertions, 14 deletions
@@ -1,3 +1,4 @@ +.cache/ build/ tags @@ -6,10 +6,10 @@ LD = ld TG = ctags BUILD = $(PWD)/build -SRC = ./src -INC = ./inc -SRCS = $(shell find $(SRC) -name '*.c') -OBJS = $(SRCS:%=$(BUILD)/%.o) +SRC = $(PWD)/src +INC = $(PWD)/inc +SRCS = $(wildcard $(SRC)/*.c) +OBJS = $(patsubst $(SRC)/%.c, $(BUILD)/%.o, $(SRCS)) # I need the following on my machine. Look it up though before using it. # export ASAN_OPTIONS=verify_asan_link_order=0 @@ -17,22 +17,23 @@ CFLAGS_DEBUG = -Wno-error -ggdb3 -Og -Wno-unused -fsanitize=address -fsanitize=u CFLAGS_WARNINGS = -Wall -Wextra -Werror -Wshadow -Wpointer-arith -Wwrite-strings -Wredundant-decls -Wnested-externs -Wformat=2 -Wmissing-declarations -Wstrict-prototypes -Wmissing-prototypes -Wcast-qual -Wswitch-default -Wswitch-enum -Wunreachable-code -Wundef -Wold-style-definition -Wvla -pedantic -Wno-switch-enum CFLAGS = $(CFLAGS_WARNINGS) -std=c99 -fno-profile-generate -fno-omit-frame-pointer -fno-common -fno-asynchronous-unwind-tables -mno-red-zone -Ofast -D_DEFAULT_SOURCE -I$(INC) $(CFLAGS_DEBUG) -all: $(BUILD) $(OBJS) $(BUILD)/milcr -compile: all sync +all: compile sync + +compile: $(BUILD) $(OBJS) $(BUILD)/milcr clean: @rm -rf $(BUILD)/* sync: # Ugly hack - @$(MAKE) --always-make --dry-run | grep -wE 'gcc' | jq -nR '[inputs|{directory: ".", command: ., file: match(" [^ ]+$$").string[1:]}]' >compile_commands.json & - @$(TG) -R --exclude=.git --exclude=build . & + @$(MAKE) $(BUILD)/milcr --always-make --dry-run | grep -wE 'gcc|g\+\+' | grep -w '\-c' | jq -nR '[inputs|{directory:".", command:., file: match(" [^ ]+$$").string[1:]}]' >compile_commands.json + @$(TG) -R --exclude=.git --exclude=build . -$(BUILD)/%.c.o: %.c - @$(CC) -c $(CFLAGS) $< -o $(patsubst $(BUILD)/$(SRC)/%.c.o,$(BUILD)/%.o,$@) +$(BUILD)/%.o: $(SRC)/%.c + @$(CC) -c -o $@ $(CFLAGS) $< $(BUILD)/milcr: $(OBJS) - $(CC) $(CFLAGS) $(patsubst $(BUILD)/$(SRC)/%.c.o,$(BUILD)/%.o,$^) -o $@ + @$(CC) -o $@ $(CFLAGS) $^ .PHONY: all compile clean sync @@ -1,3 +1,39 @@ # MILCR -> **M**ultithreaded **I**nteraction net **L**ambda **C**alculus **R**educer +> **M**ultithreaded graphically-**I**nduced **L**ambda **C**alculus +> **R**educer + +- Strong reduction (reduction inside abstractions) of call-by-need + lambda calculus +- Originally intended as reducer of the `bruijn` programming language +- Useful for proof assistants or as a high-level lambda-term reducer + of functional programming languages +- Based on bleeding-edge research results + +## Research + +In no particular order: + +0. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and + efficient implementation of strong call by need by an abstract + machine. Proceedings of the ACM on Programming Languages, 6(ICFP), + 109-136. +1. Accattoli, B., Condoluci, A., & Coen, C. S. (2021, June). Strong + call-by-value is reasonable, implosively. In 2021 36th Annual + ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 1-14). + IEEE. +2. Balabonski, T., Lanco, A., & Melquiond, G. (2021). A strong + call-by-need calculus. arXiv preprint arXiv:2111.01485. +3. Accattoli, B., Condoluci, A., Guerrieri, G., & Coen, C. S. (2019, + October). Crumbling abstract machines. In Proceedings of the 21st + International Symposium on Principles and Practice of Declarative + Programming (pp. 1-15). +4. Accattoli, B., & Coen, C. S. (2015, July). On the relative + usefulness of fireballs. In 2015 30th Annual ACM/IEEE Symposium on + Logic in Computer Science (pp. 141-155). IEEE. +5. Condoluci, A., Accattoli, B., & Coen, C. S. (2019, October). Sharing + equality is linear. In Proceedings of the 21st International + Symposium on Principles and Practice of Declarative Programming + (pp. 1-14). +6. Accattoli, B., & Leberle, M. (2021). Useful open call-by-need. arXiv + preprint arXiv:2107.06591. @@ -1,4 +1,5 @@ #include <stdio.h> + #include <parse.h> #include <term.h> diff --git a/src/parse.c b/src/parse.c index 00fd498..495f55f 100644 --- a/src/parse.c +++ b/src/parse.c @@ -1,9 +1,10 @@ // Just for debugging purposes // -> parses custom bruijn syntax +#include <stdio.h> + #include <parse.h> #include <term.h> -#include <stdio.h> static struct term *rec(const char **term) { @@ -1,7 +1,8 @@ -#include <term.h> #include <stdlib.h> #include <stdio.h> +#include <term.h> + struct term *new_term(term_type type) { struct term *term = calloc(1, sizeof(*term)); |