From c77cdee052d53539259d4f69dcb6e3cb95772368 Mon Sep 17 00:00:00 2001 From: Josh Brown Date: Mon, 23 Mar 2026 13:49:50 +1100 Subject: [PATCH] combine atom functor --- src/CombinedAtom.res | 129 +++++++++++++++++++++++++++++++++++++++++ src/HOTerm.res | 7 +-- src/Scratch.res | 6 ++ src/StringA.res | 16 +---- src/StringAxiomSet.res | 18 ++++-- src/StringSymbol.res | 81 -------------------------- src/StringSymbol.resi | 3 - src/Util.res | 24 ++++++++ 8 files changed, 176 insertions(+), 108 deletions(-) create mode 100644 src/CombinedAtom.res delete mode 100644 src/StringSymbol.res delete mode 100644 src/StringSymbol.resi diff --git a/src/CombinedAtom.res b/src/CombinedAtom.res new file mode 100644 index 0000000..95f3d12 --- /dev/null +++ b/src/CombinedAtom.res @@ -0,0 +1,129 @@ +module type ATOM = SExpFunc.ATOM +exception RawVarOrSchematic + +module MakeAtom = (Left: ATOM, Right: ATOM): { + type base = + | Left(Left.t) + | Right(Right.t) + // neither of the below should appear organically. they're purely so we can lower + // substitutions to both Left.t and Right.t + | Var({idx: int}) + | Schematic({schematic: int, allowed: array}) + include ATOM with type t = base + let match: (t, Left.t => 'a, Right.t => 'a) => 'a +} => { + type base = + | Left(Left.t) + | Right(Right.t) + | Var({idx: int}) + | Schematic({schematic: int, allowed: array}) + type t = base + type subst = Map.t + type gen = ref + let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a => + switch t { + | Left(s) => leftBranch(s) + | Right(s) => rightBranch(s) + | _ => throw(RawVarOrSchematic) + } + let parse = (s, ~scope, ~gen: option=?) => { + Left.parse(s, ~scope, ~gen?) + ->Result.map(((r, rest)) => (Left(r), rest)) + ->Util.Result.or(() => + Right.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (Right(r), rest)) + ) + } + let prettyPrint = (s, ~scope) => + s->match(left => Left.prettyPrint(left, ~scope), right => Right.prettyPrint(right, ~scope)) + let unify = (s1, s2, ~gen=?) => + switch (s1, s2) { + | (Left(s1), Left(s2)) => + Left.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Left(v))) + | (Right(s1), Right(s2)) => + Right.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => Right(v))) + | (_, _) => Seq.empty + } + let substitute = (s, subst: subst) => { + s->match( + left => { + let leftSubs = subst->Util.Map.filterMap((_, v) => + switch v { + | Left(s) => Some(s) + | _ => None + } + ) + Left(Left.substitute(left, leftSubs)) + }, + right => { + let rightSubs = subst->Util.Map.filterMap((_, v) => + switch v { + | Right(s) => Some(s) + | _ => None + } + ) + Right(Right.substitute(right, rightSubs)) + }, + ) + } + let upshift = (s, amount: int, ~from=?) => + s->match( + left => Left(left->Left.upshift(amount, ~from?)), + right => Right(right->Right.upshift(amount, ~from?)), + ) + let lowerVar = idx => Some(Var({idx: idx})) + let lowerSchematic = (schematic, allowed) => Some(Schematic({schematic, allowed})) + let substDeBruijn = (s, substs: array>, ~from=?) => + s->match( + left => { + let leftSubs = substs->Array.map(s => + switch s { + | Some(Left(s)) => Some(s) + | Some(Var({idx})) => Left.lowerVar(idx) + | Some(Schematic({schematic, allowed})) => Left.lowerSchematic(schematic, allowed) + | _ => None + } + ) + Left(Left.substDeBruijn(left, leftSubs, ~from?)) + }, + right => { + let rightSubs = substs->Array.map(s => + switch s { + | Some(Right(s)) => Some(s) + | Some(Var({idx})) => Right.lowerVar(idx) + | Some(Schematic({schematic, allowed})) => Right.lowerSchematic(schematic, allowed) + | _ => None + } + ) + Right(Right.substDeBruijn(right, rightSubs, ~from?)) + }, + ) + let concrete = s => s->match(Left.concrete, Right.concrete) +} + +module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW +module MakeAtomView = ( + Left: ATOM, + LeftView: ATOM_VIEW with module Atom := Left, + Right: ATOM, + RightView: ATOM_VIEW with module Atom := Right, + Combined: module type of MakeAtom(Left, Right), +): { + include ATOM_VIEW with module Atom := Combined +} => { + type props = {name: Combined.t, scope: array} + let make = ({name, scope}: props) => + name->Combined.match( + left => , + right => , + ) +} + +module MakeAtomAndView = ( + Left: ATOM, + LeftView: ATOM_VIEW with module Atom := Left, + Right: ATOM, + RightView: ATOM_VIEW with module Atom := Right, +) => { + module Atom = MakeAtom(Left, Right) + module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom) +} diff --git a/src/HOTerm.res b/src/HOTerm.res index 2789d31..24aeb88 100644 --- a/src/HOTerm.res +++ b/src/HOTerm.res @@ -1,4 +1,3 @@ -open Util module IntCmp = Belt.Id.MakeComparable({ type t = int let cmp = Pervasives.compare @@ -102,7 +101,7 @@ let rec mapbind0 = (term: t, f: int => result t>, ~from: int=0): t = | Ok(newIdx) => let new = newIdx + from if new < 0 { - throw(Err("mapbind: negative index")) + throw(Util.Err("mapbind: negative index")) } Var({ idx: new, @@ -132,7 +131,7 @@ let mapbind = (term: t, f: int => int, ~from: int=0): t => mapbind0(term, idx => let upshift = (term: t, amount: int, ~from: int=0) => mapbind(term, idx => idx + amount, ~from) let downshift = (term: t, amount: int, ~from: int=1) => { if amount > from { - throw(Err("downshift amount must be less than from")) + throw(Util.Err("downshift amount must be less than from")) } mapbind(term, idx => idx - amount, ~from) } @@ -651,7 +650,7 @@ let rec parseSimple = (str: string): (simple, string) => { let (tail, rest3) = parseSimple("("->String.concat(rest2)) switch tail { | ListS({xs}) => (ListS({xs: Array.concat([head], xs)}), rest3) - | _ => throw(Unreachable("bug")) + | _ => throw(Util.Unreachable("bug")) } } } diff --git a/src/Scratch.res b/src/Scratch.res index aa89cb4..9232766 100644 --- a/src/Scratch.res +++ b/src/Scratch.res @@ -42,6 +42,12 @@ module DLREView = MethodView.CombineMethodView( module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView)) module ConfS = ConfigBlock.Make(HOTerm, HOTerm) +module StringSymbol = CombinedAtom.MakeAtomAndView( + StringA.Atom, + StringA.AtomView, + Symbolic.Atom, + Symbolic.AtomView, +) module StringSExp = SExpFunc.Make(StringSymbol.Atom) module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) diff --git a/src/StringA.res b/src/StringA.res index f94cb68..440c747 100644 --- a/src/StringA.res +++ b/src/StringA.res @@ -333,24 +333,12 @@ module Atom = { type gen = ref - let prettyPrintVar = (idx: int, scope: array) => - "$" ++ - switch scope[idx] { - | Some(n) if Array.indexOf(scope, n) == idx => n - | _ => "\\"->String.concat(String.make(idx)) - } let prettyPrint = (term: t, ~scope: array) => `"${Array.map(term, piece => { switch piece { | String(str) => str - | Var({idx}) => prettyPrintVar(idx, scope) - | Schematic({schematic, allowed}) => { - let allowedStr = - allowed - ->Array.map(idx => prettyPrintVar(idx, scope)) - ->Array.join(" ") - `?${Int.toString(schematic)}(${allowedStr})` - } + | Var({idx}) => Util.prettyPrintVar(idx, scope) + | Schematic({schematic, allowed}) => Util.prettyPrintSchematic(schematic, allowed, scope) } })->Array.join(" ")}"` diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res index b444dae..eda40f1 100644 --- a/src/StringAxiomSet.res +++ b/src/StringAxiomSet.res @@ -1,5 +1,11 @@ open Component +module StringSymbol = CombinedAtom.MakeAtomAndView( + StringA.Atom, + StringA.AtomView, + Symbolic.Atom, + Symbolic.AtomView, +) module StringSExp = SExpFunc.Make(StringSymbol.Atom) module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) @@ -38,12 +44,12 @@ let getSExpName = (t: StringSExp.t): option => let destructure = (r: StringSExp.t): (StringA.Atom.t, string) => switch r { - | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name) + | Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => (s, name) | _ => throw(Util.Unreachable("expected valid induction rule")) } let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> => switch r { - | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name)) + | Compound({subexps: [Atom(Left(s)), Atom(Right(name))]}) => Some((s, name)) | _ => None } let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({ @@ -108,7 +114,7 @@ let derive = (group: judgeGroup, mentionedGroups: array): Rule.t => vars: rule.vars, premises: rule.premises->Array.concat(inductionHyps), conclusion: structure( - surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringS->Atom, + surround(s, aIdx + baseIdx, bIdx + baseIdx)->Left->Atom, Var({idx: pIdx + baseIdx}), ), } @@ -120,13 +126,13 @@ let derive = (group: judgeGroup, mentionedGroups: array): Rule.t => { Rule.vars: [], premises: [], - conclusion: structure(Var({idx: xIdx}), Atom(ConstS(group.name))), + conclusion: structure(Var({idx: xIdx}), Atom(Right(group.name))), }, ], mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))), ), conclusion: structure( - surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom, + surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->Left->Atom, Var({idx: 0}), ), // TODO: clean here } @@ -165,7 +171,7 @@ let deserialise = (str: string, ~imports as _: Ports.t) => { let grouped: dict> = Dict.make() raw->Dict.forEach(rule => switch rule.conclusion { - | Compound({subexps: [Atom(StringS(_)), Atom(ConstS(name))]}) => + | Compound({subexps: [Atom(Left(_)), Atom(Right(name))]}) => switch grouped->Dict.get(name) { | None => grouped->Dict.set(name, [rule]) | Some(rs) => rs->Array.push(rule) diff --git a/src/StringSymbol.res b/src/StringSymbol.res deleted file mode 100644 index 6b08653..0000000 --- a/src/StringSymbol.res +++ /dev/null @@ -1,81 +0,0 @@ -type t = StringS(StringA.Atom.t) | ConstS(string) - -module Atom: SExpFunc.ATOM with type t = t = { - type t = t - type subst = Map.t - type gen = ref - let parse = (s, ~scope, ~gen: option=?) => { - StringA.Atom.parse(s, ~scope, ~gen?) - ->Result.map(((r, rest)) => (StringS(r), rest)) - ->Util.Result.or(() => - Symbolic.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest)) - ) - } - let prettyPrint = (s, ~scope) => - switch s { - | StringS(s) => StringA.Atom.prettyPrint(s, ~scope) - | ConstS(s) => Symbolic.Atom.prettyPrint(s, ~scope) - } - let unify = (s1, s2, ~gen=?) => - switch (s1, s2) { - | (StringS(s1), StringS(s2)) => - StringA.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v))) - | (ConstS(s1), ConstS(s2)) => - Symbolic.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v))) - | (_, _) => Seq.empty - } - let substitute = (s, subst: subst) => - switch s { - | StringS(s) => { - let stringSubs = - subst - ->Map.entries - ->Iterator.toArrayWithMapper(((i, v)) => - switch v { - | StringS(s) => Some((i, s)) - | _ => None - } - ) - ->Array.keepSome - ->Map.fromArray - StringS(StringA.Atom.substitute(s, stringSubs)) - } - | ConstS(s) => ConstS(s) - } - let upshift = (s, amount: int, ~from=?) => - switch s { - | StringS(s) => StringS(s->StringA.Atom.upshift(amount, ~from?)) - | ConstS(s) => ConstS(s) - } - let lowerVar = idx => Some(StringS([StringA.Var({idx: idx})])) - let lowerSchematic = (schematic, allowed) => Some( - StringS([StringA.Schematic({schematic, allowed})]), - ) - let substDeBruijn = (s, substs: array>, ~from=?) => - switch s { - | StringS(s) => { - let stringSubs = substs->Array.map(s => - switch s { - | Some(StringS(s)) => Some(s) - | _ => None - } - ) - StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?)) - } - | ConstS(s) => ConstS(s) - } - let concrete = s => - switch s { - | StringS(s) => StringA.Atom.concrete(s) - | ConstS(_) => false - } -} - -module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom = { - type props = {name: Atom.t, scope: array} - let make = ({name, scope}: props) => - switch name { - | StringS(name) => - | ConstS(name) => - } -} diff --git a/src/StringSymbol.resi b/src/StringSymbol.resi deleted file mode 100644 index 6a1fbf0..0000000 --- a/src/StringSymbol.resi +++ /dev/null @@ -1,3 +0,0 @@ -type t = StringS(StringA.Atom.t) | ConstS(string) -module Atom: SExpFunc.ATOM with type t = t -module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom diff --git a/src/Util.res b/src/Util.res index 4a74652..30daf04 100644 --- a/src/Util.res +++ b/src/Util.res @@ -34,6 +34,20 @@ let prettyPrintIntMap = (m: Belt.Map.Int.t<'v>, ~showV: 'v => string=toString) = ->showArray } +let prettyPrintVar = (idx: int, scope: array) => + "$" ++ + switch scope[idx] { + | Some(n) if Array.indexOf(scope, n) == idx => n + | _ => "\\"->String.concat(String.make(idx)) + } +let prettyPrintSchematic = (schematic: int, allowed: array, scope: array) => { + let allowedStr = + allowed + ->Array.map(idx => prettyPrintVar(idx, scope)) + ->Array.join(" ") + `?${Int.toString(schematic)}(${allowedStr})` +} + let mapIntersectionWith = (m1: Map.t<'k, 'a>, m2: Map.t<'k, 'b>, f: ('a, 'b) => 'c) => { let go = (m1, m2) => { let nu: Map.t<'k, 'c> = Map.make() @@ -86,6 +100,16 @@ let mapEqual = (m1, m2) => { ->Array.length == Map.size(m2) } +module Map = { + type t<'k, 'v> = Map.t<'k, 'v> + let filterMap = (m: t<'k, 'v1>, f: ('k, 'v1) => option<'v2>): t<'k, 'v2> => + m + ->Map.entries + ->Iterator.toArrayWithMapper(((i, v)) => f(i, v)->Option.map(v => (i, v))) + ->Array.keepSome + ->Map.fromArray +} + let arrayWithIndex = (arr: array) => { React.array(arr->Array.mapWithIndex((m, i) => m )) } -- 2.51.2