-
Notifications
You must be signed in to change notification settings - Fork 3
sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
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
About
An implementation in Lambda-Prolog of the Minimalist Type Theory
Topics
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published