diff --git a/src/SExp.res b/src/SExp.res index 6c5b408..b9e635d 100644 --- a/src/SExp.res +++ b/src/SExp.res @@ -1,7 +1,7 @@ module SymbolAtom: SExpFunc.ATOM with type t = string = { type t = string type subst = Map.t - let unify = (a, b) => + let unify = (a, b, ~gen as _=?) => if a == b { Seq.once(Map.make()) } else { @@ -18,7 +18,7 @@ module SymbolAtom: SExpFunc.ATOM with type t = string = { let lowerVar = _ => "" let lowerSchematic = (_, _) => "" let ghost = "" - let substDeBruijn = (name, _, ~from as _) => name + let substDeBruijn = (name, _, ~from as _=?) => name let unifiesWithAnything = _ => false let upshift = (t, _, ~from as _=?) => t } diff --git a/src/SExpFunc.res b/src/SExpFunc.res index 4306038..b830ee9 100644 --- a/src/SExpFunc.res +++ b/src/SExpFunc.res @@ -1,7 +1,7 @@ module type ATOM = { type t type subst = Map.t - let unify: (t, t) => Seq.t + let unify: (t, t, ~gen: ref=?) => Seq.t let prettyPrint: (t, ~scope: array) => string let parse: (string, ~scope: array, ~gen: ref=?) => result<(t, string), string> let substitute: (t, subst) => t @@ -10,7 +10,7 @@ module type ATOM = { let lowerVar: int => t let lowerSchematic: (int, array) => t let ghost: t - let substDeBruijn: (t, array, ~from: int) => t + let substDeBruijn: (t, array, ~from: int=?) => t let unifiesWithAnything: t => bool } diff --git a/src/Scratch.res b/src/Scratch.res index 14fb231..26e7628 100644 --- a/src/Scratch.res +++ b/src/Scratch.res @@ -47,7 +47,7 @@ module DerivationsOrLemmasStrView = MethodView.CombineMethodView( StringSExp, StringSExp, MethodView.DerivationView(StringSExp, StringSExp), - MethodView.LemmaView(StringSExp, StringSExp, StringTermJView), + MethodView.LemmaView(StringSExp, StringSExp, StringSExpJView), ) module DLEStrView = MethodView.CombineMethodView( StringSExp, @@ -56,5 +56,5 @@ module DLEStrView = MethodView.CombineMethodView( MethodView.EliminationView(StringSExp, StringSExp), ) module TheoremStr = Editable.TextArea( - Theorem.Make(StringSExp, StringSExp, StringTermJView, DLEStrView), + Theorem.Make(StringSExp, StringSExp, StringSExpJView, DLEStrView), ) diff --git a/src/StringTerm.res b/src/StringAtom.res similarity index 99% rename from src/StringTerm.res rename to src/StringAtom.res index ea0b556..de927d5 100644 --- a/src/StringTerm.res +++ b/src/StringAtom.res @@ -503,7 +503,9 @@ let parse: (string, ~scope: array, ~gen: gen=?) => result<(t, remaining), acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents))) } -let ghostTerm = [Ghost] +let lowerSchematic = (schematic, allowed) => [Schematic({schematic, allowed})] +let lowerVar = idx => [Var({idx: idx})] +let ghost = [Ghost] let unifiesWithAnything = t => t->Array.every(p => switch p { diff --git a/src/StringTerm.resi b/src/StringAtom.resi similarity index 56% rename from src/StringTerm.resi rename to src/StringAtom.resi index ee52d77..1cd30ef 100644 --- a/src/StringTerm.resi +++ b/src/StringAtom.resi @@ -7,9 +7,4 @@ type t = array type subst = Map.t type gen = ref -include Signatures.TERM - with type t := t - and type meta = string - and type schematic = int - and type subst := subst - and type gen := gen +include SExpFunc.ATOM with type t := t and type subst := subst diff --git a/src/StringTermView.res b/src/StringAtomView.res similarity index 92% rename from src/StringTermView.res rename to src/StringAtomView.res index e6da02f..9db9cec 100644 --- a/src/StringTermView.res +++ b/src/StringAtomView.res @@ -1,4 +1,4 @@ -type props = {term: StringTerm.t, scope: array} +type props = {name: StringAtom.t, scope: array} type idx_props = {idx: int, scope: array} let viewVar = (props: idx_props) => switch props.scope[props.idx] { @@ -28,7 +28,7 @@ let intersperse = a => Util.intersperse(a, ~with=React.string(" ")) module Piece = { @react.component - let make = (~piece: StringTerm.piece, ~scope) => + let make = (~piece: StringAtom.piece, ~scope) => switch piece { | Var({idx}) => viewVar({idx, scope}) | String(s) => {React.string(s)} @@ -51,10 +51,10 @@ module Piece = { } @react.componentWithProps -let make = ({term, scope}) => +let make = ({name, scope}) => {React.string("\"")} - {term + {name ->Array.mapWithIndex((piece, i) => { let key = Int.toString(i) diff --git a/src/StringAtomView.resi b/src/StringAtomView.resi new file mode 100644 index 0000000..63adb11 --- /dev/null +++ b/src/StringAtomView.resi @@ -0,0 +1 @@ +include SExpViewFunc.ATOM_VIEW with module Atom := StringAtom diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res index b890e26..4ac8c7d 100644 --- a/src/StringAxiomSet.res +++ b/src/StringAxiomSet.res @@ -2,7 +2,7 @@ open Component module Term = StringSExp module Judgment = StringSExp -module JudgmentView = StringTermJView +module JudgmentView = StringSExpJView module Rule = Rule.Make(Term, Judgment) module RuleView = RuleView.Make(Term, Judgment, JudgmentView) @@ -38,12 +38,12 @@ let getSExpName = (t: SExp.t): option => } open StringSExp -let destructure = (r: Judgment.t): (StringTerm.t, string) => +let destructure = (r: Judgment.t): (StringAtom.t, string) => switch r { | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name) | _ => throw(Util.Unreachable("expected valid induction rule")) } -let destructureOpt = (r: Judgment.t): option<(StringTerm.t, string)> => +let destructureOpt = (r: Judgment.t): option<(StringAtom.t, string)> => switch r { | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name)) | _ => None @@ -88,8 +88,8 @@ let derive = (group: judgeGroup, mentionedGroups: array): Rule.t => let xIdx = vars->Array.findIndex(i => i == x) let aIdx = vars->Array.findIndex(i => i == a) let bIdx = vars->Array.findIndex(i => i == b) - let surround = (t: StringTerm.t, aIdx: int, bIdx: int) => { - Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})]) + let surround = (t: StringAtom.t, aIdx: int, bIdx: int) => { + Array.concat(Array.concat([StringAtom.Var({idx: aIdx})], t), [StringAtom.Var({idx: bIdx})]) } let lookupGroup = (name: string): option => mentionedGroups->Array.findIndexOpt(g => name == g.name) @@ -128,7 +128,7 @@ let derive = (group: judgeGroup, mentionedGroups: array): Rule.t => mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))), ), conclusion: structure( - surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom, + surround([StringAtom.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom, Var({idx: 0}), ), // TODO: clean here } diff --git a/src/StringSExp.res b/src/StringSExp.res index 7e1505a..2bd828d 100644 --- a/src/StringSExp.res +++ b/src/StringSExp.res @@ -1,11 +1,11 @@ -type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t) +type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t) -module StringAtom: SExpFunc.ATOM with type t = stringAtom = { - type t = stringAtom +module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom = { + type t = stringSExpAtom type subst = Map.t type gen = ref let parse = (s, ~scope, ~gen: option=?) => { - StringTerm.parse(s, ~scope, ~gen?) + StringAtom.parse(s, ~scope, ~gen?) ->Result.map(((r, rest)) => (StringS(r), rest)) ->Util.Result.or(() => SExp.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest)) @@ -13,15 +13,15 @@ module StringAtom: SExpFunc.ATOM with type t = stringAtom = { } let prettyPrint = (s, ~scope) => switch s { - | StringS(s) => StringTerm.prettyPrint(s, ~scope) + | StringS(s) => StringAtom.prettyPrint(s, ~scope) | ConstS(s) => SExp.Atom.prettyPrint(s, ~scope) } - let unify = (s1, s2) => + let unify = (s1, s2, ~gen=?) => switch (s1, s2) { | (StringS(s1), StringS(s2)) => - StringTerm.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v))) + StringAtom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v))) | (ConstS(s1), ConstS(s2)) => - SExp.Atom.unify(s1, s2)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v))) + SExp.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v))) | (_, _) => Seq.empty } let substitute = (s, subst: subst) => @@ -30,39 +30,39 @@ module StringAtom: SExpFunc.ATOM with type t = stringAtom = { let stringSubs = subst->Util.mapMapValues(v => switch v { | StringS(s) => s - | _ => [StringTerm.Ghost] + | _ => [StringAtom.Ghost] } ) - StringS(StringTerm.substitute(s, stringSubs)) + StringS(StringAtom.substitute(s, stringSubs)) } | ConstS(s) => ConstS(s) } let upshift = (s, amount: int, ~from=?) => switch s { - | StringS(s) => StringS(s->StringTerm.upshift(amount, ~from?)) + | StringS(s) => StringS(s->StringAtom.upshift(amount, ~from?)) | ConstS(s) => ConstS(s) } - let lowerVar = idx => StringS([StringTerm.Var({idx: idx})]) - let lowerSchematic = (schematic, allowed) => StringS([StringTerm.Schematic({schematic, allowed})]) - let ghost = StringS([StringTerm.Ghost]) - let substDeBruijn = (s, substs: array, ~from) => + let lowerVar = idx => StringS([StringAtom.Var({idx: idx})]) + let lowerSchematic = (schematic, allowed) => StringS([StringAtom.Schematic({schematic, allowed})]) + let ghost = StringS([StringAtom.Ghost]) + let substDeBruijn = (s, substs: array, ~from=?) => switch s { | StringS(s) => { let stringSubs = substs->Array.map(v => switch v { | StringS(s) => s - | _ => [StringTerm.String("AYAYAYSLKDJFLSKDJ")] + | _ => [StringAtom.String("AYAYAYSLKDJFLSKDJ")] } ) - StringS(StringTerm.substDeBruijn(s, stringSubs, ~from)) + StringS(StringAtom.substDeBruijn(s, stringSubs, ~from?)) } | ConstS(s) => ConstS(s) } let unifiesWithAnything = s => switch s { - | StringS(s) => StringTerm.unifiesWithAnything(s) + | StringS(s) => StringAtom.unifiesWithAnything(s) | ConstS(_) => false } } -include SExpFunc.Make(StringAtom) +include SExpFunc.Make(StringSExpAtom) diff --git a/src/StringSExp.resi b/src/StringSExp.resi index d9cb741..dbc8a49 100644 --- a/src/StringSExp.resi +++ b/src/StringSExp.resi @@ -1,8 +1,8 @@ -type stringAtom = StringS(StringTerm.t) | ConstS(SExp.Atom.t) -module StringAtom: SExpFunc.ATOM with type t = stringAtom +type stringSExpAtom = StringS(StringAtom.t) | ConstS(SExp.Atom.t) +module StringSExpAtom: SExpFunc.ATOM with type t = stringSExpAtom type rec t = - | Atom(StringAtom.t) + | Atom(StringSExpAtom.t) | Compound({subexps: array}) | Var({idx: int}) | Schematic({schematic: int, allowed: array}) @@ -14,5 +14,5 @@ include Signatures.TERM and type schematic = int and type subst = Map.t -module Atom: SExpFunc.ATOM with type t := StringAtom.t +module Atom: SExpFunc.ATOM with type t := StringSExpAtom.t let mapTerms: (t, t => t) => t diff --git a/src/StringTermJView.res b/src/StringSExpJView.res similarity index 58% rename from src/StringTermJView.res rename to src/StringSExpJView.res index 46c606b..d99cd7b 100644 --- a/src/StringTermJView.res +++ b/src/StringSExpJView.res @@ -1,13 +1,13 @@ -module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringAtom = { - type props = {name: StringSExp.StringAtom.t, scope: array} +module StringAtomView: SExpViewFunc.ATOM_VIEW with module Atom := StringSExp.StringSExpAtom = { + type props = {name: StringSExp.StringSExpAtom.t, scope: array} let make = ({name, scope}: props) => switch name { - | StringSExp.StringS(term) => + | StringSExp.StringS(name) => | StringSExp.ConstS(name) => } } -module View = SExpViewFunc.Make(StringSExp.StringAtom, StringAtomView, StringSExp) +module View = SExpViewFunc.Make(StringSExp.StringSExpAtom, StringAtomView, StringSExp) module TermView = View type props = { diff --git a/src/StringTermJView.resi b/src/StringSExpJView.resi similarity index 100% rename from src/StringTermJView.resi rename to src/StringSExpJView.resi diff --git a/src/StringTermView.resi b/src/StringTermView.resi deleted file mode 100644 index cfae887..0000000 --- a/src/StringTermView.resi +++ /dev/null @@ -1 +0,0 @@ -include Signatures.TERM_VIEW with module Term := StringTerm diff --git a/tests/RuleTest.res b/tests/RuleTest.res index 28c5364..c267428 100644 --- a/tests/RuleTest.res +++ b/tests/RuleTest.res @@ -42,14 +42,14 @@ module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { // vars: [], // premises: [], // conclusion: StringSExp.Compound( -// [StringTerm.Var({idx: 0})], -// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom, +// [StringAtom.Var({idx: 0})], +// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom, // ), // }, // ], // conclusion: ( -// [StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")], -// SExp.pAtom("p")->StringTermJudgment.ConstS->StringSExp.Atom, +// [StringAtom.String("("), StringAtom.Var({idx: 0}), StringAtom.String(")")], +// SExp.pAtom("p")->StringAtomJudgment.ConstS->StringSExp.Atom, // ), // }, // ) diff --git a/tests/StringTermTest.res b/tests/StringTermTest.res index 3294e65..75ff107 100644 --- a/tests/StringTermTest.res +++ b/tests/StringTermTest.res @@ -1,35 +1,38 @@ open Zora -open StringTerm -module Util = TestUtil.MakeTerm(StringTerm) +module Util = TestUtil.MakeAtomTester(StringAtom) +module ParseUtil = Util.ParseTester zoraBlock("parse", t => { - t->block("empty", t => t->Util.testParse(`""`, [])) + t->block("empty", t => t->ParseUtil.testParse(`""`, [])) t->block("string literal", t => { - t->Util.testParse(`"x"`, [String("x")]) - t->Util.testParse(`"xyz123"`, [String("xyz123")]) - t->Util.testParse(`"123y"`, [String("123"), String("y")]) - t->Util.testParse(`"\\"\\$\\?\\\\"`, [String("\""), String("$"), String("?"), String("\\")]) - t->Util.testParse( + t->ParseUtil.testParse(`"x"`, [String("x")]) + t->ParseUtil.testParse(`"xyz123"`, [String("xyz123")]) + t->ParseUtil.testParse(`"123y"`, [String("123"), String("y")]) + t->ParseUtil.testParse( + `"\\"\\$\\?\\\\"`, + [String("\""), String("$"), String("?"), String("\\")], + ) + t->ParseUtil.testParse( `"y(135ab!!)"`, [String("y"), String("("), String("135"), String("ab"), String("!!"), String(")")], ) - t->Util.testParseFail(`foo`) - t->Util.testParseFail(`a b" c`) + t->ParseUtil.testParseFail(`foo`) + t->ParseUtil.testParseFail(`a b" c`) }) t->block("variables", t => { - t->Util.testParse(`"$\\1"`, [Var({idx: 1})]) - t->Util.testParse(`"$\\10"`, [Var({idx: 10})]) - t->Util.testParse(`"$x"`, ~scope=["x"], [Var({idx: 0})]) - t->Util.testParse(`"?1()"`, [Schematic({schematic: 1, allowed: []})]) - t->Util.testParseFail(`"?1"`) - t->Util.testParse(`"?10()"`, [Schematic({schematic: 10, allowed: []})]) - t->Util.testParse(`"?1(1 23 4)"`, [Schematic({schematic: 1, allowed: [1, 23, 4]})]) + t->ParseUtil.testParse(`"$\\1"`, [Var({idx: 1})]) + t->ParseUtil.testParse(`"$\\10"`, [Var({idx: 10})]) + t->ParseUtil.testParse(`"$x"`, ~scope=["x"], [Var({idx: 0})]) + t->ParseUtil.testParse(`"?1()"`, [Schematic({schematic: 1, allowed: []})]) + t->ParseUtil.testParseFail(`"?1"`) + t->ParseUtil.testParse(`"?10()"`, [Schematic({schematic: 10, allowed: []})]) + t->ParseUtil.testParse(`"?1(1 23 4)"`, [Schematic({schematic: 1, allowed: [1, 23, 4]})]) }) t->block("concat", t => { - t->Util.testParse(`"x y"`, [String("x"), String("y")]) - t->Util.testParse(`"x y"`, [String("x"), String("y")]) - t->Util.testParse( + t->ParseUtil.testParse(`"x y"`, [String("x"), String("y")]) + t->ParseUtil.testParse(`"x y"`, [String("x"), String("y")]) + t->ParseUtil.testParse( `"x ?1(1 2 3) $\\1 $y"`, ~scope=["y"], [String("x"), Schematic({schematic: 1, allowed: [1, 2, 3]}), Var({idx: 1}), Var({idx: 0})], @@ -38,7 +41,9 @@ zoraBlock("parse", t => { }) let parse = (input: string) => - StringTerm.parse(input, ~scope=[], ~gen=StringTerm.makeGen())->Result.getExn->Pair.first + StringAtom.parse(input, ~scope=[], ~gen=Util.ParseWrapper.makeGen())->Result.getExn->Pair.first + +module UnifyUtil = Util.UnifyTester zoraBlock("unify", t => { let a = parse(`"a"`) @@ -46,19 +51,19 @@ zoraBlock("unify", t => { let x = parse(`"?1()"`) let y = parse(`"?2()"`) t->block("ghost", t => { - t->Util.testUnifyFail(a, StringTerm.ghostTerm) - t->Util.testUnify(x, StringTerm.ghostTerm) - t->Util.testUnify([x, y, x]->Array.flat, StringTerm.ghostTerm) + t->UnifyUtil.testUnifyFail(a, StringAtom.ghost) + t->UnifyUtil.testUnify(x, StringAtom.ghost) + t->UnifyUtil.testUnify([x, y, x]->Array.flat, StringAtom.ghost) }) t->block("schematics on at most one side", t => { - t->Util.testUnify(a, a, ~expect=[Map.make()]) - t->Util.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])]) - t->Util.testUnify(a, x, ~expect=[Map.fromArray([(1, a)])]) + t->UnifyUtil.testUnify(a, a, ~expect=[Map.make()]) + t->UnifyUtil.testUnify(x, a, ~expect=[Map.fromArray([(1, a)])]) + t->UnifyUtil.testUnify(a, x, ~expect=[Map.fromArray([(1, a)])]) let xy = parse(`"?1() ?2()"`) let ab = parse(`"a b"`) - t->Util.testUnify(x, ab, ~expect=[Map.fromArray([(1, ab)])]) - t->Util.testUnify( + t->UnifyUtil.testUnify(x, ab, ~expect=[Map.fromArray([(1, ab)])]) + t->UnifyUtil.testUnify( xy, ab, ~expect=[ @@ -68,30 +73,34 @@ zoraBlock("unify", t => { ], ) - t->Util.testUnify(parse(`"?1() b ?2()"`), ab, ~expect=[Map.fromArray([(1, a), (2, [])])]) - t->Util.testUnify( + t->UnifyUtil.testUnify(parse(`"?1() b ?2()"`), ab, ~expect=[Map.fromArray([(1, a), (2, [])])]) + t->UnifyUtil.testUnify( parse(`"?1() ?2() b"`), ab, ~expect=[Map.fromArray([(1, []), (2, a)]), Map.fromArray([(1, a), (2, [])])], ) - t->Util.testUnify( + t->UnifyUtil.testUnify( parse(`"a ?1() ?2()"`), ab, ~expect=[Map.fromArray([(1, []), (2, b)]), Map.fromArray([(1, b), (2, [])])], ) let xax = parse(`"?1() a ?1()"`) - t->Util.testUnify(xax, parse(`"a"`), ~expect=[Map.fromArray([(1, [])])]) - t->Util.testUnify(xax, parse(`"a a a"`), ~expect=[Map.fromArray([(1, a)])]) - t->Util.testUnify(xax, parse(`"a b a a b"`), ~expect=[Map.fromArray([(1, parse(`"a b"`))])]) + t->UnifyUtil.testUnify(xax, parse(`"a"`), ~expect=[Map.fromArray([(1, [])])]) + t->UnifyUtil.testUnify(xax, parse(`"a a a"`), ~expect=[Map.fromArray([(1, a)])]) + t->UnifyUtil.testUnify( + xax, + parse(`"a b a a b"`), + ~expect=[Map.fromArray([(1, parse(`"a b"`))])], + ) }) t->block("schematics appearing at most twice", t => { - t->Util.testUnify(x, x, ~expect=[Map.fromArray([(1, [])])]) - t->Util.testUnify(x, y, ~expect=[Map.fromArray([(1, []), (2, [])])]) + t->UnifyUtil.testUnify(x, x, ~expect=[Map.fromArray([(1, [])])]) + t->UnifyUtil.testUnify(x, y, ~expect=[Map.fromArray([(1, []), (2, [])])]) - t->Util.testUnify(a, parse(`"?1() a"`), ~expect=[Map.fromArray([(1, [])])]) - t->Util.testUnify( + t->UnifyUtil.testUnify(a, parse(`"?1() a"`), ~expect=[Map.fromArray([(1, [])])]) + t->UnifyUtil.testUnify( parse(`"?1() a"`), parse(`"a ?1()"`), ~expect=[ @@ -102,22 +111,22 @@ zoraBlock("unify", t => { Map.fromArray([(1, parse(`"a a a a"`))]), ], ) - t->Util.testUnify( + t->UnifyUtil.testUnify( parse(`"a ?1()"`), parse(`"?2() b`), ~expect=[Map.fromArray([(1, b), (2, a)])], ) - t->Util.testUnify( + t->UnifyUtil.testUnify( parse(`"a ?1() a"`), parse(`"?2() b a"`), ~expect=[Map.fromArray([(1, b), (2, a)])], ) - t->Util.testUnify( + t->UnifyUtil.testUnify( parse(`"b ?1() a"`), parse(`"?2() a ?1()"`), ~expect=[Map.fromArray([(1, a), (2, b)]), Map.fromArray([(1, []), (2, b)])], ) - t->Util.testUnify( + t->UnifyUtil.testUnify( parse(`"a b ?1() c ?2()"`), parse(`"?2() c ?1() b a"`), ~expect=[Map.fromArray([(1, a), (2, parse(`"a b a"`))])], diff --git a/tests/TestUtil.res b/tests/TestUtil.res index 75858fb..3e4f3e5 100644 --- a/tests/TestUtil.res +++ b/tests/TestUtil.res @@ -3,6 +3,154 @@ open Zora let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn +module type CAN_PARSE = { + type t + type meta + type gen + let parse: (string, ~scope: array, ~gen: gen=?) => result<(t, string), string> + let prettyPrint: (t, ~scope: array) => string + let makeGen: unit => gen +} + +module MakeParseTester = (Subj: CAN_PARSE) => { + let testParse = ( + t: Zora.t, + input: string, + expect: Subj.t, + ~scope=[], + ~msg=?, + ~expectRemaining=?, + ) => { + let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen()) + switch res { + | Ok((parsed, parsedRemaining)) => { + t->equal( + parsedRemaining, + expectRemaining->Option.getOr(""), + ~msg=input ++ " input consumed", + ) + // NOTE: we're checking for equality here, not equivalency + // error messages are better this way + t->equal(parsed, expect, ~msg?) + } + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) + } + } + let testParseFail = (t: Zora.t, input: string, ~scope=[]) => { + let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen()) + switch res { + | Ok((p, remaining)) => + t->fail( + ~msg=`parse intended to fail, but succeeded: ${Subj.prettyPrint( + p, + ~scope, + )}\nremaining: ${remaining}`, + ) + | Error(_) => t->ok(true) + } + } + let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => { + let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen()) + + switch res { + | Ok(res) => { + let result = Subj.prettyPrint(res->Pair.first, ~scope) + t->equal(result, expected, ~msg="prettyPrint output matches expected") + } + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) + } + } + let parse = (t: Zora.t, input: string): Subj.t => { + let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen()) + switch res { + | Ok((term, "")) => term + | Ok((_, rest)) => { + t->fail(~msg="parse incomplete: " ++ rest) + throw(Util.Unreachable("")) + } + | Error(msg) => { + t->fail(~msg="parse failed: " ++ msg) + throw(Util.Unreachable("")) + } + } + } +} + +module type CAN_UNIFY = { + type t + type subst + type gen + type meta + let unify: (t, t, ~gen: gen=?) => Seq.t + let substEqual: (subst, subst) => bool + let prettyPrintSubst: (subst, ~scope: array) => string +} + +module MakeUnifyTester = (Subj: CAN_UNIFY) => { + let testUnify = ( + t: Zora.t, + t1: Subj.t, + t2: Subj.t, + ~expect: option>=?, + ~msg=?, + ) => { + let res = Subj.unify(t1, t2)->Seq.take(10) + switch expect { + | Some(expect) => { + let expect = Seq.fromArray(expect) + let noMatches = + expect + ->Seq.filter(sub1 => Seq.find(res, sub2 => Subj.substEqual(sub1, sub2))->Option.isNone) + ->Seq.map(t => Subj.prettyPrintSubst(t, ~scope=[])) + ->Seq.toArray + let msg = + msg->Option.getOr("each substitution in `expect` should have a match in solutions") + t->equal(noMatches, [], ~msg) + } + | None => { + let msg = msg->Option.getOr("expect non-nil substitution sequence") + t->ok(res->Seq.head->Option.isSome, ~msg) + } + } + } + + let testUnifyFail = (t: Zora.t, a: Subj.t, b: Subj.t, ~msg=?) => { + let res = Subj.unify(a, b) + if res->Seq.length != 0 { + t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) + } else { + t->ok(true, ~msg=msg->Option.getOr("unification failed")) + } + } +} + +module MakeAtomTester = (Atom: SExpFunc.ATOM) => { + module ParseWrapper: CAN_PARSE + with type t = Atom.t + and type meta = string + and type gen = ref = { + include Atom + type gen = ref + type meta = string + let makeGen = () => ref(0) + } + module ParseTester = MakeParseTester(ParseWrapper) + module UnifyWrapper: CAN_UNIFY + with type t = Atom.t + and type meta = string + and type gen = ref + and type subst = Atom.subst = { + include Atom + type meta = string + type gen = ref + let prettyPrintSubst = (sub, ~scope) => + Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) + let substEqual = Util.mapEqual + } + module UnifyTester = MakeUnifyTester(UnifyWrapper) +} + +// TODO: modularise in the same way as AtomTester module MakeTerm = (Term: TERM) => { let termEquivalent = (t: Zora.t, t1: Term.t, t2: Term.t, ~msg=?) => { t->ok(