Hi Antony,
here
https://github.com/glacode/yamma/blob/master/server/src/__test__/MmpUnifier.test.ts
there
are dozens of unit tests along the lines of your repo.
You should be able to easily serve them using Express. Here's a simple
example (but there are not more "complex" examples from your standpoint:
only the .mm and the .mmp will be more complex)
First you create the mmParser
const mp2Theory = '$c ( $. $c ) $. $c -> $. $c wff $. $c |- $. $v ph $. ' +
'$v ps $. $v ch $. wph $f wff ph $. wps $f wff ps $. wch $f wff ch $.\n' +
'wi $a wff ( ph -> ps ) $.\n' +
'${ min $e |- ph $. maj $e |- ( ph -> ps ) $. ax-mp $a |- ps $. $}';
const mp2MmParser: MmParser = new MmParser(globalState);
mp2MmParser.ParseText(mp2Theory);
mp2MmParser.createParseNodesForAssertionsSync();
Then you can unify:
test('Unify 2 ax-mp', () => {
const mmpSource = `
* test comment
qed::ax-mp |- ph`;
const mmpParserParams: IMmpParserParams = {
textToParse: mmpSource,
mmParser: mp2MmParser,
workingVars: new WorkingVars(kindToPrefixMap)
};
const mmpParser: MmpParser = new MmpParser(mmpParserParams);
mmpParser.parse();
const mmpUnifier: MmpUnifier = new MmpUnifier(
{
mmpParser: mmpParser,
proofMode: ProofMode.normal,
maxNumberOfHypothesisDispositionsForStepDerivation: 0,
renumber: false,
removeUnusedStatements: false
});
mmpUnifier.unify();
const textEditArray: TextEdit[] = mmpUnifier.textEditArray;
expect(textEditArray.length).toBe(1);
const newTextExpected = `
* test comment
d1:: |- &W1
d2:: |- ( &W1 -> ph )
qed:d1,d2:ax-mp |- ph
`;
const textEdit: TextEdit = textEditArray[0];
expect(textEdit.newText).toEqual(newTextExpected);
});
That's it!
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/a7cc1e76-8872-4d5e-9b79-1bdaca7d8ffan%40googlegroups.com.
