Merge branch 'ocaml5' of git+ssh://matita.cs.unibo.it/srv/git/helm into ocaml5

Worker thread killing fixed

In old Ocaml it used to work catching a Unix signal that was raised at the
end of each timeslice. It works no more in Ocaml5.

- we now use a fixed timer (every 1s) to trigger the Unix signal
- the signal is usually caught by the non-worker thread and for some reason
  blocking the signal interferes with Gtk
- solution: if the signal is caught by the non-worker thread, the thread
  goes to sleep for 3s to let the worker thread catch the signal

Most of the time the trick works, even if some delay is introdued.

Ctr-C now is equivalent to pressing the Break button

Avoid race conditions (deadlocks)

Porting to ocaml 5

- old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation
- as a consequence, bytecode is now compile in -custom mode
- requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5
  (all currently not accepted upstream yet)
- plenty of new warnings either turned off or applied to code
- ported to most recent version of camlp5

update in delayed_updating

+ new operator on update functions

update in ground

+ some additions
+ some renaming

Worker thread killing fixed

In old Ocaml it used to work catching a Unix signal that was raised at the
end of each timeslice. It works no more in Ocaml5.

- we now use a fixed timer (every 1s) to trigger the Unix signal
- the signal is usually caught by the non-worker thread and for some reason
  blocking the signal interferes with Gtk
- solution: if the signal is caught by the non-worker thread, the thread
  goes to sleep for 3s to let the worker thread catch the signal

Most of the time the trick works, even if some delay is introdued.

Ctr-C now is equivalent to pressing the Break button

Avoid race conditions (deadlocks)

Porting to ocaml 5

- old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation
- as a consequence, bytecode is now compile in -custom mode
- requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5
  (all currently not accepted upstream yet)
- plenty of new warnings either turned off or applied to code
- ported to most recent version of camlp5

update in delayed_updating

+ some renaming

update in delayed_updating

+ more complex example in which discarding num labels in b solves unwind

update in delayed_updating

+ couterexample to dbfr_ibfr when inner labels in b are not bound in b

update in delayed_updating

+ excess added to closure condition for path
+ height for path restored

update in ground

+ some renaming

update in delayed_updating

+ guard condition removed from reduction

update in ground

+ minor addition to relocation

update in delayed_updating

+ bug fixed in the "crux of the proof" allows to certify more reductions
+ restricted form of closed path not used anymore

update in ground

+ head-tail decomposition of a relocation map
+ injectivity of pnpred

wip in delayed_updating

guard condition

update in delayed_updating

+ example of unprotected balanced reduction continued and simplified

update in delayed_updating

+ example of unprotected balanced reduction continued

update in delayed_updating

+ example of unprotected balanced β-reduction started
+ some corrections and additions

update in ground

+ positive integer two

update in ground

+ additions to subset extensionality

update in delayed_updating

+ core reduction parked
+ paths of one repeated label resumed

update in delayed_updating

commutations of balanced reduction completed

update in predefined_virtuals

+ two arrows added

update in delayed_updating

+ balanced reduction with main theorem proved
+ notation change for lift

update in delayed_updating and ground

+ single specification for protected and unprotected closed path
+ some parked files removed

update in delayed_updating

+ reference by depth with offset parked for now

partial update in delayed_updating

+ we add reference by depth with offset
+ component "syntax" updated
+ some improvements
+ height parked for now

update in ground and delayed_updating

+ example of unprotected balanced segment
+ balanced reduction parked for now
+ additions and renaming

update in delayd_updating

+ introduction of path_closed complete

update in ground

+ some renaming and some refactoring

update in static_2

+ notation update from ground

update in ground

+ notation update and renaming

addition to predefined virtuals

+ one character added

partial update in delayed_updating

+ syntax and substitution components updated
+ path_head parked and replaced by path_closed
+ balanced reductions introduced and main theorem proved
+ minor corrections to notation

