diff --git a/src/logic-concept.js b/src/logic-concept.js index 25cc8119..83d31a27 100644 --- a/src/logic-concept.js +++ b/src/logic-concept.js @@ -545,6 +545,8 @@ export class LogicConcept extends MathConcept { while ( i < sequence.length ) { // if an entry is a colon, mark the next as a given if ( givenRE.test( sequence[i] ) ) { + if ( i + 1 == sequence.length ) + problem( 'Cannot end the input with a colon' ) sequence[i+1].makeIntoA( 'given' ) sequence = sequence.without( i ) // if an entry is an attributes object, modify the previous diff --git a/src/validation/conjunctive-normal-form.js b/src/validation/conjunctive-normal-form.js index 0ff86e25..9eb9f35f 100644 --- a/src/validation/conjunctive-normal-form.js +++ b/src/validation/conjunctive-normal-form.js @@ -144,9 +144,8 @@ const highestMentioned = CNF => { } const firstUnmentioned = CNF => highestMentioned( CNF ) + 1 -// Utility function for computing an array plus an integer, in the sense that -// we get back the same array if the integer was already in it, or an array -// of length 1 greater, if we had to add the integer to it. +// Utility function for the union of two arrays of integers, treating the +// arrays as if they were sets. const arrayUnion = ( a1, a2 ) => [ ...new Set( [ ...a1, ...a2 ] ) ] // Utility for binding the previous function to an argument, i.e., currying. const unionWith = a1 => a2 => arrayUnion( a1, a2 ) diff --git a/tests/logic-concept-test.js b/tests/logic-concept-test.js index a680392e..f5eb7c0a 100644 --- a/tests/logic-concept-test.js +++ b/tests/logic-concept-test.js @@ -1029,6 +1029,10 @@ describe( 'Reading putdown notation', () => { expect( () => { LogicConcept.fromPutdown( '{ :A ::B (and A B) }' ) } ).to.throw( /^Cannot put two colons in a row/ ) + // can't have a colon that doesn't modify anything + expect( () => { + LogicConcept.fromPutdown( ':' ) + } ).to.throw( /^Cannot end the input with a colon/ ) // must end your string literal before a newline shows up expect( () => { LogicConcept.fromPutdown( '"one\ntwo"' ) diff --git a/tests/math-concept-test.js b/tests/math-concept-test.js index 41033906..312b3f3a 100644 --- a/tests/math-concept-test.js +++ b/tests/math-concept-test.js @@ -3040,6 +3040,11 @@ describe( 'Smackdown notation and interpretation', () => { symbolMC( 'one_expression' ).attr( [ [ 'label', 'that\'s an expression!' ] ] ) ) ).to.equal( true ) + expect( test1[0].interpret().equals( + LogicConcept.fromPutdown( ` + one_expression +{"label":"that\'s an expression!"} + ` )[0] + ) ).to.equal( true ) // ---------- one \label{...} applied to one environment const test2 = MathConcept.fromSmackdown( ` @@ -3055,6 +3060,11 @@ describe( 'Smackdown notation and interpretation', () => { ) ).attr( [ [ 'label', 'that one is an env' ] ] ) ) ).to.equal( true ) + expect( test2[0].interpret().equals( + LogicConcept.fromPutdown( ` + { :one (environment of things) } +{"label":"that one is an env"} + ` )[0] + ) ).to.equal( true ) // ---------- several \label{...}s in a larger putdown text const test3 = MathConcept.fromSmackdown( ` @@ -3091,6 +3101,19 @@ describe( 'Smackdown notation and interpretation', () => { [ [ 'label', 'this modifies "here"' ] ] ), ).attr( [ [ 'label', 'my favorite proof' ] ] ) ) ).to.equal( true ) + expect( test3[0].interpret().equals( + LogicConcept.fromPutdown( ` + :{ + :(> x y) +{"label":"premise-1"} + :(> y z) +{"label":"premise-2"} + (> x z) + } +{"label":"transitivity of >"} + { + maybe I would do some deduction here + +{"label":"this modifies \\"here\\""} + } +{"label":"my favorite proof"} + ` )[0] + ) ).to.equal( true ) // ---------- repeat test 1 using ref instead of label const test4 = MathConcept.fromSmackdown( ` @@ -3102,6 +3125,11 @@ describe( 'Smackdown notation and interpretation', () => { symbolMC( 'one_expression' ).attr( [ [ 'ref', 'that\'s an expression!' ] ] ) ) ).to.equal( true ) + expect( test4[0].interpret().equals( + LogicConcept.fromPutdown( ` + one_expression +{"ref":"that\'s an expression!"} + ` )[0] + ) ).to.equal( true ) // ---------- repeat test 2 using ref instead of label const test5 = MathConcept.fromSmackdown( ` @@ -3117,6 +3145,11 @@ describe( 'Smackdown notation and interpretation', () => { ) ).attr( [ [ 'ref', 'that one is an env' ] ] ) ) ).to.equal( true ) + expect( test5[0].interpret().equals( + LogicConcept.fromPutdown( ` + { :one (environment of things) } +{"ref":"that one is an env"} + ` )[0] + ) ).to.equal( true ) // ---------- repeat test 3 using ref instead of label const test6 = MathConcept.fromSmackdown( ` @@ -3153,6 +3186,19 @@ describe( 'Smackdown notation and interpretation', () => { [ [ 'ref', 'this modifies "here"' ] ] ), ).attr( [ [ 'ref', 'my favorite proof' ] ] ) ) ).to.equal( true ) + expect( test6[0].interpret().equals( + LogicConcept.fromPutdown( ` + :{ + :(> x y) +{"ref":"premise-1"} + :(> y z) +{"ref":"premise-2"} + (> x z) + } +{"ref":"transitivity of >"} + { + maybe I would do some deduction here + +{"ref":"this modifies \\"here\\""} + } +{"ref":"my favorite proof"} + ` )[0] + ) ).to.equal( true ) // ---------- mix of \label/ref{...}s in a large putdown text const test7 = MathConcept.fromSmackdown( ` @@ -3195,6 +3241,21 @@ describe( 'Smackdown notation and interpretation', () => { [ 'label', 'between these' ] ] ) ) ).to.equal( true ) + expect( test7[0].interpret().equals( + LogicConcept.fromPutdown( ` + :{ + :(> x y) +{"label":"premise-1"} + :(> y z) +{"ref":"premise-2"} + (> x z) + } +{"label":"transitivity of >"} + { + maybe I would do some deduction here + +{"label":"label for \\"here\\""} + +{"ref":"ref for \\"here\\""} + } +{"ref":"try no space"} + +{"label":"between these"} + ` )[0] + ) ).to.equal( true ) // ---------- should handle escapes (\{, \\\}, \\, etc.) correctly const test8 = MathConcept.fromSmackdown( ` @@ -3218,6 +3279,45 @@ describe( 'Smackdown notation and interpretation', () => { symbolMC( 'modify' ).attr( [ [ 'ref', 'a {whole} mess of \\slashes\\ and {CURLIES}' ] ] ) ) ).to.equal( true ) + expect( test8[0].interpret().equals( + LogicConcept.fromPutdown( ` + simple +{"label":"plain"} + ` )[0] + ) ).to.equal( true ) + expect( test8[1].interpret().equals( + LogicConcept.fromPutdown( ` + things +{"label":"open curly: {"} + ` )[0] + ) ).to.equal( true ) + expect( test8[2].interpret().equals( + LogicConcept.fromPutdown( ` + to +{"ref":"close curly: }"} + ` )[0] + ) ).to.equal( true ) + expect( test8[3].interpret().equals( + LogicConcept.fromPutdown( ` + modify +{"ref":"a {whole} mess of \\\\slashes\\\\ and {CURLIES}"} + ` )[0] + ) ).to.equal( true ) + + // ---------- does interpretation preserve non-label/ref attributes? + const test9 = MathConcept.fromSmackdown( ` + example \\label{my label} +{"other attr":"example val"} + ` ) + expect( test9 ).to.be.instanceOf( Array ) + expect( test9.length ).to.equal( 1 ) + expect( test9[0].equals( + symbolMC( 'example' ).attr( [ + [ 'label', 'my label' ], + [ 'other attr', 'example val' ] + ] ) + ) ).to.equal( true ) + expect( test9[0].interpret().equals( + LogicConcept.fromPutdown( ` + example +{"label":"my label"} + +{"other attr":"example val"} + ` )[0] + ) ).to.equal( true ) } ) it( 'Should give errors when \\label/ref{...} is wrongly used', () => { @@ -3362,8 +3462,8 @@ describe( 'Smackdown notation and interpretation', () => { expect( test5[0].equals( commandMC( 'noargcommand', '' ) ) ).to.equal( true ) - const E1=test5[1].interpret() - const E2=test5[2].interpret() + const E1 = test5[1].interpret() + const E2 = test5[2].interpret() expect( E1 ).to.be.instanceOf( Environment ) expect( E1.numChildren() ).to.equal( 1 ) expect( E1.child(0) ).to.be.instanceOf( LurchSymbol )