Ferruccio Guidi [Wed, 18 Jun 2014 15:03:20 +0000 (15:03 +0000)]
milestone connit for preservation:
- for now we remove stratified equivalence for terms
(it is much more complicated than expected)
- we park in etc a generalization of preservation
Ferruccio Guidi [Sat, 7 Jun 2014 19:32:38 +0000 (19:32 +0000)]
- advances on free variables allow to reduce lleq_lpx_trans to llor_total :)
- lazy union of local environments need a depth argument
- Makefile bugfixed
Ferruccio Guidi [Sun, 25 May 2014 20:04:55 +0000 (20:04 +0000)]
- theory of llor now includes (long awaited) non-recursive alternative definition
- poinwise extensions downgraded (current llor does not need the improved version)
- some refactoring in etc
- name changes in the rediction rules
- theory of extended substitution is active again, we hope to use it
to obtain a non-recurisive alternative definition of llpx_sn
- the relation for pointwise extensions now takes a binder as argument
- explicit alternative definition of lprs and lpxs removed
- changes in the notation for subclosures and refinements
- lazy extended reduction parked
- fpns finally removed
- "big tree" computation based again on "full" extended reduction
but improved with lazy equivalence for local environments
- llor parked for now (something to fix there)
- some work on extensions:
the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
we restore the "full" version and use it for the normaliztion of extended reduction
we still use "lazy" version for the "big-tree" theorem
commit completed:
- pointwise ordinary reduction:
we park the "lazy" version and we restore the "full" version
annotating the source with our understandings
- pointwise extended reduction:
we use the "lazy" version for now
a better understanding of the relationship between the "full" version
and the "lazy" version (lpx_sn_llpx_sn) allows to link the two
Ferruccio Guidi [Tue, 25 Mar 2014 19:55:08 +0000 (19:55 +0000)]
- partial commit: just the components below "computation"
the development of lazy pointwise extensions continues ...
- we parked not-lazy pointwise extensions in etc
Ferruccio Guidi [Sat, 8 Mar 2014 17:32:55 +0000 (17:32 +0000)]
we define the lazy poinwise extension of a relation, that should
allow to derive lleq with corrected lleq_lref, and a new defininition
for lpx (and derivatives), which now contains a bug too :( being not lazy
- we revise the definition of lazy equivakence since lleq_lref contains a bug
Code changed a bit to make it work as before with OCaml 4.0.
Without this patch, the refresh of the textual widget (e.g. the update
of the locked part) is not immediately done.
This is roughly the visual behaviour the user expects. On the other hand,
we also expect the threads that execute and that responsible for the UI
to work in parallel, which is not the case. The code I just touched stops
the worker thread for, on average, 0.1s per tactic, which is really a lot.
Switching to a multiprocess implementation (in place of a multithread) does
not seem easy. Bad OCaml, bad.
Hocus-pocus code to use the old (and deprecated) implementation of
Hashtbl.hash because the new one changes the behaviour of automation,
breaking the library.
Bug fixed: the tactic to analyze the term and understand whose inductive
type it belongs to did not put the sort in whd before concluding that
it was not a sort.
OCaml 4.0 detects a not handled case.
I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.
Ferruccio Guidi [Fri, 21 Feb 2014 16:36:20 +0000 (16:36 +0000)]
- main proposition on lsx finally proved!
- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat
projects / helm.git / log