this is an mvp to show a way of adding special builtins with access to the internal structure of atoms. the immediate use case is providing a length function on strings, which evaluates to a Nat. this expands quite drastically the set of predicates we're able to describe, because previously there was no way to separate ground parts of a string given that epsilon can unify with anything.
it's nice in that there's no need to change any of the
signatures, apart from the introduction of reduce---
Preludic.Atom simply has type t = anyValue
and gives a dummy wrap definition. where a prelude function
can be evaluated syntactically, this evaluation can take place in
parse, which directly produces the right tag and anyValue.
where we need to defer evaluation of a prelude function until a concrete substitution has been chosen, we parse into a two-dimensional anyValue:
length("$s")
│
│parse()
│
│
▼
┌───────────────┐ sub(0 -> [a b])┌───────────────┐ reduce() ┌────────────┐
│ PreludeTag ├───────────────►│ PreludeTag ├─────────────►│ NatTag │
└───────┬───────┘ └───────────────┘ └─────┬──────┘
│ │ │
│ │ │
│ │ │
┌───────┴───────┐ ┌───────┴───────┐ ┌──────────────┐
│ LengthTag │ │ LengthTag │ │ 2 │
└───────┬───────┘ └───────┬───────┘ └──────────────┘
│ │
│ │
│ │
┌───────┴───────┐ ┌───────┴───────┐
│[Var({idx: 0})]│ │ [ a, b] │
└───────────────┘ └───────────────┘