README

TODO:
a) test.elpi: splittare in codice di testing (un file) + libreria di tests (un altro file)
b) commentare i predicati entry-point (completato per gli entry-point dell'estrazione)
z) passare a un if-then-else al posto di (a, ! ; b)

FOOD FOR BRAIN:
1. abstract common code in extraction/{starify,extract,_...}_lib and main/process_entry
2. dal momento che l'input del extract_* non è ben tipato, durante l'iterazione
   sulle lib entry è inutile assumere tutte le ipotesi di tipaggio/conversione

===========

## Code extraction ##
* test.elpi:
  - pack_and_translate_library:  entrypoint
  - translib:                    entrypoint for debugging on Index-th entry
  - translate_entry:             obvious
  - ...
  - library of micro-tests for extraction, etc.

  * lib_mapping: old_entry extracted_entry mask

  - starify_lib: well typed (wt) MTTi -> (wt) MTTi
      <> propS |-> extractor_singleton
  - extract_lib: (wt) MTTi -> (wt) MTTi
  - translate_lib: (wt) MTTi -> {OCaml,Haskell}
  - translate_program_list: traduce frammenti wt MTTi ->^3 {OCaml,Haskell}
  - get_call_signature:

* extraction.elpi:
  defines {starify,extract}_lib

* to_language.elpi:
  defines translate_lib