From ba2925d8a7cd8687fe04e8eae7adeae8308c4a5d Mon Sep 17 00:00:00 2001 From: Josh Brown Date: Sat, 25 Apr 2026 14:34:19 +1000 Subject: [PATCH] add atom prelude functionality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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] │ └───────────────┘ └───────────────┘ ``` --- index.html | 35 ++++++++++++++ src/AssocComm.res | 1 + src/AtomDef.res | 4 ++ src/HOTerm.res | 1 + src/Preludic.res | 108 ++++++++++++++++++++++++++++++++++++++++++ src/SExp.res | 7 ++- src/Scratch.res | 14 ++++-- src/StringA.res | 2 + src/Symbolic.res | 1 + tests/PreludeTest.res | 14 ++++++ 10 files changed, 181 insertions(+), 6 deletions(-) create mode 100644 src/Preludic.res create mode 100644 tests/PreludeTest.res diff --git a/index.html b/index.html index 3b4f2ea..91c1747 100644 --- a/index.html +++ b/index.html @@ -248,6 +248,9 @@ .symbol-nat { color: var(--symbol-nat-col) } + .symbol-prelude { + color: var(--symbol-prelude-col) + } .symbol-turnstile { padding-left: 6px; padding-right: 6px; @@ -675,6 +678,38 @@ (Term (Cons (f nat(2)) (Cons (a nat(0)) Empty)) (Func f (Cons (Const a) (Cons (Var nat(1)) Empty)))) |- ? + + a. + -------- Eq + (Eq a a) + + s. + (Eq length("$s") nat(1)) + ---------------------- Singleton + (Singleton "$s") + + s. (Singleton "$s") + ---------------------- Rev-1 + (Rev "$s" "$s") + + s. ss. ssRev. (Rev "$ss" "$ssRev") (Singleton "$s") + ----------------------- Rev-n + (Rev "$s $ss" "$ssRev $s") + + s. sRev. (Rev "$s" "$sRev") + ---------------------- Palindrome-Even + (Palindrome "$s $sRev") + + s. sRev. m. (Rev "$s" "$sRev") + ---------------------- Palindrome-Odd + (Palindrome "$s $m $sRev") + + + ------------------ dlads + (Palindrome "a b c b a") + |- ? + + a. -------------- eq-refl diff --git a/src/AssocComm.res b/src/AssocComm.res index 10c1240..9cac980 100644 --- a/src/AssocComm.res +++ b/src/AssocComm.res @@ -204,6 +204,7 @@ module Make = ( let full = term->between(token(Const.openTerm), token(Const.closeTerm)) Parser.runParser(full, str) } + let reduce = t => t let substitute = (atom: t, subst: subst): t => { let substituted = diff --git a/src/AtomDef.res b/src/AtomDef.res index fff14f3..6a84b47 100644 --- a/src/AtomDef.res +++ b/src/AtomDef.res @@ -11,6 +11,7 @@ module type ATOM = { let upshift: (t, int, ~from: int=?) => t let substDeBruijn: (t, array>, ~from: int=?) => t let concrete: t => bool + let reduce: t => t let coerce: anyValue => option } @@ -45,6 +46,7 @@ module EmptyAtomChoice: ATOM_CHOICE = { let upshift = (_, _, ~from as _=?) => throw(AtomExpected) let substDeBruijn = (_, _, ~from as _=?) => throw(AtomExpected) let concrete = _ => throw(AtomExpected) + let reduce = _ => throw(AtomExpected) } module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): ( @@ -105,6 +107,8 @@ module MakeAtomChoice = (Left: ATOM, Right: ATOM_CHOICE): ( )->LeftBase.wrap ) ->getOrElse(() => Right.substDeBruijn(atom, substs, ~from?)) + let reduce = atom => + atom->onLeft(val => Left.reduce(val)->LeftBase.wrap)->getOrElse(() => Right.reduce(atom)) let concrete = atom => atom->onLeft(Left.concrete)->getOrElse(() => Right.concrete(atom)) } diff --git a/src/HOTerm.res b/src/HOTerm.res index 899e102..73ac3eb 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -36,6 +36,7 @@ module DefaultAtom = { let concrete = _ => true let upshift = (t, _, ~from as _=?) => t let coerce = _ => None + let reduce = t => t } module Make = (Atom: AtomDef.ATOM): { diff --git a/src/Preludic.res b/src/Preludic.res new file mode 100644 index 0000000..4ce8d8b --- /dev/null +++ b/src/Preludic.res @@ -0,0 +1,108 @@ +module Base = { + type t = AtomBase.anyValue + type AtomBase.atomTag<_> += Tag: AtomBase.atomTag + let wrap = t => t + let wrapForReal = t => AtomBase.AnyValue(Tag, t) +} + +type AtomBase.atomTag<_> += LengthTag: AtomBase.atomTag + +exception ShouldNotCallPrelude +exception NonPreludicValuePassed +module Atom = { + module Base = Base + type t = AtomBase.anyValue + type subst = Map.t + // this is probably wrong: we want to unify with any nat + let unify = (AtomBase.AnyValue(tagA, a), AtomBase.AnyValue(tagB, b), ~gen=?) => { + switch (tagA, tagB) { + | (LengthTag, LengthTag) => + StringA.Atom.unify(a, b, ~gen?)->Seq.map(subst => + subst->Util.mapMapValues(s => AtomBase.AnyValue(AtomBase.String.Tag, s)) + ) + | _ => Seq.empty + } + } + let prettyPrint = (AtomBase.AnyValue(tag, a), ~scope: array) => { + switch tag { + | LengthTag => `length(${StringA.Atom.prettyPrint(a, ~scope)})` + | _ => throw(NonPreludicValuePassed) + } + } + let parse = (str, ~scope: array, ~gen=?) => { + open Parser + liftParse(StringA.Atom.parse, ~scope, ~gen?) + ->between(token("length("), token(")")) + ->map(s => AtomBase.AnyValue(LengthTag, s)->Base.wrapForReal) + ->runParser(str) + } + + let substitute = (AtomBase.AnyValue(tag, a), subst) => { + switch tag { + | LengthTag => + AtomBase.AnyValue( + LengthTag, + a->StringA.Atom.substitute(subst->Util.Map.filterMap((_, v) => StringA.Atom.coerce(v))), + )->Base.wrapForReal + | _ => throw(NonPreludicValuePassed) + } + } + let substDeBruijn = (AtomBase.AnyValue(tag, a), subst, ~from=?) => { + switch tag { + | LengthTag => { + let subst = + a->StringA.Atom.substDeBruijn( + subst->Array.map(v => v->Option.flatMap(StringA.Atom.coerce)), + ~from?, + ) + + AtomBase.AnyValue(LengthTag, subst)->Base.wrapForReal + } + | _ => throw(NonPreludicValuePassed) + } + } + + let reduce = atom => { + let AtomBase.AnyValue(tag, a) = atom + switch tag { + | LengthTag => + if ( + a->Array.every(p => + switch p { + | AtomBase.String.String(_) => true + | _ => false + } + ) + ) { + AtomBase.AnyValue(AssocCommBase.Nat.Tag, AssocCommBase.Nat.const(Array.length(a))) + } else { + atom + } + | _ => throw(NonPreludicValuePassed) + } + } + let concrete = _ => true + let upshift = (AtomBase.AnyValue(tag, a), amount, ~from=?) => { + switch tag { + | LengthTag => AtomBase.AnyValue(LengthTag, a->StringA.Atom.upshift(amount, ~from?))->Base.wrap + | _ => throw(NonPreludicValuePassed) + } + } + let coerce = atom => Some(atom) +} + +module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom = { + type props = {atom: Atom.t, scope: array} + let make = ({atom, scope}) => { + let AtomBase.AnyValue(tag, a) = atom + switch tag { + | LengthTag => + + {React.string("length(")} + {StringA.AtomView.make({atom: a, scope})} + {React.string(")")} + + | _ => throw(NonPreludicValuePassed) + } + } +} diff --git a/src/SExp.res b/src/SExp.res index 1d65356..bf23992 100644 --- a/src/SExp.res +++ b/src/SExp.res @@ -38,7 +38,12 @@ module Make = (Atom: AtomDef.ATOM): { let equivalent = (a: t, b: t) => { a == b } - let reduce = (term: t) => term + let rec reduce = (term: t) => + switch term { + | Atom(a) => Atom(Atom.reduce(a)) + | Compound({subexps}) => Compound({subexps: subexps->Array.map(reduce)}) + | _ => term + } let rec schematicsIn: t => Belt.Set.t = (it: t) => switch it { | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) diff --git a/src/Scratch.res b/src/Scratch.res index 05082a4..33d84d2 100644 --- a/src/Scratch.res +++ b/src/Scratch.res @@ -60,12 +60,16 @@ module StringNatSymbol = AtomDef.MakeAtomChoiceAndView( StringSymbol.Atom, StringSymbol.AtomView, ) -module StringSExp = SExp.Make(StringNatSymbol.Atom) -module TermView = SExpView.Make(StringNatSymbol.Atom, StringNatSymbol.AtomView, StringSExp) -module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) -module AxiomStr = Editable.TextArea( - StringAxiomSet.Make(StringNatSymbol.Atom, StringSExp, StringSExpJView), +module Final = AtomDef.MakeAtomChoiceAndView( + Preludic.Atom, + Preludic.AtomView, + StringNatSymbol.Atom, + StringNatSymbol.AtomView, ) +module StringSExp = SExp.Make(Final.Atom) +module TermView = SExpView.Make(Final.Atom, Final.AtomView, StringSExp) +module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) +module AxiomStr = Editable.TextArea(StringAxiomSet.Make(Final.Atom, StringSExp, StringSExpJView)) module DerivationsOrLemmasStrView = MethodView.CombineMethodView( StringSExp, diff --git a/src/StringA.res b/src/StringA.res index a0e3f0b..ad44264 100644 --- a/src/StringA.res +++ b/src/StringA.res @@ -454,6 +454,7 @@ module Atom = { acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents))) } + let reduce = t => t let concrete = t => t->Array.every(p => switch p { @@ -471,6 +472,7 @@ module Atom = { | Schematic({schematic, allowed}) => Schematic({schematic, allowed}) }, ]) + | AtomBase.String.Tag => Some(a) | AssocCommBase.Nat.Tag => { module IntMap = Belt.Map.Int if a.schemas->IntMap.size == 0 && a.vars->IntMap.size == 0 { diff --git a/src/Symbolic.res b/src/Symbolic.res index cf40c66..db0fe04 100644 --- a/src/Symbolic.res +++ b/src/Symbolic.res @@ -23,6 +23,7 @@ module Atom = { let substDeBruijn = (name, _, ~from as _=?) => name let concrete = _ => true let upshift = (t, _, ~from as _=?) => t + let reduce = t => t let coerce = _ => None } diff --git a/tests/PreludeTest.res b/tests/PreludeTest.res new file mode 100644 index 0000000..f908718 --- /dev/null +++ b/tests/PreludeTest.res @@ -0,0 +1,14 @@ +open Zora + +module Util = TestUtil.MakeAtomTester(Preludic.Atom) +module ParseUtil = Util.ParseTester + +zoraBlock("parse prelude", t => + t->ParseUtil.testParse( + `length("$s")`, + ~scope=["s"], + Preludic.Base.wrapForReal( + AtomBase.AnyValue(Preludic.LengthTag, [AtomBase.String.Var({idx: 0})]), + ), + ) +) -- 2.51.2