diff --git a/src/SExpFunc.res b/src/SExpFunc.res index a4d7e56..86fa858 100644 --- a/src/SExpFunc.res +++ b/src/SExpFunc.res @@ -1,3 +1,5 @@ +exception SubstNotCompatible(string) + module type ATOM = { type t type subst = Map.t @@ -9,7 +11,7 @@ module type ATOM = { // used for when trying to substitute a variable of the wrong type let lowerVar: int => option let lowerSchematic: (int, array) => option - let substDeBruijn: (t, Map.t, ~from: int=?, ~to: int) => t + let substDeBruijn: (t, array>, ~from: int=?) => t let concrete: t => bool } @@ -160,15 +162,7 @@ module Make = (Atom: ATOM): { } let rec substDeBruijn = (term: t, substs: array, ~from: int=0) => switch term { - | Atom(s) => { - let symbolSubsts = - substs - ->Array.mapWithIndex((t, i) => lower(t)->Option.map(a => (i, a))) - ->Array.keepSome - ->Map.fromArray - - Atom(Atom.substDeBruijn(s, symbolSubsts, ~from, ~to=Array.length(substs))) - } + | Atom(s) => Atom(Atom.substDeBruijn(s, Array.map(substs, lower), ~from)) | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))}) diff --git a/src/StringA.res b/src/StringA.res index 7c74f95..f94cb68 100644 --- a/src/StringA.res +++ b/src/StringA.res @@ -270,7 +270,8 @@ module Atom = { } // law: unify(a,b) == [{}] iff equivalent(a,b) - let substDeBruijn = (string: t, substs: Map.t, ~from: int=0, ~to: int) => { + let substDeBruijn = (string: t, substs: array>, ~from: int=0) => { + let to = Array.length(substs) Array.flatMap(string, piece => switch piece { | String(_) => [piece] @@ -278,7 +279,13 @@ module Atom = { if var < from { [piece] } else if var - from < to { - Map.get(substs, var - from)->Option.getOr([piece]) + switch Option.getUnsafe(substs[var - from]) { + | Some(v) => v + | None => + throw( + SExpFunc.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`), + ) + } } else { [Var({idx: var - to})] } diff --git a/src/StringSymbol.res b/src/StringSymbol.res index 1c30166..6b08653 100644 --- a/src/StringSymbol.res +++ b/src/StringSymbol.res @@ -51,21 +51,16 @@ module Atom: SExpFunc.ATOM with type t = t = { let lowerSchematic = (schematic, allowed) => Some( StringS([StringA.Schematic({schematic, allowed})]), ) - let substDeBruijn = (s, substs: Map.t, ~from=?, ~to: int) => + let substDeBruijn = (s, substs: array>, ~from=?) => switch s { | StringS(s) => { - let stringSubs = - substs - ->Map.entries - ->Iterator.toArrayWithMapper(((i, v)) => - switch v { - | StringS(s) => Some((i, s)) - | _ => None - } - ) - ->Array.keepSome - ->Map.fromArray - StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?, ~to)) + 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) } diff --git a/src/Symbolic.res b/src/Symbolic.res index 4bde6a9..7ffba16 100644 --- a/src/Symbolic.res +++ b/src/Symbolic.res @@ -18,7 +18,7 @@ module Atom = { let substitute = (name, _) => name let lowerVar = _ => None let lowerSchematic = (_, _) => None - let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name + let substDeBruijn = (name, _, ~from as _=?) => name let concrete = _ => false let upshift = (t, _, ~from as _=?) => t } -- 2.51.2 From e9d084ce3f90874de1d158a968cba80a86ff7465 Mon Sep 17 00:00:00 2001 From: Josh Brown Date: Sat, 21 Mar 2026 11:05:04 +1100 Subject: [PATCH 2/3] add checks for substitution failure --- src/SExpFunc.res | 12 ++++++++++-- src/Theorem.res | 24 ++++++++++++++++++++---- 2 files changed, 30 insertions(+), 6 deletions(-) diff --git a/src/SExpFunc.res b/src/SExpFunc.res index 86fa858..6672150 100644 --- a/src/SExpFunc.res +++ b/src/SExpFunc.res @@ -144,9 +144,17 @@ module Make = (Atom: ATOM): { unifyTerm(x, y)->Seq.flatMap(s1 => a ->Array.sliceToEnd(~start=1) - ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1))) + ->Array.filterMap(((t1, t2)) => + try {Some((substitute(t1, s1), substitute(t2, s1)))} catch { + | SubstNotCompatible(_) => None + } + ) ->unifyArray - ->Seq.map(s2 => combineSubst(s1, s2)) + ->Seq.filterMap(s2 => + try {Some(combineSubst(s1, s2))} catch { + | SubstNotCompatible(_) => None + } + ) ) } } diff --git a/src/Theorem.res b/src/Theorem.res index 950f3c2..12d3074 100644 --- a/src/Theorem.res +++ b/src/Theorem.res @@ -14,7 +14,13 @@ module Make = ( open RuleView module RuleView = RuleView.Make(Term, Judgment, JudgmentView) module Ports = Ports(Term, Judgment) - type state = {name: string, rule: Rule.t, proof: Proof.t, gen: Term.gen} + type state = { + name: string, + rule: Rule.t, + proof: Proof.t, + gen: Term.gen, + substFailed: option, + } type props = { content: state, imports: Ports.t, @@ -39,7 +45,7 @@ module Make = ( Error("Trailing input: "->String.concat(s')) | Ok((proof, _)) => Ok(( - {name, rule, proof, gen}, + {name, rule, proof, gen, substFailed: None}, {Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None}, )) } @@ -51,15 +57,21 @@ module Make = ( let checked = Proof.check(ctx, props.content.proof, props.content.rule) let sidebarRef = React.useRef(Nullable.null) let proofChanged = (proof, subst) => { + let proof = Proof.uncheck(proof)->Proof.substitute(subst) props.onChange( - {...props.content, proof: Proof.uncheck(proof)->Proof.substitute(subst)}, + try { + Proof.check(ctx, proof, props.content.rule)->ignore + {...props.content, proof, substFailed: None} + } catch { + | SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)} + }, ~exports={ Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]), ruleStyle: None, }, ) } - +

{React.string("Theorem")}

@@ -69,6 +81,10 @@ module Make = ( + {switch props.content.substFailed { + | Some(msg) => React.string(msg) + | None => React.null + }}
} -- 2.51.2 From 5ab6ecc75a7b3a31ade479a7170205d241566c7f Mon Sep 17 00:00:00 2001 From: Josh Brown Date: Sat, 21 Mar 2026 11:53:14 +1100 Subject: [PATCH 3/3] add example showing type coercion failure --- index.html | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/index.html b/index.html index b7ae8f3..eae7148 100644 --- a/index.html +++ b/index.html @@ -657,6 +657,27 @@ |- ? + + a. + -------------- eq-refl + (Eq a a) + + a. b. (Eq a b) + -------------- eq-sym + (Eq b a) + + a. b. c. (Eq a b) (Eq "$b" c) + -------------- eq-trans-weird + (Eq a c) + + -------------- eq-a-comp + (Eq "a" (Foo Bar)) + + + ------------- eq-a-c + (Eq "a" "a") + |- ? +