Skip to content

Add REF nodes for lazy allocation, and extract closed sub-exprs into new definitions#15

Open
Boscop wants to merge 21 commits into
VictorTaelin:typedfrom
HigherOrderCO-archive:typed
Open

Add REF nodes for lazy allocation, and extract closed sub-exprs into new definitions#15
Boscop wants to merge 21 commits into
VictorTaelin:typedfrom
HigherOrderCO-archive:typed

Conversation

@Boscop
Copy link
Copy Markdown

@Boscop Boscop commented Jun 27, 2023

This PR adds the REF nodes for lazy allocation of def sub-nets.
It also implements extraction of sub-terms into new definitions when possible.
E.g.

  def double = λn (n (λp (S (S (double p)))) Z)

gets pre-processed to:

  def double = λn (n EXTRACTED_0 Z)
  def $EXTRACTED_0 = λp (S (S (double p)))

but only when definition_book.extract_closed_subterms(); is called (like it is in main.rs).
Currently, main is printing the before and after:

definition_book.print();
definition_book.extract_closed_subterms();
definition_book.print();

When a REF node is interacted with, it gets substituted with its term's net, and then the normal rewriting continues.

@Boscop Boscop marked this pull request as ready for review June 29, 2023 17:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants