Skip to content

Commit

Permalink
Merge pull request #518 from HigherOrderCO/512-put-constructor-tags-b…
Browse files Browse the repository at this point in the history
…ehind-a-reference-in-num-scott-adt-encoding

#512 Put constructor tags behind a reference in num scott adt encoding
  • Loading branch information
imaqtkatt authored May 28, 2024
2 parents 0433311 + 983bd90 commit ba8fa19
Show file tree
Hide file tree
Showing 67 changed files with 534 additions and 208 deletions.
2 changes: 1 addition & 1 deletion Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
name = "bend-lang"
description = "A high-level, massively parallel programming language"
license = "Apache-2.0"
version = "0.2.24"
version = "0.2.25"
edition = "2021"
rust-version = "1.74"
exclude = ["tests/snapshots/"]
Expand Down
46 changes: 29 additions & 17 deletions docs/compiler-options.md
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
# Options

| flag | Default | What it does? |
|----------------|----------|---------------|
| `-Oall` | Disabled | Enables all compiler passes |
| `-Ono-all` | Disabled | Disables all compiler passes |
| `-Oeta` `-Ono-eta` | Disabled | [eta-reduction](#eta-reduction) |
| `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) |
| `-Olinearize-matches` `-Olinearize-matches-alt` `-Ono-linearize-matches` | Enabled | [linearize-matches](#linearize-matches) |
| `-Ofloat_combinators` `-Ono-float_combinators` | Enabled | [float-combinators](#float-combinators) |
| `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) |
| `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) |
| `-Ocheck-net-size` `-Ono-check-net-size` | Disabled | [check-net-size](#check-net-size) |
| `-Oadt-scott` `-Oadt-num-scott` | adt-num-scott | [adt-encoding](#adt-encoding) | |
| flag | Default | What it does? |
| ------------------------------------------------------------------------ | ------------- | ----------------------------------------- |
| `-Oall` | Disabled | Enables all compiler passes |
| `-Ono-all` | Disabled | Disables all compiler passes |
| `-Oeta` `-Ono-eta` | Disabled | [eta-reduction](#eta-reduction) |
| `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) |
| `-Olinearize-matches` `-Olinearize-matches-alt` `-Ono-linearize-matches` | Enabled | [linearize-matches](#linearize-matches) |
| `-Ofloat_combinators` `-Ono-float_combinators` | Enabled | [float-combinators](#float-combinators) |
| `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) |
| `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) |
| `-Ocheck-net-size` `-Ono-check-net-size` | Disabled | [check-net-size](#check-net-size) |
| `-Oadt-scott` `-Oadt-num-scott` | adt-num-scott | [adt-encoding](#adt-encoding) |

## Eta-reduction

Expand All @@ -20,6 +20,7 @@ Enables or disables Eta Reduction for defined functions.
Eta reduction simplifies lambda expressions, removing redundant parameters. [See also](https://wiki.haskell.org/Eta_conversion).

Example:

```py
# program
id = λx x
Expand All @@ -37,6 +38,7 @@ id_id = λz (id z)
If enabled, removes all unused definitions.

Example:

```py
# program
Id = λx x
Expand All @@ -63,6 +65,7 @@ Main = (Id 42)
If enabled, merges definitions that are identical at the term level.

Example:

```py
# Original program
id = λx x
Expand Down Expand Up @@ -105,6 +108,7 @@ Linearizes the variables between match cases, transforming them into combinators
When the `linearize-matches` option is used, only linearizes variables that would generate an eta-reducible application.

Example:

```py
λa λb switch a { 0: b; _: b }

Expand All @@ -118,6 +122,7 @@ Example:
When the `linearize-matches-extra` option is used, it linearizes all variables used in the arms.

example:

```py
λa λb λc switch b { 0: a; _: c }

Expand All @@ -144,6 +149,7 @@ Extracts closed terms to new definitions. See [lazy definitions](lazy-definition
Since HVM-Core is an eager runtime, this pass is enabled by default to prevent infinite expansions.

Example:

```py
True = λt λf λm t
False = λt λf λm f
Expand All @@ -164,6 +170,7 @@ fold = λinit λf λxs (xs λh λt (fold (f init h) f t) init)
If enabled, inlines terms that compile to nullary inet nodes (refs, numbers, erasures).

Example:

```py
# program
foo = 2
Expand All @@ -189,9 +196,10 @@ If enabled, checks that the size of each function after compilation has at most
This is a memory restriction of the CUDA runtime, if you're not using the `*-cu` you can disable it.

Example:

```py
# Without -Ocheck-net-size compiles normally.
# But with -Ocheck-net-size it fails with
# But with -Ocheck-net-size it fails with
# `Definition is too large for hvm`
(Radix n) =
let r = Map_/Used
Expand Down Expand Up @@ -224,10 +232,10 @@ Example:

## ADT Encoding

Selects the lambda encoding for types defined with `data`, `type` and `object`.
Selects the lambda encoding for types defined with `type` and `object`.

`-Oadt-scott` uses Scott encoding.
`-Oadt-num-scott` uses a variation of Scott encoding where instead of one lambda per constructor, we use a numeric tag to indicate which constructor it is. The numeric tag is assigned to the constructors in the order they are defined.
`-Oadt-num-scott` uses a variation of Scott encoding where instead of one lambda per constructor, we use a numeric tag to indicate which constructor it is. The numeric tag is assigned to the constructors in the order they are defined and each tag is accessible as a definition by `<type>/<ctr>/tag`.

```py
# Generates functions Option/Some and Option/None
Expand All @@ -240,8 +248,12 @@ Option/Some = λvalue λSome λNone (Some value)
Option/None = λSome λNone (None)

# With -Oadt-num-scott they become:
Option/Some = λvalue λx (x 0 value)
Option/None = λx (x 1)
Option/Some = λvalue λx (x Option/Some/tag value)
Option/None = λx (x Option/None/tag)

# Generated -Oadt-num-scott tags:
Option/Some/tag = 0
Option/None/tag = 1
```

Pattern-matching with `match` and `fold` is generated according to the encoding.
Expand Down
4 changes: 4 additions & 0 deletions src/fun/builtins.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ pub const LIST: &str = "List";
pub const LCONS: &str = "List/Cons";
pub const LNIL: &str = "List/Nil";
pub const LCONS_TAG: u32 = 1;
pub const LNIL_TAG_REF: &str = "List/Nil/tag";
pub const LCONS_TAG_REF: &str = "List/Cons/tag";

pub const HEAD: &str = "head";
pub const TAIL: &str = "tail";
Expand All @@ -15,6 +17,8 @@ pub const STRING: &str = "String";
pub const SCONS: &str = "String/Cons";
pub const SNIL: &str = "String/Nil";
pub const SCONS_TAG: u32 = 1;
pub const SNIL_TAG_REF: &str = "String/Nil/tag";
pub const SCONS_TAG_REF: &str = "String/Cons/tag";

pub const NAT: &str = "Nat";
pub const NAT_SUCC: &str = "Nat/Succ";
Expand Down
35 changes: 28 additions & 7 deletions src/fun/transform/encode_adts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,31 @@ impl Book {
/// Defines a function for each constructor in each ADT in the book.
pub fn encode_adts(&mut self, adt_encoding: AdtEncoding) {
let mut defs = vec![];
for adt in self.adts.values() {
let mut tags = vec![];

for (adt_name, adt) in self.adts.iter() {
for (ctr_idx, (ctr_name, fields)) in adt.ctrs.iter().enumerate() {
let ctrs: Vec<_> = adt.ctrs.keys().cloned().collect();

let body = match adt_encoding {
AdtEncoding::Scott => encode_ctr_scott(fields.iter().map(|f| &f.nam), ctrs, ctr_name),
AdtEncoding::NumScott => encode_ctr_num_scott(fields.iter().map(|f| &f.nam), ctr_idx),
AdtEncoding::NumScott => {
let is_object = adt_name == ctr_name;
if is_object {
let tag = Name::new(format!("{ctr_name}/tag"));
let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
let tag_def = make_tag_def(ctr_idx, &tag, adt);
tags.push((tag, tag_def));
body
} else {
let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'");
let tag = Name::new(format!("{typ}/{ctr}/tag"));
let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
let tag_def = make_tag_def(ctr_idx, &tag, adt);
tags.push((tag, tag_def));
body
}
}
};

let rules = vec![Rule { pats: vec![], body }];
Expand All @@ -22,6 +40,7 @@ impl Book {
}
}
self.defs.extend(defs);
self.defs.extend(tags);
}
}

Expand All @@ -36,16 +55,18 @@ fn encode_ctr_scott<'a>(
ctr_args.cloned().rfold(lam, |acc, arg| Term::lam(Pattern::Var(Some(arg)), acc))
}

fn encode_ctr_num_scott<'a>(
ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone,
ctr_idx: usize,
) -> Term {
fn encode_ctr_num_scott<'a>(ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone, tag: &str) -> Term {
let nam = Name::new("%x");
// λa1 .. λan λx (x TAG a1 .. an)
let term = Term::Var { nam: nam.clone() };
let tag = Term::Num { val: Num::U24(ctr_idx as u32) };
let tag = Term::r#ref(tag);
let term = Term::app(term, tag);
let term = Term::call(term, ctr_args.clone().cloned().map(|nam| Term::Var { nam }));
let term = Term::lam(Pattern::Var(Some(nam)), term);
Term::rfold_lams(term, ctr_args.cloned().map(Some))
}

fn make_tag_def(ctr_idx: usize, tag: &Name, adt: &crate::fun::Adt) -> Definition {
let tag_rule = vec![Rule { pats: vec![], body: Term::Num { val: Num::U24(ctr_idx as u32) } }];
Definition { name: tag.clone(), rules: tag_rule, builtin: adt.builtin }
}
11 changes: 5 additions & 6 deletions src/fun/transform/resugar_list.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
use crate::{
fun::{builtins, Num, Pattern, Tag, Term},
fun::{builtins, Pattern, Tag, Term},
maybe_grow, AdtEncoding,
};
use builtins::LCONS_TAG;

impl Term {
/// Converts lambda-encoded lists ending with List/Nil to list literals.
Expand Down Expand Up @@ -33,8 +32,8 @@ impl Term {
if let Term::App { tag: Tag::Static, fun, arg: head } = fun.as_mut() {
if let Term::App { tag: Tag::Static, fun, arg } = fun.as_mut() {
if let Term::Var { nam: var_app } = fun.as_mut() {
if let Term::Num { val: Num::U24(LCONS_TAG) } = arg.as_mut() {
if var_lam == var_app {
if let Term::Ref { nam } = arg.as_mut() {
if var_lam == var_app && nam == builtins::LCONS_TAG_REF {
let l = build_list_num_scott(tail.as_mut(), vec![std::mem::take(head)]);
match l {
Ok(l) => *self = Term::List { els: l.into_iter().map(|x| *x).collect() },
Expand Down Expand Up @@ -160,8 +159,8 @@ fn build_list_num_scott(term: &mut Term, mut l: Vec<Box<Term>>) -> Result<Vec<Bo
if let Term::App { tag: Tag::Static, fun, arg: head } = fun.as_mut() {
if let Term::App { tag: Tag::Static, fun, arg } = fun.as_mut() {
if let Term::Var { nam: var_app } = fun.as_mut() {
if let Term::Num { val: Num::U24(LCONS_TAG) } = arg.as_mut() {
if var_lam == var_app {
if let Term::Ref { nam } = arg.as_mut() {
if var_lam == var_app && nam == builtins::LCONS_TAG_REF {
// New list element, append and recurse
l.push(std::mem::take(head));
let l = build_list_num_scott(tail, l);
Expand Down
12 changes: 5 additions & 7 deletions src/fun/transform/resugar_string.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
use builtins::SCONS_TAG;

use crate::{
fun::{builtins, Num, Pattern, Tag, Term},
fun::{builtins, Name, Num, Pattern, Tag, Term},
maybe_grow, AdtEncoding,
};

Expand Down Expand Up @@ -34,9 +32,9 @@ impl Term {
if let Term::App { tag: Tag::Static, fun, arg: head } = fun.as_mut() {
if let Term::App { tag: Tag::Static, fun, arg } = fun.as_mut() {
if let Term::Var { nam: var_app } = fun.as_mut() {
if let Term::Num { val: Num::U24(SCONS_TAG) } = arg.as_mut() {
if let Term::Ref { nam: Name(nam) } = arg.as_mut() {
if let Term::Num { val: Num::U24(head) } = head.as_mut() {
if var_lam == var_app {
if var_lam == var_app && nam == builtins::SCONS_TAG_REF {
let head = char::from_u32(*head).unwrap_or(char::REPLACEMENT_CHARACTER);
if let Some(str) = build_string_num_scott(tail, head.to_string()) {
*self = Term::str(&str);
Expand Down Expand Up @@ -154,9 +152,9 @@ fn build_string_num_scott(term: &Term, mut s: String) -> Option<String> {
if let Term::App { tag: Tag::Static, fun, arg: head } = fun.as_ref() {
if let Term::App { tag: Tag::Static, fun, arg } = fun.as_ref() {
if let Term::Var { nam: var_app } = fun.as_ref() {
if let Term::Num { val: Num::U24(SCONS_TAG) } = arg.as_ref() {
if let Term::Ref { nam } = arg.as_ref() {
if let Term::Num { val: Num::U24(head) } = head.as_ref() {
if var_lam == var_app {
if var_lam == var_app && nam == builtins::SCONS_TAG_REF {
// New string character, append and recurse
let head = char::from_u32(*head).unwrap_or(char::REPLACEMENT_CHARACTER);
s.push(head);
Expand Down
8 changes: 6 additions & 2 deletions tests/snapshots/cli__compile_strict_loop.bend.snap
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,13 @@ input_file: tests/golden_tests/cli/compile_strict_loop.bend
@A = (((?((0 (* (* (a b)))) c) c) d) d)
& @A ~ (a b)

@List/Cons = (a (b ((1 (a (b c))) c)))
@List/Cons = (a (b ((@List/Cons/tag (a (b c))) c)))

@List/Nil = ((0 a) a)
@List/Cons/tag = 1

@List/Nil = ((@List/Nil/tag a) a)

@List/Nil/tag = 0

@main = c
& @A ~ (b c)
Expand Down
24 changes: 18 additions & 6 deletions tests/snapshots/cli__no_check_net_size.bend.snap
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,17 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/cli/no_check_net_size.bend
---
@Arr/Leaf = (a ((1 (a b)) b))
@Arr/Leaf = (a ((@Arr/Leaf/tag (a b)) b))

@Arr/Node = (a (b ((2 (a (b c))) c)))
@Arr/Leaf/tag = 1

@Arr/Null = ((0 a) a)
@Arr/Node = (a (b ((@Arr/Node/tag (a (b c))) c)))

@Arr/Node/tag = 2

@Arr/Null = ((@Arr/Null/tag a) a)

@Arr/Null/tag = 0

@Gen = (a b)
& @Gen.go ~ (a (0 b))
Expand All @@ -30,11 +36,17 @@ input_file: tests/golden_tests/cli/no_check_net_size.bend
@Main__C2 = a
& @Sort ~ (@Main__C1 a)

@Map_/Both = (a (b ((2 (a (b c))) c)))
@Map_/Both = (a (b ((@Map_/Both/tag (a (b c))) c)))

@Map_/Both/tag = 2

@Map_/Free = ((@Map_/Free/tag a) a)

@Map_/Free/tag = 0

@Map_/Free = ((0 a) a)
@Map_/Used = ((@Map_/Used/tag a) a)

@Map_/Used = ((1 a) a)
@Map_/Used/tag = 1

@Merge = ((@Merge__C13 a) a)

Expand Down
8 changes: 6 additions & 2 deletions tests/snapshots/compile_file__huge_tree.bend.snap
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,13 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file/huge_tree.bend
---
@Tree/Leaf = (a ((1 (a b)) b))
@Tree/Leaf = (a ((@Tree/Leaf/tag (a b)) b))

@Tree/Node = (a (b (c (d ((0 (a (b (c (d e))))) e)))))
@Tree/Leaf/tag = 1

@Tree/Node = (a (b (c (d ((@Tree/Node/tag (a (b (c (d e))))) e)))))

@Tree/Node/tag = 0

@main = e
& @Tree/Node ~ (a (b (c (d e))))
Expand Down
16 changes: 12 additions & 4 deletions tests/snapshots/compile_file__redex_order_recursive.bend.snap
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,13 @@ input_file: tests/golden_tests/compile_file/redex_order_recursive.bend

@List.sum__C1 = (?(((a a) @List.sum__C0) b) b)

@List/Cons = (a (b ((1 (a (b c))) c)))
@List/Cons = (a (b ((@List/Cons/tag (a (b c))) c)))

@List/Nil = ((0 a) a)
@List/Cons/tag = 1

@List/Nil = ((@List/Nil/tag a) a)

@List/Nil/tag = 0

@Tree.flip = ((@Tree.flip__C2 a) a)

Expand Down Expand Up @@ -132,9 +136,13 @@ input_file: tests/golden_tests/compile_file/redex_order_recursive.bend

@Tree.nodes__C1 = (?((@Tree.nodes__C0 (* (* 0))) a) a)

@Tree/leaf = (a ((1 (a b)) b))
@Tree/leaf = (a ((@Tree/leaf/tag (a b)) b))

@Tree/leaf/tag = 1

@Tree/node = (a (b ((@Tree/node/tag (a (b c))) c)))

@Tree/node = (a (b ((0 (a (b c))) c)))
@Tree/node/tag = 0

@add = ((@add__C0 ((a a) b)) b)

Expand Down
Loading

0 comments on commit ba8fa19

Please sign in to comment.