update in delayed_updating

+ focused reduction takes just one focus
+ changed minor premise of ifr_unwind_bi
+ some renaming

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

commit in delayed_updating

+ reversing paths completed updating component "reduction"

update in ground

+ additions to nap and xap

update in delayed_updating

+ three old lemmas restored
+ some parked lemmas removed
+ minor renaming

partial commit in delayed_updating

+ reversing paths in component "unwind"

partial commit in delayed_updating

+ reversing paths in component "substitution"
+ lift reformulated in terms of simpler functions

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

partial commit in delayed_updating

+ reversing paths in component "syntax"
+ some renaming

update in ground

+ one more lemma with list_append

partial commit in delayed_updating

+ parchin reverse operator for paths

update in delayed_updating

+ bind condition simplified for ifr and dfr

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

update in delayed updating

+ two lemmas on path_head
+ invocation added to first file

update in delayed_updating

+ some additions
+ minor improvements

update in delayed_updating

+ ifr_lift proved
+ ifr corrected
+ minor corrections

update in delayed_updating

+ unwind2_path_after_lift
+ prelift
+ refactoring for lift

update in ground

+ minor corrections

update in delayed updating

+ dfr_lift_bi proved

update in delayed_updating

+ WIP on lift
+ notation changed for delayed updating (term constructor)
+ minor corrections

update in delayed_updating

+ additions for lift
+ advances in dfr_lift_bi
+ some corrections
+ some parked files removed

update in delayed_updating

+ final definition of lift
+ WIP on dfr_lift_bi
+ updates and corrections
+ old definition of lift parked

update in delayed_updating

+ bug fixed in ifr allows to prove ifr_unwind_bi

update in delayed_updating

+ lift changed to lift after unwind in ifr
+ notion of lift swapped again
+ some additions to prove a side condition of ifr_unwind_bi

update in ground

* subset overlap

update  in lib

+ notation for overlap decentralized

update in delayed_updating

+ some files parked

update in delayed_updating

+ lift: additions and refactoring
+ reduction: WIP

update in ground and delayed_updating

+ main theorem about dfr proved!
+ ground: duplicated lemma removed
+ some refactoring

update in delayed_updating

+ crux of the main proof completed
+ notation for path_reverse fixed

update in delayed_updating

+ unwind completed with an important result on lift

update in ground

+ additions to lifts

update in ground

+ new notation for application of a relocation

update in delayed_updating

+ generic unwind meeds to be  even more generic

update in delayed_updating

+ generic unwind for path
+ some old files parked

update in delayed_updating

+ main function to locate the referred binder
+ update function for unfold

update in delayed_updating

+ notation for reversed path

update in delayed_updating

+ conflicts solved

update in delayed_updating

+ closed paths
+ updated notation for height
+ some parked files added

update in delayed_updating

+ some notation updated
+ some unused files removed

update in delayed_updating

+ alternative definition of unwind based on lift

update in delayed updating

updated notation

update in delayed updating

+ new version of lift
+ corrected and updated notation

update in ground

+ some addittions and corrections

update un delayed updating

+ some parked files

WIP in delayed_updating

+ we re focusing on a special case of the main theorem

update in delayed updating

+ additions to lift

update in ground

+ some additions and corrections

update in delayed_updating

+ lift
+ two versions of unwind
+ some renaming, additions and corrections

update in delayed_updating

+ some additions and corrections

update in ground

+ some additions

partial update in delayed_updating

+ WIP

update in ground

+ minor corrections and additions

update in delayed_updating

+ important additionsand corrections

update in ground

+ some additions and corrections

update in delayed_updating

+ update count for paths
+ minor additions and corrections

update in ground

+ additions to tr_compose

update in delayed_updating

+ WIP on dfr_lift_bi
+ minor corrections

update in ground

+ main commutation of tr_compose and tr_uni

update in delayed_updating

+ relationship between grafted trees and updating clarified in the case of interest so far