And how do you unlock it for the constructors that are supposed to do the proper locking?
Hmm.
(let real-annotate annotate
(def theorem (f)
(if (check-f-is-valid-theorem f)
(real-annotate 'theorem f)
(err "Not a valid theorem")))
(= annotate
(fn (type obj)
(if (is type 'theorem)
(err "Spank! Spank! Under the boots of your master!!")
(real-annotate tpye obj)))))
It does have the drawback that you can't, say, reload the file, but hey, you did say you didn't want anyone else to create theorems except by that method, so even redefining that method won't work!
> accessing libraries is rather easy through mzscheme or the experimental FFI (it has to be improved, sure, but it's not that hard if someone wants to)
As an aside, this appears to be popular, it might be possible to add this to the ssyntax extension.
As an aside, I suspect that much of the slowdown from the new ssyntax/ssexpand comes from scheme-side 'ac emitting a lot of 'ar-eval calls, but I'm not sure, since I haven't studied 'ac output much yet.
> Hmmh, I don't really think it is against the spirit of the language. After all, I think you cannot just annotate arbitrary things to be of type integer (or can you?).
Yes, you can: (annotate 'int #\newline). It won't be useful, but yes, you can.
> The above solution would surely work in principle, but in practice I create millions of intermediate theorems, I do not want to store all of them!
Standard answer: Garbage collection
In any case: you can always destructure the annotation wrapper and work with the raw data (probably by using some sort of higher-order function, like combinators), only wrapping it in the annotation type. Sort of like explicit monads.
Garbage collection does not work here if you keep a track of all the defined theorems in a list as 'known*. We would need weak references to achieve this.
It might be possible to do so by using some sort of dynamic global (a la kennytilton's implementation some time back, but using 'thread-local objects to handle it).
I will do so soon, and hopefully when I get a chance to study ssyntax.arc a little more, I will add a-ssyntax-bottom.
What might be nice would be to have numerical precedence levels (reals, not integers), so that you could add an operator later with the right precedence without redefining everything.
