What is bug 256?

[LdBeth]

I see it is mentioned several times among comments in filter directory. I think it is time to migrate to CamlP5 8.00 and if I'd like to know if there's any chance this CamlP5 related bug can be resolved during this migration since the rewriting of filter_ocaml is necessary anyway.

* XXX: TODO: This converts the old-style location data into the modern one.
* Ideally, we should be able to embed location data as comments (bug 256).

Unfortunately the original bugzilla seems unavailable now and I didn't get any luck from archive.org either. It is hard for me to be sure about what the proposed "comment" concept is.

 * XXX: TODO: Once comments on terms or soft abstractions are implemented (bugs 256/261),
 *            the "le"/"gt" forms should have a comment that makes sure they will be displayed
 *            as "le"/"gt".

I do know what soft abstraction is from NuPRL, so I just made a bold guess that there will be a new slot added to opname that will record these additional properties, which is opaque to the refiner but visible to other utils like dform?

@ANogin @jyh

[ANogin]

Right, a couple of months ago I tried to see whether I have a backup of the MetaPRL Bugzilla somewhere, but did not find it :(. I wonder whether @jyh has it somewhere...

I do not remember whether we had a specific design for comments worked out. But yes, having an extra opname slot might be one way - although I think it would make sense for it be and extra component of the term/term' type, rather than a part of opname.

For soft abstractions - these should act similar to definitions, except that all matching operations (refiner, lookup tables, etc) would automatically unfold them if the match would otherwise fail (note - correct behavior of dforms would follow from correct behavior of lookup tables). This would be something that would have to be very carefully designed so that

1. You only pay the costs of the mechanism when you actually use it, and there is no noticeable slowdown on performing refiner/lookup/etc operations in theories with no soft abstractions,
2. You do not unfold the soft abstractions unless you actually have to, but at the same time
3. You do not get into situations where you have to keep unfolding it over and over for the same term

[ANogin]

P.S. As far as rewriting filter_ocaml goes, I am not sure whether the right thing is to rewrite it, or to [partially] throw it out. The intent was to enable reasoning about OCaml code, but we never actually fully implemented that. It makes sense to keep it available and supporting a limited subset of OCaml, in case somebody does want to do that, but it makes no sense to require that all of MetaPRL theories have to undergo OCaml -> term -> OCaml translation prior to compilation... What does need to happen is to revisit .cmoz/.prlb/.prla mess:

• Only things created in the interactive [proof] editor should be kept in .prlb/.prla (or maybe all interactive rules/rewrites, including the ones that have just the statements that came from .ml and have not yet been touched in the editor in any way) - there is no reason to keep a copy of the parsed .ml in there. (This will preclude a theoretical possibility of editing more than just proofs in the interactive editor, but that is probably reasonable).
• Optionally: .prla format should probably be something a little more manual editing friendly (but not sure how to best do it in a way that maintains its cons-hashing nature with no duplication of any subterms - without that, things get unreasonably big).

[LdBeth]

I am not sure whether the right thing is to rewrite it, or to [partially] throw it out.

I have just fixed the term_list function so filtering items out from prla won't results in these items not been displayed by ls anymore.

Rendering ML code is probably still a needed feature, but maybe I can do that by tools directly available from CamlP5 instead, since the layout options of dform is limited, so MLast data types can be saved without converting to terms.