diff --git a/.gitignore b/.gitignore index 1febac53..9462ae9b 100644 --- a/.gitignore +++ b/.gitignore @@ -37,6 +37,7 @@ coverage.info coverage_filtered.info test_output.log .github/skills +.codegraph # Refactoring testing baseline (optional: remove this line to track in git) test_baseline/ diff --git a/Makefile b/Makefile index 9385d398..5c94da83 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ list-cores test indent indent-src indent-generated docs \ install-sqlite3 install-raylib coverage extracov view-coverage \ coverage-target test-a test-fail test-sh test-c test-unit test-b test-big-c help \ -test-gfx test-gfx-stress establish-baseline test-refactoring update-baseline clean-baseline \ +test-rewrite test-gfx test-gfx-stress establish-baseline test-refactoring update-baseline clean-baseline \ scratch bench-regex-cache rebuild-default rebuild-raylib # pass on the command line, i.e. `make test MODE=prod` @@ -97,6 +97,23 @@ EXTRA_TARGETS= \ $(GENDIR)/cps_kont_impl.h \ $(GENDIR)/cps_kont_impl.c +GENERATED_BOOTSTRAP= \ + $(EXTRA_H_TARGETS) \ + $(EXTRA_OBJTYPES_H_TARGETS) \ + $(EXTRA_DEBUG_H_TARGETS) \ + $(GENDIR)/UnicodeData.inc \ + $(GENDIR)/UnicodeCasing.inc \ + $(GENDIR)/UnicodeDigits.inc \ + $(GENDIR)/UnicodeNumbers.inc \ + $(GENDIR)/anf_kont.h \ + $(GENDIR)/anf_kont_objtypes.h \ + $(GENDIR)/anf_kont_debug.h \ + $(GENDIR)/anf_kont_impl.inc \ + $(GENDIR)/cps_kont.h \ + $(GENDIR)/cps_kont_objtypes.h \ + $(GENDIR)/cps_kont_debug.h \ + $(GENDIR)/cps_kont_impl.h + MAIN=$(SRCDIR)/main.c PREAMBLE=$(GENDIR)/preamble.c CFILES=$(filter-out $(MAIN), $(wildcard $(SRCDIR)/*.c)) @@ -153,15 +170,15 @@ FN_BFILES=$(patsubst $(FNDIR)/%,$(TMPDIR)/%,$(patsubst %.fn,%.fnc,$(FN_FILES))) FN_OFILES=$(patsubst %.c,%.o,$(FN_CFILES)) FN_BINARIES=$(patsubst %.o,%,$(FN_OFILES)) -TARGET_ARGS=--include=fn --flat-closure +TARGET_ARGS=--include=fn --assertions-accumulate $(TEST_FN_CFILES): $(TMPDIR)/%.c: $(TEST_FN_DIR)/%.fn $(TARGET) | $(TMPDIR) - $(TARGET) $(TARGET_ARGS) --target-c=$@~ $< && mv $@~ $@ + $(TARGET) $(TARGET_ARGS) --flat-closure --target-c=$@~ $< && mv $@~ $@ indent $@ rm -f $@~ $(FN_CFILES): $(TMPDIR)/%.c: $(FNDIR)/%.fn $(TARGET) | $(TMPDIR) - $(TARGET) $(TARGET_ARGS) --target-c=$@~ $< && mv $@~ $@ + $(TARGET) $(TARGET_ARGS) --flat-closure --target-c=$@~ $< && mv $@~ $@ indent $@ rm -f $@~ @@ -172,10 +189,10 @@ $(FN_BFILES): $(TMPDIR)/%.fnc: $(FNDIR)/%.fn $(TARGET) | $(TMPDIR) $(TARGET) --binary-out=$@~ $< && mv $@~ $@ $(TEST_FN_SFILES): $(TMPDIR)/%.scm: $(TEST_FN_DIR)/%.fn $(TARGET) | $(TMPDIR) - $(TARGET) $(TARGET_ARGS) --target-c --dump-inline-f $< > $@~ && mv $@~ $@ + $(TARGET) $(TARGET_ARGS) --flat-closure --target-c --dump-inline-f $< > $@~ && mv $@~ $@ $(FN_SFILES): $(TMPDIR)/%.scm: $(FNDIR)/%.fn $(TARGET) | $(TMPDIR) - $(TARGET) $(TARGET_ARGS) --target-c --dump-inline-f $< > $@~ && mv $@~ $@ + $(TARGET) $(TARGET_ARGS) --flat-closure --target-c --dump-inline-f $< > $@~ && mv $@~ $@ $(FN_OFILES) $(TEST_FN_OFILES): %.o: %.c $(LAXCC) $(INCLUDE_PATHS) -c $< -o $@ @@ -240,7 +257,7 @@ Double \ Control EXTRA_INDENT_ARGS=$(patsubst %,-T %,$(EXTRA_TYPES)) -include $(ALL_DEP) +-include $(ALL_DEP) $(PREAMBLE): $(PREAMBLE_SRC) | $(GENDIR) tools/make-preamble.sh @@ -291,61 +308,49 @@ $(GENDIR)/cps_kont_impl.c: tools/cps_continuations.yaml $(GENDEPS) $(SRCDIR)/pri $(EXTRA_DOCS): $(DOCDIR)/%.md: $(SRCDIR)/%.yaml $(GENDEPS) $(SRCDIR)/primitives.yaml | $(DOCDIR) $(MAKE_AST) $< md > $@~ && mv $@~ $@ -.generated: $(EXTRA_TARGETS) - touch $@ - tags: $(SRCDIR)/* $(EXTRA_TARGETS) ctags $(SRCDIR)/* $(EXTRA_TARGETS) xref: $(SRCDIR)/* $(EXTRA_TARGETS) ctags -x $(SRCDIR)/* $(EXTRA_TARGETS) > $@ -$(MAIN_OBJ) $(OBJ): $(OBJDIR)/%.o: $(SRCDIR)/%.c | $(OBJDIR) - $(CC) $(INCLUDE_PATHS) -c $< -o $@ - -$(EXTRA_OBJ) $(PREAMBLE_OBJ): $(OBJDIR)/%.o: $(GENDIR)/%.c | $(OBJDIR) - $(CC) $(INCLUDE_PATHS) -c $< -o $@ - -$(TEST_OBJ): $(OBJDIR)/%.o: $(TSTDIR)/src/%.c | $(OBJDIR) - $(LAXCC) $(INCLUDE_PATHS) -c $< -o $@ - -$(MAIN_DEP) $(DEP): $(DEPDIR)/%.d: $(SRCDIR)/%.c .generated | $(DEPDIR) - $(CC) $(INCLUDE_PATHS) -MM -MT $(patsubst $(DEPDIR)/%,$(OBJDIR)/%,$(patsubst %.d,%.o,$@)) -o $@ $< +$(MAIN_OBJ) $(OBJ): $(OBJDIR)/%.o: $(SRCDIR)/%.c | $(OBJDIR) $(DEPDIR) $(GENERATED_BOOTSTRAP) + $(CC) $(INCLUDE_PATHS) -MMD -MP -MF $(DEPDIR)/$*.d -MT $@ -c $< -o $@ -$(EXTRA_DEP) $(PREAMBLE_DEP): $(DEPDIR)/%.d: $(GENDIR)/%.c .generated | $(DEPDIR) - $(CC) $(INCLUDE_PATHS) -MM -MT $(patsubst $(DEPDIR)/%,$(OBJDIR)/%,$(patsubst %.d,%.o,$@)) -o $@ $< +$(EXTRA_OBJ) $(PREAMBLE_OBJ): $(OBJDIR)/%.o: $(GENDIR)/%.c | $(OBJDIR) $(DEPDIR) $(GENERATED_BOOTSTRAP) + $(CC) $(INCLUDE_PATHS) -MMD -MP -MF $(DEPDIR)/$*.d -MT $@ -c $< -o $@ -$(TEST_DEP): $(DEPDIR)/%.d: $(TSTDIR)/src/%.c .generated | $(DEPDIR) - $(CC) $(INCLUDE_PATHS) -MM -MT $(patsubst $(DEPDIR)/%,$(OBJDIR)/%,$(patsubst %.d,%.o,$@)) -o $@ $< +$(TEST_OBJ): $(OBJDIR)/%.o: $(TSTDIR)/src/%.c | $(OBJDIR) $(DEPDIR) $(GENERATED_BOOTSTRAP) + $(LAXCC) $(INCLUDE_PATHS) -MMD -MP -MF $(DEPDIR)/$*.d -MT $@ -c $< -o $@ -test: test-unit test-a test-b test-sh test-fail +test: test-unit test-a test-b test-sh test-fail test-rewrite @echo "All tests passed." -test-unit: all $(TEST_TARGETS) - for t in $(TEST_TARGETS) ; do echo '***' $$t '***' ; $$t || exit 1 ; done +test-unit: $(TEST_TARGETS) + set -x; for t in $(TEST_TARGETS) ; do $$t || exit 1 ; done @echo "All unit tests passed." test-a: all - for t in $(TSTDIR)/fn/test_*.fn ; do echo '***' $$t '***' ; ./$(TARGET) --include=fn --assertions-accumulate $$t || exit 1 ; done + set -x; for t in $(TSTDIR)/fn/test_*.fn ; do $(TARGET) $(TARGET_ARGS) $$t || exit 1 ; done @echo "All a tests passed." test-sh: all - for t in $(TSTDIR)/sh/*.sh ; do [ -e $$t ] || continue ; echo '***' $$t '***' ; bash $$t || exit 1 ; done + set -x ; for t in $(TSTDIR)/sh/*.sh ; do bash $$t || exit 1 ; done @echo "All sh tests passed." test-fail: all - for t in $(TSTDIR)/fn/fail_*.fn ; do echo '***' $$t '***' ; ! ./$(TARGET) --include=fn --assertions-accumulate $$t >/dev/null 2>&1 || exit 1 ; done + set -x ; for t in $(TSTDIR)/fn/fail_*.fn ; do ! ./$(TARGET) $(TARGET_ARGS) $$t >/dev/null 2>&1 || exit 1 ; done @echo "All negative tests passed." test-c: all $(TEST_FN_BINARIES) - @for t in $(TEST_FN_BINARIES) ; do echo $$t ; $$t || exit 1 ; done + set -x ; for t in $(TEST_FN_BINARIES) ; do $$t || exit 1 ; done @echo All generated C tests pass test-big-c: all $(TMPDIR)/test_harness $(TMPDIR)/test_harness test-b: all - @for t in $(TEST_FN_FILES) ; do set -x; $(TARGET) $(TARGET_ARGS) --target-b $$t || exit 1 ; done + set -x; for t in $(TSTDIR)/fn/test_*.fn ; do $(TARGET) $(TARGET_ARGS) --flat-closure --target-b $$t || exit 1 ; done @echo All B-code tests pass test-gfx: all @@ -357,6 +362,10 @@ test-gfx-stress: all @for t in $(TSTDIR)/fn/test_gfx_shader_reload_smoke.fn $(TSTDIR)/fn/test_gfx_resource_churn_smoke.fn ; do echo '***' $$t '***' ; ./$(TARGET) --include=fn --assertions-accumulate --stress-gc $$t || exit 1 ; done @echo "All gfx stress smoke tests passed." +test-rewrite: all + set -x; for t in fn/rewrite/tests/test_*.fn ; do $(TARGET) $(TARGET_ARGS) --flat-closure --target-b $$t || exit 1 ; done + @echo All rewrite tests pass + $(TEST_TARGETS): $(TSTDIR)/%: $(OBJDIR)/%.o $(ALL_OBJ) $(CC) -o $@ $< $(ALL_OBJ) $(LIBS) @@ -398,7 +407,7 @@ realclean: clean rm -rf tags xref $(UNIDIR) clean: deps - rm -rf $(BINDIR) $(OBJDIR) callgrind.out.* $(GENDIR) $(TEST_TARGETS) .typedefs $(SRCDIR)/*~ .generated gmon.out *.fnc core.* coverage_html coverage_report.txt gcov_output *.gcda *.gcno coverage.info coverage_filtered.info test_output.log $(TEST_FN_CFILES) $(TEST_FN_OFILES) $(TEST_FN_BINARIES) $(TEST_FN_SFILES) $(TMPDIR) + rm -rf $(BINDIR) $(OBJDIR) callgrind.out.* $(GENDIR) $(TEST_TARGETS) $(SRCDIR)/*~ gmon.out *.fnc core.* coverage_html coverage_report.txt gcov_output *.gcda *.gcno coverage.info coverage_filtered.info test_output.log $(TEST_FN_CFILES) $(TEST_FN_OFILES) $(TEST_FN_BINARIES) $(TEST_FN_SFILES) $(TMPDIR) $(MAKE) -C scratch clean rebuild-default: @@ -441,18 +450,6 @@ profile-parse: all leak-check: all valgrind --leak-check=full ./$(TARGET) $(FNDIR)/$(PROF_SRC).fn -indent: indent-src indent-generated - -indent-src: .typedefs .indent.pro - indent `cat .typedefs | sort -u | xargs` $(EXTRA_INDENT_ARGS) $(SRCDIR)/*.[ch] - rm -f $(SRCDIR)/*~ - -indent-generated: .typedefs .indent.pro - indent `cat .typedefs | sort -u | xargs` $(EXTRA_INDENT_ARGS) $(GENDIR)/*.[ch] - rm -f $(GENDIR)/*~ - -.typedefs: .generated - list-cores: @ls -rt1 /var/lib/apport/coredump/* | tail -1 diff --git a/docs/TODO.md b/docs/TODO.md index ecbab23c..e07cb16d 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -2,40 +2,33 @@ More of a wish-list than a hard and fast plan. +* Fn/Rewrite. + * Add an interpreter for the final IR. + * Add a parser and AST. + * Type Checking. + * etc. * More folding opportunities. - * fold boolean expressions `true and false => false`. - * tricky because `and`, `or` etc. are not primitive, they are lazy operators defined in terms of `if` in the preamble. - * fold comparisons `a == a => true`, `a >= a => true` etc. DONE - * fold constant conditions `(if true a b) => a`. DONE - * This solves the boolean expression folding problem, after β/η-reduction: - * `true and false => (if true false false) => false` - * fold duplicate condition branches `(if x a a) => a`. + * Fold duplicate condition branches `(if x a a) => a`. * Continuations. - * Reinstate `cut` (prunes current back continuation). DONE * Implement delimited continuations. -* Regular Expressions. - * Enlist the new regex engine to support the core Pratt scanner. + * delimit/capture instead of reset/shift? * Types. * Consider type classes as a general solution to `EQ `, `map` etc. * Records should create accessor functions for each tag. * if there is only one type variant. - * extend the `typedef` keyword. - * `typedef container(#t);` is shorthand for `typedef container(#t) { container(#t) };` - * `typedef container(char);` is shorthand for `typedef container { container(char) };` - * no additional AST should be required, or if it is it gets immediately desugared so doesn't leak downstream. * Namespaces. - * We want `import function ` and `import functions`. DONE mostly. - * And `import typedef ` and `import typedefs`. + * `import typedef ` and `import typedefs`. * Parser. - * re-elist the now-available `macro` keyword for proper syntactic extensibility. DONE - * if/then/else => `(fn { (true) {then} (false) {else} }(if))` (we already do this but hard-coded in the parser). - * `do` notation for monads. + * if/then/else => `(fn { (true) {then} (false) {else} }(if))` (we already do this but hard-coded in the parser). + * `do` notation for monads. * Memory Management. * Replace mark and sweep GC with a generational stop and copy. * Pipeline. * Re-order Type Checking before TPMC. * Target LLVM. * Generate. + * Add a generator for equivalent F♮ `typedef`s to facilitate `fn/rewrite/`. + * Will need F♮ support for hashes, symbols arrays etc. * Move all signatures into `signature_helper.py`, not just the shared ones. * More numbers. * Vectors. @@ -51,7 +44,6 @@ More of a wish-list than a hard and fast plan. * does `a / 6` match `2 / 3` and bind `a` to `4`. * match would fail if the actual argument is not integer or rational. * `b` would be bound to `1` if the argument was an integer. - * can't allow arbitrary ops and combinations because i.e. `a * b` can't uniquely determine `a` and `b`, and `a ** 2` would require `a` to be bound to the square root of the actual argument. * allow unpacking of the real and imaginary parts of a complex number in patterns. * another special case: `a + b`, `b` would be bound to `0i` if the actual argument is not complex. * `mathutils.fn` for `factorial`, `gcd`, `lcm`, `fib`, `pi` etc. diff --git a/docs/delimited_continuations_notes.md b/docs/delimited_continuations_notes.md new file mode 100644 index 00000000..700b830a --- /dev/null +++ b/docs/delimited_continuations_notes.md @@ -0,0 +1,140 @@ +# Delimited Continuations + +Standared `shift/reset` semantics: + +* `reset (1 + shift k { 10 + k(2) }) = 13` +* `reset (1 + shift k { 2 }) = 2` +* `reset (1 + shift k { k(2) }) = 3` +* `reset (1 + shift k { k(2) + k(3) }) = 7` +* `reset (1 + shift k { 100 + k(k(2)) }) = 104` +* `reset (1 + shift k { 100 + k(2) + 1000 }) = 1103` +* `reset (1 + (reset (2 + shift k { k(3) }))) = 6` +* `reset (1) = 1` +* `reset (1 + shift k { 2 }) = 2` +* `1 + reset (shift k { 2 }) = 3` + +## Difference between `shift/reset` and `control/prompt` + +* `reset ((1 + shift k { 2 + k(3) }) + shift h { h(4) + h(5) }) = 19` +* `prompt ((1 + control k { 2 + k(3) }) + control h { h(4) + h(5) }) = 21` + +### The `shift/reset` example + +* `reset ((1 + shift k { 2 + k(3) }) + shift h { h(4) + h(5) }) = 19` + +To understand that `shift/reset` example first, let + +```fn +T = reset ( + (1 + shift k { 2 + k(3) }) + + shift h { h(4) + h(5) } +) +``` + +The first `shift` captures the context: + +```fn +E1 = (1 + [ ]) + shift h { h(4) + h(5) } +``` + +So under `shift/reset`: + +```txt +k(v) = reset( (1 + v) + shift h { h(4) + h(5) } ) +// ^^^^^ +``` + +That extra `reset` is the crucial part. So the term becomes: + +```fn +T = reset( 2 + k(3) ) + = reset( 2 + reset( (1 + 3) + shift h { h(4) + h(5) } ) ) +``` + +Now look at the inner `reset`: + +```fn + reset( (1 + 3) + shift h { h(4) + h(5) } ) += reset( 4 + shift h { h(4) + h(5) } ) +``` + +`h` captures only + +```fn +E2 = 4 + [ ] +``` + +so + +```fn +h(v) = reset(4 + v) +``` + +Hence: + +```fn +h(4) = 8 +h(5) = 9 +``` + +so the inner reset is: + +```fn + reset( h(4) + h(5) ) += reset( 8 + 9 ) += 17 +``` + +and therefore the whole term is: + +```fn +reset( 2 + 17 ) = 19 +``` + +## The Difference + +```fn +shift/reset: +reset ( + (1 + shift k { 2 + k(3) }) + + shift h { h(4) + h(5) } +) +``` + +```fn +control/prompt: +prompt ( + (1 + control k { 2 + k(3) }) + + control h { h(4) + h(5) } +) +``` + +### shift/reset + +```fn +reset ((1 + shift k { 2 + k(3) }) + shift h { h(4) + h(5) }) = 19 +E1 = (1 + [ ]) + shift h { h(4) + h(5) } +k(v) = reset((1 + v ) + shift h { h(4) + h(5) }) +reset(2 + reset((1 + 3 ) + shift h { h(4) + h(5) })) +E2 = 4 + [ ] +h(v) = reset(4 + v) +h(4) = 8 +h(5) = 9 +inner reset: 17 +final result: 19 +``` + +### control/prompt + +```fn +prompt ((1 + control k { 2 + k(3) }) + control h { h(4) + h(5) }) = 21 +E1 = (1 + [ ]) + control h { h(4) + h(5) } +k(v) = (1 + v ) + control h { h(4) + h(5) } +prompt(2 + ((1 + 3 ) + control h { h(4) + h(5) })) +prompt(6 + control h { h(4) + h(5) }) +E2 = 6 + [ ] +h(v) = 6 + v +h(4) = 10 +h(5) = 11 +final result: 21 +``` diff --git a/docs/lambda-calculus.md b/docs/lambda-calculus.md index fcbe055d..8a3cf059 100644 --- a/docs/lambda-calculus.md +++ b/docs/lambda-calculus.md @@ -41,10 +41,10 @@ $$ \\ \mathcal{F}(e_0\ e_1) &= \mathcal{F}e_0\cup \mathcal{F}e_1 \\ -\mathcal{F}\lambda x.e &= \mathcal{F}e - \set{ x } && \text{(1)} +\tag{1}\mathcal{F}\lambda x.e &= \mathcal{F}e - \set{ x } \\ -\mathcal{F}(\mathtt{letrec}\ (( x_0:\lambda_0)\dots( x_n:\lambda_n))\ e) &= -\Big( \mathcal{F}e\cup\bigcup_{i=0}^n\mathcal{F}\lambda_i\Big) - \set{x_0\dots x_n} && \text{(2)} +\tag{2}\mathcal{F}(\mathtt{letrec}\ (( x_0:\lambda_0)\dots( x_n:\lambda_n))\ e) &= +\Big( \mathcal{F}e\cup\bigcup_{i=0}^n\mathcal{F}\lambda_i\Big) - \set{x_0\dots x_n} \end{align*} $$ @@ -70,25 +70,36 @@ $$ \begin{align*} \alpha_{\rho}\mathtt{C} &= \mathtt{C} \\ -\alpha_{\rho}x &= \rho(x) && && \text{(1)} +\tag{1} +\alpha_{\rho}x &= \rho(x) + \\ \alpha_{\rho}(e_0\ e_1) &= (\alpha_{\rho}e_0\ \alpha_{\rho}e_1) + \\ +\tag{2} \alpha_{\rho}\lambda x.e &= \lambda x'.\alpha_{\rho[x \mapsto x']}e -&& \text{where } x' = \mathrm{fresh}(x) && \text{(2)} +& \text{where } & x' = \mathrm{fresh}(x) + \\ +\tag{3} l &= (\mathtt{letrec}\ (b_0\dots b_n)\ e) -&& && \text{(3)} + \\ \rho' &= \rho[x_0 \mapsto x'_0,\dots,x_n \mapsto x'_n] -&& \text{where } b_i = (x_i:\lambda y_i.e_i),\ x'_i = \mathrm{fresh}(x_i) && \text{(4)} +& \text{where } & b_i = (x_i:\lambda y_i.e_i), + +\\ +\tag{4} +&&&x'_i = \mathrm{fresh}(x_i) + \\ -\alpha_{\rho}l &= +\tag{5}\alpha_{\rho}l &= (\mathtt{letrec}\ (\alpha_{\rho'}b_0\dots\alpha_{\rho'}b_n)\ \alpha_{\rho'}e) -&& && \text{(5)} + \\ -\alpha_{\rho}(x:\lambda y.e) &= (\rho(x):\lambda y'.\alpha_{\rho[y \mapsto y']}e) -&& \text{where } y' = \mathrm{fresh}(y) && \text{(6)} +\tag{6}\alpha_{\rho}(x:\lambda y.e) &= (\rho(x):\lambda y'.\alpha_{\rho[y \mapsto y']}e) +& \text{where } & y' = \mathrm{fresh}(y) \end{align*} $$ @@ -119,18 +130,23 @@ y &\text{otherwise} \\ \mathcal{S}_{[x/r]}(e_0\ e_1) &= (\mathcal{S}_{[x/r]}e_0\ \mathcal{S}_{[x/r]}e_1) \\ +\tag{1} \mathcal{S}_{[x/r]}\lambda y.e_0 &= \begin{cases} -\lambda y.e_0 &\text{if } x = y\ \mathrm{(1)} +\lambda y.e_0 &\text{if } x = y \\ \lambda y.\mathcal{S}_{[x/r]}e_0 &\text{otherwise} \end{cases} + \\ l &= (\mathtt{letrec}\ ((y_0:\lambda z_0.e_0)\dots(y_n:\lambda z_n.e_n))\ e) \\ +\tag{2} \mathcal{S}_{[x/r]}l &= \begin{cases} -l &\text{if } x \in \set{y_0\dots y_n}\ \mathrm{(2)} +l &\text{if } x \in \set{y_0\dots y_n} +\\ +(\mathtt{letrec}\ ((y_0:\lambda z_0.\mathcal{S}_{[x/r]}e_0)\dots \\ -(\mathtt{letrec}\ ((y_0:\lambda z_0.\mathcal{S}_{[x/r]}e_0)\dots(y_n:\lambda z_n.\mathcal{S}_{[x/r]}e_n))\ \mathcal{S}_{[x/r]}e) &\text{otherwise} +\phantom{\mathtt{letrec}\ ((} (y_n:\lambda z_n.\mathcal{S}_{[x/r]}e_n))\ \mathcal{S}_{[x/r]}e) &\text{otherwise} \end{cases} \end{align*} $$ @@ -144,8 +160,9 @@ $$ \begin{align*} \mathcal{S}^{cs}_{[x/r]}y &= y \\ +\tag{3} \mathcal{S}^{cs}_{[x/r]}(e_0\ e_1) &= \begin{cases} -(r\ \mathcal{S}^{cs}_{[x/r]}e_1) &\text{if } e_0 = x\ \mathrm{(3)} +(r\ \mathcal{S}^{cs}_{[x/r]}e_1) &\text{if } e_0 = x \\ (\mathcal{S}^{cs}_{[x/r]}e_0\ \mathcal{S}^{cs}_{[x/r]}e_1) &\text{otherwise} \end{cases} @@ -166,7 +183,8 @@ $$ \\ \beta x &= x \\ -\beta((\lambda x.e_0)\ e_1) &= \mathcal{S}_{[x/\beta e_1]}\beta e_0 && \text{(1)} +\tag{1} +\beta((\lambda x.e_0)\ e_1) &= \mathcal{S}_{[x/\beta e_1]}\beta e_0 \\ \beta (e_0\ e_1) &= (\beta e_0\ \beta e_1) \\ @@ -193,8 +211,9 @@ $$ \\ \eta (e_0\ e_1) &= (\eta e_0\ \eta e_1) \\ +\tag{1} \eta\lambda x.(e\ x) &= \begin{cases} -\eta e &\text{iff } x \not \in \mathcal{F}e\ \mathrm{(1)} +\eta e &\text{iff } x \not \in \mathcal{F}e \\ \lambda x .\eta(e\ x) &\text{otherwise} \end{cases} @@ -223,26 +242,32 @@ $$ \\ \mathcal{T}\lambda x . e &= \lambda x.\mathcal{T}e \\ -l &= (\mathtt{letrec}\ (( x_0:\lambda_0)\dots ( x_n:\lambda_n))\ e) && \text{(1)} +\tag{1} +l &= (\mathtt{letrec}\ (( x_0:\lambda_0)\dots ( x_n:\lambda_n))\ e) \\ -l' &= (\mathtt{letrec}\ (( x_0:\lambda'_0)\dots ( x_n:\lambda'_n))\ e') && \text{(2)} +l' &= (\mathtt{letrec}\ (( x_0:\lambda'_0)\dots ( x_n:\lambda'_n))\ e') \\ -&\text{where }\lambda'_i = \mathcal{T}\lambda_i \text{ and }e' = \mathcal{T}e +\tag{2} +&\phantom{=}\text{where }\lambda'_i = \mathcal{T}\lambda_i \text{ and }e' = \mathcal{T}e \\ -K &= \set{x_0\dots x_n} && \text{(3)} +\tag{3} +K &= \set{x_0\dots x_n} \\ -\vec{D} &= \set{ x_i \rightarrow x_j | x_i \in K,\ x_j \in K \cap \mathcal{F}\lambda'_i} && \text{(4)} +\tag{4} +\vec{D} &= \set{ x_i \rightarrow x_j | x_i \in K,\ x_j \in K \cap \mathcal{F}\lambda'_i} \\ -B &= \mathcal{F}e' \cap K && \text{(5)} +\tag{5} +B &= \mathcal{F}e' \cap K \\ -L &= \bigcup_{x\in B} \vec{D}^{\ast}x && \text{(6)} +\tag{6} +L &= \bigcup_{x\in B} \vec{D}^{\ast}x \\ +\tag{7} \mathcal{T}l &= (\mathtt{letrec}\ (\set{(x_i:\lambda'_i) | x_i \in L})\ e') -&& \text{(7)} \\ +\tag{8} \mathcal{T}(\mathtt{letrec}\ (\ )\ e) &= \mathcal{T}e -&& \text{(8)} \end{align*} $$ @@ -287,7 +312,9 @@ l &= (\mathtt{letrec}\ ((x_0:\lambda_0)\dots(x_n:\lambda_n))\ e) \\ \mathcal{S}_{cs}^{\ast}y &= \mathcal{S}^{cs}_{[x_0/\lambda_0]}\dots\mathcal{S}^{cs}_{[x_m/\lambda_m]}y \\ -R &= \set{(x_i:\lambda_i) \in \set{(x_0:\lambda_0)\dots(x_n:\lambda_n)} | \mathrm{safe}(x_i, \lambda_i, l)} = \set{(x_0:\lambda_0)\dots(x_m:\lambda_m)} +R &= \set{(x_i:\lambda_i) \in \set{(x_0:\lambda_0)\dots(x_n:\lambda_n)} | \mathrm{safe}(x_i, \lambda_i, l)} +\\ +&= \set{(x_0:\lambda_0)\dots(x_m:\lambda_m)} \\ \mathrm{safe}(x_i, \lambda_i, l) &= \mathcal{Z}\lambda_i < \mathtt{MAX} \land \lnot\mathcal{R}x_i \land \mathcal{C}_{x_i}l = 1 \land \mathcal{C}^{cs}_{x_i}l = 1 \end{align*} @@ -309,9 +336,11 @@ $$ \\ \mathcal{Z}\lambda x.e &= 1 + \mathcal{Z}e \\ -\mathcal{Z}(\mathtt{letrec}\ (b_0\dots b_n)\ e) &= 1 + \sum_{i=0}^n\mathcal{Z}b_i + \mathcal{Z}e +\mathcal{Z}(\mathtt{letrec}\ (b_0\dots b_n)\ e) &= 1 + \mathcal{Z}e + \textstyle\sum_{i=0}^n\mathcal{Z}b_i +\\ +\mathcal{Z}b &= 1+ \mathcal{Z}e \\ -\mathcal{Z}(x:\lambda y.e) &= 1+ \mathcal{Z}e +&\phantom{=}\text{where } b = (x:\lambda y.e) \end{align*} $$ @@ -326,17 +355,22 @@ $$ \begin{align*} \text{given} \\ -l &= (\mathtt{letrec}\ ((x_0:\lambda_0)\dots(x_n:\lambda_n))\ e) & \text{(1)} +\tag{1} +l &= (\mathtt{letrec}\ ((x_0:\lambda_0)\dots(x_n:\lambda_n))\ e) \\ -K &= \set{x_0\dots x_n} & \text{(2)} +\tag{2} +K &= \set{x_0\dots x_n} \\ -\vec{D} &= \set{x_i \mapsto x_j | x_i \in K,\ x_j \in K \cap \mathcal{F}\lambda_i} & \text{(3)} +\tag{3} +\vec{D} &= \set{x_i \mapsto x_j | x_i \in K,\ x_j \in K \cap \mathcal{F}\lambda_i} \\ -x &\in K & \text{(4)} +\tag{4} +x &\in K \\ \text{then} \\ -\mathcal{R}x &= (x \mapsto x) \in \vec{D}^+ & \text{(5)} +\tag{5} +\mathcal{R}x &= (x \mapsto x) \in \vec{D}^+ \end{align*} $$ @@ -375,7 +409,7 @@ $$ \mathcal{C}_x(\mathtt{letrec}\ ((y_0:\lambda z_0.e_0)\dots(y_n:\lambda z_n.e_n))\ e) &= \begin{cases} 0 & \text{if } x \in \set{y_0\dots y_n} \\ -\mathcal{C}_x e + \sum_{i=0}^{i=n}\mathcal{C}_x(\lambda z_i.e_i) &\text{otherwise} +\mathcal{C}_x e + \sum_{i=0}^{n}\mathcal{C}_x(\lambda z_i.e_i) &\text{otherwise} \end{cases} \end{align*} $$ diff --git a/fn/ambutils.fn b/fn/ambutils.fn index 479cd332..d4996494 100644 --- a/fn/ambutils.fn +++ b/fn/ambutils.fn @@ -84,3 +84,7 @@ fn integers_between(lower, upper) { export operator "_.._" 8 integers_between; +fn random(seed) { + let r = rand(seed); + in r then random(r) +} \ No newline at end of file diff --git a/fn/dictutils.fn b/fn/dictutils.fn index c15ebf5d..5bf90f26 100644 --- a/fn/dictutils.fn +++ b/fn/dictutils.fn @@ -202,10 +202,18 @@ fn make (keys, values) { add_lists(keys, values, E) } +fn add_list (list, dict) { + list.foldl(fn (#(k, v), d) { insert(k, v, d) }, dict, list) +} + fn add_lists (keys, values, dict) { - list.foldl(fn (#(k, v), d) { insert(k, v, d) }, dict, list.zip(keys, values)) + add_list(list.zip(keys, values), dict) } fn delete_list (keys, dict) { list.foldl(fn (k, d) { delete(k, d) }, dict, keys) +} + +fn from_list (list) { + add_list(list, empty()) } \ No newline at end of file diff --git a/fn/gfx_2d_primitives_demo.fn b/fn/gfx_2d_primitives_demo.fn index c9e3e70a..1d0778f4 100644 --- a/fn/gfx_2d_primitives_demo.fn +++ b/fn/gfx_2d_primitives_demo.fn @@ -4,9 +4,16 @@ let link "gfxutils.fn" as gfx; import gfx macro key_pressed_action; + import gfx.rgb; + import gfx.white; + import gfx.draw_text_at; + import gfx.frame; + import gfx.should_close; + import gfx.fill_triangle; + import gfx.draw_triangle; fn loop(angle) { - if (gfx.should_close()) { true } + if (should_close()) { true } else if (key_pressed_action[ escape => { true }; default => { false } @@ -15,33 +22,33 @@ let let angle2 = angle + 2; in - gfx.frame(gfx.rgb(18, 20, 28), fn () { - gfx.draw_text_at("2D Primitives Demo", gfx.point(20, 18), 30, gfx.white()); - gfx.draw_text_at("Esc: quit", gfx.point(20, 54), 18, gfx.rgb(210, 230, 255)); + frame(rgb(18, 20, 28), fn () { + draw_text_at("2D Primitives Demo", gfx.point(20, 18), 30, white()); + draw_text_at("Esc: quit", gfx.point(20, 54), 18, rgb(210, 230, 255)); - assert(gfx.fill_triangle( + assert(fill_triangle( gfx.point(100, 170), gfx.point(40, 280), gfx.point(160, 280), - gfx.rgb(120, 200, 255) + rgb(120, 200, 255) )); - assert(gfx.draw_triangle( + assert(draw_triangle( gfx.point(240, 170), gfx.point(180, 280), gfx.point(300, 280), - gfx.white() + white() )); - assert(gfx.fill_polygon(gfx.point(460, 230), 6, 70, angle, gfx.rgb(255, 170, 120))); - assert(gfx.draw_polygon(gfx.point(640, 230), 8, 80, 0 - angle, gfx.rgb(170, 255, 180))); + assert(gfx.fill_polygon(gfx.point(460, 230), 6, 70, angle, rgb(255, 170, 120))); + assert(gfx.draw_polygon(gfx.point(640, 230), 8, 80, 0 - angle, rgb(170, 255, 180))); - assert(gfx.draw_arc(gfx.point(820, 230), 90, 20, 320, 40, gfx.rgb(255, 220, 120))); + assert(gfx.draw_arc(gfx.point(820, 230), 90, 20, 320, 40, rgb(255, 220, 120))); assert(gfx.draw_rect_rounded( gfx.rect(740, 330, 160, 90), 0.35, 16, 4, - gfx.rgb(200, 220, 255) + rgb(200, 220, 255) )); gfx.with_camera2d( @@ -55,20 +62,20 @@ let 0.2, 12, 3, - gfx.rgb(90, 110, 150) + rgb(90, 110, 150) )); - assert(gfx.fill_polygon(gfx.point(0, 0), 5, 70, angle2, gfx.rgb(140, 120, 230))); - assert(gfx.draw_arc(gfx.point(0, 0), 120, 0, 270, 48, gfx.rgb(230, 200, 130))); + assert(gfx.fill_polygon(gfx.point(0, 0), 5, 70, angle2, rgb(140, 120, 230))); + assert(gfx.draw_arc(gfx.point(0, 0), 120, 0, 270, 48, rgb(230, 200, 130))); assert(gfx.draw_triangle( gfx.point(-110, 80), gfx.point(0, -110), gfx.point(110, 80), - gfx.white() + white() )) } ); - gfx.draw_text_at("Camera2D section at lower-middle", gfx.point(440, 700), 20, gfx.rgb(190, 210, 240)) + draw_text_at("Camera2D section at lower-middle", gfx.point(440, 700), 20, rgb(190, 210, 240)) }); loop(angle2) } diff --git a/fn/gfx_test.fn b/fn/gfx_test.fn index c8a23122..f4088611 100644 --- a/fn/gfx_test.fn +++ b/fn/gfx_test.fn @@ -1,21 +1,25 @@ let link "gfxutils.fn" as gfx; - - fn animate(x) { - if (gfx.should_close()) { - true - } else { - let - next = if (x > 800) { 0 } else { x + 2 }; - in - gfx.frame(gfx.black(), fn () { - gfx.draw_text("Hello!", x, 200, 24, gfx.white()) - }); - animate(next) + width = 800; + height = 600; +in { + let + fn animate(x) { + if (gfx.should_close()) { + true + } else { + let + next = if (x > width) { 0 } else { x + 2 }; + in + gfx.frame(gfx.black(), fn () { + gfx.draw_text("Hello!", x, height/3, 24, gfx.white()) + }); + animate(next) + } } - } -in - gfx.with_window(800, 600, "Moving Text", fn () { - assert(gfx.set_target_fps(60)); - animate(0) - }) \ No newline at end of file + in + gfx.with_window(width, height, "Moving Text", fn () { + assert(gfx.set_target_fps(60)); + animate(0) + }) +} \ No newline at end of file diff --git a/fn/gfxutils.fn b/fn/gfxutils.fn index 034f99c7..b71d7d9a 100644 --- a/fn/gfxutils.fn +++ b/fn/gfxutils.fn @@ -1,23 +1,171 @@ namespace -typedef Color { rgba(number, number, number, number) } -typedef Point { point(number, number) } -typedef Vec3 { vec3(number, number, number) } -typedef Vec4 { vec4(number, number, number, number) } -typedef Size { extent(number, number) } -typedef Rect { rect(number, number, number, number) } -typedef Light { point_light(Vec3, Vec3, number) | directional_light(Vec3, Vec3, number) } -typedef LightingConfig { lighting_config(Vec3, number, number) } +typedef rgba(number, number, number, number); +typedef point(number, number); +typedef vec3(number, number, number); +typedef vec4(number, number, number, number); +typedef extent(number, number); +typedef rect(number, number, number, number); +typedef Light { point_light(vec3, vec3, number) | directional_light(vec3, vec3, number) } +typedef lighting_config(vec3, number, number); fn rgb(r, g, b) { rgba(r, g, b, 255) } -fn black() { rgba(0, 0, 0, 255) } -fn white() { rgba(255, 255, 255, 255) } -fn red() { rgba(255, 0, 0, 255) } -fn green() { rgba(0, 255, 0, 255) } -fn blue() { rgba(0, 0, 255, 255) } +fn alice_blue() { rgb(240, 248, 255) } +fn antique_white() { rgb(250, 235, 215) } +fn aquamarine() { rgb(127, 255, 212) } +fn aqua() { rgb(0, 255, 255) } +fn azure() { rgb(240, 255, 255) } +fn beige() { rgb(245, 245, 220) } +fn bisque() { rgb(255, 228, 196) } +fn black() { rgb(0, 0, 0) } +fn blanched_almond() { rgb(255, 235, 205) } +fn blue() { rgb(0, 0, 255) } +fn blue_violet() { rgb(138, 43, 226) } +fn brown() { rgb(165, 42, 42) } +fn burlywood() { rgb(222, 184, 135) } +fn cadet_blue() { rgb(95, 158, 160) } +fn chartreuse() { rgb(127, 255, 0) } +fn chocolate() { rgb(210, 105, 30) } +fn coral() { rgb(255, 127, 80) } +fn cornflower_blue() { rgb(100, 149, 237) } +fn cornsilk() { rgb(255, 248, 220) } +fn crimson() { rgb(220, 20, 60) } +fn cyan() { rgb(0, 255, 255) } +fn dark_blue() { rgb(0, 0, 139) } +fn dark_cyan() { rgb(0, 139, 139) } +fn dark_goldenrod() { rgb(184, 134, 11) } +fn dark_gray() { rgb(169, 169, 169) } +fn dark_green() { rgb(0, 100, 0) } +fn dark_khaki() { rgb(189, 183, 107) } +fn dark_magenta() { rgb(139, 0, 139) } +fn dark_olive_green() { rgb(85, 107, 47) } +fn dark_orange() { rgb(255, 140, 0) } +fn dark_orchid() { rgb(153, 50, 204) } +fn dark_red() { rgb(139, 0, 0) } +fn dark_salmon() { rgb(233, 150, 122) } +fn dark_sea_green() { rgb(143, 188, 143) } +fn dark_slate_blue() { rgb(72, 61, 139) } +fn dark_slate_gray() { rgb(47, 79, 79) } +fn dark_turquoise() { rgb(0, 206, 209) } +fn dark_violet() { rgb(148, 0, 211) } +fn deep_pink() { rgb(255, 20, 147) } +fn deep_sky_blue() { rgb(0, 191, 255) } +fn dim_gray() { rgb(105, 105, 105) } +fn dodger_blue() { rgb(30, 144, 255) } +fn firebrick() { rgb(178, 34, 34) } +fn floral_white() { rgb(255, 250, 240) } +fn forest_green() { rgb(34, 139, 34) } +fn fuchsia() { rgb(255, 0, 255) } +fn gainsboro() { rgb(220, 220, 220) } +fn ghost_white() { rgb(248, 248, 255) } +fn goldenrod() { rgb(218, 165, 32) } +fn gold() { rgb(255, 215, 0) } +fn gray() { rgb(190, 190, 190) } +fn green() { rgb(0, 255, 0) } +fn green_yellow() { rgb(173, 255, 47) } +fn honeydew() { rgb(240, 255, 240) } +fn hot_pink() { rgb(255, 105, 180) } +fn indian_red() { rgb(205, 92, 92) } +fn indigo() { rgb(75, 0, 130) } +fn ivory() { rgb(255, 255, 240) } +fn khaki() { rgb(240, 230, 140) } +fn lavender_blush() { rgb(255, 240, 245) } +fn lavender() { rgb(230, 230, 250) } +fn lawn_green() { rgb(124, 252, 0) } +fn lemon_chiffon() { rgb(255, 250, 205) } +fn light_blue() { rgb(173, 216, 230) } +fn light_coral() { rgb(240, 128, 128) } +fn light_cyan() { rgb(224, 255, 255) } +fn light_goldenrod() { rgb(238, 221, 130) } +fn light_goldenrod_yellow() { rgb(250, 250, 210) } +fn light_gray() { rgb(211, 211, 211) } +fn light_green() { rgb(144, 238, 144) } +fn light_pink() { rgb(255, 182, 193) } +fn light_salmon() { rgb(255, 160, 122) } +fn light_sea_green() { rgb(32, 178, 170) } +fn light_sky_blue() { rgb(135, 206, 250) } +fn light_slate_blue() { rgb(132, 112, 255) } +fn light_slate_gray() { rgb(119, 136, 153) } +fn light_steel_blue() { rgb(176, 196, 222) } +fn light_yellow() { rgb(255, 255, 224) } +fn lime_green() { rgb(50, 205, 50) } +fn lime() { rgb(0, 255, 0) } +fn linen() { rgb(250, 240, 230) } +fn magenta() { rgb(255, 0, 255) } +fn maroon() { rgb(176, 48, 96) } +fn medium_aquamarine() { rgb(102, 205, 170) } +fn medium_blue() { rgb(0, 0, 205) } +fn medium_orchid() { rgb(186, 85, 211) } +fn medium_purple() { rgb(147, 112, 219) } +fn medium_sea_green() { rgb(60, 179, 113) } +fn medium_slate_blue() { rgb(123, 104, 238) } +fn medium_spring_green() { rgb(0, 250, 154) } +fn medium_turquoise() { rgb(72, 209, 204) } +fn medium_violet_red() { rgb(199, 21, 133) } +fn midnight_blue() { rgb(25, 25, 112) } +fn mint_cream() { rgb(245, 255, 250) } +fn misty_rose() { rgb(255, 228, 225) } +fn moccasin() { rgb(255, 228, 181) } +fn navajo_white() { rgb(255, 222, 173) } +fn navy_blue() { rgb(0, 0, 128) } +fn navy() { rgb(0, 0, 128) } +fn old_lace() { rgb(253, 245, 230) } +fn olive_drab() { rgb(107, 142, 35) } +fn olive() { rgb(128, 128, 0) } +fn orange_red() { rgb(255, 69, 0) } +fn orange() { rgb(255, 165, 0) } +fn orchid() { rgb(218, 112, 214) } +fn pale_goldenrod() { rgb(238, 232, 170) } +fn pale_green() { rgb(152, 251, 152) } +fn pale_turquoise() { rgb(175, 238, 238) } +fn pale_violet_red() { rgb(219, 112, 147) } +fn papaya_whip() { rgb(255, 239, 213) } +fn peach_puff() { rgb(255, 218, 185) } +fn peru() { rgb(205, 133, 63) } +fn pink() { rgb(255, 192, 203) } +fn plum() { rgb(221, 160, 221) } +fn powder_blue() { rgb(176, 224, 230) } +fn purple() { rgb(160, 32, 240) } +fn rebecca_purple() { rgb(102, 51, 153) } +fn red() { rgb(255, 0, 0) } +fn rosy_brown() { rgb(188, 143, 143) } +fn royal_blue() { rgb(65, 105, 225) } +fn saddle_brown() { rgb(139, 69, 19) } +fn salmon() { rgb(250, 128, 114) } +fn sandy_brown() { rgb(244, 164, 96) } +fn sea_green() { rgb(46, 139, 87) } +fn seashell() { rgb(255, 245, 238) } +fn sienna() { rgb(160, 82, 45) } +fn silver() { rgb(192, 192, 192) } +fn sky_blue() { rgb(135, 206, 235) } +fn slate_blue() { rgb(106, 90, 205) } +fn slate_gray() { rgb(112, 128, 144) } +fn snow() { rgb(255, 250, 250) } +fn spring_green() { rgb(0, 255, 127) } +fn steel_blue() { rgb(70, 130, 180) } +fn tan() { rgb(210, 180, 140) } +fn teal() { rgb(0, 128, 128) } +fn thistle() { rgb(216, 191, 216) } +fn tomato() { rgb(255, 99, 71) } +fn turquoise() { rgb(64, 224, 208) } +fn violet_red() { rgb(208, 32, 144) } +fn violet() { rgb(238, 130, 238) } +fn web_gray() { rgb(128, 128, 128) } +fn web_green() { rgb(0, 128, 0) } +fn web_maroon() { rgb(128, 0, 0) } +fn web_purple() { rgb(128, 0, 128) } +fn wheat() { rgb(245, 222, 179) } +fn white() { rgb(255, 255, 255) } +fn white_smoke() { rgb(245, 245, 245) } +fn x11_gray() { rgb(190, 190, 190) } +fn x11_green() { rgb(0, 255, 0) } +fn x11_maroon() { rgb(176, 48, 96) } +fn x11_purple() { rgb(160, 32, 240) } +fn yellow_green() { rgb(154, 205, 50) } +fn yellow() { rgb(255, 255, 0) } fn material_map_albedo() { 0 } fn material_map_normal() { 1 } diff --git a/fn/rewrite/README.md b/fn/rewrite/README.md index 0225f9df..ddfc3b1e 100644 --- a/fn/rewrite/README.md +++ b/fn/rewrite/README.md @@ -6,6 +6,12 @@ Even if it doesn't pan out, this is still useful as it provides concise referenc For agent-oriented guidance on the rewrite prototyping/self-hosting workflow (`test_harness.fn`, pass ordering, and `samples.fn` usage), see [`docs/agents/rewrite-self-hosting-guide.md`](../../docs/agents/rewrite-self-hosting-guide.md). +For a prototype-oriented design note on adding delimited control to the rewrite CPS pass, see [`docs/delimited-cps.md`](docs/delimited-cps.md). + +For a companion note on how `shift/reset` might be typed safely, especially when `shift` appears in named functions, see [`docs/delimited-types.md`](docs/delimited-types.md). + +For a short current status note on rewrite inference and typedef coverage, see [`docs/status-update.md`](docs/status-update.md). + * [`alphaconvert.fn`](alphaconvert.fn) - ɑ-conversion algorithm over `expr`. * [`appel.fn`](appel.fn) - The continuation type from Appel's book (unused). * [`beta_reduce.fn`](beta_reduce.fn) - β-reduction algorithm. diff --git a/fn/rewrite/annotate.fn b/fn/rewrite/annotate.fn index 0acff42c..82c66878 100644 --- a/fn/rewrite/annotate.fn +++ b/fn/rewrite/annotate.fn @@ -53,7 +53,7 @@ fn annotate(expr) { (M.lambda(params, body)) { // map param => location let locations = 0 :: ((len params) - 1); - env = D.make(params, locations) + env = D.add_lists(params, locations, e) in M.lambda(params, ann_rec(env, body)) } @@ -61,7 +61,7 @@ fn annotate(expr) { // map param => location let vars = bindings |> fn (#(var, _)) { var }; locations = 0::((len bindings) - 1); - env = D.make(vars, locations) + env = D.add_lists(vars, locations, e) in M.letrec_expr( bindings |> fn (#(var, #(val, arity))) { #(var, #(ann_rec(env, val), arity)) @@ -95,7 +95,8 @@ fn annotate(expr) { M.var(s @@ "<" @@ $n @@ ">") } (nothing) { - M.var(s @@ "") // should be an error really + error("unbound variable " @@ s) + // M.var(s @@ "") // should be an error really } } } diff --git a/fn/rewrite/beta_reduce.fn b/fn/rewrite/beta_reduce.fn index bd36d826..b8b24254 100644 --- a/fn/rewrite/beta_reduce.fn +++ b/fn/rewrite/beta_reduce.fn @@ -48,6 +48,14 @@ fn reduce { M.cut_expr(reduce(e)) } + (M.reset_expr(e)) { + M.reset_expr(reduce(e)) + } + + (M.shift_expr(e)) { + M.shift_expr(reduce(e)) + } + (M.cond_expr(test, branches)) { M.cond_expr(reduce(test), branches |> reduce && reduce) } diff --git a/fn/rewrite/cps.fn b/fn/rewrite/cps.fn index eaabd2ff..df9340bb 100644 --- a/fn/rewrite/cps.fn +++ b/fn/rewrite/cps.fn @@ -17,20 +17,56 @@ namespace fn M { (M.lambda(vars, body)) { - let c = GS.genstring("$k"); - in M.lambda(vars @@ [c], T_c(body, M.var(c))) + let + k = GS.genstring("$k"); + m = GS.genstring("$m"); + in M.lambda(vars @@ [k, m], T_c(body, M.var(k), M.var(m))) } (x) { x } } fn kToC(k) { - let rv = GS.genstring("$rv"); - in M.lambda([rv], k(M.var(rv))) + let + rv = GS.genstring("$rv"); + m = GS.genstring("$m"); + in M.lambda([rv, m], k(M.var(rv), M.var(m))) } - fn T_k(e, k) { + fn makeIdk() { + let + v = GS.genstring("$v"); + m = GS.genstring("$m"); + in M.lambda([v, m], M.apply(M.var(m), [M.var(v)])) + } + + fn captureCont(c) { + let + x = GS.genstring("$x"); + k = GS.genstring("$k"); + m = GS.genstring("$m"); + v = GS.genstring("$v"); + km = M.lambda([v], M.apply(M.var(k), [M.var(v), M.var(m)])); + in M.lambda([x, k, m], M.apply(c, [M.var(x), km])) + } + + fn captureWhole(c, m) { + let + x = GS.genstring("$x"); + k = GS.genstring("$k"); + m2 = GS.genstring("$m"); + in M.lambda([x, k, m2], M.apply(c, [M.var(x), m])) + } + + fn T(expr, halt) { + let + v = GS.genstring("$v"); + m = M.lambda([v], M.apply(halt, [M.var(v)])); + in T_c(expr, makeIdk(), m) + } + + fn T_k(e, k, m) { if (isAexpr(e)) { - k(M(e)) + k(M(e), m) } else { switch (e) { (M.back_expr) { @@ -41,69 +77,71 @@ namespace let c = kToC(k); in - M.amb_expr(T_c(expr1, c), T_c(expr2, c)) - } - - (M.apply(_, _)) { - let - c = kToC(k); - in - T_c(e, c) + M.amb_expr(T_c(expr1, c, m), T_c(expr2, c, m)) } - (M.callcc_expr(e)) { + (M.apply(_, _)) | + (M.callcc_expr(_)) | + (M.reset_expr(_)) | + (M.shift_expr(_)) { let c = kToC(k); in - T_c(M.callcc_expr(e), c) + T_c(e, c, m) } (M.cut_expr(e)) { - M.cut_expr(T_c(e, kToC(k))) + M.cut_expr(T_c(e, kToC(k), m)) } (M.cond_expr(test, branches)) { let c = kToC(k); in - T_k(test, fn (atest) { - M.cond_expr(atest, branches |> identity && T_c flip c) - }) + T_k(test, fn (atest, m1) { + M.cond_expr(atest, branches |> fn { + (#(e1, e2)) { + #(T_c(e1, c, m1), T_c(e2, c, m1)) + } + }) + }, m) } (M.if_expr(exprc, exprt, exprf)) { let c = kToC(k); in - T_k(exprc, fn(aexp) { - M.if_expr(aexp, T_c(exprt, c), T_c(exprf, c)) - }) + T_k(exprc, fn(aexp, m1) { + M.if_expr(aexp, T_c(exprt, c, m1), T_c(exprf, c, m1)) + }, m) } (M.letrec_expr(bindings, expr)) { - M.letrec_expr(bindings |> identity && (M && identity), T_k(expr, k)) + M.letrec_expr(bindings |> identity && (M && identity), T_k(expr, k, m)) } (M.make_vec(size, args)) { - Ts_k(args, fn (sargs) { - k(M.make_vec(size, sargs)) - }) + Ts_k(args, fn (sargs, m1) { + k(M.make_vec(size, sargs), m1) + }, m) } (M.match_cases(test, cases)) { let c = kToC(k); in - T_k(test, fn (atest) { - M.match_cases(atest, cases |> identity && T_c flip c) - }) + T_k(test, fn (atest, m1) { + M.match_cases(atest, cases |> identity && fn (caseExpr) { + T_c(caseExpr, c, m1) + }) + }, m) } - (M.sequence([expr])) { T_k(expr, k) } + (M.sequence([expr])) { T_k(expr, k, m) } (M.sequence(expr @ exprs)) { - T_k(expr, fn (ignored) { - T_k(M.sequence(exprs), k) - }) + T_k(expr, fn (ignored, m1) { + T_k(M.sequence(exprs), k, m1) + }, m) } (x) { @@ -115,9 +153,9 @@ namespace } } - fn T_c(expr, c) { + fn T_c(expr, c, m) { if (isAexpr(expr)) { - M.apply(c, [M(expr)]) + M.apply(c, [M(expr), m]) } else { switch(expr) { (M.back_expr) { @@ -127,86 +165,112 @@ namespace (M.amb_expr(expr1, expr2)) { let sk = GS.genstring("$k"); + sm = GS.genstring("$m"); vsk = M.var(sk); + vsm = M.var(sm); in - M.apply(M.lambda([sk], - M.amb_expr(T_c(expr1, vsk), - T_c(expr2, vsk))), - [c]) + M.apply(M.lambda([sk, sm], + M.amb_expr(T_c(expr1, vsk, vsm), + T_c(expr2, vsk, vsm))), + [c, m]) } (M.apply(p=M.primop(_), [e1, e2])) { - T_k(e1, fn (s1) { - T_k(e2, fn (s2) { - M.apply(c, [M.apply(p, [s1, s2])]) - }) - }) + T_k(e1, fn (s1, m1) { + T_k(e2, fn (s2, m2) { + M.apply(c, [M.apply(p, [s1, s2]), m2]) + }, m1) + }, m) } (M.apply(f, es)) { - T_k(f, fn(sf) { - Ts_k(es, fn (ses) {M.apply(sf, ses @@ [c])}) - }) + T_k(f, fn(sf, m1) { + Ts_k(es, fn (ses, m2) {M.apply(sf, ses @@ [c, m2])}, m1) + }, m) } (M.callcc_expr(e)) { - T_k(e, fn (sf) { - M.apply( - M.parse("(λ (f cc) (f (λ (x i) (cc x)) cc))"), - [sf, c] - ) - }) + T_k(e, fn (sf, m1) { + M.apply(sf, [captureWhole(c, m1), c, m1]) + }, m) } (M.cut_expr(e)) { - M.cut_expr(T_c(e, c)) + M.cut_expr(T_c(e, c, m)) + } + + (M.reset_expr(e)) { + let + v = GS.genstring("$v"); + in + T_c(e, + makeIdk(), + M.lambda([v], M.apply(c, [M.var(v), m]))) + } + + (M.shift_expr(e)) { + T_k(e, fn (sf, m1) { + M.apply(sf, [captureCont(c), makeIdk(), m1]) + }, m) } (M.cond_expr(test, branches)) { let sk = GS.genstring("$k"); + sm = GS.genstring("$m"); vsk = M.var(sk); + vsm = M.var(sm); in - M.apply(M.lambda([sk], T_k(test, fn (atest) { - M.cond_expr(atest, branches |> identity && T_c flip vsk) - })), [c]) + M.apply(M.lambda([sk, sm], T_k(test, fn (atest, m1) { + M.cond_expr(atest, branches |> fn { + (#(e1, e2)) { + #(T_c(e1, vsk, m1), T_c(e2, vsk, m1)) + } + }) + }, vsm)), [c, m]) } (M.if_expr(exprc, exprt, exprf)) { let sk = GS.genstring("$k"); + sm = GS.genstring("$m"); vsk = M.var(sk); + vsm = M.var(sm); in - M.apply(M.lambda([sk], T_k(exprc, fn (aexp) { - M.if_expr(aexp, T_c(exprt, vsk), T_c(exprf, vsk)) - })), [c]) + M.apply(M.lambda([sk, sm], T_k(exprc, fn (aexp, m1) { + M.if_expr(aexp, T_c(exprt, vsk, m1), T_c(exprf, vsk, m1)) + }, vsm)), [c, m]) } (M.letrec_expr(bindings, expr)) { - M.letrec_expr(bindings |> identity && (M && identity), T_c(expr, c)) + M.letrec_expr(bindings |> identity && (M && identity), T_c(expr, c, m)) } (M.make_vec(size, args)) { - Ts_k(args, fn (sargs) { - M.apply(c, [M.make_vec(size, sargs)]) - }) + Ts_k(args, fn (sargs, m1) { + M.apply(c, [M.make_vec(size, sargs), m1]) + }, m) } (M.match_cases(test, cases)) { let sk = GS.genstring("$k"); + sm = GS.genstring("$m"); vsk = M.var(sk); + vsm = M.var(sm); in - M.apply(M.lambda([sk], T_k(test, fn (atest) { - M.match_cases(atest, cases |> identity && T_c flip vsk) - })), [c]) + M.apply(M.lambda([sk, sm], T_k(test, fn (atest, m1) { + M.match_cases(atest, cases |> identity && fn (caseExpr) { + T_c(caseExpr, vsk, m1) + }) + }, vsm)), [c, m]) } - (M.sequence([expr])) { T_c(expr, c) } + (M.sequence([expr])) { T_c(expr, c, m) } (M.sequence(expr @ exprs)) { - T_k(expr, fn (ignored) { - T_c(M.sequence(exprs), c) - }) + T_k(expr, fn (ignored, m1) { + T_c(M.sequence(exprs), c, m1) + }, m) } (x) { @@ -219,12 +283,12 @@ namespace } fn Ts_k { - ([], k) { k([]) } - (h @ t, k) { - T_k(h, fn (hd) { - Ts_k(t, fn (tl) { - k(hd @ tl) - }) - }) + ([], k, m) { k([], m) } + (h @ t, k, m) { + T_k(h, fn (hd, m1) { + Ts_k(t, fn (tl, m2) { + k(hd @ tl, m2) + }, m1) + }, m) } } \ No newline at end of file diff --git a/fn/rewrite/desugar.fn b/fn/rewrite/desugar.fn index 6adf95e7..78dfa8fe 100644 --- a/fn/rewrite/desugar.fn +++ b/fn/rewrite/desugar.fn @@ -60,6 +60,14 @@ namespace M.cut_expr(desugar(e)) } + (E.reset_expr(e)) { + M.reset_expr(desugar(e)) + } + + (E.shift_expr(e)) { + M.shift_expr(desugar(e)) + } + (E.cond_expr(test, branches)) { M.cond_expr(desugar(test), branches |> desugar && desugar); } diff --git a/fn/rewrite/docs/delimited-cps.md b/fn/rewrite/docs/delimited-cps.md new file mode 100644 index 00000000..0d149777 --- /dev/null +++ b/fn/rewrite/docs/delimited-cps.md @@ -0,0 +1,358 @@ +# Delimited control CPS sketch for `fn/rewrite` + +This note defines a prototype rewrite target for `reset` and `shift` on the `fn/rewrite` CPS path. + +The goal is not to commit to final surface syntax or runtime representation yet. The goal is to pin down rewrite rules precise enough that: + +- they can be prototyped in `fn/rewrite/cps.fn` +- they can be validated against small examples in `fn/rewrite/samples.fn` +- they can later inform the C implementation on the `--target-b` / `--target-c` path + +## Scope + +This sketch assumes: + +- `shift/reset`, not `control/prompt` +- captured continuations behave as ordinary reusable values in the prototype +- delimited control only affects the ordinary success continuation +- `amb` remains a later, separate pass exactly as it is today + +That last point matches the current rewrite and C pipelines: first CPS, then `amb`/failure continuation plumbing. + +The rewrite prototype should model the standard multi-shot semantics by default. That keeps the laws and worked examples simple, and it matches the ordinary reading of a captured continuation as a function value that may be called more than once. If a later runtime wants one-shot continuations for performance or representation reasons, that should be introduced as a separate implementation restriction rather than baked into the prototype semantics. + +## IR extension + +The rewrite prototype will need two new forms in both `expr.fn` and `minexpr.fn`: + +```text +reset_expr(expr) +shift_expr(expr) +``` + +Suggested surface syntax for the prototype parser: + +```text +(reset e) +(shift f) +``` + +The operand of `shift` should evaluate to a function that receives the captured continuation as its first ordinary argument. + +## Why the current CPS transform is not enough + +`fn/rewrite/cps.fn` currently mirrors the C CPS pass closely: + +- `M` rewrites lambdas to accept one continuation argument +- `T_k` converts into higher-order CPS +- `T_c` converts against an explicit continuation expression + +That works for `call/cc`, because `call/cc` captures the whole current continuation already represented by the existing CPS pass. + +It is not enough for delimited control, because `reset` introduces a boundary that the transform itself must preserve. If we wait until after ordinary CPS, the boundary is no longer explicit in the right way. + +## Delimited CPS judgment + +Replace the one-continuation CPS judgment with a two-layer judgment: + +```text +T^d_k(e, k, m) +T^d_c(e, c, m) +M^d(e) +``` + +where: + +- `k` is the current continuation up to the nearest enclosing `reset` +- `m` is the meta continuation outside that `reset` +- `c` is the first-order representation of `k`, as in the current `T_c` + +Intuitively: + +- ordinary computation returns to `k` +- completing a delimited region returns through `m` +- `shift` captures `k`, not `m` + +## Calling convention + +The prototype should generalize the current CPS calling convention from: + +```text +lambda(args, body) => lambda(args @@ [k], ...) +``` + +to: + +```text +lambda(args, body) => lambda(args @@ [k, m], ...) +``` + +The generated continuation `k` itself becomes a two-argument function: + +```text +k(v, m) +``` + +This is the most direct generalization of the existing rewrite code, because applications can still append continuation parameters at the end. + +## Atomic translation + +For atomic expressions, the current computation just calls the local continuation: + +```text +T^d_c(a, c, m) = c(M^d(a), m) +``` + +The meta continuation is threaded through unchanged. + +## Lambda translation + +The atomic translation of lambdas becomes: + +```text +M^d(λ(args). body) = λ(args, k, m). T^d_c(body, k, m) +M^d(x) = x +``` + +This is the direct delimited analogue of the current `M` in `fn/rewrite/cps.fn`. + +## Helper continuations + +Two helper continuations are useful in the prototype. + +The first is the ordinary bridge from higher-order `T^d_k` to first-order `T^d_c`: + +```text +kToC^d(k) = λ(rv, m). k(rv, m) +``` + +The second is the empty continuation for the inside of a fresh `reset`: + +```text +idk = λ(v, m). m(v) +``` + +`idk` means: there is no more local work inside this reset; hand the value to the meta continuation for the reset. + +## Ordinary forms + +Every existing rule in `cps.fn` lifts by threading `m` through unchanged. + +Examples: + +```text +T^d_c((f e1 ... en), c, m) + = T^d_k(f, λ(sf, m1). + T^d_{s,k}(e1 ... en, + λ(sargs, m2). sf(sargs @@ [c, m2]), + m1), + m) +``` + +```text +T^d_c((if e1 e2 e3), c, m) + = T^d_k(e1, + λ(a1, m1). if a1 then T^d_c(e2, c, m1) else T^d_c(e3, c, m1), + m) +``` + +```text +T^d_c((begin e1 ... en), c, m) + = T^d_k(e1, + λ(_, m1). T^d_c((begin e2 ... en), c, m1), + m) +``` + +The important invariant is simple: unless a rule is specifically about `reset` or `shift`, it preserves the current delimiter structure and only threads `m` onward. + +## Reset rule + +`reset` installs a fresh local continuation boundary. + +The body of the reset runs with: + +- a fresh empty local continuation `idk` +- a meta continuation that resumes the surrounding local continuation + +Formally: + +```text +T^d_c(reset e, c, m) + = T^d_c(e, + idk, + λ(v). c(v, m)) +``` + +Read this as: + +- inside the reset, the current local continuation starts empty +- when the reset body finishes, its result is handed back to the continuation outside the reset + +This rule is the delimiter. It is the main reason this transform must be built into CPS itself rather than bolted on later. + +## Shift rule + +`shift` captures the current local continuation `c`, packages it as a function value, and removes that local continuation from the remainder of the body. + +The captured continuation must re-enter the saved context under a fresh delimiter. In this two-layer CPS formulation, that means the reified continuation receives its own caller continuation and meta continuation. + +Define the captured continuation as: + +```text +capture(c) = λ(x, k2, m2). c(x, λ(v). k2(v, m2)) +``` + +Intuition: + +- `c` is the saved local continuation up to the nearest reset +- calling the captured continuation with `x` plugs `x` into that saved context +- once that reinstated context reaches the reset boundary, control continues with the caller's current continuation `k2` + +The `shift` rule is then: + +```text +T^d_c(shift f, c, m) + = T^d_k(f, + λ(sf, m1). sf(capture(c), idk, m1), + m) +``` + +Read this as: + +- evaluate `f` +- pass it the captured continuation +- run the body of `f` with the current local continuation removed (`idk`) +- if the shift body returns normally, it exits to the enclosing reset via `m` + +This is the key distinction from `call/cc`: only the current delimited continuation is captured. + +## Call/cc in the unified transform + +Once the prototype is unified into a single two-layer CPS transform, `call/cc` should remain expressible directly rather than through a separate legacy path. + +In the unified transform, `call/cc` captures the whole current continuation, which in this representation is the pair `(c, m)`. + +The captured continuation can therefore be represented as: + +```text +captureWhole(c, m) = λ(x, k2, m2). c(x, m) +``` + +It ignores the continuation at the call site because invoking a `call/cc` continuation aborts the current continuation and reinstalls the captured one. + +The corresponding rule is: + +```text +T^d_c(call/cc f, c, m) + = T^d_k(f, + λ(sf, m1). sf(captureWhole(c, m1), c, m1), + m) +``` + +This keeps `call/cc` and `shift/reset` in a single reference transform while preserving their semantic difference: + +- `call/cc` captures the whole continuation `(c, m1)` +- `shift` captures only the local continuation `c` + +## Validation laws + +The rewrite prototype should validate against these laws first. + +These laws assume the captured continuation can be invoked multiple times. That is intentional: the rewrite prototype is the semantic reference point. A later one-shot runtime would need either a dynamic restriction on repeated invocation or a separate user-facing contract. + +### Basic reset laws + +```text +reset(v) ==> v +reset(reset(e)) ==> reset(e) +``` + +### Shift/reset law + +For an evaluation context `E` that does not cross `reset`: + +```text +reset(E[shift k. e]) + ==> reset(e[(λx. reset(E[x])) / k]) +``` + +This is the main substitution law the prototype should preserve. + +### Worked examples + +These are good first samples for `fn/rewrite/samples.fn` once parsing exists: + +```text +(reset 1) ==> 1 +(reset (+ 1 (shift (λ (k) 2)))) ==> 2 +(reset (+ 1 (shift (λ (k) (k 2))))) ==> 3 +(reset (+ 1 (shift (λ (k) (+ (k 2) (k 3)))))) ==> 7 +(+ 1 (reset (shift (λ (k) 2)))) ==> 3 +``` + +Those examples are small enough to inspect through the prototype pipeline stage-by-stage. + +## Prototype plan in `fn/rewrite` + +The minimal prototype sequence should be: + +1. Extend `fn/rewrite/expr.fn` with `reset_expr` and `shift_expr`, printer support, and parser support. +2. Extend `fn/rewrite/minexpr.fn` with the same two forms and printer support. +3. Extend `fn/rewrite/desugar.fn` to lower the new `expr` forms directly to `minexpr`. +4. Unify `fn/rewrite/cps.fn` around a single two-layer CPS transform. +5. Reuse the existing passes after CPS without changing their role. +6. Add small samples in `fn/rewrite/samples.fn` and inspect output through `fn/rewrite/test_harness.fn`. + +The recommended implementation strategy in `cps.fn` is: + +- generalize `T_k` / `T_c` to thread the extra meta continuation +- generalize lambda translation so all CPS-transformed lambdas accept `k` and `m` +- express `call/cc`, `reset`, and `shift` inside that single transform + +The temporary forked prototype can be useful while the equations are still in flux, but the reference implementation should converge back to one transform before informing the C implementation. + +## Interaction with `amb` + +Do not fold `amb` into the delimited-control design initially. + +The current architecture already treats success and failure control separately. The prototype should keep that split: + +- delimited CPS first, producing success-side control plumbing +- `amb.fn` afterwards, appending failure continuation structure + +If later work wants delimited failure control too, that should be a separate design step. + +## What to validate in the prototype + +There are two distinct validation targets. + +### Structural validation + +Inspect the generated CPS for these invariants: + +- transformed lambdas now accept `k` and `m` +- ordinary applications append both continuation parameters +- `reset` introduces `idk` +- `shift` packages the current continuation with `capture(c)` + +### Behavioral validation + +Use small samples and compare them against the laws above. + +For the first round, it is enough to confirm: + +- `shift` can discard the surrounding local context +- invoking the captured continuation re-enters the saved context +- that re-entry is delimited and returns to the call site of the captured continuation + +## Non-goals for the first prototype + +These should stay out of the first cut: + +- prompt tags +- `control`/`prompt` semantics +- runtime enforcement of one-shot use +- CEKF runtime support +- user-facing generator syntax + +If the prototype validates, the next step is to decide whether to expose raw `shift/reset` surface syntax or to build `yield` as the user-facing feature on top of the same machinery. diff --git a/fn/rewrite/docs/delimited-infer-expr-checklist.md b/fn/rewrite/docs/delimited-infer-expr-checklist.md new file mode 100644 index 00000000..bb165c7e --- /dev/null +++ b/fn/rewrite/docs/delimited-infer-expr-checklist.md @@ -0,0 +1,425 @@ +# Implementation Checklist for `infer_expr.fn` + +This note turns [delimited-typing-rules.md](delimited-typing-rules.md) into a file-local checklist against [infer_expr.fn](../infer_expr.fn). + +The goal is not to restate the full design. The goal is to make it obvious, from the structure of `infer_expr.fn` itself, what needs to change and in what order. + +This checklist is intentionally scoped to one file. It assumes the representation choice from [delimited-type-representation.md](delimited-type-representation.md) and the breadth-first analyzer plan from [delimited-typing-rules.md](delimited-typing-rules.md). + +## Current File Shape + +`infer_expr.fn` currently has five broad regions: + +1. `typeExp` plus small type constructors such as `tupleType`, `thunkType`, and `funType` +2. generic type operations such as substitution, occurs check, unification, instantiation, rendering, and canonicalization +3. support predicates and expression-list helpers +4. environment, letrec, constructor, and primitive-analysis helpers +5. the main `analyzeExpr` dispatcher plus `infer`, `infer_string`, and `infer_to_string` + +The safest implementation order is to preserve that structure while making each region delimited-control aware. + +## Working Rule for This Checklist + +When this note says a function should be “threaded”, it means the function should be updated to carry: + +```text +answerIn, answerOut, controlAllowed +``` + +either directly in its signature or indirectly via a narrower helper that preserves the same information. + +## Section A: Type Representation Block + +This section covers the top of the file through the basic type constructors. + +### `typeExp` + +- [x] Replace the current callable encoding inside `operType` with explicit callable constructors. +- [x] Keep `varType` unchanged. +- [x] Keep `operType` for non-callable named constructors such as `Int`, `Bool`, `Null`, `list`, and `Tuple`. +- [x] Add explicit constructors for pure and controlful thunks. +- [x] Add explicit constructors for pure and controlful unary functions. + +### Small type constructor helpers + +- [x] Keep `intType`, `boolType`, `charType`, `stringType`, `nullValueType`, and `tupleType` as ordinary named-type helpers. +- [x] Rewrite `thunkType` and `funType` to construct explicit callable nodes rather than `operType("Thunk", ...)` and `operType("->", ...)`. +- [x] Keep `funTypeList`, but make it build explicit nested callable nodes. +- [x] Add `controlThunkType` helper. +- [x] Add `controlFunType` helper. +- [x] Add a helper that normalizes `controlThunkType(R, A, A)` to `thunkType(R)`. +- [x] Add a helper that normalizes `controlFunType(X, R, A, A)` to `funType(X, R)`. +- [x] Add a helper for building curried callables whose rightmost callable node is controlful. + +### Fresh variables and names + +- [x] Keep `freshTypeVar` unchanged. +- [x] Keep `typeVarName` unchanged. +- [x] Do not introduce a second fresh-variable source specifically for answer types. + +## Section B: Generic Type Operations + +This section covers the functions that walk or compare `typeExp` structurally. + +### Substitution + +- [x] Update `applySubst` to recurse through each new callable constructor explicitly. +- [x] Keep `applySubstList` for `operType` argument lists. +- [ ] Add any callable-specific child helpers only if the pattern matching becomes too repetitive. + +### Occurs check + +- [x] Update `occursInType` to recurse through explicit thunk and function constructors. +- [x] Keep `occursInTypeList` for `operType` argument lists. + +### Unification + +- [x] Extend `unifyType` with structural cases for: + - pure thunk with pure thunk + - pure function with pure function + - controlful thunk with controlful thunk + - controlful function with controlful function +- [x] Keep `operType` unification for ordinary named constructors. +- [ ] Do not add implicit coercions between pure callables and controlful callables here. +- [ ] Keep purity normalization outside the unifier. +- [x] Preserve the current occurs-check behavior for type variables. +- [x] Keep `unifyArgs` for `operType` argument lists. + +### Instantiation and freshness + +- [x] Update `instantiateApplied` to recurse structurally through the new callable constructors. +- [x] Keep `instantiateArgs` for `operType` argument lists. +- [x] Keep `freshType` as the environment-instantiation entrypoint. +- [x] Make sure freshening preserves controlful callables instead of flattening them back into generic operators. + +### Rendering and canonicalization + +- [x] Update `renderType` with explicit cases for pure and controlful thunks. +- [x] Update `renderType` with explicit cases for pure and controlful functions. +- [x] Update `renderDomType` so controlful callable domains print with parentheses when needed. +- [x] Keep readable output for pure types unchanged where possible. +- [x] Update `canonicalizeType` to recurse structurally through the new callable constructors. +- [x] Keep `canonicalizeArgs` for `operType` argument lists. +- [ ] Verify that canonicalization plus rendering still produce stable letrec snapshots. + +## Section C: Support Predicates and Front-Door Gating + +This section covers the `supports*` family. + +### `supports` + +- [x] Add explicit support handling for `reset_expr` once the branch is implemented. +- [x] Add explicit support handling for `shift_expr` once the branch is implemented. +- [x] Decide whether unsupported delimited-control expressions should return `false` here before their typing branches land, rather than falling through implicitly. +- [x] Keep `make_vec` unsupported. +- [x] Keep the current primitive allowlist until delimited typing is stable. + +### `supportsList`, `supportsNonEmptyList`, `supportsBindings`, `supportsCondCases`, `supportsCondCasesTail`, `supportsMatchCases`, `supportsMatchCasesTail` + +- [x] Update only as needed for `reset_expr` and `shift_expr` propagation. +- [x] Do not redesign these helpers unless the analyzer rollout exposes a concrete gap. + +## Section D: New Analyzer-Level Helper Layer + +This section is new work rather than migration of existing helpers. + +### Analyzer entry helpers to add + +- [x] Add an effect-aware `analyzeExpr` signature carrying `answerIn`, `answerOut`, and `controlAllowed`. +- [ ] Add a small wrapper for pure ambient contexts, if that keeps branches readable. +- [x] Add a helper that creates fresh local answer-type pairs for lambda bodies and reset bodies. + +### Callable builder helpers to add + +- [x] Add `makeLambdaCallable` for zero-argument lambdas. +- [x] Add `makeLambdaCallableChain` for curried lambdas. +- [x] Make these helpers responsible for purity normalization after substitution has been applied. + +### Callable consumer helpers to add + +- [x] Add `consumeThunkCallable`. +- [x] Add `consumeCurriedCallable`. +- [x] Keep callable-consumption logic out of `unifyType`. +- [x] Let these helpers enforce `controlAllowed` when a controlful callable is actually invoked. +- [x] Let these helpers instantiate type variables to controlful callable skeletons when needed. + +### Argument threading helpers to add or replace + +- [x] Replace the current `analyzeArgs` with an effect-threaded version. +- [x] Thread answer types left-to-right through argument evaluation. +- [x] Preserve current source evaluation order. + +## Section E: Existing Mid-Level Helper Migration + +This section covers the helpers below the support predicates and above the `analyzeExpr` dispatcher. + +### `analyzeArgs` + +- [x] Expand the signature to thread `answerIn`, `answerOut`, and `controlAllowed`. +- [x] Preserve left-to-right evaluation. +- [x] Return the argument type list plus the updated substitution as it does now. + +### `analyzeCondCases` and `analyzeMatchCases` + +- [x] Expand both helpers to thread answer types explicitly. +- [x] Ensure each branch starts from the same post-test answer state. +- [ ] Keep branch result-type unification logic unchanged in spirit. + +### `bindParams` + +- [x] Keep parameter binding structurally unchanged. +- [x] Do not add answer-type variables here; those belong to lambda-body analysis, not parameter binding. + +### `analyzeLetBindings` + +- [x] Expand the helper to thread answer types left-to-right through binding expression evaluation. +- [ ] Keep the environment-extension result unchanged in shape. + +### `extendTypeEnv` + +- [x] No semantic change expected. +- [ ] Only touch if explicit callable constructors require a small representation update. + +### `analyzeSequence` + +- [x] Expand the helper to thread answer types left-to-right. +- [x] Preserve “last expression determines result type”. + +### Letrec helpers + +This group includes: + +- `bindRecBindings` +- `finalizeRecBindings` +- `snapshotRecBindings` +- `snapshotRecBindingsAcc` +- `processRecBinding` +- `checkRecBindings` +- `processFirstRecBindings` +- `checkRecLambdaBindings` +- `iterateRecBindings` + +Checklist: + +- [x] Keep the broad letrec strategy unchanged for the first pass. +- [x] Update recursive binder snapshots so controlful callables print deterministically. +- [x] Expand `processRecBinding` so lambda bodies are analyzed through the new effect-aware analyzer. +- [x] Keep answer-type generalization policy out of this first migration. +- [x] Defer any letrec soundness redesign beyond what the new representation and analyzer interface force. + +### Primitive and constructor helpers + +This group includes: + +- `analyzePrimitive` +- `analyzeConstruct` +- `ctorTypeToTypeExp` +- `ctorTypeArgList` +- `spineArg` +- `spineResult` + +Checklist: + +- [x] Expand `analyzePrimitive` to thread answer types through left and right operands. +- [x] Keep the primitive result-type rules unchanged. +- [x] Expand `analyzeConstruct` only through the new application path. +- [x] Update `ctorTypeToTypeExp` so constructor arrows become explicit pure `funType` nodes. +- [x] Update `spineArg` to match explicit `funType` instead of `operType("->", ...)`. +- [x] Update `spineResult` to walk explicit `funType` nodes. +- [ ] Decide explicitly whether constructor types should remain always pure in the first cut. + +## Section F: `analyzeExpr` Branch Checklist + +This section maps each current branch family to the intended migration work. + +## Atomic and wrapper branches + +This group includes: + +- `E.var` +- `E.bigint` +- `E.stdint` +- `E.character` +- constant branches +- `E.cut_expr` +- `E.typeof_expr` +- `E.print_exp` +- `E.tag` + +Checklist: + +- [x] Make atomic value branches unify `answerIn` with `answerOut`. +- [x] Keep their direct result types unchanged. +- [x] Make wrapper branches preserve their child expression's answer threading rather than silently forcing purity. + +## Lambda branches + +This group includes: + +- `E.lambda([], body)` +- `E.lambda(params, body)` + +Checklist: + +- [x] Analyze lambda bodies under fresh local answer types. +- [x] Analyze lambda bodies with `controlAllowed = true`. +- [x] Keep lambda construction itself pure in the surrounding context. +- [x] Route the result through the new callable-builder helpers. +- [x] Normalize pure latent effects back to pure callable types when possible. + +## Application branches + +This group includes: + +- `E.apply(fun, [])` +- `E.apply(fun, args)` + +Checklist: + +- [x] Decompose application into function evaluation, argument evaluation, and callable consumption. +- [x] Thread answer types through function evaluation. +- [x] Thread answer types through argument evaluation in source order. +- [x] Route zero-argument calls through `consumeThunkCallable`. +- [x] Route non-empty applications through `consumeCurriedCallable`. +- [x] Reject controlful callable invocation when `controlAllowed = false`. + +## Control-related existing branch + +This group includes: + +- `E.callcc_expr` + +Checklist: + +- [x] Keep this branch special-cased for the first pass. +- [x] Update it only enough to use explicit pure `funType` construction. +- [x] Do not force `call/cc` into the new delimited-control rule set yet. +- [x] Treat `call/cc` as a whole-continuation operator, not as evidence that a lambda should be classified as a reset-gated controlful callable. +- [ ] Revisit `call/cc` only in the later reconciliation phase once `answerIn` / `answerOut` threading is stable across the analyzer. + +## Branching expressions + +This group includes: + +- `E.if_expr` +- `E.cond_expr` +- `E.match_cases` + +Checklist: + +- [x] Evaluate the test or scrutinee first and thread the answer state through it. +- [x] Start each branch from the same post-test answer state. +- [x] Make both branches or all cases end at the same final `answerOut`. +- [x] Keep existing branch result-type unification logic. + +## Binding expressions + +This group includes: + +- `E.let_expr` +- `E.letrec_expr` +- `E.letstar_expr` + +Checklist: + +- [x] Thread answer types through binding evaluation before entering the body. +- [x] Keep environment extension logic structurally unchanged. +- [x] Keep the letrec fixpoint loop intact unless the new analyzer interface forces a small local rewrite. + +## Data and constructor expressions + +This group includes: + +- `E.construct` +- `E.deconstruct` +- `E.make_tuple` +- `E.make_vec` +- `E.primapp` +- `E.tuple_index` +- `E.typedefs` + +Checklist: + +- [x] Thread answer types through any evaluated subexpressions. +- [x] Keep the final constructor or tuple shape itself pure. +- [x] Keep `make_vec` unsupported. +- [x] Keep typedef environment extension behavior unchanged. + +## Sequence and nondeterminism-adjacent expressions + +This group includes: + +- `E.sequence` +- `E.amb_expr` +- `E.back_expr` + +Checklist: + +- [x] Expand `sequence` to explicit left-to-right answer threading. +- [x] Decide whether `amb_expr` should simply thread both sides through the new analyzer without deeper redesign in this pass. +- [x] Decide whether `back_expr` remains a placeholder returning a fresh type variable for now. +- [x] Keep these decisions explicit rather than letting them drift as accidental behavior. + +## New branches to add + +This group includes: + +- `E.reset_expr` +- `E.shift_expr` + +Checklist: + +- [x] Add `E.reset_expr` only after the general analyzer threading is in place. +- [x] Analyze `reset` bodies under fresh local answer types and `controlAllowed = true`. +- [x] Make `reset` pure to the outside by unifying the surrounding `answerIn` with `answerOut`. +- [x] Return the body's outgoing answer type as the direct result type of `reset`. +- [x] Add `E.shift_expr` only after callable builders and consumers are stable. +- [x] Require `controlAllowed = true` in `shift`. +- [x] Check `shift` operands against the rewrite function-argument form described in the rules note. +- [x] Make `shift` return the captured hole type, not the shift-body result type. +- [x] Use the ambient answer-type change of the `shift` expression itself to carry the captured answer to shift-body result transition. + +## Section G: Entry Points and Public Surface + +This section covers the bottom of the file. + +### `infer` + +- [x] Make `infer` create one fresh top-level answer variable. +- [x] Call the effect-aware `analyzeExpr` with identical `answerIn` and `answerOut` at top level. +- [x] Set top-level `controlAllowed = false`. +- [x] Normalize the final type after substitution so pure callables do not print as controlful callables with identical answer types. + +### `infer_string` and `infer_to_string` + +- [x] Keep both entrypoints structurally unchanged. +- [x] Let them inherit the new normalized output through `infer` and `renderType`. + +## Section H: Suggested Implementation Order + +Use this order to keep diffs reviewable and failures localized. + +1. [x] Change `typeExp` plus the small callable constructor helpers. +2. [x] Update substitution, occurs check, unification, instantiation, rendering, and canonicalization. +3. [x] Update constructor spine helpers and any pure arrow assumptions. +4. [x] Add the new analyzer signature and thread it through existing helpers without changing branch meaning yet. +5. [x] Add callable builders, callable consumers, and effect-threaded `analyzeArgs`. +6. [x] Migrate lambda and apply branches. +7. [x] Migrate ordered pure branches, branching forms, and binding forms. +8. [x] Add `reset_expr`. +9. [x] Add `shift_expr`. +10. [x] Revisit `supports` and any temporary placeholders such as `amb_expr` and `back_expr`. + +## Section I: Minimal Validation Checklist + +This note is file-local, but a few checks should be tied to the implementation order. + +1. [x] After explicit callable constructors land, verify that pure programs still render pure arrow and thunk types unchanged. +2. [x] After the analyzer signature is threaded everywhere, verify that the file still supports the existing non-delimited expression subset. +3. [x] After lambda and apply migration, verify that partial application still produces the expected nested callable types. +4. [x] After `reset_expr` lands, verify that internal answer-type change is hidden from the surrounding context. +5. [x] After `shift_expr` lands, verify that named helpers infer latent controlful callable types and that invoking them outside a delimiter is rejected. + +## Final Intent + +The implementation target for [infer_expr.fn](../infer_expr.fn) should now be explicit enough to track line-by-line work without having to reinterpret the broader planning notes each time. diff --git a/fn/rewrite/docs/delimited-type-representation.md b/fn/rewrite/docs/delimited-type-representation.md new file mode 100644 index 00000000..f8d40ba1 --- /dev/null +++ b/fn/rewrite/docs/delimited-type-representation.md @@ -0,0 +1,365 @@ +# Plan for Delimited Type Representation in `fn/rewrite` + +This note narrows Phase 2 of [delimited-typechecking-plan.md](delimited-typechecking-plan.md). + +Breadth-first analyzer rule skeletons using this representation are expanded in [delimited-typing-rules.md](delimited-typing-rules.md). + +The goal here is not to finish the typing rules. The goal is to choose a concrete representation for delimited-control types in [infer_expr.fn](../infer_expr.fn) so the later rule work has a stable target. + +This note is intentionally scoped to `fn/rewrite`. Porting choices are out of scope for now, but when two representations are otherwise comparable this note prefers the one that will be easier to translate into explicit C structures later. + +## Current Anchor + +The current rewrite inferencer uses this shape: + +```text +typedef typeExp { + varType(string) + | operType(string, list(typeExp)) +} +``` + +That means all structured types are currently encoded through `operType`, including: + +- ordinary arrows via `operType("->", [dom, cod])` +- thunks via `operType("Thunk", [type])` +- tuples via `operType("Tuple", parts)` + +This works for ordinary HM because the inferencer only needs generic traversal plus a few printer and matcher special cases. + +Delimited control changes the pressure on this design for three reasons. + +First, a named function must carry latent answer-type behavior in its own type. + +Second, zero-argument lambdas are represented distinctly as thunks in [infer_expr.fn](../infer_expr.fn), so the representation has to account for controlful thunks as well as controlful arrows. + +Third, recursive-binding convergence currently depends on `canonicalizeType` and `renderType` producing stable strings, so any new type shape must remain easy to canonicalize and print deterministically. + +## Representation Requirements + +The chosen representation should satisfy all of these. + +### Requirement 1: Latent control must live in the type + +The control behavior of a named function cannot be reconstructed later from syntax. + +That rules out plans that keep answer-type change only in expression-analysis side state or only on `shift` syntax nodes. + +### Requirement 2: Answer types stay ordinary types + +For the first cut, the answer types in + +$$ +[\alpha \mapsto \beta] +$$ + +should remain ordinary `typeExp` values. + +Do not introduce a second class of answer-only variables or a second substitution engine. The same unifier should continue to handle: + +- value result types +- function argument types +- pre-shift answer types +- post-shift answer types + +The restriction on answer-type polymorphism should be enforced by generalization policy, not by inventing a separate representation for answer variables. + +### Requirement 3: Partial application must preserve the latent effect + +If a multi-argument function body contains `shift`, then partially applying the first arguments should produce another function value that still carries the latent answer-type change. + +For example, if the source-level reading is: + +```text +lambda(x, y). body +``` + +with body result type `R` and latent answer-type change `[A => B]`, then after applying the first argument the resulting value must still know that applying the remaining argument may change the answer type from `A` to `B`. + +### Requirement 4: Zero-argument lambdas must be handled explicitly + +Current rewrite inference treats `lambda([], body)` as a thunk, not as an ordinary unary function over unit. + +That means a representation that only adds a controlful arrow and leaves thunks pure is incomplete. + +### Requirement 5: The representation should remain first-order and explicit + +The inferencer already performs direct recursive traversals in: + +- `applySubst` +- `occursInType` +- `unifyType` +- `instantiateApplied` +- `canonicalizeType` +- `renderType` + +The delimited-control representation should fit that style cleanly. It should not require higher-order encodings, hidden side tables, or effect-specific unification logic scattered across the analyzer. + +### Requirement 6: Debug output must stay readable + +Recursive binding iteration uses canonicalized string snapshots, so `renderType` must remain easy to read and easy to stabilize. + +If the representation is difficult to print clearly, it will be difficult to debug letrec behavior later. + +## Options Considered + +## Option A: Keep everything inside `operType` + +One possibility is to keep `typeExp` unchanged and encode delimited-control callables with new operator names such as: + +```text +operType("Ctl->", [arg, result, answerIn, answerOut]) +operType("CtlThunk", [result, answerIn, answerOut]) +``` + +### Option A Advantages + +- smallest immediate change to the `typeExp` definition +- generic substitution, unification, and instantiation continue to work automatically +- easy to prototype quickly + +### Option A Disadvantages + +- callable shapes remain stringly typed +- printer logic has to keep recognizing special operator names manually +- the representation gives up static structure exactly where the typechecker most needs clarity +- later C porting would have to recover explicit structure that rewrite chose not to model directly + +### Option A Verdict + +This is acceptable as a quick spike but not as the representation to plan around. + +## Option B: Represent delimited control as a wrapped computation result + +Another possibility is to keep ordinary arrows pure and wrap only the codomain of controlful functions, conceptually along these lines: + +```text +funType(arg, controlResultType(result, answerIn, answerOut)) +``` + +Under this approach, application would produce a special computation-result type, and expression analysis would interpret that wrapper as the latent answer-type change. + +### Option B Advantages + +- partial application works naturally because the effect lives at the end of the arrow chain +- ordinary arrows stay syntactically ordinary + +### Option B Disadvantages + +- the distinction between value types and computation types becomes more implicit +- zero-argument thunks still need special treatment +- variables and environment entries now carry a wrapper that is not itself a normal value type +- this drifts away from the direct-style function reading in [delimited-types.md](delimited-types.md) + +### Option B Verdict + +This is conceptually possible, but it makes the representation less direct than necessary for the first cut. + +## Option C: Add explicit controlful callable constructors + +This option keeps ordinary named types in `operType` but makes callable shapes explicit. + +Recommended shape: + +```text +typedef typeExp { + varType(string) + | operType(string, list(typeExp)) + | thunkType(typeExp) + | funType(typeExp, typeExp) + | controlThunkType(typeExp, typeExp, typeExp) + | controlFunType(typeExp, typeExp, typeExp, typeExp) +} +``` + +with the following intended meanings: + +- `thunkType(result)` means a pure zero-argument computation returning `result` +- `funType(arg, result)` means a pure unary function +- `controlThunkType(result, answerIn, answerOut)` means a zero-argument computation with latent answer-type change +- `controlFunType(arg, result, answerIn, answerOut)` means a unary function whose body may change the answer type when called under `reset` + +### Option C Advantages + +- latent control is explicit in the type tree +- pure and controlful callables are easy to distinguish in application rules +- zero-argument lambdas are handled directly instead of as a footnote +- later C porting will be easier because callable forms are already explicit structures +- printer support can remain readable and deterministic + +### Option C Disadvantages + +- more initial rewrite work than Option A +- the generic type walkers need new cases for callable constructors + +### Option C Verdict + +This is the recommended representation. + +## Recommended Representation + +Use Option C. + +More specifically: + +1. Keep ordinary algebraic and named types in `operType`. +2. Pull callable forms out into explicit constructors. +3. Represent answer input and answer output as ordinary `typeExp` children. +4. Keep pure callables and controlful callables distinct in the representation. +5. Let generalization policy, not the type representation, decide which answer variables are non-generic. + +This gives the rewrite inferencer an explicit internal model without forcing it to redesign all non-callable types at the same time. + +## How Multi-Argument Functions Should Be Represented + +Current rewrite inference already represents multi-argument functions as nested unary arrows. + +That should remain true. + +The latent answer-type change should live at the rightmost callable node, because that is the point where the function body actually runs. + +For a pure two-argument function: + +```text +A -> B -> R +``` + +keep the current nested shape: + +```text +funType(A, funType(B, R)) +``` + +For a two-argument function whose body has latent answer-type change `[X => Y]`, use: + +```text +funType(A, controlFunType(B, R, X, Y)) +``` + +That means partial application to the first argument returns a value whose type still records the remaining control behavior. + +For a zero-argument function with latent answer-type change `[X => Y]`, use: + +```text +controlThunkType(R, X, Y) +``` + +This is the main reason the representation needs both controlful arrows and controlful thunks. + +## How `shift` Should See the Captured Continuation + +For the first cut, the captured continuation passed into `shift` should still use ordinary pure callable types. + +Under the binder presentation: + +$$ +k : \tau \to \alpha +$$ + +the continuation is just an ordinary function from the hole type to the pre-shift answer type. + +That means the representation does not need a special continuation constructor. + +For rewrite `(shift f)`, the first implementation target remains: + +$$ +f : (\tau \to \alpha) \to \beta +$$ + +with the ambient answer-type change carried by the surrounding expression analysis, not by a separate continuation-specific type family. + +## Suggested Printer Shape + +The exact printer syntax can still change, but the representation plan should reserve readable forms for debugging. + +Suggested forms: + +- pure thunk: `#() -> R` +- controlful thunk: `#() -[X=>Y]-> R` +- pure function: `A -> R` +- controlful function: `A -[X=>Y]-> R` + +Examples: + +- `funType(A, controlFunType(B, R, X, Y))` prints as `A -> (B -[X=>Y]-> R)` +- `controlThunkType(R, X, Y)` prints as `#() -[X=>Y]-> R` + +This keeps snapshots readable while making latent answer-type behavior hard to miss. + +## Consequences for `infer_expr.fn` + +Even before adding `reset` and `shift` rules, the representation change will require coordinated updates in a small number of places. + +### Callable constructors and builders + +- replace helper functions that currently encode arrows and thunks via `operType` +- keep a helper for pure arrow chains +- add a helper for building arrow chains whose rightmost callable node is controlful + +### Recursive type walkers + +- `applySubst` +- `occursInType` +- `instantiateApplied` +- `canonicalizeType` + +Each of these should recurse structurally through the new callable constructors. + +### Unification + +`unifyType` should treat: + +- pure thunk with pure thunk +- pure function with pure function +- controlful thunk with controlful thunk +- controlful function with controlful function + +as ordinary structural unification cases. + +Do not add magical coercions from pure callable types to controlful callable types inside `unifyType`. If a rule wants to treat purity as the special case where `answerIn == answerOut`, it should do so explicitly in the analyzer logic. + +### Rendering and snapshot stability + +- `renderType` +- `renderDomType` +- `canonicalizeType` +- recursive binding snapshots + +These must all gain explicit cases for controlful callables so the letrec fixpoint logic remains stable and debuggable. + +## Recommended Staging Inside `fn/rewrite` + +Implement the representation in three small steps. + +### Stage 1: Make callable forms explicit without changing behavior + +- introduce explicit pure `thunkType` and `funType` constructors in `typeExp` +- keep all existing inference behavior otherwise unchanged +- preserve the current printed surface for pure types + +### Stage 2: Add controlful callable constructors + +- add `controlThunkType` and `controlFunType` +- update substitution, unification, canonicalization, and rendering +- do not yet add `reset` or `shift` typing rules + +### Stage 3: Build rules on top of the new representation + +- lambda typing chooses between pure and controlful callable constructors +- application threads answer types and consumes the new callable shapes +- `reset` and `shift` rules are added only after the representation is stable + +This keeps the representation decision isolated from the later rule work. + +## Final Recommendation + +For `fn/rewrite`, the representation plan should be: + +- keep `operType` for ordinary named type constructors +- make pure callables explicit +- add explicit `controlFunType` and `controlThunkType` +- keep answer types as ordinary `typeExp` children +- store latent answer-type change at the rightmost callable node in a curried chain +- avoid stringly `operType` encodings for controlful callables + +That is the best balance between rewrite-local clarity, incremental implementation, and later portability into explicit C data structures. diff --git a/fn/rewrite/docs/delimited-typechecking-plan.md b/fn/rewrite/docs/delimited-typechecking-plan.md new file mode 100644 index 00000000..115e3960 --- /dev/null +++ b/fn/rewrite/docs/delimited-typechecking-plan.md @@ -0,0 +1,351 @@ +# Plan for Typechecking Delimited Continuations + +This document expands [delimited-types.md](delimited-types.md) into an implementation roadmap. + +The goal is not to settle every typing detail up front. The goal is to define a sequence of steps that can be validated one at a time in the rewrite prototype, then translated into the C typechecker without redesigning the whole approach again. + +The recommended order is driven by the real compiler pipeline: + +1. Fix the source-level typing model at the shared early typechecking stage, before ANF or target-specific CPS. +2. Carry those guarantees through the rest of the pipeline instead of trying to recover them after lowering. +3. Use the rewrite CPS transform as a semantic cross-check, not as the main typing gate. +4. Keep the rewrite prototype and the C typechecker aligned around that same early model. + +That keeps the guarantees available to earlier transforms, works for both the ANF-based CEKF path and the target-b path, and still leaves room to use the rewrite CPS note as an operational oracle. + +## Current Starting Point + +- The rewrite IR already contains `reset_expr` and `shift_expr` in [expr.fn](../expr.fn) and [minexpr.fn](../minexpr.fn). +- The rewrite inference engine in [infer_expr.fn](../infer_expr.fn) still assumes plain HM types and only has a special case for `callcc_expr`. +- The C typechecker in [src/tc.yaml](../../../src/tc.yaml) and [src/tc_analyze.c](../../../src/tc_analyze.c) likewise models ordinary function types plus a special-case `call/cc` rule. +- In the real compiler pipeline, typechecking is supposed to establish guarantees before later lowering steps such as ANF or any target-specific CPS split. Delimited-control typing therefore has to live at that shared earlier stage. +- More concretely, that early stage is the `expr.fn` / `src/lambda.yaml`-like layer. Desugaring to `minexpr.fn` / `src/minlam.yaml` happens shortly afterward, and most later transforms then run on that minimal core. +- [delimited-types.md](delimited-types.md) defines the direct-style semantic judgment + +$$ +\Gamma \vdash e : \tau [\alpha \mapsto \beta] +$$ + + and the corresponding latent function type carrying answer-type change. + +- The rewrite syntax uses `(shift f)` rather than the binder presentation `shift k. e`, so the implementation plan must state how those two views correspond. + +## Desired End State + +By the end of this work: + +- source-level typing can express that an expression has both a value type and an answer-type effect +- named functions can carry latent delimited-control behavior in their function types +- `reset` discharges internal answer-type change at the delimiter boundary +- `shift` captures only the local continuation up to the nearest `reset` +- the implementation uses explicit type structures rather than syntax-local inspection at call sites +- both target-b and the older CEKF/ANF path rely on the same early typing guarantees +- the rewrite prototype and the C typechecker follow the same conceptual model + +## Decisions To Freeze Before Coding + +These choices should be fixed before implementing source-level typing. + +### 1. Keep delimited typing on the shared early pipeline + +Delimited-continuation typing cannot be deferred to post-CPS typing. + +The reasons are structural: + +- earlier transforms need the guarantees that typing provides +- the CEKF/ANF path never passes through target-b CPS +- later lowerings should consume already-typed source terms rather than becoming the place where well-typedness is rediscovered + +The rewrite CPS transform is still useful, but only as a secondary semantic cross-check. + +### 2. Keep the direct-style note as the semantic source of truth + +[delimited-types.md](delimited-types.md) should remain the reference for the typing judgment and the intended meaning of `reset` and `shift`. + +The implementation may use different helper functions or a different internal representation, but it should not invent a second semantic story. + +### 3. Treat rewrite `shift` syntax as the implementation form of the binder rule + +The note presents: + +```text +shift k. e +``` + +The rewrite prototype currently represents: + +```text +(shift f) +``` + +For the first typing pass, treat `(shift f)` as the implementation form of `shift k. e`, where `f` is a pure function that receives the captured continuation. + +Recommended first constraint: + +$$ +f : (\tau \to \alpha) \to \beta +$$ + +and therefore: + +$$ +\Gamma \vdash \operatorname{shift}\ f : \tau [\alpha \mapsto \beta] +$$ + +This keeps the first implementation close to the rule in [delimited-types.md](delimited-types.md) without forcing a new binder form into the rewrite syntax. + +### 4. Keep answer-type variables monomorphic at first + +Do not attempt full answer-type polymorphism in the first implementation. + +For the first cut: + +- answer-type variables are non-generalizable by default +- bindings whose types mention answer-type variables remain monomorphic unless there is an explicit annotation story +- recursive controlful bindings should remain restricted until the basic rules are stable + +This matches the caution already described in [delimited-types.md](delimited-types.md). + +### 5. Use an explicit implementation representation for controlful functions + +The theory can present all functions uniformly, but the implementation should make the control effect explicit. + +Recommended incremental representation: + +- in the rewrite inferencer, add a dedicated controlful function type constructor, or an equivalent `operType` encoding with explicit `answerIn` and `answerOut` +- in the C typechecker, add a corresponding explicit `TcType` variant or generated structure rather than relying on side channels + +Pure functions can then be treated as the special case where `answerIn` and `answerOut` unify. + +This is easier to inspect, easier to print in errors, and easier to port into generated C structures than an implicit effect discipline. + +## Phase 1: Fix the Shared Typing Boundary + +**Objective:** place delimited-continuation typing at the same shared early stage as the rest of source-level typechecking. + +### Phase 1 Work + +- Anchor delimited-continuation typing at the `expr.fn` / `src/lambda.yaml`-like layer, before `desugar.fn` / `src/lambda_desugar.c` lowers into `minexpr.fn` / `src/minlam.yaml`. +- Document which guarantees later passes are allowed to rely on once delimited typing succeeds. +- Decide whether those guarantees need explicit type annotations on the earlier lambda/expr nodes or whether the successful checker plus existing environments are sufficient. +- State explicitly which guarantees the later `minexpr` / `minlam` pipeline inherits after desugaring. +- Treat the rewrite CPS transform as out-of-band validation rather than as the source of truth for typing. + +### Phase 1 Rationale + +If typing moves later than the shared source pipeline, most earlier transforms lose its guarantees and one of the active backends never sees the check at all. + +Putting delimited typing at the shared early stage keeps the architecture consistent with the rest of the compiler. + +### Phase 1 Exit Criteria + +- there is one documented early typing boundary at the `expr` / `lambda.yaml` layer that both target-b and the CEKF/ANF path share +- later passes can state which delimited-control guarantees they are allowed to assume +- the handoff from `expr` / `lambda.yaml` typing into the `minexpr` / `minlam` core is explicit +- no implementation step depends on post-CPS typing to make source programs well-typed + +## Phase 2: Define the Source-Level Implementation Model + +**Objective:** choose the internal representation and analyzer shape that will carry answer-type modification through the shared early checker. + +Representation choices for this phase are expanded in [delimited-type-representation.md](delimited-type-representation.md). + +### Phase 2 Work + +- Change the mental model of expression analysis from “an expression returns one type” to “an expression is checked relative to an incoming and outgoing answer type”. +- Keep the expression rule conceptually in this form: + +```text +analyzeExpr(expr, env, ng, subst, answerIn, answerOut) -> #(valueType, subst) +``` + +- Represent pure expressions by unifying `answerIn` with `answerOut`. +- Represent controlful functions explicitly, with fields for: + - argument type + - result type + - pre-call answer type + - post-call answer type +- Decide how plain functions embed into that representation. +- Decide whether later passes need the inferred control behavior attached to nodes, environments, or both. + +### Phase 2 Recommended Approach + +Use a distinct controlful function representation in the implementation, even if the semantic note continues to describe pure and controlful functions uniformly. + +That preserves incremental adoption: + +- existing pure function typing can remain readable +- application can lift pure functions into the identity-effect case when needed +- printed types can make controlful bindings obvious + +### Phase 2 Exit Criteria + +- there is one agreed implementation shape for controlful function types +- there is one agreed analyzer signature for threading ambient answer types +- the role of `call/cc` inside that model is documented, even if it remains a special case temporarily + +## Phase 3: Implement the Direct-Style Rules in the Rewrite Inferencer + +**Objective:** add answer-type-modifying typing to [infer_expr.fn](../infer_expr.fn) as a reference implementation of the early source-level rules. + +Breadth-first rule skeletons for this phase are expanded in [delimited-typing-rules.md](delimited-typing-rules.md). + +### Phase 3 Work + +- Extend substitution, occurs checking, instantiation, rendering, and unification so the controlful function representation behaves like any other type constructor. +- Add source rules in evaluation order. + +#### Phase 3 Pure Forms + +- variables and constants preserve the ambient answer type +- arithmetic, tuples, constructors, and other transparent forms only thread answer-type change from their subexpressions +- sequencing forms preserve left-to-right answer-type threading + +#### Phase 3 Lambda + +- analyze the body under fresh answer-type variables +- store the latent answer-type change on the resulting function type +- keep lambda construction itself pure + +#### Phase 3 Application + +- thread intermediate answer types through: + - evaluation of the function expression + - evaluation of the argument expressions + - the latent answer-type behavior of the callee body +- make pure application the special case where the callee preserves the answer type + +#### Phase 3 Reset + +- introduce a fresh local delimiter boundary +- analyze the body with a fresh local answer-type pair +- discharge the internal answer-type change before returning to the outer context + +#### Phase 3 Shift + +- implement the rule for rewrite `(shift f)`, not only the binder presentation from the note +- require the operand to type as a pure function from the captured continuation to the body result in the first cut +- only relax that restriction after the core machinery is stable + +### Phase 3 Exit Criteria + +- the small examples from [delimited-types.md](delimited-types.md) infer the expected result types +- a named helper containing `shift` visibly carries latent control behavior in its inferred type +- the checker rejects using such a helper without an enclosing `reset` + +## Phase 4: Add a Safe Generalization Policy + +**Objective:** prevent unsound answer-type polymorphism while keeping the first implementation usable. + +### Phase 4 Work + +- treat answer-type variables as non-generic in `let` and `letrec` +- keep bindings with latent answer-type change monomorphic unless annotations are added intentionally +- document this as a design restriction, not a temporary accident +- decide whether recursive controlful bindings require stricter rules than non-recursive ones + +### Phase 4 Exit Criteria + +- intended monomorphic control examples typecheck +- deliberately polymorphic answer-type examples are rejected for an explicit reason +- the restriction is documented next to the implementation rather than hidden in behavior + +## Phase 5: Reconcile `shift/reset` with Existing `call/cc` Support + +**Objective:** avoid ending with two unrelated control-typing mechanisms. + +### Phase 5 Work + +- compare the current special-case `callcc_expr` rule in [infer_expr.fn](../infer_expr.fn) with the new delimited-control representation +- decide whether `call/cc` should: + - remain a small special case, or + - be re-expressed using the same underlying type machinery where practical +- document the exact difference between whole-continuation capture and delimited capture in implementation terms + +### Phase 5 Exit Criteria + +- the relationship between `call/cc` and `shift/reset` is explicit +- any remaining special cases are small and intentional + +## Phase 6: Port the Model to the C Typechecker + +**Objective:** translate the validated rewrite design into the real compiler's existing early typechecking stage. + +### Phase 6 Work + +- extend [src/tc.yaml](../../../src/tc.yaml) with an explicit representation for controlful function types +- update [src/tc_analyze.c](../../../src/tc_analyze.c) so expression analysis threads answer-type information through the same control points as the rewrite prototype, while the program is still in the `src/lambda.yaml`-like layer and before later lowering to `src/minlam.yaml`, ANF, or any target-specific CPS path +- preserve the same implementation order used in the prototype: + - transparent pure forms first + - lambda and application threading + - `reset` + - `shift` + - let-generalization restrictions after the core rules work +- keep this early checker authoritative rather than introducing a second later typing pass as the source of truth +- add helper constructors and helper analyzers for: + - pure vs controlful function creation + - application threading + - delimiter discharge + - answer-type mismatch diagnostics + +### Phase 6 Practical Mapping + +The current C implementation already has a useful comparison point in the `call/cc` path inside [src/tc_analyze.c](../../../src/tc_analyze.c). + +Use that as a regression oracle, but do not let the new design depend on syntax-local inspection of lambda bodies at call sites. The control behavior must travel in the type representation. + +### Phase 6 Exit Criteria + +- the C typechecker has an explicit representation for latent delimited-control behavior +- the C analyzer no longer depends on local syntax to know whether a named function may alter the answer type +- rewrite examples have corresponding C-side tests once the front-end can construct the relevant AST + +## Phase 7: Validation Matrix + +**Objective:** make the typing discipline executable and regression-resistant. + +### Phase 7 Positive Cases + +- immediate resumption through the captured continuation +- discarding the captured continuation +- reusing the captured continuation multiple times +- named helper containing `shift` under `reset` +- nested `reset` cases where only the nearest delimiter is captured + +### Phase 7 Negative Cases + +- `shift` without an enclosing `reset` +- unsafe let-generalization of a controlful binding +- answer-type mismatch across branches or sequence points +- misuse of a controlful helper in a context that expects a pure function result + +### Phase 7 Two Validation Layers + +Run validation at both levels: + +1. source-level terms should typecheck with the answer-type-modifying rules at the shared early checker +2. where the rewrite CPS transform exists, transformed terms may still be checked with ordinary HM as a secondary oracle + +This separates source-level typing mistakes from operational rewrite mistakes without making CPS a prerequisite for sound typing. + +## Non-Goals for the First Implementation + +The first implementation should not try to solve these at the same time: + +- full answer-type polymorphism +- prompt tags +- `control/prompt` +- one-shot continuation restrictions +- combining `amb` and delimited control in one typing change + +## Recommended Order of Attack + +1. Fix the shared early typing boundary before ANF or any target-specific CPS split. +2. Freeze the internal representation for controlful function types and ambient answer-type threading. +3. Implement the direct-style rules in [infer_expr.fn](../infer_expr.fn) as a reference model for the early checker. +4. Add safe monomorphic restrictions before attempting richer inference. +5. Reconcile the new model with the existing `call/cc` support. +6. Port the validated design into [src/tc.yaml](../../../src/tc.yaml) and [src/tc_analyze.c](../../../src/tc_analyze.c) at the existing early `lambda.yaml`-level typechecking stage, before desugaring to `minlam`. +7. Keep the rewrite CPS transform available as a secondary semantic oracle, not as the place where typing first becomes valid. + +This order keeps the operational model and the typing model aligned while preserving the guarantees needed by the rest of the real pipeline. diff --git a/fn/rewrite/docs/delimited-types.md b/fn/rewrite/docs/delimited-types.md new file mode 100644 index 00000000..d76dba87 --- /dev/null +++ b/fn/rewrite/docs/delimited-types.md @@ -0,0 +1,344 @@ +# Delimited control typing sketch for `fn/rewrite` + +This note complements [delimited-cps.md](delimited-cps.md). + +That note fixes a candidate operational account for `reset` and `shift` in the rewrite CPS prototype. This note asks a narrower question: what static typing discipline can describe that behavior safely, especially when `shift` appears inside a named function and the matching `reset` is only present at some later call site. + +The short answer is that plain Hindley-Milner types over ordinary arrows are not enough. A `shift` occurrence does not just compute a result of some type $\tau$. It also changes the answer type of the surrounding delimited computation. Once `shift` can sit inside a named function, that control behavior becomes latent in the function type and cannot be reconstructed only from the local syntax at the eventual call site. + +For the real compiler pipeline, this judgment belongs on the earlier `expr.fn` / `src/lambda.yaml`-like structures. Desugaring to `minexpr.fn` / `src/minlam.yaml` happens shortly afterward, and the majority of later transforms then operate on that reduced core, so the delimited-control guarantees need to exist before that handoff. + +## Goal + +The goal of this sketch is not to commit to a full inference algorithm yet. The goal is to pin down a type judgment precise enough that: + +- it explains why `shift` and `reset` are co-dependent +- it handles named functions whose bodies contain `shift` +- it matches the intended two-layer CPS reading in [delimited-cps.md](delimited-cps.md) +- it makes clear which part is easy to prototype and which part is likely to need annotations or a value restriction + +## Why ordinary HM is not enough + +The current rewrite inference prototype in [infer.fn](../infer.fn) only infers ordinary expression types and ordinary arrow types. + +That works for `call/cc`, because `call/cc` can be given a self-contained type schema: + +$$ +((a \to b) \to a) \to a +$$ + +The direct-style type of `shift` is different. Its meaning depends on the nearest enclosing `reset`, because `shift` captures only the continuation up to that `reset`. That means the source typing judgment needs to track not just the type of the local subexpression, but also how that subexpression changes the answer type of the enclosing `reset` body. + +The named-function case makes this unavoidable: + +```text +let f = λx. shift k. e +in reset (C[f v]) +``` + +Operationally, the `shift` in `f` captures the continuation from the call site `C[□]`, not from the definition site of `f`. + +Statically, that means `f` cannot be assigned a plain type like $\sigma \to \tau$. The fact that calling `f` requires an enclosing `reset` and may modify the answer type has to appear in the type of `f` itself. + +## Candidate judgment + +Use an answer-type-modifying judgment: + +$$ +\Gamma \vdash e : \tau [\alpha\mapsto\beta] +$$ + +The conceptual point is simple: an expression has both a value type and a control behavior. +The value type is $\tau$. The control behavior says what answer type the nearest enclosing `reset` body starts with and what answer type it ends with. + +So: + +- pure expressions have the form $\Gamma \vdash e : \tau [\alpha\mapsto\alpha]$ +- `shift` is the construct that can change $\alpha$ to a different $\beta$ +- `reset` hides that internal answer-type change and restores an ordinary outer judgment + +This is the standard answer-type-modification view of `shift/reset`, adapted to the rewrite prototype. + +## Function types + +Functions whose bodies may use `shift` need types that record latent +control behavior. A function type has to describe not just the value +it returns, but also the answer-type change its body may perform when +called under `reset`. + +$$ +\sigma \xrightarrow[\lbrack {\alpha\mapsto\beta} \rbrack]{} \tau +$$ + +Read this as a function type $\sigma \to \tau$ that carries an +answer-type change $[\alpha\mapsto\beta]$. + +This is important for named functions: a function that contains `shift` carries the answer-type change in its own type, so a later caller under `reset` can instantiate that latent control behavior. + +## Core rules + +The full language would need rules for all forms, but the core picture can be fixed with just values, lambdas, application, `reset`, and `shift`. + +### Variables and constants + +Pure expressions preserve the ambient answer type: + +$$ +\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau [\alpha\mapsto\alpha]}\texttt{[VAR]} +$$ + +and similarly for constants. + +### Lambda + +Building a function value is pure, even when calling that function later may not be: + +$$ +\frac{\Gamma, x : \sigma \vdash e : \tau [\alpha\mapsto\beta]} + {\Gamma \vdash \lambda x.e : \sigma \xrightarrow[\lbrack \alpha\mapsto\beta \rbrack]{} \tau [\gamma\mapsto\gamma]}\texttt{[LAMBDA]} +$$ + +The important distinction is between defining a function and calling it. Defining the lambda is pure. The possible answer-type change is stored on the function type and only becomes relevant when the function is later applied. + +### Application + +Application composes the latent answer-type change from the function body with the current context: + +$$ +\frac{\Gamma \vdash f : \sigma \xrightarrow[\lbrack \alpha\mapsto\beta \rbrack]{} \tau [\gamma\mapsto\delta] \qquad + \Gamma \vdash a : \sigma [\delta\mapsto\alpha]} + {\Gamma \vdash f\ a : \tau [\gamma\mapsto\beta]}\texttt{[APPLY]} +$$ + +The easiest way to read this rule is as a left-to-right call-by-value decomposition. + +First evaluate `f`, which may already change the ambient answer type from $\gamma$ to $\delta$. Then evaluate the argument `a`, which takes that intermediate answer type from $\delta$ to $\alpha$. Only after both are available do we enter the function body, whose latent behavior changes the answer type from $\alpha$ to $\beta$. The whole application therefore changes the answer type from $\gamma$ to $\beta$. + +This is the point where a named function with latent control effect becomes active. The effect does not come from re-reading the syntax of the lambda at the call site. It comes from the latent $[\alpha\mapsto\beta]$ annotation on the function value. + +If `f` is pure, this collapses to the ordinary rule because $\alpha = \beta$. + +### Reset + +`reset` delimits answer-type change and returns an ordinary expression result to its surrounding context: + +$$ +\frac{\Gamma \vdash e : \tau [\tau\mapsto\sigma]} + {\Gamma \vdash \operatorname{reset}\ e : \sigma [\alpha\mapsto\alpha]}\texttt{[RESET]} +$$ + +Inside the `reset`, the body starts in a context expecting a $\tau$ and may change the answer type from $\tau$ to $\sigma$. The `reset` itself discharges that internal change and is pure to the outside world. + +The repeated $\tau$ on the left is intentional. This rule is about typing the whole body of a fresh `reset`, where the initial local continuation is the top-level hole of that body. Subexpressions inside the body can still have other value types. The point is only that, at the boundary introduced by `reset`, the pre-`shift` answer type is the type that the body would deliver if no answer-type change occurred. + +This matches the operational idea from [delimited-cps.md](delimited-cps.md): inside a fresh `reset`, the local continuation starts at `idk`, and once the body completes, control returns to the outer meta continuation as an ordinary result. + +### Shift + +`shift` captures the local continuation up to the nearest `reset`. + +The continuation variable gets the ordinary function type from the hole type to the pre-shift answer type: + +$$ +\frac{\Gamma, k : \tau \to \alpha \vdash e : \beta [\beta\mapsto\beta]} + {\Gamma \vdash \operatorname{shift}\ k.e : \tau [\alpha\mapsto\beta]}\texttt{[SHIFT]} +$$ + +Conceptually, the surrounding context is waiting for a value of type $\tau$, and if that context were resumed normally it would produce answer type $\alpha$. Inside the body of `shift`, that suspended context is available as an ordinary function $k : \tau \to \alpha$. Because the local continuation has been removed, the `shift` body is checked as an ordinary computation producing $\beta$. The whole `shift` therefore changes the answer type from $\alpha$ to $\beta$. + +This rule is the source-level counterpart of the CPS rule where `shift` passes a reified local continuation to its operand and resumes with `idk` inside the body. + +### Other Rules + +Most of the omitted rules are structurally transparent to answer-type change. They do not introduce new control behavior; they only preserve or thread the ambient $[\alpha\mapsto\beta]$ information according to evaluation order. For example, arithmetic and tuple construction are pure once their subexpressions are evaluated, so they just pass through whatever answer-type change those subexpressions already induce. A `let x = e_1 in e_2` rule would similarly thread the answer type from `e_1` into `e_2`, much like sequencing. The non-transparent cases are the control operators themselves, especially `reset` and `shift`, because they are the forms that delimit or reify continuation structure. + +## Named function case + +Now consider the case that motivated this note: + +```text +let f = λx. shift k. e +in reset (C[f v]) +``` + +The body of `f` is checked under some answer-type change $[\alpha\mapsto\beta]$, so the lambda gets a type of the form: + +$$ +f : \sigma \xrightarrow[\lbrack \alpha\mapsto\beta \rbrack]{} \tau +$$ + +That is the static record of the latent control behavior. + +At the call site inside `reset`, the ambient context `C[□]` inside that `reset` determines the specific instantiation of $\alpha$ and $\beta$. The caller does not discover the control effect by re-inspecting the syntax of `f`. It learns it from the type of `f`. + +This is the essential reason a syntax-local rule for `shift` is not enough once `shift` can appear behind a variable reference. + +## Small examples + +### Pure use of the captured continuation + +```text +reset (1 + shift k. k 2) +``` + +Operationally, the body captures the pending `1 + □` continuation and immediately reinstalls it with `2`, so the whole reset behaves like `reset (1 + 2)`. + +The hole type is `Int`, and resuming the captured continuation also yields `Int`, so the answer type does not change. This is the easy case where the internal answer-type change is +$[\operatorname{Int}\mapsto\operatorname{Int}]$. + +### Discarding the local continuation + +```text +reset (1 + shift k. 2) +``` + +Operationally, the `1 + □` continuation is captured and then discarded. The body returns directly from the enclosing `reset`, so the pending addition never resumes. + +The surrounding local continuation still expects an `Int`, so the left side of the answer-type change is `Int`. But the shift body returns `2` directly from the reset body, so the right side is also `Int` in this particular example. + +Operationally the local continuation is discarded. Typing alone does not force `k` to be used. + +### Named helper + +```text +let f = λx. shift k. k x +in reset (1 + f 2) +``` + +Operationally, `f` captures the caller's pending `1 + □` continuation, not anything from its definition site. That is exactly why the effect has to travel with the function value. + +The important part is not the final result type. The important part is that `f` cannot be typed as only `Int -> Int`. Its type must include the answer-type behavior of its body, even though the actual delimiter is only introduced around `f 2`. + +## Generalization and safety + +This is where the design gets subtle. + +Once function types mention answer-type variables, unrestricted HM-style let-generalization becomes questionable. A binding like: + +```text +let f = λx. shift k. e +``` + +may appear to want a polymorphic type scheme over $\alpha$ and $\beta$. In the literature, unrestricted answer-type polymorphism interacts badly with ordinary let-polymorphism unless the language adopts additional restrictions. + +For a first prototype, the safe options are deliberately narrower: + +1. Require explicit type annotations on any binding whose type mentions answer-type variables. +2. Treat answer-type variables as non-generalizable by default, analogous to a value restriction. +3. Prototype the typing story after CPS first, where the continuation structure is explicit and ordinary function typing can validate the transform. + +Option 1 is the cleanest if the immediate goal is clarity rather than maximal inference power. + +## Relationship to the two-layer CPS note + +The proposed judgment matches the two-layer CPS story directly. + +In [delimited-cps.md](delimited-cps.md): + +- `k` is the local continuation up to the nearest `reset` +- `m` is the meta continuation outside that `reset` +- `shift` captures `k` but not `m` + +In this typing note: + +- $\tau$ is the type expected by the captured local continuation hole +- $\alpha$ is the answer type produced if that local continuation runs normally +- $\beta$ is the answer type produced by the `shift` body after the local continuation has been removed + +So the answer-type change $[\alpha\mapsto\beta]$ is the type-level shadow of the operational split between local continuation and meta continuation. + +The application rule above mirrors the ordinary left-to-right threading of `k` and `m` in the CPS note. The `reset` rule mirrors the installation of `idk` plus a fresh meta continuation. The `shift` rule mirrors the point where the local continuation is reified as a value and the current local continuation is replaced by `idk`. + +## Recommended first implementation target + +For the rewrite prototype and the real compiler, the pragmatic staged plan is: + +1. Keep this note as the direct-style semantic reference. +2. Implement delimited typing at the existing early source-level typechecking stage over the `expr.fn` / `src/lambda.yaml`-like structures, before desugaring to `minexpr.fn` / `src/minlam.yaml`, ANF, or any target-specific CPS split. +3. Use the delimited CPS transform as a secondary validation oracle in the rewrite prototype, not as the place where typing first becomes valid. +4. If inference is too ambitious at first, start with explicit annotations on controlful named functions and on `reset` bodies, together with monomorphic answer-type variables. + +That order preserves guarantees for earlier transforms, works for both the ANF-based CEKF path and the target-b path, and still lets the CPS note act as an operational cross-check. + +## Worked example + +This example makes the difference between the local hole type and the enclosing answer type explicit: + +```text +reset (tostring (1 + shift k. true)) +``` + +The captured evaluation context around `shift` is: + +```text +tostring (1 + □) +``` + +So the hole expects an `Int`, and if resumed normally the surrounding `reset` body would produce a `String`. That means the captured continuation has type: + +$$ +k : \operatorname{Int} \to \operatorname{String} +$$ + +The body of the `shift` is just `true`, so under that continuation binding it is a pure `Bool` computation: + +$$ +\Gamma, k : \operatorname{Int} \to \operatorname{String} +\vdash +\operatorname{true} +: +\operatorname{Bool} +[\operatorname{Bool}\mapsto\operatorname{Bool}] +$$ + +Applying the `shift` rule gives: + +$$ +\Gamma \vdash +\operatorname{shift}\ k.\operatorname{true} +: +\operatorname{Int} +[\operatorname{String}\mapsto\operatorname{Bool}] +$$ + +This is the key judgment. The `shift` expression sits in a place expecting an `Int`, but evaluating it changes the enclosing `reset` answer type from `String` to `Bool`. + +The surrounding pure contexts preserve that same answer-type modification, so: + +$$ +\Gamma \vdash +1 + \operatorname{shift}\ k.\operatorname{true} +: +\operatorname{Int} +[\operatorname{String}\mapsto\operatorname{Bool}] +$$ + +and then: + +$$ +\Gamma \vdash +\operatorname{tostring}(1 + \operatorname{shift}\ k.\operatorname{true}) +: +\operatorname{String} +[\operatorname{String}\mapsto\operatorname{Bool}] +$$ + +Finally, `reset` discharges the internal answer-type change: + +$$ +\Gamma \vdash +\operatorname{reset}(\operatorname{tostring}(1 + \operatorname{shift}\ k.\operatorname{true})) +: +\operatorname{Bool} +[\alpha\mapsto\alpha] +$$ + +So the whole expression has type `Bool`. + +This example is useful because the three roles stay visibly distinct: + +- the local hole type at the `shift` site is `Int` +- the pre-`shift` answer type inside the `reset` is `String` +- the post-`shift` answer type is `Bool` + +Operationally, the pending continuation $\lambda n.\,\operatorname{tostring}(1+n)$ is captured and discarded, so the body `true` returns directly from the nearest `reset`. diff --git a/fn/rewrite/docs/delimited-typing-rules.md b/fn/rewrite/docs/delimited-typing-rules.md new file mode 100644 index 00000000..a3872175 --- /dev/null +++ b/fn/rewrite/docs/delimited-typing-rules.md @@ -0,0 +1,579 @@ +# Plan for Delimited Typing Rules in `fn/rewrite` + +This note expands the representation choice in [delimited-type-representation.md](delimited-type-representation.md) into analyzer-level rule skeletons. + +The file-local implementation breakdown for [infer_expr.fn](../infer_expr.fn) is in [delimited-infer-expr-checklist.md](delimited-infer-expr-checklist.md). + +The goal here is breadth first, not depth first. This note should answer: + +- what the new analyzer interface needs to look like +- how the existing `infer_expr.fn` cases roughly map onto that interface +- where `lambda`, `apply`, `reset`, and `shift` need distinct handling +- which cross-cutting helpers should exist before rule-by-rule coding starts + +This note is still scoped to `fn/rewrite`. It intentionally stops short of a C port. + +## Current Anchor in `infer_expr.fn` + +The current inferencer revolves around: + +```text +analyzeExpr(expr, envt, ng, subst) -> #(valueType, subst) +``` + +The current callable-related cases are structurally simple: + +- `lambda([], body)` analyzes `body` and returns `thunkType(bodyType)` +- `lambda(params, body)` analyzes `body` and returns a nested pure arrow chain +- `apply(fun, [])` unifies the function with `thunkType(resultType)` +- `apply(fun, args)` unifies the function with `funTypeList(argTypes, resultType)` + +That is exactly the surface we want to preserve conceptually, but it is not enough once answer-type change becomes part of function types. + +## Main Refinement to the Earlier Sketch + +The earlier planning note used this conceptual form: + +```text +analyzeExpr(expr, envt, ng, subst, answerIn, answerOut) -> #(valueType, subst) +``` + +That is necessary, but not quite sufficient. + +It does not by itself prevent these invalid situations: + +- a bare `shift` at top level +- applying a latent controlful function in a context with no enclosing `reset` + +Answer-type equality alone is not enough to rule those out. A controlful callable may have `answerIn == answerOut` and still require a delimiter. + +So the analyzer needs one more piece of context. + +## Recommended Analyzer Interface + +Use this conceptual form: + +```text +analyzeExpr(expr, envt, ng, subst, answerIn, answerOut, controlAllowed) -> #(valueType, subst) +``` + +where: + +- `valueType` is the direct-style value type of the expression +- `answerIn` is the answer type expected before the expression runs in the current local control context +- `answerOut` is the answer type produced after the expression runs in that same local control context +- `controlAllowed` says whether this expression position may consume or introduce delimited control + +Recommended initial meaning of `controlAllowed`: + +- `false` at the top-level program entrypoint +- `true` inside the body of `reset` +- `true` inside lambda bodies, because lambdas may carry latent control behavior even when defined outside `reset` +- inherited by ordinary subexpressions + +This keeps the answer-type machinery focused on typing, while the extra flag enforces the separate syntactic fact that delimited control must have a delimiter available somewhere in the relevant control context. + +## Top-Level Entry Point + +The public `infer(expr)` entrypoint should continue to return an ordinary type. + +Conceptually: + +```text +let topAnswer = freshTypeVar() +in analyzeExpr(expr, nullTcEnv, [], nullSubstEnv, topAnswer, topAnswer, false) +``` + +This does two things: + +- top-level expressions must be pure in the ambient context +- a top-level `shift` or top-level application of a controlful callable is rejected because `controlAllowed` is `false` + +## Cross-Cutting Helper Layer + +Before changing individual expression rules, the inferencer should gain a small helper layer. + +## Helper 1: Pure-effect wrapper + +Many existing rules are semantically pure in the ambient context. + +Recommended helper shape: + +```text +analyzeExprPure(expr, envt, ng, subst, answer) -> #(valueType, subst) +``` + +which simply calls: + +```text +analyzeExpr(expr, envt, ng, subst, answer, answer, false-or-inherited) +``` + +The exact wrapper signature can vary, but the point is to make the “this position is pure in the ambient context” intent explicit. + +## Helper 2: Callable normalization + +The representation note chose explicit pure and controlful callable constructors: + +- `thunkType(result)` +- `funType(arg, result)` +- `controlThunkType(result, answerIn, answerOut)` +- `controlFunType(arg, result, answerIn, answerOut)` + +For inference, it is useful to have a normalization helper that collapses controlful callables whose answer types have unified: + +```text +controlThunkType(R, A, A) => thunkType(R) +controlFunType(X, R, A, A) => funType(X, R) +``` + +This should happen in analyzer-side helper logic or final type normalization, not inside generic unification. + +That keeps inference workable for unknown callables while preserving a clean surface form for pure results. + +## Helper 3: Callable builders + +The lambda rules should not manually decide between pure and controlful constructors inline. + +Recommended helpers: + +- `makeLambdaCallable(bodyType, answerIn, answerOut, subst)` for zero-argument lambdas +- `makeLambdaCallableChain(paramTypes, bodyType, answerIn, answerOut, subst)` for curried lambdas + +These helpers should: + +- place the latent answer-type behavior at the rightmost callable node +- normalize the final callable shape when `answerIn` and `answerOut` unify + +## Helper 4: Callable consumers + +Application should not inline the distinction between: + +- pure thunk +- controlful thunk +- pure function +- controlful function +- unknown type variable later forced into one of those callable shapes + +Recommended helpers: + +- `consumeThunkCallable(type, resultType, callAnswerIn, callAnswerOut, controlAllowed, subst)` +- `consumeCurriedCallable(type, argTypes, resultType, callAnswerIn, callAnswerOut, controlAllowed, subst)` + +These helpers are where application-specific coercion logic belongs. + +In particular, if a type variable is used in callable position, these helpers may instantiate it to a controlful callable shape first and rely on later normalization to collapse the pure case. + +That is analyzer logic, not unifier magic. + +## Helper 5: Effect-threaded argument analysis + +Current `analyzeArgs` only accumulates argument types. + +Delimited typing needs the evaluation order to stay explicit. + +Recommended conceptual shape: + +```text +analyzeArgs(args, envt, ng, subst, answerIn, answerOut, controlAllowed) -> #(argTypes, subst) +``` + +The helper should evaluate argument expressions left-to-right, threading answer types through them exactly the same way the direct application rule in [delimited-types.md](delimited-types.md) does. + +## Breadth-First Rule Skeletons + +The sections below do not try to finish every edge case. They define the intended skeleton and where each existing `infer_expr.fn` branch should land. + +## Rule Group 1: Atomic Pure Forms + +These forms remain pure in the ambient context: + +- variables +- integer and character literals +- boolean and null constants +- constructor names already stored in the type environment + +Skeleton: + +```text +analyze atomic form under (answerIn, answerOut, controlAllowed) +unify answerIn with answerOut +return ordinary value type +``` + +This group is the direct counterpart of the `VAR` and constant rules in [delimited-types.md](delimited-types.md). + +## Rule Group 2: Transparent Wrappers + +These forms do not add control behavior of their own but simply forward the result of a subexpression: + +- `print_exp` +- `tag` +- `typeof_expr` if it remains supported in this path + +Skeleton: + +```text +analyze child under the same (answerIn, answerOut, controlAllowed) +return the child result type or the wrapper-specific result type +``` + +The key point is that these wrappers do not force purity. They preserve whatever ambient answer-type threading their child already induces. + +## Rule Group 3: Lambda Introduction + +## Lambda Zero-Argument Skeleton + +For: + +```text +lambda([], body) +``` + +use fresh body answer variables: + +```text +bodyAnswerIn = freshTypeVar() +bodyAnswerOut = freshTypeVar() +``` + +Then: + +1. analyze `body` under `(bodyAnswerIn, bodyAnswerOut, true)` +2. build either `thunkType(bodyType)` or `controlThunkType(bodyType, bodyAnswerIn, bodyAnswerOut)` via the callable builder +3. unify the ambient `answerIn` with `answerOut`, because constructing the thunk is pure +4. return the callable value type + +## Lambda Parameterized Skeleton + +For: + +```text +lambda(params, body) +``` + +use the existing parameter-binding machinery, but analyze the body under fresh answer variables and `controlAllowed = true`. + +Then build the callable chain so that only the rightmost callable node carries the latent answer-type change. + +Conceptually: + +```text +paramTypes = [A, B, C] +bodyType = R +body effect = [X => Y] +``` + +becomes: + +```text +funType(A, funType(B, controlFunType(C, R, X, Y))) +``` + +followed by normalization if `X` and `Y` unify. + +As with the zero-argument case, lambda construction itself is pure in the surrounding ambient context. + +## Rule Group 4: Application + +Application is where the direct-style latent effect becomes active. + +It should be implemented as a three-stage decomposition. + +## Application Stage 1: Evaluate the function expression + +For either `apply(fun, [])` or `apply(fun, args)`: + +1. create a fresh intermediate answer variable `afterFun` +2. analyze `fun` under `(answerIn, afterFun, controlAllowed)` + +This captures the fact that evaluating the function position may itself contain control behavior. + +## Application Stage 2: Evaluate the arguments + +For `apply(fun, args)` with arguments present: + +1. create a fresh intermediate answer variable `beforeCall` +2. analyze the argument list under `(afterFun, beforeCall, controlAllowed)` +3. obtain the list of argument types in source evaluation order + +For `apply(fun, [])`, this stage is skipped and `afterFun` is used directly as the call-entry answer type. + +## Application Stage 3: Consume the callable type + +After function and argument evaluation are complete: + +- `apply(fun, [])` uses `consumeThunkCallable` +- `apply(fun, args)` uses `consumeCurriedCallable` + +These helpers must distinguish four semantic cases. + +### Pure thunk call + +If the callable is `thunkType(result)`: + +- unify `callAnswerIn` with `callAnswerOut` +- return `result` + +### Controlful thunk call + +If the callable is `controlThunkType(result, thunkIn, thunkOut)`: + +- require `controlAllowed = true` +- unify `callAnswerIn` with `thunkIn` +- unify `callAnswerOut` with `thunkOut` +- return `result` + +### Pure curried function call + +If the callable is a pure arrow chain whose final node is pure: + +- unify arguments against the pure chain as usual +- unify `callAnswerIn` with `callAnswerOut` +- return the remaining result type + +### Controlful curried function call + +If the callable is a chain whose rightmost callable node is controlful: + +- require `controlAllowed = true` +- unify arguments against the chain +- use the rightmost callable node's `answerIn` and `answerOut` as the latent body effect +- return the resulting value type after the consumed arguments + +## Unknown callable variables in application + +This is the main inference wrinkle. + +If a type variable appears in callable position, application cannot wait for some other rule to decide whether it is pure or controlful. + +Recommended approach: + +- instantiate unknown callables to a controlful callable skeleton during callable consumption +- keep the fresh answer variables explicit +- normalize later if those answer variables unify + +For example, a zero-argument unknown callable can be forced to: + +```text +controlThunkType(result, freshIn, freshOut) +``` + +and a unary unknown callable can be forced to: + +```text +controlFunType(arg, result, freshIn, freshOut) +``` + +This keeps application deterministic without adding special disjunctive logic to generic unification. + +## Rule Group 5: Sequence and Other Ordered Pure Forms + +These forms remain structurally transparent to answer-type change but must preserve evaluation order. + +This group includes: + +- `sequence` +- tuple construction +- primitive arithmetic and comparisons +- constructor argument lists +- deconstruction scrutinees +- tuple index scrutinees + +Skeleton: + +1. evaluate subexpressions left-to-right using threaded answer variables +2. once all subexpressions are available, build the ordinary result type +3. do not introduce new latent effect at the final constructor itself + +That means the resulting answer-type behavior comes entirely from the subexpressions already analyzed. + +## Rule Group 6: Branching Forms + +This group includes: + +- `if_expr` +- `cond_expr` +- `match_cases` + +## Branching test position + +The test or scrutinee expression is evaluated first and may itself change the current answer type. + +So each branching rule should introduce an intermediate answer variable after the test position. + +## Branching branch positions + +Each branch should then be checked from the same post-test answer type to the same final `answerOut`. + +Conceptually for `if_expr`: + +```text +answerIn --test--> afterTest +afterTest --consequent--> answerOut +afterTest --alternative--> answerOut +``` + +The branch result types must unify as usual. + +## Rule Group 7: Binding Forms + +This group includes: + +- `let_expr` +- `letstar_expr` +- `letrec_expr` + +## Let and let* + +For a simple binding sequence, keep the current environment logic but make answer threading explicit. + +For `let`: + +1. analyze the binding expressions left-to-right from `answerIn` to `afterBindings` +2. extend the environment with the inferred binding types +3. analyze the body from `afterBindings` to `answerOut` + +For `let*`, the same structure applies, but the environment extends after each binding as it does now. + +## Letrec + +The recursive-binding fixpoint logic remains, but the stored binder types may now be controlful callable types. + +Breadth-first consequences only: + +- recursive binder snapshots must print normalized controlful callables deterministically +- recursive lambda bodies must be analyzed under `controlAllowed = true` +- generalization policy is still deferred to the later dedicated phase + +No deeper letrec policy should be decided in this note. + +## Rule Group 8: `reset` + +`reset` creates a fresh local delimiter and is pure to its surrounding context. + +Recommended skeleton: + +1. create fresh `bodyAnswerIn` +2. create fresh `bodyAnswerOut` +3. analyze the body under `(bodyAnswerIn, bodyAnswerOut, true)` +4. unify the body value type with `bodyAnswerIn` +5. unify the surrounding `answerIn` with `answerOut` +6. return `bodyAnswerOut` + +This is the direct analyzer counterpart of the rule from [delimited-types.md](delimited-types.md): + +$$ +\frac{\Gamma \vdash e : \tau [\tau\mapsto\sigma]} + {\Gamma \vdash \operatorname{reset}\ e : \sigma [\alpha\mapsto\alpha]} +$$ + +Two consequences matter. + +First, the body of `reset` gets a fresh local answer-type context, independent of the ambient outer one. + +Second, `reset` itself is pure to the outside world even when its body is not. + +## Rule Group 9: `shift` + +Rewrite syntax uses: + +```text +(shift f) +``` + +not the binder notation from the semantic note. + +For the first cut, implement `shift` through the function-argument reading already described in [delimited-types.md](delimited-types.md) and [delimited-type-representation.md](delimited-type-representation.md). + +Recommended skeleton: + +1. require `controlAllowed = true` +2. create fresh `holeType` +3. create fresh `capturedAnswer` +4. analyze `f` under a pure ambient context for the shift body result +5. require `f` to have type: + +```text +funType(funType(holeType, capturedAnswer), shiftBodyResult) +``` + +or its zero-argument equivalent only if the surface syntax later allows it + +1. return `holeType` as the value type of the whole `shift` +2. treat the ambient answer-type change of the `shift` expression itself as: + +```text +[capturedAnswer => shiftBodyResult] +``` + +This is the rewrite equivalent of the binder rule: + +$$ +\frac{\Gamma, k : \tau \to \alpha \vdash e : \beta [\beta\mapsto\beta]} + {\Gamma \vdash \operatorname{shift}\ k.e : \tau [\alpha\mapsto\beta]} +$$ + +The important implementation point is that `shift` does not itself return the body result type. It returns the hole type expected by the captured continuation. + +## Rule Group 10: `call/cc` + +`call/cc` can remain a temporary special case while `shift/reset` work lands. + +Breadth-first recommendation: + +- keep the existing `callcc_expr` branch separate initially +- update it only as much as needed to work with explicit pure `funType` rather than the old stringly arrow encoding +- do not force it into the delimited-control framework until `shift/reset` typing is stable + +That keeps the scope of the first pass bounded. + +## Suggested Breadth-First Rollout + +Implement these rules in four passes. + +## Rollout Pass 1: Thread the new context everywhere + +- change `analyzeExpr` to accept `answerIn`, `answerOut`, and `controlAllowed` +- update all existing branches to thread those values, initially preserving current pure behavior +- keep `reset` and `shift` unsupported for the moment + +The goal of this pass is structural: make the entire analyzer effect-aware without changing its meaning yet. + +## Rollout Pass 2: Switch callable representation and helpers + +- land explicit callable constructors +- land callable builders, consumers, and normalization +- update current lambda and apply rules to use the new helpers +- keep the behavior pure except where helper logic must reserve space for controlful callables + +The goal of this pass is to make lambda and apply ready for latent effects before adding the control operators themselves. + +## Rollout Pass 3: Add `reset` + +- implement the delimiter boundary rule +- verify that ordinary pure programs still infer unchanged visible types +- confirm that `reset` can hide internal answer-type change and return an ordinary value type outwardly + +This pass establishes the boundary before adding continuation capture. + +## Rollout Pass 4: Add `shift` + +- implement the rewrite `(shift f)` rule +- reject `shift` when `controlAllowed = false` +- verify that named helpers now carry latent control behavior in their inferred callable types + +This is the point where the representation and the analyzer interface finally meet the source feature. + +## Final Recommendation + +For `fn/rewrite`, the rule plan should be: + +- refine the analyzer interface to thread answer types and delimiter availability explicitly +- keep lambda construction pure but analyze lambda bodies in a control-enabled latent context +- decompose application into function evaluation, argument evaluation, and callable consumption +- treat `reset` as the boundary that reinitializes local answer types and returns pure to the outside +- treat `shift` as requiring explicit delimiter availability, not merely answer-type compatibility +- keep `call/cc` separate until the delimited rules are stable + +That gives `infer_expr.fn` a breadth-first target that matches the chosen type representation and is specific enough to implement incrementally. diff --git a/fn/rewrite/docs/status-update.md b/fn/rewrite/docs/status-update.md new file mode 100644 index 00000000..6b7c8aa6 --- /dev/null +++ b/fn/rewrite/docs/status-update.md @@ -0,0 +1,20 @@ +# Rewrite Status Update + +Current status for the rewrite prototype is narrower and healthier than it looked earlier. + +- `fn/rewrite/infer_expr.fn` now supports flat `typedefs(list(ctorScheme), expr)` constructor schemes for type inference. +- `construct` and `deconstruct` are both typed through those constructor schemes. +- The focused rewrite regression suite in `fn/rewrite/tests/test_infer_typedefs.fn` now covers user-defined type families including `maybe`, `either`, and recursive `list`. +- Those tests confirm concrete result typing and deconstruction of payload fields and recursive tails without changing the current flat `ctorScheme` representation. + +What this means in practice: + +- richer user-defined type heads such as `maybe('a)`, `either('a, 'b)`, and `list('a)` are already recognised by the rewrite type checker +- the immediate pressure is no longer on redesigning rewrite typedef syntax +- the useful next work should come from new failing type-checking scenarios, not from front-end typedef representation changes + +Recommended validation path remains: + +1. `make test-rewrite` +2. `./bin/fn fn/rewrite/test_harness.fn` for optional pipeline smoke coverage +3. `make test` after the focused rewrite slice is stable (not usually necessary if nothing outside of `fn/rewrite` has changed). diff --git a/fn/rewrite/eta_reduce.fn b/fn/rewrite/eta_reduce.fn index 7ac96ac6..736ae21b 100644 --- a/fn/rewrite/eta_reduce.fn +++ b/fn/rewrite/eta_reduce.fn @@ -46,6 +46,14 @@ fn reduce { M.cut_expr(reduce(e)) } + (M.reset_expr(e)) { + M.reset_expr(reduce(e)) + } + + (M.shift_expr(e)) { + M.shift_expr(reduce(e)) + } + (M.cond_expr(test, branches)) { M.cond_expr(reduce(test), branches |> reduce && reduce) } diff --git a/fn/rewrite/expr.fn b/fn/rewrite/expr.fn index b40b5a56..4ba397f0 100644 --- a/fn/rewrite/expr.fn +++ b/fn/rewrite/expr.fn @@ -2,6 +2,14 @@ namespace link "../listutils.fn" as list; import list operator "_|>_"; + typedef ctorScheme(string, ctorType); + + typedef ctorType { + funType(ctorType, ctorType) | + operType(string, list(ctorType)) | + varType(string) + }; + typedef expr { amb_expr(expr, expr) | apply(expr, list(expr)) | @@ -29,16 +37,93 @@ namespace namespaces(list(expr)) | primapp(string, expr, expr) | print_exp(expr) | + reset_expr(expr) | sequence(list(expr)) | + shift_expr(expr) | stdint(number) | tag(expr) | tuple_index(number, number, expr) | - typedefs(number, expr) | + typedefs(list(ctorScheme), expr) | typeof_expr(expr) | var(string) } // Helper printers + fn print_ctorScheme(x=ctorScheme(name, type)) { + puts("("); + puts(name); + puts(" "); + print_ctorType(type); + puts(")"); + x + } + + // funType(ctorType, ctorType) | + // operType(string, list(ctorType)) | + // varType(string) + fn print_ctorType { + (x=funType(a, b)) { + puts("(-> "); + print_ctorType(a); + puts(" "); + print_ctorType(b); + puts(")"); + x; + } + (x=operType(name, lst)) { + let fn h { + ([]) { true } + ([last]) { + print_ctorType(last); + true; + } + (next @ rest) { + print_ctorType(next); + puts(" "); + h(rest); + } + } + in + puts("("); + puts(name); + switch (lst) { + ([]) { true } + (_) { + puts(" ") + h(lst); + true; + } + } + puts(")"); + x; + } + (x=varType(name)) { + puts("'"); + puts(name); + x; + } + } + + fn print_list_ctorScheme(l) { + let fn h { + ([]) { true } + ([scheme]) { + print_ctorScheme(scheme); + true; + } + (scheme @ rest ) { + print_ctorScheme(scheme); + puts(" "); + h(rest); + } + } + in + puts("["); + h(l); + puts("]"); + l; + } + fn print_list(indices, putter, space) { switch (indices) { ([]) { "" } @@ -96,14 +181,14 @@ namespace } (x=typedefs(defs, expr)) { puts("(typedefs "); - putn(defs); + print_list_ctorScheme(defs); puts(" "); print_expr(expr); puts(")"); x; } (x=tuple_index(size, index, expr)) { - puts("(tuple-index "); + puts("(tuple_index "); putn(size); puts(" "); putn(index); @@ -128,12 +213,24 @@ namespace puts(")"); x; } + (x=reset_expr(e)) { + puts("(reset "); + print_expr(e); + puts(")"); + x; + } (x=print_exp(e)) { puts("(print "); print_expr(e); puts(")"); x; } + (x=shift_expr(e)) { + puts("(shift "); + print_expr(e); + puts(")"); + x; + } (x=primapp(name, e1, e2)) { puts("("); puts(name); @@ -151,7 +248,7 @@ namespace x; } (x=match_cases(exp, cases)) { - puts("(match-cases "); + puts("(match_cases "); print_expr(exp); list.for_each (fn { (#(indices, caseExpr)) { @@ -166,14 +263,14 @@ namespace x; } (x=make_vec(size, elements)) { - puts("(make-vec "); + puts("(make_vec "); putn(size); print_sequence(elements); puts(")"); x; } (x=make_tuple(elements)) { - puts("(make-tuple"); + puts("(make_tuple"); print_sequence(elements); puts(")"); x; @@ -207,7 +304,7 @@ namespace x; } (x=constructor_info(name)) { - puts("(constructor-info "); + puts("(constructor_info "); puts(name); puts(")"); x; @@ -368,6 +465,8 @@ namespace (sexp([atom("amb"), a, b])) { amb_expr(to_expr(a), to_expr(b)) } (sexp([atom("call/cc"), e])) { callcc_expr(to_expr(e)) } (sexp([atom("cut"), e])) { cut_expr(to_expr(e)) } + (sexp([atom("reset"), e])) { reset_expr(to_expr(e)) } + (sexp([atom("shift"), e])) { shift_expr(to_expr(e)) } (sexp([atom("if"), e1, e2, e3])) { if_expr(to_expr(e1), to_expr(e2), to_expr(e3)) } (sexp(atom("cond") @ test @ branches)) { cond_expr(to_expr(test), branches |> fn { (sexp([e1, e2])) { #(to_expr(e1), to_expr(e2)) } @@ -439,8 +538,8 @@ namespace (sexp([atom(">="), e1, e2])) { primapp(">=", to_expr(e1), to_expr(e2)) } (sexp([atom("print"), e])) { print_exp(to_expr(e)) } (sexp([atom("tag"), e])) { tag(to_expr(e)) } - (sexp([atom("tuple_index"), atom(size), atom(index), e])) { tuple_index(1, 1, to_expr(e)) } - (sexp([atom("typedefs"), atom(defs), e])) { typedefs(1, to_expr(e)) } + (sexp([atom("tuple_index"), atom(size), atom(index), e])) { tuple_index(to_number(size), to_number(index), to_expr(e)) } + (sexp([atom("typedefs"), sexp(defs), e])) { typedefs(defs |> to_ctorScheme, to_expr(e)) } (sexp([atom("typeof"), e])) { typeof_expr(to_expr(e)) } (sexp([])) { error("Empty expression") } (sexp(func @ args)) { apply(to_expr(func), args |> to_expr) } @@ -450,6 +549,37 @@ namespace } } + + // ctorScheme(string, ctorType); + fn to_ctorScheme { + (sexp([atom(name), type])) { + ctorScheme(name, to_ctorType(type)); + } + (x) { + print x; + error("Cannot parse ctorScheme"); + } + } + + // funType(ctorType, ctorType) | + // operType(string, list(ctorType)) | + // varType(string) + fn to_ctorType { + (sexp([atom("->"), a, b])) { + funType(to_ctorType(a), to_ctorType(b)); + } + (atom('\'' @ name)) { + varType(name) + } + (sexp(atom(name) @ types)) { + operType(name, types |> to_ctorType); + } + (x) { + print x; + error("Cannot parse ctorType"); + } + } + // "Tokenizer" function fn parse_sexpr(s) { let diff --git a/fn/rewrite/infer.fn b/fn/rewrite/infer.fn index 87dae64d..f6494e85 100644 --- a/fn/rewrite/infer.fn +++ b/fn/rewrite/infer.fn @@ -46,7 +46,7 @@ let typedef DeclClass { defClass(list(char), ExpClass) | seqClass(DeclClass, DeclClass) - | recClass(Decl) + | recClass(DeclClass) } fn newTypeVar() { varType(nullType) } @@ -59,7 +59,7 @@ let fn occursInType { (var, type) { - switch(prune(type)) { + unsafe switch(prune(type)) { (x = varType(_)) { var == x } (operType(_, args)) { occursInTypeList(var, args) } } @@ -117,7 +117,7 @@ let } fn fresh(typeExp, ng, envt) { - switch(prune(typeExp)) { + unsafe switch(prune(typeExp)) { (x = varType(_)) { if (isGeneric(x, ng)) { freshVar(x, envt, envt) @@ -150,9 +150,9 @@ let fn analyzeExp { (ideClass(ide), envt, ng) { retrieve(ide, envt, ng) } - (condClass(test, cons, alt), envt, ng) { + (condClass(test, con, alt), envt, ng) { unifyType(test, boolType) and - unifyType(analyzeExp(cons, envt, ng), analyzeExp(alt, envt, ng)) + unifyType(analyzeExp(con, envt, ng), analyzeExp(alt, envt, ng)) // return type of cons } (lambClass(binder, body), envt, ng) { diff --git a/fn/rewrite/infer_expr.fn b/fn/rewrite/infer_expr.fn new file mode 100644 index 00000000..d00342ef --- /dev/null +++ b/fn/rewrite/infer_expr.fn @@ -0,0 +1,1281 @@ +namespace +link "expr.fn" as E; +link "../listutils.fn" as list; +link "../ioutils.fn" as IO; +import IO operator "$_"; +import list operator "_|>_"; + +typedef typeExp { + varType(string) + | thunkType(typeExp) + | funType(typeExp, typeExp) + | controlThunkType(typeExp, typeExp, typeExp) + | controlFunType(typeExp, typeExp, typeExp, typeExp) + | operType(string, list(typeExp)) +} + +typedef copyEnv { + cpEnv(string, typeExp, copyEnv) + | nullCpEnv +} + +typedef typeCheckEnv { + tcEnv(string, typeExp, typeCheckEnv) + | nullTcEnv +} + +typedef sEnv { + bindSubst(string, typeExp, sEnv) + | nullSubstEnv +} + +operator "_=>_" left 8 fn (arg, fun) { fun(arg) }; + +fn freshTypeVar() { varType("'" @@ $incr()) } + +unsafe fn typeVarName(varType(name)) { name } + +fn intType() { operType("Int", []) } + +fn boolType() { operType("Bool", []) } + +fn charType() { operType("Char", []) } + +fn stringType() { operType("list", [charType()]) } + +fn nullValueType() { operType("Null", []) } + +fn tupleType(parts) { operType("Tuple", parts) } + +fn funTypeList { + ([], cod) { cod } + (dom @ rest, cod) { funType(dom, funTypeList(rest, cod)) } +} + +fn controlFunTypeList { + ([], cod, _, _) { cod } + ([dom], cod, aIn, aOut) { + controlFunType(dom, cod, aIn, aOut) + } + (dom @ rest, cod, aIn, aOut) { + funType(dom, controlFunTypeList(rest, cod, aIn, aOut)) + } +} + +fn normalizeControlThunkType { + (type, ans, ans) { thunkType(type) } + (type, aIn, aOut) { controlThunkType(type, aIn, aOut) } +} + +fn normalizeControlFunType { + (dom, cod, ans, ans) { funType(dom, cod) } + (dom, cod, aIn, aOut) { controlFunType(dom, cod, aIn, aOut) } +} + +fn normalizeType { + (varType(name)) { varType(name) } + (thunkType(type)) { thunkType(normalizeType(type)) } + (funType(dom, cod)) { funType(normalizeType(dom), normalizeType(cod)) } + (controlThunkType(type, aIn, aOut)) { + normalizeControlThunkType(normalizeType(type), + normalizeType(aIn), + normalizeType(aOut)) + } + (controlFunType(dom, cod, aIn, aOut)) { + normalizeControlFunType(normalizeType(dom), + normalizeType(cod), + normalizeType(aIn), + normalizeType(aOut)) + } + (operType(name, args)) { operType(name, args |> normalizeType) } +} + +fn freshLocalAnswers() { + let ansType = freshTypeVar() + in #(ansType, ansType) +} + +fn makeLambdaCallable { + (bType, false, _, _) { thunkType(bType) } + (bType, true, aIn, aOut) { + normalizeControlThunkType(bType, aIn, aOut) + } +} + +fn makeLambdaCallableChain { + (paramTypes, bType, false, _, _) { funTypeList(paramTypes, bType) } + (paramTypes, bType, true, aIn, aOut) { + normalizeType(controlFunTypeList(paramTypes, bType, aIn, aOut)) + } +} + +fn callableAnswers { + (thunkType(_)) { nothing } + (controlThunkType(_, aIn, aOut)) { just(#(aIn, aOut)) } + (funType(_, cod)) { callableAnswers(cod) } + (controlFunType(_, _, aIn, aOut)) { just(#(aIn, aOut)) } + (_) { nothing } +} + +fn consumeThunkCallable(callableType, + resultType, + callAnswerIn, + callAnswerOut, + cAll, + dAct, + s) { + let resolvedCallable = applySubst(callableType, s) + in switch (resolvedCallable) { + (varType(_)) { + if (dAct) { + let s1 = unifyType(callableType, + controlThunkType(resultType, + callAnswerIn, + callAnswerOut), + s) + in #(applySubst(resultType, s1), s1) + } else { + let s1 = unifyType(callableType, thunkType(resultType), s); + s2 = preserveAnswers(callAnswerIn, callAnswerOut, s1) + in #(applySubst(resultType, s2), s2) + } + } + (controlThunkType(_, _, _)) { + if (cAll) { + let s1 = unifyType(callableType, + controlThunkType(resultType, + callAnswerIn, + callAnswerOut), + s) + in #(applySubst(resultType, s1), s1) + } else { + error("infer_expr: controlful callable application requires reset") + } + } + (_) { + let s1 = unifyType(callableType, thunkType(resultType), s); + s2 = preserveAnswers(callAnswerIn, callAnswerOut, s1) + in #(applySubst(resultType, s2), s2) + } + } +} + +fn consumeCurriedCallable(callableType, + argTypes, + resultType, + callAnswerIn, + callAnswerOut, + cAll, + dAct, + s) { + let resolvedCallable = applySubst(callableType, s) + in switch (resolvedCallable) { + (varType(_)) { + if (dAct) { + let s1 = unifyType(callableType, + controlFunTypeList(argTypes, + resultType, + callAnswerIn, + callAnswerOut), + s) + in #(applySubst(resultType, s1), s1) + } else { + let s1 = unifyType(callableType, funTypeList(argTypes, resultType), s); + s2 = preserveAnswers(callAnswerIn, callAnswerOut, s1) + in #(applySubst(resultType, s2), s2) + } + } + (_) { + switch (callableAnswers(resolvedCallable)) { + (just(_)) { + if (cAll) { + let s1 = unifyType(callableType, + controlFunTypeList(argTypes, + resultType, + callAnswerIn, + callAnswerOut), + s) + in #(applySubst(resultType, s1), s1) + } else { + error("infer_expr: controlful callable application requires reset") + } + } + (nothing) { + let s1 = unifyType(callableType, funTypeList(argTypes, resultType), s); + s2 = preserveAnswers(callAnswerIn, callAnswerOut, s1) + in #(applySubst(resultType, s2), s2) + } + } + } + } +} + +fn preserveAnswers(aIn, aOut, s) { + unifyType(aIn, aOut, s) +} + +fn pureResult(resultType, s, aIn, aOut) { + let s1 = preserveAnswers(aIn, aOut, s) + in #(resultType, s1) +} + +fn ensure { + (true, _) { true } + (false, msg) { error("infer_expr: " @@ msg) } +} + +fn lookupSubst { + (name, bindSubst(name, type, _)) { just(type) } + (_, nullSubstEnv) { nothing } + (name, bindSubst(_, _, tail)) { lookupSubst(name, tail) } +} + +fn applySubst { + (varType(name), s) { + switch (lookupSubst(name, s)) { + (just(type)) { applySubst(type, s) } + (nothing) { varType(name) } + } + } + (thunkType(type), s) { + thunkType(applySubst(type, s)) + } + (funType(dom, cod), s) { + funType(applySubst(dom, s), + applySubst(cod, s)) + } + (controlThunkType(type, aIn, aOut), s) { + controlThunkType(applySubst(type, s), + applySubst(aIn, s), + applySubst(aOut, s)) + } + (controlFunType(dom, cod, aIn, aOut), s) { + controlFunType(applySubst(dom, s), + applySubst(cod, s), + applySubst(aIn, s), + applySubst(aOut, s)) + } + (operType(name, args), s) { + operType(name, applySubstList(args, s)) + } +} + +fn applySubstList { + ([], _) { [] } + (h @ t, s) { applySubst(h, s) @ applySubstList(t, s) } +} + +fn occursInType (name, type, s) { + switch (applySubst(type, s)) { + (varType(other)) { name == other } + (thunkType(inner)) { occursInType(name, inner, s) } + (funType(dom, cod)) { + occursInType(name, dom, s) or occursInType(name, cod, s) + } + (controlThunkType(inner, aIn, aOut)) { + occursInType(name, inner, s) or + occursInType(name, aIn, s) or + occursInType(name, aOut, s) + } + (controlFunType(dom, cod, aIn, aOut)) { + occursInType(name, dom, s) or + occursInType(name, cod, s) or + occursInType(name, aIn, s) or + occursInType(name, aOut, s) + } + (operType(_, args)) { occursInTypeList(name, args, s) } + } +} + +fn occursInTypeList { + (_, [], _) { false } + (name, h @ t, s) { + occursInType(name, h, s) or occursInTypeList(name, t, s) + } +} + +fn unifyType(left, right, s) { + switch (applySubst(left, s), applySubst(right, s)) { + (varType(name1), varType(name2)) { + if (name1 == name2) { + s + } else { + bindSubst(name1, varType(name2), s) + } + } + (varType(name), type) { + ensure(not occursInType(name, type, s), "occurs check failed for " @@ name); + bindSubst(name, type, s) + } + (type, varType(name)) { + unifyType(varType(name), type, s) + } + (thunkType(leftType), thunkType(rightType)) { + unifyType(leftType, rightType, s) + } + (funType(leftDom, leftCod), funType(rightDom, rightCod)) { + unifyType(leftCod, rightCod, unifyType(leftDom, rightDom, s)) + } + (controlThunkType(leftType, leftIn, leftOut), + controlThunkType(rightType, rightIn, rightOut)) { + let s1 = unifyType(leftType, rightType, s); + s2 = unifyType(leftIn, rightIn, s1) + in unifyType(leftOut, rightOut, s2) + } + (controlFunType(leftDom, leftCod, leftIn, leftOut), + controlFunType(rightDom, rightCod, rightIn, rightOut)) { + let s1 = unifyType(leftDom, rightDom, s); + s2 = unifyType(leftCod, rightCod, s1); + s3 = unifyType(leftIn, rightIn, s2) + in unifyType(leftOut, rightOut, s3) + } + (funType(leftDom, leftCod), + controlFunType(rightDom, rightCod, rightIn, rightOut)) { + let s1 = unifyType(leftDom, rightDom, s); + s2 = unifyType(leftCod, rightCod, s1) + in unifyType(rightIn, rightOut, s2) + } + (controlFunType(leftDom, leftCod, leftIn, leftOut), + funType(rightDom, rightCod)) { + let s1 = unifyType(leftDom, rightDom, s); + s2 = unifyType(leftCod, rightCod, s1) + in unifyType(leftIn, leftOut, s2) + } + (thunkType(leftType), + controlThunkType(rightType, rightIn, rightOut)) { + let s1 = unifyType(leftType, rightType, s) + in unifyType(rightIn, rightOut, s1) + } + (controlThunkType(leftType, leftIn, leftOut), + thunkType(rightType)) { + let s1 = unifyType(leftType, rightType, s) + in unifyType(leftIn, leftOut, s1) + } + (operType(name1, args1), + operType(name2, args2)) { + ensure(name1 == name2, "type mismatch between " @@ name1 @@ " and " @@ name2); + unifyArgs(args1, args2, s) + } + (_, _) { + error("infer_expr: incompatible types") + } + } +} + +fn unifyArgs { + ([], [], s) { s } + (h1 @ t1, h2 @ t2, s) { + unifyArgs(t1, t2, unifyType(h1, h2, s)) + } + (_, _, _) { + error("infer_expr: type constructor arity mismatch") + } +} + +fn lookupCopy { + (name, cpEnv(name, type, _)) { just(type) } + (_, nullCpEnv) { nothing } + (name, cpEnv(_, _, tail)) { lookupCopy(name, tail) } +} + +fn instantiateApplied { + (varType(name), ng, cp) { + if (list.member(name, ng)) { + #(varType(name), cp) + } else { + switch (lookupCopy(name, cp)) { + (just(type)) { #(type, cp) } + (nothing) { + let fresh = freshTypeVar() + in #(fresh, cpEnv(name, fresh, cp)) + } + } + } + } + (thunkType(type), ng, cp) { + let #(newType, cp1) = instantiateApplied(type, ng, cp); + in #(thunkType(newType), cp1) + } + (funType(dom, cod), ng, cp) { + let #(newDom, cp1) = instantiateApplied(dom, ng, cp); + #(newCod, cp2) = instantiateApplied(cod, ng, cp1); + in #(funType(newDom, newCod), cp2) + } + (controlThunkType(type, aIn, aOut), ng, cp) { + let #(newType, cp1) = instantiateApplied(type, ng, cp); + #(newAnswerIn, cp2) = instantiateApplied(aIn, ng, cp1); + #(newAnswerOut, cp3) = instantiateApplied(aOut, ng, cp2); + in #(controlThunkType(newType, newAnswerIn, newAnswerOut), cp3) + } + (controlFunType(dom, cod, aIn, aOut), ng, cp) { + let #(newDom, cp1) = instantiateApplied(dom, ng, cp); + #(newCod, cp2) = instantiateApplied(cod, ng, cp1); + #(newAnswerIn, cp3) = instantiateApplied(aIn, ng, cp2); + #(newAnswerOut, cp4) = instantiateApplied(aOut, ng, cp3); + in #(controlFunType(newDom, newCod, newAnswerIn, newAnswerOut), cp4) + } + (operType(name, args), ng, cp) { + let #(newArgs, cp2) = instantiateArgs(args, ng, cp); + in #(operType(name, newArgs), cp2) + } +} + +fn instantiateArgs { + ([], _, cp) { #([], cp) } + (h @ t, ng, cp) { + let #(newHead, cp1) = instantiateApplied(h, ng, cp); + #(newTail, cp2) = instantiateArgs(t, ng, cp1); + in #(newHead @ newTail, cp2) + } +} + +fn freshType(type, ng, s) { + fst(instantiateApplied(applySubst(type, s), ng, nullCpEnv)); +} + +fn retrieve { + (name, tcEnv(name, type, _), ng, s) { freshType(type, ng, s) } + (name, nullTcEnv, _, _) { error("infer_expr: unbound variable '" @@ name @@ "'") } + (name, tcEnv(_, _, tail), ng, s) { retrieve(name, tail, ng, s) } +} + +fn retrieveBound { + (name, tcEnv(name, type, _)) { type } + (name, nullTcEnv) { error("infer_expr: unbound variable '" @@ name @@ "'") } + (name, tcEnv(_, _, tail)) { retrieveBound(name, tail) } +} + +fn freshTupleParts { + (0) { [] } + (size) { freshTypeVar() @ freshTupleParts(size - 1) } +} + +fn makeTupleTemplate(size) { + tupleType(freshTupleParts(size)) +} + +fn tupleEntry { + (0, entry @ _) { entry } + (index, _ @ rest) { tupleEntry(index - 1, rest) } + (_, []) { error("infer_expr: tuple index out of bounds") } +} + +fn renderType { + (varType(name)) { name } + (thunkType(type)) { + "#() -> " @@ renderType(type) + } + (funType(dom, cod)) { + renderDomType(dom) @@ " -> " @@ renderType(cod) + } + (controlThunkType(type, aIn, aOut)) { + "#() -[" @@ renderType(aIn) @@ "=>" @@ renderType(aOut) @@ "]-> " @@ renderType(type) + } + (controlFunType(dom, cod, aIn, aOut)) { + renderDomType(dom) @@ " -[" @@ renderType(aIn) @@ "=>" @@ renderType(aOut) @@ "]-> " @@ renderType(cod) + } + (operType("Tuple", args)) { + "#(" @@ renderTypeList(args) @@ ")" + } + (operType(name, [])) { name } + (operType(name, args)) { + name @@ "(" @@ renderTypeList(args) @@ ")" + } +} + +fn renderDomType { + (type = funType(_, _)) { "(" @@ renderType(type) @@ ")" } + (type = thunkType(_)) { "(" @@ renderType(type) @@ ")" } + (type = controlFunType(_, _, _, _)) { "(" @@ renderType(type) @@ ")" } + (type = controlThunkType(_, _, _)) { "(" @@ renderType(type) @@ ")" } + (type) { renderType(type) } +} + +fn renderTypeList { + ([]) { "" } + (type @ []) { renderType(type) } + (type @ rest) { renderType(type) @@ ", " @@ renderTypeList(rest) } +} + +fn print_type(type) { puts(renderType(type)) } + +fn normalizeVarName(counter) { "'" @@ $counter } + +fn canonicalizeType { + (varType(name), re, counter) { + switch (lookupCopy(name, re)) { + (just(type)) { #(type, re, counter) } + (nothing) { + let canonical = varType(normalizeVarName(counter)) + in #(canonical, cpEnv(name, canonical, re), counter + 1) + } + } + } + (thunkType(type), re, counter) { + let #(canonicalType, re1, counter1) = canonicalizeType(type, re, counter); + in #(thunkType(canonicalType), re1, counter1) + } + (funType(dom, cod), re, counter) { + let #(canonicalDom, re1, counter1) = canonicalizeType(dom, re, counter); + #(canonicalCod, re2, counter2) = canonicalizeType(cod, re1, counter1); + in #(funType(canonicalDom, canonicalCod), re2, counter2) + } + (controlThunkType(type, aIn, aOut), re, counter) { + let #(canonicalType, re1, counter1) = canonicalizeType(type, re, counter); + #(canonicalIn, re2, counter2) = canonicalizeType(aIn, re1, counter1); + #(canonicalOut, re3, counter3) = canonicalizeType(aOut, re2, counter2); + in #(controlThunkType(canonicalType, canonicalIn, canonicalOut), re3, counter3) + } + (controlFunType(dom, cod, aIn, aOut), re, counter) { + let #(canonicalDom, re1, counter1) = canonicalizeType(dom, re, counter); + #(canonicalCod, re2, counter2) = canonicalizeType(cod, re1, counter1); + #(canonicalIn, re3, counter3) = canonicalizeType(aIn, re2, counter2); + #(canonicalOut, re4, counter4) = canonicalizeType(aOut, re3, counter3); + in #(controlFunType(canonicalDom, canonicalCod, canonicalIn, canonicalOut), + re4, + counter4) + } + (operType(name, args), re, counter) { + let #(canonicalArgs, re2, counter2) = canonicalizeArgs(args, re, counter); + in #(operType(name, canonicalArgs), re2, counter2) + } +} + +fn canonicalizeTop(type) { + let #(canonicalType, _, _) = canonicalizeType(type, nullCpEnv, 0); + in canonicalType +} + +fn latentControlInExprList(exprs, e, ng, s) { + list.any(fn (expr) { latentControlInBody(expr, e, ng, s) }, exprs) +} + +fn latentControlInBindings(bindings, e, ng, s) { + list.any(fn { + (#(_, expr)) { latentControlInBody(expr, e, ng, s) } + }, bindings) +} + +fn latentControlInCondCases(cases, e, ng, s) { + list.any(fn { + (#(matchExpr, resultExpr)) { + latentControlInBody(matchExpr, e, ng, s) or + latentControlInBody(resultExpr, e, ng, s) + } + }, cases) +} + +fn latentControlInMatchCases(cases, e, ng, s) { + list.any(fn { + (#(_, resultExpr)) { latentControlInBody(resultExpr, e, ng, s) } + }, cases) +} + +fn directControlfulApplyBody { + (E.apply(fun, args), e, ng, s) { + let ansType = freshTypeVar(); + #(funTypeExp, s1) = analyzeExpr(fun, e, ng, s, ansType, ansType, true, true); + #(argTypes, s2) = analyzeArgs(args, e, ng, s1, ansType, ansType, true, true); + in isControlCallable(applySubst(funTypeExp, s2)) or + hasControlCallableType(argTypes) + } + (_, _, _, _) { false } +} + +fn latentControlInBody { + (E.amb_expr(left, right), e, ng, s) { + latentControlInBody(left, e, ng, s) or + latentControlInBody(right, e, ng, s) + } + (E.shift_expr(_), _, _, _) { true } + (expr = E.apply(_, _), e, ng, s) { + directControlfulApplyBody(expr, e, ng, s) + } + (E.sequence(exprs), e, ng, s) { + latentControlInExprList(exprs, e, ng, s) + } + (E.if_expr(test, con, alt), e, ng, s) { + latentControlInBody(test, e, ng, s) or + latentControlInBody(con, e, ng, s) or + latentControlInBody(alt, e, ng, s) + } + (E.cond_expr(test, cases), e, ng, s) { + latentControlInBody(test, e, ng, s) or + latentControlInCondCases(cases, e, ng, s) + } + (E.match_cases(indexExpr, cases), e, ng, s) { + latentControlInBody(indexExpr, e, ng, s) or + latentControlInMatchCases(cases, e, ng, s) + } + (E.let_expr(bindings, body), e, ng, s) | + (E.letstar_expr(bindings, body), e, ng, s) | + (E.letrec_expr(bindings, body), e, ng, s) { + latentControlInBindings(bindings, e, ng, s) or + latentControlInBody(body, e, ng, s) + } + (E.construct(_, _, args), e, ng, s) { + latentControlInExprList(args, e, ng, s) + } + (E.make_tuple(exprs), e, ng, s) { + latentControlInExprList(exprs, e, ng, s) + } + (E.primapp(_, left, right), e, ng, s) { + latentControlInBody(left, e, ng, s) or + latentControlInBody(right, e, ng, s) + } + (E.deconstruct(_, _, expr), e, ng, s) | + (E.tuple_index(_, _, expr), e, ng, s) | + (E.cut_expr(expr), e, ng, s) | + (E.tag(expr), e, ng, s) | + (E.print_exp(expr), e, ng, s) | + (E.typeof_expr(expr), e, ng, s) | + (E.typedefs(_, expr), e, ng, s) { + latentControlInBody(expr, e, ng, s) + } + (_, _, _, _) { false } +} + +fn isControlCallable { + (controlThunkType(_, _, _)) { true } + (controlFunType(_, _, _, _)) { true } + (_) { false } +} + +fn hasControlCallableType { + (types) { list.any(isControlCallable, types) } +} + +fn canonicalizeArgs { + ([], re, counter) { #([], re, counter) } + (arg @ rest, re, counter) { + let #(canonicalArg, re1, counter1) = canonicalizeType(arg, re, counter); + #(canonicalRest, re2, counter2) = canonicalizeArgs(rest, re1, counter1); + in #(canonicalArg @ canonicalRest, re2, counter2) + } +} + +fn supportedPrimitive { + ("+") | ("-") | ("*") | ("/") | ("%") | ("**") | + ("=") | ("==") | ("!=") | ("<") | (">") | ("<=") | (">=") { + true + } + (_) { false } +} + +fn supports { + (E.amb_expr(left, right)) { + supports(left) and supports(right) + } + (E.back_expr) { + true + } + (E.callcc_expr(expr)) | + (E.print_exp(expr)) | + (E.reset_expr(expr)) | + (E.shift_expr(expr)) | + (E.tag(expr)) | + (E.cut_expr(expr)) | + (E.typeof_expr(expr)) { + supports(expr) + } + (E.var(_)) | + (E.bigint(_)) | + (E.stdint(_)) | + (E.character(_)) { + true + } + (E.constant("true", _)) | + (E.constant("false", _)) | + (E.constant("null", _)) { + true + } + (E.constant(_, _)) { + false + } + (E.lambda([], body)) | + (E.lambda(_, body)) { + supports(body) + } + (E.apply(fun, [])) | + (E.apply(fun, args)) { + supports(fun) and supportsList(args) + } + (E.if_expr(test, con, alt)) { + supports(test) and supports(con) and supports(alt) + } + (E.cond_expr(test, cases)) { + supports(test) and supportsCondCases(cases) + } + (E.match_cases(expr, cases)) { + supports(expr) and supportsMatchCases(cases) + } + (E.let_expr(bindings, body)) | + (E.letrec_expr(bindings, body)) | + (E.letstar_expr(bindings, body)) { + supportsBindings(bindings) and supports(body) + } + (E.make_tuple(exprs)) { + supportsList(exprs) + } + (E.make_vec(_, _)) { false } + (E.primapp(name, left, right)) { + supportedPrimitive(name) and supports(left) and supports(right) + } + (E.tuple_index(_, _, expr)) { + supports(expr) + } + (E.construct(_, _, args)) { + supportsList(args) + } + (E.deconstruct(_, _, scrutinee)) { + supports(scrutinee) + } + (E.sequence(exprs)) { + supportsNonEmptyList(exprs) + } + (E.typedefs(_, body)) { + supports(body) + } + (_) { + false + } +} + +fn supportsList { + (exprs) { list.all(supports, exprs) } +} + +fn supportsNonEmptyList { + (exprs) { not list.empty(exprs) and supportsList(exprs) } +} + +fn supportsBindings { + (bindings) { + list.all(fn { + (#(_, expr)) { supports(expr) } + }, bindings) + } +} + +fn supportsCondCases { + (cases) { not list.empty(cases) and supportsCondCasesTail(cases) } +} + +fn supportsCondCasesTail { + (cases) { + list.all(fn { + (#(matchExpr, resultExpr)) { + supports(matchExpr) and supports(resultExpr) + } + }, cases) + } +} + +fn supportsMatchCases { + (cases) { not list.empty(cases) and supportsMatchCasesTail(cases) } +} + +fn supportsMatchCasesTail { + (cases) { + list.all(fn { + (#(_, resultExpr)) { supports(resultExpr) } + }, cases) + } +} + +fn analyzeArgs { + ([], _, _, s, aIn, aOut, _, _) { + #([], preserveAnswers(aIn, aOut, s)) + } + (h @ t, e, ng, s, aIn, aOut, cAll, dAct) { + let afterHead = freshTypeVar() + #(headType, s1) = analyzeExpr(h, e, ng, s, aIn, afterHead, cAll, dAct); + #(tailTypes, s2) = analyzeArgs(t, e, ng, s1, + applySubst(afterHead, s1), + aOut, cAll, dAct); + in #(headType @ tailTypes, s2) + } +} + +fn analyzeCondCases { + (#(matchExpr, resultExpr) @ [], e, ng, s, resultType, aIn, aOut, cAll, dAct) { + let #(matchType, s1) = analyzeExpr(matchExpr, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(matchType, intType(), s1); + #(caseType, s3) = analyzeExpr(resultExpr, e, ng, s2, aIn, aOut, cAll, dAct); + s4 = unifyType(resultType, caseType, s3); + in #(applySubst(resultType, s4), s4); + } + (#(matchExpr, resultExpr) @ rest, e, ng, s, resultType, aIn, aOut, cAll, dAct) { + let #(matchType, s1) = analyzeExpr(matchExpr, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(matchType, intType(), s1); + #(caseType, s3) = analyzeExpr(resultExpr, e, ng, s2, aIn, aOut, cAll, dAct); + s4 = unifyType(resultType, caseType, s3); + in analyzeCondCases(rest, e, ng, s4, + applySubst(resultType, s4), + aIn, aOut, cAll, dAct) + } + ([], _, _, _, _, _, _, _, _) { + error("infer_expr: cond requires at least one case") + } +} + +fn analyzeMatchCases { + (#(_, resultExpr) @ [], e, ng, s, resultType, aIn, aOut, cAll, dAct) { + let #(caseType, s1) = analyzeExpr(resultExpr, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(resultType, caseType, s1); + in #(applySubst(resultType, s2), s2) + } + (#(_, resultExpr) @ rest, e, ng, s, resultType, aIn, aOut, cAll, dAct) { + let #(caseType, s1) = analyzeExpr(resultExpr, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(resultType, caseType, s1) + in analyzeMatchCases(rest, e, ng, s2, + applySubst(resultType, s2), + aIn, aOut, cAll, dAct) + } + ([], _, _, s, resultType, aIn, aOut, _, _) { + let s1 = preserveAnswers(aIn, aOut, s) + in #(applySubst(resultType, s1), s1) + } +} + +fn bindParams { + ([], e, ng) { #([], e, ng) } + (param @ rest, e, ng) { + let paramType = freshTypeVar(); + paramName = typeVarName(paramType) + #(restTypes, e2, ng2) = bindParams(rest, + tcEnv(param, paramType, e), + paramName @ ng); + in #(paramType @ restTypes, e2, ng2) + } +} + +fn analyzeLetBindings { + ([], _, _, s, aIn, aOut, _, _) { + #([], preserveAnswers(aIn, aOut, s)) + } + (#(name, expr) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let afterBinding = freshTypeVar() + #(exprType, s1) = analyzeExpr(expr, e, ng, s, aIn, afterBinding, cAll, dAct); + #(restBindings, s2) = analyzeLetBindings(rest, e, ng, s1, + applySubst(afterBinding, s1), + aOut, cAll, dAct); + in #( #(name, applySubst(exprType, s2)) @ restBindings, s2 ) + } +} + +fn extendTypeEnv { + ([], e) { e } + (#(name, type) @ rest, e) { + extendTypeEnv(rest, tcEnv(name, type, e)) + } +} + +fn analyzeSequence { + (expr @ [], e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(expr, e, ng, s, aIn, aOut, cAll, dAct) + } + (expr @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let afterExpr = freshTypeVar() + #(_, s1) = analyzeExpr(expr, e, ng, s, aIn, afterExpr, cAll, dAct); + in analyzeSequence(rest, e, ng, s1, applySubst(afterExpr, s1), aOut, cAll, dAct) + } + ([], _, _, _, _, _, _, _) { error("infer_expr: empty sequence") } +} + +fn bindRecBindings { + ([], e) { e } + (#(name, expr = E.lambda(_, _)) @ rest, e) { + let binderType = freshTypeVar(); + in bindRecBindings(rest, tcEnv(name, binderType, e)) + } + (#(_, _) @ rest, e) { + bindRecBindings(rest, e) + } +} + +fn finalizeRecBindings { + ([], _, s) { [] } + (#(name, _) @ rest, e, s) { + #(name, applySubst(retrieveBound(name, e), s)) @ finalizeRecBindings(rest, e, s) + } +} + +fn snapshotRecBindings(bindings, e, s) { + snapshotRecBindingsAcc(bindings, e, s, nullCpEnv, 0) => fn (#(snapshot, _, _)) { + snapshot + } +} + +fn snapshotRecBindingsAcc { + ([], _, _, re, counter) { #("", re, counter) } + (#(name, expr = E.lambda(_, _)) @ rest, e, s, re, counter) { + let #(canonicalType, re1, counter1) = + canonicalizeType(applySubst(retrieveBound(name, e), s), re, counter); + #(tailSnapshot, re2, counter2) = + snapshotRecBindingsAcc(rest, e, s, re1, counter1); + in #(name @@ "::" @@ renderType(canonicalType) @@ ";" @@ tailSnapshot, re2, counter2) + } + (#(_, _) @ rest, e, s, re, counter) { + snapshotRecBindingsAcc(rest, e, s, re, counter) + } +} + +fn processRecBinding(name, expr, e, ng, s, aIn, aOut, cAll, dAct) { + let binderType = retrieveBound(name, e); + ng2 = typeVarName(binderType) @ ng + in analyzeExpr(expr, e, ng2, s, aIn, aOut, cAll, dAct) => fn (#(exprType, s1)) { + unifyType(binderType, exprType, s1) + } +} + +fn checkRecBindings { + ([], _, _, s, _, _, _, _) { s } + (#(name, expr) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let s1 = processRecBinding(name, expr, e, ng, s, aIn, aOut, cAll, dAct) + in checkRecBindings(rest, e, ng, s1, aIn, aOut, cAll, dAct) + } +} + +fn processFirstRecBindings { + ([], e, _, s, _, _, _, _) { #(e, s) } + (#(name, expr = E.lambda(_, _)) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let s1 = processRecBinding(name, expr, e, ng, s, aIn, aOut, cAll, dAct) + in processFirstRecBindings(rest, e, ng, s1, aIn, aOut, cAll, dAct) + } + (#(name, expr) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let binderType = freshTypeVar(); + e2 = tcEnv(name, binderType, e); + s1 = processRecBinding(name, expr, e2, ng, s, aIn, aOut, cAll, dAct) + in processFirstRecBindings(rest, e2, ng, s1, aIn, aOut, cAll, dAct) + } +} + +fn checkRecLambdaBindings { + ([], _, _, s, _, _, _, _) { s } + (#(name, expr = E.lambda(_, _)) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + let s1 = processRecBinding(name, expr, e, ng, s, aIn, aOut, cAll, dAct) + in checkRecLambdaBindings(rest, e, ng, s1, aIn, aOut, cAll, dAct) + } + (#(_, _) @ rest, e, ng, s, aIn, aOut, cAll, dAct) { + checkRecLambdaBindings(rest, e, ng, s, aIn, aOut, cAll, dAct) + } +} + +fn iterateRecBindings { + (_, _, _, s, 0, _, _, _, _, _) { s } + (bindings, e, ng, s, passesLeft, previousSnapshot, aIn, aOut, cAll, dAct) { + let s1 = checkRecLambdaBindings(bindings, e, ng, s, aIn, aOut, cAll, dAct); + currentSnapshot = snapshotRecBindings(bindings, e, s1) + in if (currentSnapshot == previousSnapshot) { + s1 + } else { + iterateRecBindings(bindings, e, ng, s1, passesLeft - 1, + currentSnapshot, aIn, aOut, cAll, dAct) + } + } +} + +fn analyzeLetStar { + ([], body, e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(body, e, ng, s, aIn, aOut, cAll, dAct) + } + (#(name, expr) @ rest, body, e, ng, s, aIn, aOut, cAll, dAct) { + let afterBinding = freshTypeVar(); + #(exprType, s1) = analyzeExpr(expr, e, ng, s, aIn, afterBinding, cAll, dAct); + in analyzeLetStar(rest, body, + tcEnv(name, applySubst(exprType, s1), e), + ng, s1, + applySubst(afterBinding, s1), + aOut, cAll, dAct) + } +} + +fn isArithOp { + ("+") | ("-") | ("*") | ("/") | ("%") | ("**") { true } + (_) { false } +} + +fn isCmpOp { + ("=") | ("==") | ("!=") | ("<") | (">") | ("<=") | (">=") { true } + (_) { false } +} + +fn analyzePrimitive(name, left, right, e, ng, s, aIn, aOut, cAll, dAct) { + let afterLeft = freshTypeVar() + #(leftType, s1) = analyzeExpr(left, e, ng, s, aIn, afterLeft, cAll, dAct); + #(rightType, s2) = analyzeExpr(right, e, ng, s1, + applySubst(afterLeft, s1), + aOut, cAll, dAct); + s3 = unifyType(leftType, intType(), s2); + s4 = unifyType(rightType, intType(), s3) + in + if (isArithOp(name)) { + #(intType(), s4) + } else if (isCmpOp(name)) { + #(boolType(), s4) + } else { + error("infer_expr: unsupported primitive " @@ name) + } +} + +fn analyzeConstruct(name, args, e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(E.apply(E.var(name), args), e, ng, s, aIn, aOut, cAll, dAct) +} + +fn ctorTypeToTypeExp { + (E.varType(name)) { varType("'" @@ name) } + (E.operType(name, args)) { operType(name, ctorTypeArgList(args)) } + (E.funType(a, b)) { funType(ctorTypeToTypeExp(a), ctorTypeToTypeExp(b)) } +} + +fn ctorTypeArgList { + ([]) { [] } + (h @ t) { ctorTypeToTypeExp(h) @ ctorTypeArgList(t) } +} + +fn ctorSchemesToBindings { + ([]) { [] } + (E.ctorScheme(name, ctorType) @ rest) { + #(name, ctorTypeToTypeExp(ctorType)) @ ctorSchemesToBindings(rest) + } +} + +fn spineArg { + (0, funType(arg, _)) { arg } + (n, funType(_, rest)) { spineArg(n - 1, rest) } + (0, controlFunType(arg, _, _, _)) { arg } + (n, controlFunType(_, rest, _, _)) { spineArg(n - 1, rest) } + (_, _) { error("infer_expr: deconstruct index out of range for constructor type") } +} + +fn spineResult { + (funType(_, rest)) { spineResult(rest) } + (controlFunType(_, rest, _, _)) { spineResult(rest) } + (type) { type } +} + +fn analyzeExpr { + (E.amb_expr(left, right), e, ng, s, aIn, aOut, cAll, dAct) { + let #(leftType, s1) = analyzeExpr(left, e, ng, s, aIn, aOut, cAll, dAct); + #(rightType, s2) = analyzeExpr(right, e, ng, s1, aIn, aOut, cAll, dAct); + s3 = unifyType(leftType, rightType, s2) + in #(applySubst(leftType, s3), s3) + } + (E.back_expr, _, _, s, aIn, aOut, _, _) { + pureResult(freshTypeVar(), s, aIn, aOut) + } + (E.cut_expr(expr), e, ng, s, aIn, aOut, cAll, dAct) | + (E.print_exp(expr), e, ng, s, aIn, aOut, cAll, dAct) | + (E.tag(expr), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(expr, e, ng, s, aIn, aOut, cAll, dAct) + } + (E.typeof_expr(expr), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(expr, e, ng, s, aIn, aOut, cAll, dAct) => fn (#(_, s1)) { + #(stringType(), s1) + } + } + (E.var(name), e, ng, s, aIn, aOut, _, _) { + let s1 = preserveAnswers(aIn, aOut, s) + in #(retrieve(name, e, ng, s1), s1) + } + (E.bigint(_), _, _, s, aIn, aOut, _, _) | + (E.stdint(_), _, _, s, aIn, aOut, _, _) { + pureResult(intType(), s, aIn, aOut) + } + (E.character(_), _, _, s, aIn, aOut, _, _) { + pureResult(charType(), s, aIn, aOut) + } + (E.constant("true", _), _, _, s, aIn, aOut, _, _) | + (E.constant("false", _), _, _, s, aIn, aOut, _, _) { + pureResult(boolType(), s, aIn, aOut) + } + (E.constant("null", _), _, _, s, aIn, aOut, _, _) { + pureResult(nullValueType(), s, aIn, aOut) + } + (E.constant(name, _), _, _, _, _, _, _, _) { + error("infer_expr: unsupported constant " @@ name) + } + (E.lambda([], body), e, ng, s, aIn, aOut, _, _) { + let #(bAnsIn, bAnsOut) = freshLocalAnswers(); + #(bType, s1) = analyzeExpr(body, e, ng, s, bAnsIn, bAnsOut, true, false); + in if (latentControlInBody(body, e, ng, s1)) { + let s2 = preserveAnswers(aIn, aOut, s1) + in #(makeLambdaCallable(applySubst(bType, s2), true, + applySubst(bAnsIn, s2), + applySubst(bAnsOut, s2)), s2) + } else { + let resBType = applySubst(bType, s1) + s2 = preserveAnswers(aIn, aOut, s1) + in #(makeLambdaCallable(resBType, false, resBType, resBType), s2) + } + } + (E.lambda(params, body), e, ng, s, aIn, aOut, _, _) { + let #(paramTypes, e2, ng2) = bindParams(params, e, ng); + #(bAnsIn, bAnsOut) = freshLocalAnswers(); + #(bType, s1) = analyzeExpr(body, e2, ng2, s, bAnsIn, bAnsOut, true, false); + in if (latentControlInBody(body, e2, ng2, s1)) { + let s2 = preserveAnswers(aIn, aOut, s1) + in #(makeLambdaCallableChain(paramTypes, + applySubst(bType, s2), + true, + applySubst(bAnsIn, s2), + applySubst(bAnsOut, s2)), s2) + } else { + let resBType = applySubst(bType, s1) + s2 = preserveAnswers(aIn, aOut, s1) + in #(makeLambdaCallableChain(paramTypes, + resBType, + false, + resBType, + resBType), s2) + } + } + (E.apply(fun, []), e, ng, s, aIn, aOut, cAll, dAct) { + let afterFun = freshTypeVar(); + #(funTypeExp, s1) = analyzeExpr(fun, e, ng, s, aIn, afterFun, cAll, dAct); + resultType = freshTypeVar(); + in consumeThunkCallable(funTypeExp, resultType, + applySubst(afterFun, s1), + aOut, cAll, dAct, s1) + } + (E.apply(fun, args), e, ng, s, aIn, aOut, cAll, dAct) { + let afterFun = freshTypeVar() + #(funTypeExp, s1) = analyzeExpr(fun, e, ng, s, aIn, afterFun, cAll, dAct); + #(argTypes, s2) = analyzeArgs(args, e, ng, s1, + applySubst(afterFun, s1), + aOut, cAll, dAct); + resultType = freshTypeVar() + in consumeCurriedCallable(funTypeExp, argTypes, resultType, + applySubst(afterFun, s2), + aOut, cAll, dAct, s2) + } + (E.callcc_expr(called), e, ng, s, aIn, aOut, cAll, dAct) { + let #(calledType, s1) = analyzeExpr(called, e, ng, s, aIn, aOut, cAll, dAct); + a = freshTypeVar(); + b = freshTypeVar(); + continuationType = funType(a, b); + callccType = funType(continuationType, a); + s2 = unifyType(calledType, callccType, s1) + in #(applySubst(a, s2), s2) + } + (E.reset_expr(expr), e, ng, s, aIn, aOut, _, _) { + let #(bAnsIn, bAnsOut) = freshLocalAnswers(); + #(bType, s1) = analyzeExpr(expr, e, ng, s, bAnsIn, bAnsOut, true, true); + s2 = unifyType(bType, bAnsIn, s1); + s3 = preserveAnswers(aIn, aOut, s2) + in #(applySubst(bAnsOut, s3), s3) + } + (E.shift_expr(expr), e, ng, s, aIn, aOut, cAll, _) { + if (cAll) { + let shiftBodyResult = freshTypeVar() + #(shiftedType, s1) = analyzeExpr(expr, e, ng, s, + shiftBodyResult, + shiftBodyResult, + false, false); + holeType = freshTypeVar(); + capturedAnswer = freshTypeVar(); + continuationType = funType(holeType, capturedAnswer); + shiftedFunType = funType(continuationType, shiftBodyResult); + s2 = unifyType(shiftedType, shiftedFunType, s1); + s3 = unifyType(aIn, capturedAnswer, s2); + s4 = unifyType(aOut, shiftBodyResult, s3) + in #(applySubst(holeType, s4), s4) + } else { + error("infer_expr: shift requires reset") + } + } + (E.if_expr(test, con, alt), e, ng, s, aIn, aOut, cAll, dAct) { + let #(testType, s1) = analyzeExpr(test, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(testType, boolType(), s1); + #(conType, s3) = analyzeExpr(con, e, ng, s2, aIn, aOut, cAll, dAct); + #(altType, s4) = analyzeExpr(alt, e, ng, s3, aIn, aOut, cAll, dAct); + s5 = unifyType(conType, altType, s4); + in #(applySubst(conType, s5), s5) + } + (E.cond_expr(test, cases), e, ng, s, aIn, aOut, cAll, dAct) { + let #(testType, s1) = analyzeExpr(test, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(testType, intType(), s1); + resultType = freshTypeVar() + in analyzeCondCases(cases, e, ng, s2, resultType, aIn, aOut, cAll, dAct) + } + (E.match_cases(indexExpr, cases), e, ng, s, aIn, aOut, cAll, dAct) { + let #(indexType, s1) = analyzeExpr(indexExpr, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(indexType, intType(), s1); + resultType = freshTypeVar() + in analyzeMatchCases(cases, e, ng, s2, resultType, aIn, aOut, cAll, dAct) + } + (E.let_expr(bindings, body), e, ng, s, aIn, aOut, cAll, dAct) { + let #(bindingTypes, s1) = + analyzeLetBindings(bindings, e, ng, s, aIn, aOut, cAll, dAct); + in analyzeExpr(body, extendTypeEnv(bindingTypes, e), ng, s1, aIn, aOut, cAll, dAct) + } + (E.letrec_expr(bindings, body), e, ng, s, aIn, aOut, cAll, dAct) { + let e2 = bindRecBindings(bindings, e); + #(e3, s1) = processFirstRecBindings(bindings, e2, ng, s, aIn, aOut, cAll, dAct); + snapshot = snapshotRecBindings(bindings, e3, s1); + s2 = iterateRecBindings(bindings, e3, ng, s1, 9, snapshot, aIn, aOut, cAll, dAct); + finalized = finalizeRecBindings(bindings, e3, s2) + in analyzeExpr(body, extendTypeEnv(finalized, e), ng, s2, aIn, aOut, cAll, dAct) + } + (E.letstar_expr(bindings, body), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeLetStar(bindings, body, e, ng, s, aIn, aOut, cAll, dAct) + } + (E.construct(name, _, args), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeConstruct(name, args, e, ng, s, aIn, aOut, cAll, dAct) + } + (E.deconstruct(name, index, scrutinee), e, ng, s, aIn, aOut, cAll, dAct) { + let ctorType = retrieve(name, e, ng, s); + fieldType = spineArg(index, ctorType); + resultType = spineResult(ctorType) + #(scrutType, s1) = analyzeExpr(scrutinee, e, ng, s, aIn, aOut, cAll, dAct); + s2 = unifyType(scrutType, resultType, s1) + in #(applySubst(fieldType, s2), s2) + } + (E.make_tuple(exprs), e, ng, s, aIn, aOut, cAll, dAct) { + let #(partTypes, s1) = analyzeArgs(exprs, e, ng, s, aIn, aOut, cAll, dAct); + in #(tupleType(partTypes), s1) + } + (E.make_vec(_, _), _, _, _, _, _, _, _) { + error("infer_expr: make_vec is unsupported before desugaring") + } + (E.primapp(name, left, right), e, ng, s, aIn, aOut, cAll, dAct) { + analyzePrimitive(name, left, right, e, ng, s, aIn, aOut, cAll, dAct) + } + (E.tuple_index(size, index, expr), e, ng, s, aIn, aOut, cAll, dAct) { + let #(exprType, s1) = analyzeExpr(expr, e, ng, s, aIn, aOut, cAll, dAct); + template = makeTupleTemplate(size); + s2 = unifyType(exprType, template, s1) + in switch (applySubst(template, s2)) { + (operType("Tuple", parts)) { #(tupleEntry(index, parts), s2) } + (_) { error("infer_expr: tuple template mismatch") } + } + } + (E.sequence(exprs), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeSequence(exprs, e, ng, s, aIn, aOut, cAll, dAct) + } + (E.typedefs(defs, body), e, ng, s, aIn, aOut, cAll, dAct) { + analyzeExpr(body, extendTypeEnv(ctorSchemesToBindings(defs), e), + ng, s, aIn, aOut, cAll, dAct) + } + (x, _, _, _, _, _, _, _) { + E.print_expr(x); + puts("\n"); + error("infer_expr: unsupported expression") + } +} + +fn infer(expr) { + let topAnswer = freshTypeVar() + #(type, s) = analyzeExpr(expr, nullTcEnv, [], nullSubstEnv, + topAnswer, topAnswer, false, false); + in normalizeType(applySubst(type, s)) +} + +fn infer_string(source) { + infer(E.parse(source)) +} + +fn infer_to_string(expr) { + renderType(canonicalizeTop(infer(expr))) +} \ No newline at end of file diff --git a/fn/rewrite/minexpr.fn b/fn/rewrite/minexpr.fn index 4e32d0c1..3b44cc3e 100644 --- a/fn/rewrite/minexpr.fn +++ b/fn/rewrite/minexpr.fn @@ -24,7 +24,9 @@ namespace make_vec(number, list(expr)) | match_cases(expr, list(#(list(number), expr))) | primop(string) | + reset_expr(expr) | sequence(list(expr)) | + shift_expr(expr) | stdint(number) | var(string) } @@ -193,6 +195,13 @@ namespace puts(")"); x; } + (reset_expr(e)) { + puts("(reset"); + put_indent(depth + 1); + go(depth + 1, e); + puts(")"); + x; + } (stdint(i)) { putn(i); x; @@ -203,8 +212,15 @@ namespace puts(")"); x; } + (shift_expr(e)) { + puts("(shift"); + put_indent(depth + 1); + go(depth + 1, e); + puts(")"); + x; + } (match_cases(exp, cases)) { - puts("(match-cases"); + puts("(match_cases"); put_indent(depth + 1); go(depth + 1, exp); list.for_each(fn(#(indices, caseExpr)) { @@ -220,7 +236,7 @@ namespace x; } (make_vec(size, elements)) { - puts("(make-vec "); + puts("(make_vec "); putn(size); go_sequence(depth, elements); puts(")"); @@ -388,6 +404,8 @@ namespace (sexp([atom("amb"), a, b])) { amb_expr(to_expr(a), to_expr(b)) } (sexp([atom("call/cc"), e])) { callcc_expr(to_expr(e)) } (sexp([atom("cut"), e])) { cut_expr(to_expr(e)) } + (sexp([atom("reset"), e])) { reset_expr(to_expr(e)) } + (sexp([atom("shift"), e])) { shift_expr(to_expr(e)) } (sexp([atom("if"), e1, e2, e3])) { if_expr(to_expr(e1), to_expr(e2), to_expr(e3)) } (sexp(atom("cond") @ test @ branches)) { cond_expr(to_expr(test), branches |> fn { (sexp([e1, e2])) { #(to_expr(e1), to_expr(e2)) } diff --git a/fn/rewrite/samples.fn b/fn/rewrite/samples.fn index 9e3ead19..d639e137 100644 --- a/fn/rewrite/samples.fn +++ b/fn/rewrite/samples.fn @@ -1,10 +1,10 @@ namespace fn data() {[ ";1. Basic application", - "(g a)", + "(letrec ((g (λ (x) x))) (let ((a 1)) (g a)))", ";2. Simple λ application", - "((λ (x) (h x)) (g 4))", + "(letrec ((g (λ (n) (+ n 1))) (h (λ (x) x))) ((λ (x) (h x)) (g 4)))", ";3. Lambda definition with primitives", "(λ (a b) (+ a (* b 2)))", @@ -13,7 +13,10 @@ namespace "((λ (a b) (+ a (* b 2))) 3 4)", ";5. Lambda application with function call in primitive", - "((λ (a b) (+ a (* (f b) 2))) 3 4)", + "(letrec ((f (λ (x) (+ x 1)))) ((λ (a b) (+ a (* (f b) 2))) 3 4))", + + ";5b. Letrec identity used polymorphically in body", + "(letrec ((id (λ (x) x))) (if (id true) (id 1) (id 2)))", ";6. Amb operator (non-determinism)", "(amb 1 2)", @@ -27,6 +30,33 @@ namespace ";9. Call/cc with computation before escape", "(call/cc (λ (k) (+ 10 (k 5))))", + ";9b. reset/shift that discards the surrounding context", + "(reset (+ 1 (shift (λ (k) 2))))", + + ";9c. reset/shift with multi-shot continuation reuse", + "(reset (+ 1 (shift (λ (k) (+ (k 2) (k 3))))))", + + ";9a. reset/shift with a single continuation resume", + "(reset (+ 1 (shift (λ (k) (k 2)))))", + + ";9d. reset inside an outer computation", + "(+ 1 (reset (shift (λ (k) 2))))", + + ";9d2. reset/shift under a taken if branch", + "(reset (if (= 1 1) (+ 1 (shift (λ (k) (k 2)))) 99))", + + ";9d3. reset/shift under an untaken if branch", + "(reset (if (= 1 2) 99 (+ 1 (shift (λ (k) (k 2))))))", + + ";9d4. reset/shift in a begin tail position", + "(reset (begin 10 (+ 1 (shift (λ (k) (k 2))))))", + + ";9d5. reset/shift aborting the rest of a begin", + "(reset (begin (+ 100 23) (shift (λ (k) 2)) 99))", + + ";9e. reset/shift in the presence of amb", + "(amb (reset (+ 1 (shift (λ (k) 2)))) 9)", + ";10. Nested call/cc", "(call/cc (λ (k1) (call/cc (λ (k2) (k1 (k2 7))))))", @@ -46,13 +76,13 @@ namespace "(((λ (x) (λ (y) (+ x y))) 5) 3)", ";16. If expression with complex branches", - "(if (= x 0) (f 1) (g 2))", + "(letrec ((f (λ (n) (+ n 1))) (g (λ (n) (+ n 2)))) (let ((x 0)) (if (= x 0) (f 1) (g 2))))", ";17. If with nested if", - "(if (= x 0) (if (= y 0) 1 2) 3)", + "(let ((x 0) (y 1)) (if (= x 0) (if (= y 0) 1 2) 3))", ";18. Sequence (begin in Racket)", - "(begin (f 1) (g 2) (h 3))", + "(letrec ((f (λ (x) x)) (g (λ (x) x)) (h (λ (x) x))) (begin (f 1) (g 2) (h 3)))", ";19. Letrec with mutual recursion", "(letrec ((even (λ (n) (if (= n 0) true (odd (- n 1)))))" @@ -72,7 +102,7 @@ namespace "(+ (amb (begin (back) 10) 20) 3)", ";21. Nested application", - "(f (g (h x)))", + "(letrec ((h (λ (x) (+ x 1))) (g (λ (x) (+ x 2))) (f (λ (x) (+ x 3)))) (let ((x 1)) (f (g (h x)))))", ";22. Multiple primitives in sequence", "(+ (* 2 3) (- 5 1))", @@ -87,127 +117,127 @@ namespace "(+ 1 (+ 2 (+ 3 (+ 4 5))))", ";26. Deeply nested primitives with a function call", - "(+ 1 (+ 2 (+ 3 (+ 4 (f 5)))))", + "(letrec ((f (λ (x) (+ x 1)))) (+ 1 (+ 2 (+ 3 (+ 4 (f 5))))))", ";27. Application with multiple complex arguments", - "(f (g a) (h b) (i c))", + "(letrec ((g (λ (x) (+ x 1))) (h (λ (x) (+ x 2))) (i (λ (x) (+ x 3))) (f (λ (x y z) (+ x (+ y z))))) (let ((a 1) (b 2) (c 3)) (f (g a) (h b) (i c))))", ";28. If where branches have applications", - "(if test (f (g x)) (h (i y)))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2))) (h (λ (x) (+ x 3))) (i (λ (x) (+ x 4)))) (let ((test true) (x 1) (y 2)) (if test (f (g x)) (h (i y)))))", ";29. Sequence with amb", "(begin (amb 1 2) (amb 3 4))", ";30. Call/cc that passes continuation to another function", - "(call/cc (λ (k) (f k)))", + "(letrec ((f (λ (k) (k 42)))) (call/cc (λ (k) (f k))))", ";31. cond expression - like switch/case", - "(cond x (1 (result1)) (2 (result2)) (3 (result3)))", + "(letrec ((result1 (λ () 11)) (result2 (λ () 22)) (result3 (λ () 33))) (let ((x 2)) (cond x (1 (result1)) (2 (result2)) (3 (result3)))))", ";32. cond with complex test and results", - "(cond (f x) (1 (g 1)) (2 (h 2)))", + "(letrec ((f (λ (x) x)) (g (λ (x) (+ x 10))) (h (λ (x) (+ x 20)))) (let ((x 2)) (cond (f x) (1 (g 1)) (2 (h 2)))))", ";33. construct with atomic arguments", - "(construct pair 1 2)", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (construct pair 0 1 2))", ";34. construct with complex arguments", - "(construct pair (f 1) (g 2))", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (construct pair 0 (f 1) (g 2))))", ";35. nested construct", - "(construct cons (f x) (construct cons (g y) (constant nil)))", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (let ((x 1) (y 2)) (construct pair 0 (f x) (construct pair 0 (g y) 42)))))", ";36. deconstruct with atomic argument", - "(deconstruct pair 0 p)", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (let ((p (construct pair 0 10 20))) (deconstruct pair 0 p)))", ";37. deconstruct with complex argument", - "(deconstruct pair 1 (f x))", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (letrec ((f (λ (x) (construct pair 0 x (+ x 1))))) (let ((x 1)) (deconstruct pair 1 (f x)))))", ";38. nested deconstruct", - "(deconstruct pair 0 (deconstruct pair 1 (f x)))", + "(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b))))) (letrec ((f (λ (x) (construct pair 0 (construct pair 0 x (+ x 1)) (+ x 2))))) (let ((x 1)) (deconstruct pair 0 (deconstruct pair 0 (f x))))))", ";39. let with atomic value", - "(let ((x 42)) (f x))", + "(letrec ((f (λ (v) v))) (let ((x 42)) (f x)))", ";40. let with complex value", - "(let ((x (f 10))) (g x))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (let ((x (f 10))) (g x)))", ";41. nested let", - "(let ((x (f 1)) (y (g x))) (h x y))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2))) (h (λ (x y) (+ x y)))) (let ((x (f 1))) (let ((y (g x))) (h x y))))", ";42. nested let*", - "(let* ((x (f 1)) (y (g x))) (h x y))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2))) (h (λ (x y) (+ x y)))) (let* ((x (f 1)) (y (g x))) (h x y)))", ";46. make_tuple with atomic args", "(make_tuple 1 2 3)", ";47. make_tuple with complex args", - "(make_tuple (f 1) (g 2))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (make_tuple (f 1) (g 2)))", ";48. make_tuple with mixed args", - "(make_tuple x (f y) 42)", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1) (y 2)) (make_tuple x (f y) 42)))", ";49. make_vec with atomic args", "(make_vec 3 1 2 3)", ";50. make_vec with complex args", - "(make_vec 2 (f 1) (g 2))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (make_vec 2 (f 1) (g 2)))", ";51. make_vec with mixed args", - "(make_vec 3 x (f y) 42)", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1) (y 2)) (make_vec 3 x (f y) 42)))", ";52. match_cases with atomic test", - "(match_cases x ((1 2) (result1)) ((3 4 5) (result2)))", + "(let ((x 3)) (match_cases x ((1 2) 10) ((3 4 5) 20)))", ";53. match_cases with complex test", - "(match_cases (f x) ((1) (g 1)) ((2) (h 2)))", + "(letrec ((f (λ (x) x)) (g (λ (x) (+ x 1))) (h (λ (x) (+ x 2)))) (let ((x 2)) (match_cases (f x) ((1) (g 1)) ((2) (h 2)))))", ";54. match_cases with complex results", - "(match_cases x ((1) (f 1)) ((2) (g 2)))", + "(letrec ((f (λ (x) (+ x 1))) (g (λ (x) (+ x 2)))) (let ((x 2)) (match_cases x ((1) (f 1)) ((2) (g 2)))))", ";59. print_exp with atomic argument", - "(print x)", + "(let ((x 42)) (print x))", ";60. print_exp with complex argument", - "(print (f x))", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (print (f x))))", ";61. print_exp nested in computation", - "(+ (print (f x)) 10)", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (+ (print (f x)) 10)))", ";62. tag with atomic argument", - "(tag x)", + "(let ((x 42)) (tag x))", ";63. tag with complex argument", - "(tag (f x))", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (tag (f x))))", ";64. tag in cond test", - "(cond (tag (f x)) (1 (result1)) (2 (result2)))", + "(letrec ((f (λ (x) (+ x 1))) (result1 (λ () 11)) (result2 (λ () 22))) (let ((x 1)) (cond (tag (f x)) (1 (result1)) (2 (result2)))))", ";65. tuple_index with atomic tuple", - "(tuple_index 3 0 t)", + "(let ((t (make_tuple 10 20 30))) (tuple_index 3 0 t))", ";66. tuple_index with complex tuple", - "(tuple_index 2 1 (f x))", + "(letrec ((f (λ (x) (make_tuple x (+ x 1))))) (let ((x 1)) (tuple_index 2 1 (f x))))", ";67. nested tuple_index", - "(tuple_index 2 0 (tuple_index 3 1 (f x)))", + "(letrec ((f (λ (x) (make_tuple 0 (make_tuple x (+ x 1)) 2)))) (let ((x 1)) (tuple_index 2 0 (tuple_index 3 1 (f x)))))", ";68. typedefs with simple expression", - "(typedefs 0 x)", + "(typedefs () 42)", ";69. typedefs with letrec body", - "(typedefs 0 (letrec ((f (λ (x) (g x)))) (f 42)))", + "(typedefs () (letrec ((g (λ (x) x)) (f (λ (x) (g x)))) (f 42)))", ";70. typedefs with complex body", - "(typedefs 0 (f (g x)))", + "(typedefs ((nil (list 'a)) (cons (-> 'a (-> (list 'a) (list 'a))))) (letrec ((g (λ (x) (+ x 1))) (f (λ (x) (g x)))) (let ((x 1)) (f (g x)))))", ";72. typeof_expr with atomic argument", - "(typeof x)", + "(typeof 42)", ";73. typeof_expr with complex argument", - "(typeof (f x))", + "(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (typeof (f x))))", - ";74. typeof_expr in conditional", - "(if (typeof (f x)) (g 1) (h 2))", + ";74. typeof_expr in conditional branches", + "(letrec ((f (λ (x) x)) (g (λ (x) (+ x 1))) (h (λ (x) (+ x 2)))) (let ((x 1)) (if (= x 1) (typeof (f x)) (typeof (h 2)))))", ";75. curried function application", "(letrec ((add (λ (x y) (+ x y)))) ((add 2) 3))", @@ -225,130 +255,130 @@ namespace "(+ (+ 1 2) (+ 3 4))", ";78. Number + variable combinations", - "(+ 0 x)", - "(+ x 0)", - "(+ 5 (+ 3 x))", - "(+ 5 (+ x 3))", - "(+ (+ x 3) 5)", - "(+ (+ 3 x) 5)", + "(let ((x 10)) (+ 0 x))", + "(let ((x 10)) (+ x 0))", + "(let ((x 10)) (+ 5 (+ 3 x)))", + "(let ((x 10)) (+ 5 (+ x 3)))", + "(let ((x 10)) (+ (+ x 3) 5))", + "(let ((x 10)) (+ (+ 3 x) 5))", ";79. Adding expressions with both + and -", - "(+ 2 (- 5 x))", - "(+ 2 (- x 5))", - "(+ (- 3 x) 4)", - "(+ (- x 3) 4)", + "(let ((x 10)) (+ 2 (- 5 x)))", + "(let ((x 10)) (+ 2 (- x 5)))", + "(let ((x 10)) (+ (- 3 x) 4))", + "(let ((x 10)) (+ (- x 3) 4))", ";80. Two compound expressions", - "(+ (+ 2 x) (+ 3 y))", - "(+ (+ x 2) (+ y 3))", - "(+ (+ 2 x) (- 3 y))", - "(+ (- 2 x) (- 3 y))", - "(+ (- x 2) (- y 3))", - "(+ (- x 2) (- 3 y))", + "(let ((x 10) (y 20)) (+ (+ 2 x) (+ 3 y)))", + "(let ((x 10) (y 20)) (+ (+ x 2) (+ y 3)))", + "(let ((x 10) (y 20)) (+ (+ 2 x) (- 3 y)))", + "(let ((x 10) (y 20)) (+ (- 2 x) (- 3 y)))", + "(let ((x 10) (y 20)) (+ (- x 2) (- y 3)))", + "(let ((x 10) (y 20)) (+ (- x 2) (- 3 y)))", ";81. Subtraction with numbers and variables ---", "(- 10 3)", - "(- x 0)", - "(- 0 x)", - "(- 5 (+ 2 x))", - "(- 5 (+ x 2))", - "(- 5 (- 2 x))", - "(- 5 (- x 2))", - "(- (+ 5 x) 3)", - "(- (+ x 5) 3)", - "(- (- 5 x) 3)", - "(- (- x 5) 3)", + "(let ((x 10)) (- x 0))", + "(let ((x 10)) (- 0 x))", + "(let ((x 10)) (- 5 (+ 2 x)))", + "(let ((x 10)) (- 5 (+ x 2)))", + "(let ((x 10)) (- 5 (- 2 x)))", + "(let ((x 10)) (- 5 (- x 2)))", + "(let ((x 10)) (- (+ 5 x) 3))", + "(let ((x 10)) (- (+ x 5) 3))", + "(let ((x 10)) (- (- 5 x) 3))", + "(let ((x 10)) (- (- x 5) 3))", ";82. Two compound sub expressions", - "(- (+ 5 x) (+ 2 y))", - "(- (- 5 x) (+ 2 y))", - "(- (+ 5 x) (- 2 y))", - "(- (+ 5 x) (- y 2))", - "(- (- 5 x) (- 2 y))", - "(- (- x 5) (- y 2))", - "(- (- 5 x) (- y 2))", + "(let ((x 10) (y 20)) (- (+ 5 x) (+ 2 y)))", + "(let ((x 10) (y 20)) (- (- 5 x) (+ 2 y)))", + "(let ((x 10) (y 20)) (- (+ 5 x) (- 2 y)))", + "(let ((x 10) (y 20)) (- (+ 5 x) (- y 2)))", + "(let ((x 10) (y 20)) (- (- 5 x) (- 2 y)))", + "(let ((x 10) (y 20)) (- (- x 5) (- y 2)))", + "(let ((x 10) (y 20)) (- (- 5 x) (- y 2)))", ";83. Multiplication with numbers and variables ---", "(* 3 4)", - "(* 0 x)", - "(* x 0)", - "(* 1 x)", - "(* x 1)", - "(* 2 (* 3 x))", - "(* 2 (* x 3))", - "(* (* x 2) 3)", - "(* (* 2 x) 3)", + "(let ((x 10)) (* 0 x))", + "(let ((x 10)) (* x 0))", + "(let ((x 10)) (* 1 x))", + "(let ((x 10)) (* x 1))", + "(let ((x 10)) (* 2 (* 3 x)))", + "(let ((x 10)) (* 2 (* x 3)))", + "(let ((x 10)) (* (* x 2) 3))", + "(let ((x 10)) (* (* 2 x) 3))", ";84. Multiplication distributing over addition/subtraction", - "(* 3 (+ x 4))", - "(* 3 (+ 4 x))", - "(* (+ x 4) 3)", - "(* 3 (- x 4))", - "(* 3 (- 4 x))", - "(* (- x 4) 3)", - "(* (- 4 x) 3)", + "(let ((x 10)) (* 3 (+ x 4)))", + "(let ((x 10)) (* 3 (+ 4 x)))", + "(let ((x 10)) (* (+ x 4) 3))", + "(let ((x 10)) (* 3 (- x 4)))", + "(let ((x 10)) (* 3 (- 4 x)))", + "(let ((x 10)) (* (- x 4) 3))", + "(let ((x 10)) (* (- 4 x) 3))", ";85. Multiplication with division", - "(* 6 (/ 2 x))", - "(* 6 (/ x 2))", - "(* (/ x 2) 6)", - "(* (/ 2 x) 6)", + "(let ((x 10)) (* 6 (/ 2 x)))", + "(let ((x 10)) (* 6 (/ x 2)))", + "(let ((x 10)) (* (/ x 2) 6))", + "(let ((x 10)) (* (/ 2 x) 6))", ";86. Division with numbers and variables ---", "(/ 12 4)", - "(/ x 1)", - "(/ 0 x)", - "(/ (/ x 2) 3)", - "(/ (/ 6 x) 2)", - "(/ 6 (/ 2 x))", - "(/ 6 (/ x 2))", - "(/ 6 (* x 2))", - "(/ 6 (* 2 x))", - "(/ (* 6 x) 2)", - "(/ (* x 6) 2)", + "(let ((x 10)) (/ x 1))", + "(let ((x 10)) (/ 0 x))", + "(let ((x 10)) (/ (/ x 2) 3))", + "(let ((x 10)) (/ (/ 6 x) 2))", + "(let ((x 10)) (/ 6 (/ 2 x)))", + "(let ((x 10)) (/ 6 (/ x 2)))", + "(let ((x 10)) (/ 6 (* x 2)))", + "(let ((x 10)) (/ 6 (* 2 x)))", + "(let ((x 10)) (/ (* 6 x) 2))", + "(let ((x 10)) (/ (* x 6) 2))", ";87. Division distributing over numerator addition/subtraction", - "(/ (+ 6 x) 2)", - "(/ (+ x 6) 2)", - "(/ (- 6 x) 2)", - "(/ (- x 6) 2)", + "(let ((x 10)) (/ (+ 6 x) 2))", + "(let ((x 10)) (/ (+ x 6) 2))", + "(let ((x 10)) (/ (- 6 x) 2))", + "(let ((x 10)) (/ (- x 6) 2))", ";88. Compound division expressions", - "(* (/ x 2) (/ y 3))", - "(* (/ 2 x) (/ 3 y))", - "(/ (/ x 2) (/ y 3))", - "(/ (/ 2 x) (/ 3 y))", + "(let ((x 10) (y 20)) (* (/ x 2) (/ y 3)))", + "(let ((x 10) (y 20)) (* (/ 2 x) (/ 3 y)))", + "(let ((x 10) (y 20)) (/ (/ x 2) (/ y 3)))", + "(let ((x 10) (y 20)) (/ (/ 2 x) (/ 3 y)))", ";89. Power with numbers and variables ---", "(** 2 3)", - "(** x 0)", - "(** x 1)", - "(** 0 x)", - "(** 1 x)", - "(** (** x 2) 3)", - "(* (** x 2) (** x 3))", - "(** (* x 2) 3)", - "(** (* 2 x) 3)", + "(let ((x 10)) (** x 0))", + "(let ((x 10)) (** x 1))", + "(let ((x 3)) (** 0 x))", + "(let ((x 3)) (** 1 x))", + "(let ((x 10)) (** (** x 2) 3))", + "(let ((x 10)) (* (** x 2) (** x 3)))", + "(let ((x 10)) (** (* x 2) 3))", + "(let ((x 10)) (** (* 2 x) 3))", ";90. Mixed operations - deeper nesting ---", - "(+ 1 (+ 2 (+ 3 (+ 4 x))))", - "(+ 1 (+ 2 (+ 3 (+ 4 (+ 5 (+ 6 x))))))", - "(* 2 (* 3 (* 4 (* 5 x))))", - "(- 10 (- 9 (- 8 (- 7 (- 6 x)))))", - "(+ 1 (- 2 (+ 3 (- 4 (+ 5 x)))))", - "(* 2 (+ 3 (* 4 (+ 5 (* 6 x)))))", - "(/ (/ (/ (* 24 x) 2) 3) 4)", - "(** (** x 2) 3)", - "(* 2 (+ 3 (* 4 x)))", - "(+ (* 2 3) (* 4 x))", - "(- (* 2 (+ x 3)) 5)", - "(/ (+ (* 2 x) 6) 2)", + "(let ((x 10)) (+ 1 (+ 2 (+ 3 (+ 4 x)))))", + "(let ((x 10)) (+ 1 (+ 2 (+ 3 (+ 4 (+ 5 (+ 6 x)))))))", + "(let ((x 10)) (* 2 (* 3 (* 4 (* 5 x)))))", + "(let ((x 10)) (- 10 (- 9 (- 8 (- 7 (- 6 x))))))", + "(let ((x 10)) (+ 1 (- 2 (+ 3 (- 4 (+ 5 x))))))", + "(let ((x 10)) (* 2 (+ 3 (* 4 (+ 5 (* 6 x))))))", + "(let ((x 10)) (/ (/ (/ (* 24 x) 2) 3) 4))", + "(let ((x 10)) (** (** x 2) 3))", + "(let ((x 10)) (* 2 (+ 3 (* 4 x))))", + "(let ((x 10)) (+ (* 2 3) (* 4 x)))", + "(let ((x 10)) (- (* 2 (+ x 3)) 5))", + "(let ((x 10)) (/ (+ (* 2 x) 6) 2))", ";91. Complex expressions with multiple variables ---", - "(+ (+ x 1) (+ y 2))", - "(+ (* 2 x) (* 3 y))", - "(- (* 2 (+ x 1)) (* 3 (- y 1)))", - "(/ (+ (* 2 x) 4) 2)", + "(let ((x 10) (y 20)) (+ (+ x 1) (+ y 2)))", + "(let ((x 10) (y 20)) (+ (* 2 x) (* 3 y)))", + "(let ((x 10) (y 20)) (- (* 2 (+ x 1)) (* 3 (- y 1))))", + "(let ((x 10)) (/ (+ (* 2 x) 4) 2))", ";92. Expressions that should fully reduce to constants ---", "(+ (+ 1 2) (+ 3 4))", @@ -362,35 +392,35 @@ namespace "(+ (* 2 (+ 3 4)) (- (* 5 6) (/ 20 4)))", ";93. Edge cases ---", - "(+ (- x x) 5)", - "(* (/ x x) 5)", - "(+ x (- 0 x))", - "(* x (/ 1 x))", + "(let ((x 10)) (+ (- x x) 5))", + "(let ((x 10)) (* (/ x x) 5))", + "(let ((x 10)) (+ x (- 0 x)))", + "(let ((x 10)) (* x (/ 1 x)))", ";94. Nested with function calls (should partially fold) ---", - "(+ 3 (+ 4 (f x)))", - "(* 2 (+ 3 (f x)))", - "(+ (* 2 3) (f x))", - "(- (+ 5 (f x)) 3)", - "(/ (* 6 (f x)) 2)", - "(+ 1 (+ 2 (+ 3 (+ 4 (f x)))))", - "(* 2 (* 3 (* 4 (f x))))", - "(+ (* 2 (+ 3 4)) (f x))", - "(- (* 2 (+ 5 (f x))) 10)", - "(/ (* 6 (+ 2 (f x))) 3)", - "(+ (f x) (+ 1 (+ 2 (+ 3 4))))", - "(* (+ 2 3) (+ (f x) 10))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (+ 3 (+ 4 (f x)))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (* 2 (+ 3 (f x)))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (+ (* 2 3) (f x))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (- (+ 5 (f x)) 3)))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (/ (* 6 (f x)) 2)))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (+ 1 (+ 2 (+ 3 (+ 4 (f x)))))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (* 2 (* 3 (* 4 (f x))))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (+ (* 2 (+ 3 4)) (f x))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (- (* 2 (+ 5 (f x))) 10)))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (/ (* 6 (+ 2 (f x))) 3)))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (+ (f x) (+ 1 (+ 2 (+ 3 4))))))", + "(letrec ((f (λ (n) (+ n 1)))) (let ((x 10)) (* (+ 2 3) (+ (f x) 10))))", ";95. Test eta reduction ---", - "(λ (x) (f x))", - "(λ (x) ((h p) x))", - "(λ (y) ((λ (x) (g x)) y))", - "(λ (y) ((λ (x) ((h p) x)) y))", + "(letrec ((f (λ (y) y))) (λ (x) (f x)))", + "(letrec ((h (λ (p x) (+ p x)))) (let ((p 1)) (λ (x) ((h p) x))))", + "(letrec ((g (λ (x) (+ x 1)))) (λ (y) ((λ (x) (g x)) y)))", + "(letrec ((h (λ (p x) (+ p x)))) (let ((p 1)) (λ (y) ((λ (x) ((h p) x)) y))))", ";96. NEW simplification targets ---", - "(+ (/ x 2) (/ y 2))", - "(- (/ x 2) (/ y 2))", - "(/ (* k x) (* k y))", + "(let ((x 10) (y 20)) (+ (/ x 2) (/ y 2)))", + "(let ((x 10) (y 20)) (- (/ x 2) (/ y 2)))", + "(let ((k 2) (x 10) (y 20)) (/ (* k x) (* k y)))", ";97. cut ---", "(amb (amb (cut 1) 2) 3)", diff --git a/fn/rewrite/test_harness.fn b/fn/rewrite/test_harness.fn index c049f00b..a0a2bde0 100644 --- a/fn/rewrite/test_harness.fn +++ b/fn/rewrite/test_harness.fn @@ -3,6 +3,7 @@ let link "beta_reduce.fn" as β; link "eta_reduce.fn" as η; link "constant_folding.fn" as OF; + link "infer_expr.fn" as INFER; link "expr.fn" as E; link "minexpr.fn" as M; link "../listutils.fn" as list; @@ -30,12 +31,17 @@ in halt = M.var("□"); fail = M.var("Ω"); a = E.parse(str); + inferred = if (INFER.supports(a)) { + INFER.infer_to_string(a) + } else { + "" + }; b = DS.desugar(a); c = C.curry(b); cc = β.reduce(c); - d = η.reduce(c); - dd = U.uncurry(c); - e = CPS.T_c(dd, halt); + d = η.reduce(cc); + dd = U.uncurry(d); + e = CPS.T(dd, halt); f = β.reduce(e); g = OF.fold(f); gg = AMB.amb(g, fail); @@ -47,6 +53,9 @@ in nltab = "\n"; in E.print_expr(a); + puts("\n"); + // puts("\n==> infer_expr\n"); + puts(inferred); // puts("\n==> desugar"); // puts(nltab); // M.print_expr(b); @@ -80,9 +89,9 @@ in // puts("\n==> closure unconvert"); // puts(nltab); // M.print_expr(hh); - puts("\n==> annotate"); - puts(nltab); - M.print_expr(hhh); + // puts("\n==> annotate"); + // puts(nltab); + // M.print_expr(hhh); puts("\n\n") } }, Samples.data()); \ No newline at end of file diff --git a/fn/rewrite/tests/test_infer_delimited.fn b/fn/rewrite/tests/test_infer_delimited.fn new file mode 100644 index 00000000..c93174f5 --- /dev/null +++ b/fn/rewrite/tests/test_infer_delimited.fn @@ -0,0 +1,35 @@ +let + link "../infer_expr.fn" as INFER; + link "../expr.fn" as E; + + fn infer_type(source) { + INFER.infer_to_string(E.parse(source)) + } + + fn supports(source) { + INFER.supports(E.parse(source)) + } +in + assert(infer_type("(reset 1)") == "Int"); + assert(infer_type("(reset (+ 1 (shift (λ (k) 2))))") == "Int"); + assert(infer_type("(reset (shift (λ (k) true)))") == "Bool"); + assert(infer_type("(reset (+ 1 (shift (λ (k) (k 2)))))") == "Int"); + assert(supports("(reset (+ 1 (shift (λ (k) (k 2)))))")); + assert(supports("(amb 1 2)")); + assert(supports("back")); + assert(supports("(make_vec 2 0)") == false); + assert(infer_type("(let ((f (λ (x) (shift (λ (k) (k x)))))) f)") == "'0 -> '0"); + assert(infer_type("(reset (let ((f (λ (x) (shift (λ (k) (k x)))))) (+ 1 (f 2))))") == "Int"); + assert(infer_type("(reset (let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (+ 1 (apply1 g))))") == "Int"); + assert(infer_type("(let ((h (λ (f) (reset (+ 1 (f)))))) h)") == "(#() -> Int) -> Int"); + assert(infer_type("(let ((f (λ () (reset (+ 1 (shift (λ (k) 2))))))) f)") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (apply1 g)))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (begin 0 (apply1 g))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (if true (apply1 g) 0)))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (let ((x 0)) (apply1 g))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (cond 2 (1 0) (2 (apply1 g)))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (match_cases 2 ((1) 0) ((2) (apply1 g)))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (typedefs () (apply1 g))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (tuple_index 2 0 (make_tuple (apply1 g) 0))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (typedefs ((wrap (-> 'a (Box 'a)))) (deconstruct wrap 0 (construct wrap 0 (apply1 g))))))") == "#() -> Int"); + assert(infer_type("(let ((apply1 (λ (f) (f 1))) (g (λ (x) (shift (λ (k) (k x)))))) (λ () (amb (apply1 g) 0)))") == "#() -> Int"); \ No newline at end of file diff --git a/fn/rewrite/tests/test_infer_expr.fn b/fn/rewrite/tests/test_infer_expr.fn new file mode 100644 index 00000000..3f595078 --- /dev/null +++ b/fn/rewrite/tests/test_infer_expr.fn @@ -0,0 +1,42 @@ +let + link "../infer_expr.fn" as INFER; + link "../expr.fn" as E; + + fn infer_type(source) { + INFER.infer_to_string(E.parse(source)) + } +in + assert(infer_type("((λ (x) x) 1)") == "Int"); + assert(infer_type("(if true (back) 1)") == "Int"); + assert(infer_type("(λ () 42)") == "#() -> Int"); + assert(infer_type("((λ () 42))") == "Int"); + assert(infer_type("(cut 1)") == "Int"); + assert(infer_type("(typeof 42)") == "list(Char)"); + assert(infer_type("(letrec ((f (λ (x) x)) (h (λ (x) (+ x 2)))) (let ((x 1)) (if (= x 1) (typeof (f x)) (typeof (h 2)))))") == "list(Char)"); + assert(infer_type("(print 42)") == "Int"); + assert(infer_type("(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (print (f x))))") == "Int"); + assert(infer_type("(typeof (print 42))") == "list(Char)"); + assert(infer_type("(amb 1 2)") == "Int"); + assert(infer_type("(call/cc (λ (k) (k 5)))") == "Int"); + assert(infer_type("(call/cc (λ (k) 42))") == "Int"); + assert(infer_type("(call/cc (λ (k) (+ 10 (k 5))))") == "Int"); + assert(infer_type("(let ((x 42)) (tag x))") == "Int"); + assert(infer_type("(letrec ((f (λ (x) (+ x 1)))) (let ((x 1)) (tag (f x))))") == "Int"); + assert(infer_type("(letrec ((f (λ (x) (+ x 1))) (result1 (λ () 11)) (result2 (λ () 22))) (let ((x 1)) (cond (tag (f x)) (1 (result1)) (2 (result2)))))") == "Int"); + assert(infer_type("(amb ((λ (x) x) 1) ((λ (y) y) 2))") == "Int"); + assert(infer_type("(amb 1 (begin (back) 2))") == "Int"); + assert(infer_type("(+ (amb (begin (back) 10) 20) 3)") == "Int"); + assert(infer_type("(amb (amb (cut 1) 2) 3)") == "Int"); + assert(infer_type("(cond 2 (1 10) (2 20) (3 30))") == "Int"); + assert(infer_type("(match_cases 3 ((1 2) 10) ((3 4 5) 20))") == "Int"); + assert(infer_type("(letrec ((result1 (λ () 11)) (result2 (λ () 22)) (result3 (λ () 33))) (let ((x 2)) (cond x (1 (result1)) (2 (result2)) (3 (result3)))))") == "Int"); + assert(infer_type("(letrec ((f (λ (x) x)) (g (λ (x) (+ x 1))) (h (λ (x) (+ x 2)))) (let ((x 2)) (match_cases (f x) ((1) (g 1)) ((2) (h 2)))))") == "Int"); + assert(infer_type("(letrec ((id (λ (x) x))) (if (id true) (id 1) (id 2)))") == "Int"); + assert(infer_type("(letrec ((f (λ (x) x)) (g (λ (x) (+ x 10))) (h (λ (x) (+ x 20)))) (let ((x 2)) (cond (f x) (1 (g 1)) (2 (h 2)))))") == "Int"); + assert(infer_type("(letrec ((i (λ (x) x)) (j (λ (x y) (begin (i x) (i y))))) (j true 1))") == "Int"); + assert(infer_type("(letrec ((f (λ (x) (g x))) (g (λ (n) (+ n 1)))) (f 1))") == "Int"); + assert(infer_type("(letrec ((fact (λ (n) (if (= n 0) 1 (* n (fact (- n 1))))))) (fact 5))") == "Int"); + assert(infer_type("(letrec ((pair (λ (x y) x))) (construct pair 0 1 true))") == "Int"); + assert(infer_type("(make_tuple 1 true 'a')") == "#(Int, Bool, Char)"); + assert(infer_type("(tuple_index 3 1 (make_tuple 1 true 'a'))") == "Bool"); + assert(infer_type("(tuple_index 2 0 (letrec ((pair (λ (x) (make_tuple x (+ x 1))))) (pair 4)))") == "Int"); \ No newline at end of file diff --git a/fn/rewrite/tests/test_infer_typedefs.fn b/fn/rewrite/tests/test_infer_typedefs.fn new file mode 100644 index 00000000..1f27b2f9 --- /dev/null +++ b/fn/rewrite/tests/test_infer_typedefs.fn @@ -0,0 +1,59 @@ +let + link "../infer_expr.fn" as INFER; + link "../expr.fn" as E; + + fn infer_type(source) { + INFER.infer_to_string(E.parse(source)) + } + + fn supports(source) { + INFER.supports(E.parse(source)) + } +in + // typedefs: empty constructor env passes body through unchanged + assert(infer_type("(typedefs () 42)") == "Int"); + assert(infer_type("(typedefs () (letrec ((f (λ (x) (+ x 1)))) (f 1)))") == "Int"); + // typedefs: non-empty constructor env extends the type environment + assert(infer_type("(typedefs ((id (-> 'a 'a))) (id 1))") == "Int"); + // typedefs: constructor env bindings are polymorphic (fresh vars per use) + assert(infer_type("(typedefs ((id (-> 'a 'a))) (if (id true) (id 1) (id 2)))") == "Int"); + // typedefs: construct form uses typedef-defined constructor from env + assert(infer_type("(typedefs ((wrap (-> 'a 'a))) (construct wrap 0 42))") == "Int"); + // typedefs: construct with typedef env is reported as supported + assert(supports("(typedefs ((wrap (-> 'a 'a))) (construct wrap 0 42))")); + // typedefs: user-defined maybe constructors unify to a concrete custom type + assert(infer_type("(typedefs ((just (-> 'a (maybe 'a))) (nothing (maybe 'a)))" + "(if true (construct just 0 42) nothing))") == "maybe(Int)"); + // typedefs: deconstructing just from maybe(Int) recovers the payload type + assert(infer_type("(typedefs ((just (-> 'a (maybe 'a))) (nothing (maybe 'a)))" + "(deconstruct just 0 (construct just 0 42)))") == "Int"); + // typedefs: the same maybe family instantiates at another concrete type + assert(infer_type("(typedefs ((just (-> 'a (maybe 'a))) (nothing (maybe 'a)))" + "(if true (construct just 0 true) nothing))") == "maybe(Bool)"); + // typedefs: either constructors unify to a concrete two-parameter custom type + assert(infer_type("(typedefs ((left (-> 'a (either 'a 'b))) (right (-> 'b (either 'a 'b))))" + "(if true (construct left 0 42) (construct right 1 true)))") == "either(Int, Bool)"); + // typedefs: deconstructing left from either(Int, Bool) recovers the left payload type + assert(infer_type("(typedefs ((left (-> 'a (either 'a 'b))) (right (-> 'b (either 'a 'b))))" + "(deconstruct left 0 (construct left 0 42)))") == "Int"); + // typedefs: deconstructing right from either(Int, Bool) recovers the right payload type + assert(infer_type("(typedefs ((left (-> 'a (either 'a 'b))) (right (-> 'b (either 'a 'b))))" + "(deconstruct right 0 (construct right 1 true)))") == "Bool"); + // typedefs: recursive list constructors unify to a concrete recursive custom type + assert(infer_type("(typedefs ((nil (list 'a)) (cons (-> 'a (-> (list 'a) (list 'a)))))" + "(if true (construct cons 0 1 nil) nil))") == "list(Int)"); + // typedefs: deconstructing cons from list(Int) recovers the head payload type + assert(infer_type("(typedefs ((nil (list 'a)) (cons (-> 'a (-> (list 'a) (list 'a)))))" + "(deconstruct cons 0 (construct cons 0 1 nil)))") == "Int"); + // typedefs: deconstructing cons from list(Int) recovers the tail payload type + assert(infer_type("(typedefs ((nil (list 'a)) (cons (-> 'a (-> (list 'a) (list 'a)))))" + "(deconstruct cons 1 (construct cons 0 1 nil)))") == "list(Int)"); + // deconstruct: reported as supported + assert(supports("(typedefs ((box (-> 'a (Box 'a))))" + "(deconstruct box 0 (construct box 0 42)))")); + // deconstruct: extracts field type from constructor scheme + assert(infer_type("(typedefs ((box (-> 'a (Box 'a))))" + "(deconstruct box 0 (construct box 0 42)))") == "Int"); + // deconstruct: selects correct field by index from multi-field constructor + assert(infer_type("(typedefs ((pair (-> 'a (-> 'b (Pair 'a 'b)))))" + "(deconstruct pair 1 (construct pair 0 42 true)))") == "Bool");