exposed `assumptions` struct

(hey, nice to see you again..)
maybe I don't know enough C, but does not this expose the assumptions struct?

Lines 8 to 12 in d88471c

    
           struct assumptions { 
        
               int label; 
        
               struct formula *formula; 
        
               struct assumptions *next; 
        
           };

It does, but that's okay! Because in natural deduction, assumptions may be freely introduced. So you don't need to call a function to get an assumptions struct, you can just make one up yourself, and in that case it's OK to look at what's inside it, etc.

At least, that was the idea.

We still do need to make sure you can't go back and modify assumptions that you've already based a proof on. I think when I was writing this, I enforced this by having every function that takes assumptions make a private copy of the assumptions that was passed to it, for its own use. The user can't see that copy, so they can't modify it, and if they modify their own copy, nothing in the proof changes.

Of course, I can't be absolutely certain (especially now, not having looked at the code for a while) that I implemented that correctly everywhere in the code, so it may be possible to find a hole in it somewhere, and if so, that'd be a bug.

I'll give the code a review with this in mind sometime when I can find time.

Yeah, I think I can see it now:

Philomath/src/theorem.c

Lines 50 to 56 in d88471c

    
           struct theorem * 
        
           suppose(struct formula *formula, int label) { 
        
               return mk_theorem( 
        
                   assume(label, formula, NULL), 
        
                   formula 
        
               ); 
        
           }

This is the only function for creating a theorem, and it does copy the assumption.
HOWEVER, it does not copy the formula in the conclusion argument to the mk_theorem function.
I think we can modify the conclusion of a theorem, since the formula struct is also exposed.

Also, the formula pointer is simply shared, so we can modify the assumption's formula too.

Yeah, fair enough.

I think when I was writing this, I enforced this by having every function that takes assumptions make a private copy of the assumptions

I've been reading over the code a little, and I don't see anywhere that I did this 😓

It's also not enough. struct formula is exposed too, and a couple of functions take a pointer to those too. But these all seem to feed into mk_theorem. So I think it's probably sufficient to rewrite the end of mk_theorem to be like

    t->assumptions = clone_assumptions(assumptions);
    t->conclusion = clone_formula(conclusion);
    return t;

where the clone_* functions perform deep copies.

(I'll also note that I think it's possible to try to address this problem by adding const keywords to these type signatures, and the struct definitions; but that's not what I had in mind when I wrote it, so I'm not inclined to go in that direction.)

I can try to address this and release a new version sometime in the next little while.

Thanks for finding this!

[..] where the clone_* functions perform deep copies.

I agree that this solution solves the issue as far as i can see.

I managed to do some development on this. It turned out that struct formula was actually more problematic than struct assumptions, because the latter is only being created and used internal to struct theorem. But, now struct formula is being deep-copied in the places where it is being used in theorems and assumptions. I added a few more test cases along the way and tagged the new version as 1.1. So I'm going to mark this issue as resolved, but if you do find another hole feel free to open another one 😁

	struct assumptions {
	int label;
	struct formula *formula;
	struct assumptions *next;
	};

	struct theorem *
	suppose(struct formula *formula, int label) {
	return mk_theorem(
	assume(label, formula, NULL),
	formula
	);
	}