search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

Record presence of holes in the proof state #26

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
At the moment, the scheduler is started after every command, and when at the 
top level it searches the entire proof state. This is much too slow. News 
update also unnecessarily traverses the entire tree.

For each region in the hierarchy, we need to record whether it contains any 
holes with elaboration problems attached. The news propagation mechanism also 
needs to know whether the definitions are saturated (i.e. contain no references 
to holes).

Original issue reported on code.google.com by adamgundry on 9 Jun 2010 at 10:47

GoogleCodeExporter commented 9 years ago 
I've added a field in developments (and layers) to record whether they contain 
any unstable elaboration problems. This improves performance significantly when 
working interactively with large test cases (e.g. Demo.pig).

We still need to consider how to deal with news updates. There are various 
possibilities for recording saturation or representing terms with a single 
hole.

Original comment by adamgundry on 21 Jun 2010 at 8:59