source:
extracted
@
2998
| Name | Size | Rev | Age | Author | Last Change |
|---|---|---|---|---|---|
| ../ | |||||
| untrusted | 2997 | 8 years | New extraction. | ||
| abstractStatus.ml | 4.2 KB | 2905 | 8 years | Semantics of ASM in place (up to return values and function call … | |
| abstractStatus.mli | 1.5 KB | 2905 | 8 years | Semantics of ASM in place (up to return values and function call … | |
| arithmetic.ml | 27.1 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| arithmetic.mli | 8.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| aSM.ml | 227.7 KB | 2997 | 8 years | New extraction. | |
| aSM.mli | 63.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| aSMCosts.ml | 30.2 KB | 2993 | 8 years | 1. performance improved: the type inference was inferring … | |
| aSMCosts.mli | 2.0 KB | 2910 | 8 years | Abstract statuses for ASM and OC completed. A simple test program can … | |
| aSMCostsSplit.ml | 3.3 KB | 2997 | 8 years | New extraction. | |
| aSMCostsSplit.mli | 1.3 KB | 2997 | 8 years | New extraction. | |
| assembly.ml | 179.9 KB | 2905 | 8 years | Semantics of ASM in place (up to return values and function call … | |
| assembly.mli | 3.9 KB | 2905 | 8 years | Semantics of ASM in place (up to return values and function call … | |
| assocList.ml | 979 bytes | 2842 | 8 years | The compiler can now show all back-end traces too (assembly and object … | |
| assocList.mli | 534 bytes | 2842 | 8 years | The compiler can now show all back-end traces too (assembly and object … | |
| aST.ml | 55.2 KB | 2997 | 8 years | New extraction. | |
| aST.mli | 19.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| backEndOps.ml | 45.7 KB | 2977 | 8 years | New extraction after several bug fixes. | |
| backEndOps.mli | 8.6 KB | 2933 | 8 years | New extraction, several bug fixed. RTL_semantics fixed by hand, will … | |
| bEMem.ml | 1.0 KB | 2829 | 8 years | Semantics files committed. | |
| bEMem.mli | 801 bytes | 2829 | 8 years | Semantics files committed. | |
| bigops.ml | 11.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bigops.mli | 5.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bind_new.ml | 4.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| bind_new.mli | 2.2 KB | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| bindLists.ml | 1.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bindLists.mli | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bitVector.ml | 2.1 KB | 2780 | 8 years | Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were … | |
| bitVector.mli | 1.1 KB | 2780 | 8 years | Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were … | |
| bitVectorTrie.ml | 11.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| bitVectorTrie.mli | 3.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bitVectorTrieSet.ml | 3.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bitVectorTrieSet.mli | 924 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bitVectorZ.ml | 2.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| bitVectorZ.mli | 743 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| blocks.ml | 2.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| blocks.mli | 1.7 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| bool.ml | 2.5 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| bool.mli | 924 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| build | 279 bytes | 2789 | 8 years | Some changes to the driver to aid debugging. | |
| byteValues.ml | 40.8 KB | 2997 | 8 years | New extraction. | |
| byteValues.mli | 13.8 KB | 2933 | 8 years | New extraction, several bug fixed. RTL_semantics fixed by hand, will … | |
| casts.ml | 892 bytes | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| casts.mli | 746 bytes | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| cexec.ml | 48.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| cexec.mli | 3.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| cexecInd.ml | 548 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| cexecInd.mli | 548 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| cexecSound.ml | 875 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| cexecSound.mli | 875 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| classifyOp.ml | 40.2 KB | 2997 | 8 years | New extraction. | |
| classifyOp.mli | 18.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| clight_abstract.ml | 2.8 KB | 2803 | 8 years | More code extracted, used to debug the compiler. | |
| clight_abstract.mli | 1.4 KB | 2803 | 8 years | More code extracted, used to debug the compiler. | |
| clight_classified_system.ml | 1.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| clight_classified_system.mli | 1.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| cminor_abstract.ml | 3.3 KB | 2810 | 8 years | Cminor semantics exported. | |
| cminor_abstract.mli | 1.8 KB | 2810 | 8 years | Cminor semantics exported. | |
| cminor_classified_system.ml | 1.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| cminor_classified_system.mli | 1.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| cminor_semantics.ml | 36.2 KB | 2997 | 8 years | New extraction. | |
| cminor_semantics.mli | 11.1 KB | 2810 | 8 years | Cminor semantics exported. | |
| cminor_syntax.ml | 41.5 KB | 2997 | 8 years | New extraction. | |
| cminor_syntax.mli | 19.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| compiler.ml | 24.2 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| compiler.mli | 8.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| coqlib.ml | 363 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| coqlib.mli | 238 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| core_notation.ml | 15 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| core_notation.mli | 15 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| costCheck.ml | 5.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costCheck.mli | 1.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costInj.ml | 1.9 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| costInj.mli | 1.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| costLabel.ml | 711 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costLabel.mli | 547 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costMisc.ml | 816 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costMisc.mli | 816 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costSpec.ml | 4.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| costSpec.mli | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| csem.ml | 50.6 KB | 2997 | 8 years | New extraction. | |
| csem.mli | 13.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| csyntax.ml | 56.7 KB | 2997 | 8 years | New extraction. | |
| csyntax.mli | 22.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| deqsets.ml | 4.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| deqsets.mli | 1.8 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| deqsets_extra.ml | 454 bytes | 2730 | 8 years | Exported again. | |
| deqsets_extra.mli | 314 bytes | 2730 | 8 years | Exported again. | |
| div_and_mod.ml | 3.4 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| div_and_mod.mli | 1.5 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| division.ml | 7.2 KB | 2827 | 8 years | Everything extracted again. | |
| division.mli | 1.6 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| errorMessages.ml | 1.3 KB | 2997 | 8 years | New extraction. | |
| errorMessages.mli | 1.3 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| errors.ml | 9.5 KB | 2997 | 8 years | New extraction. | |
| errors.mli | 4.5 KB | 2743 | 8 years | Latest version of the compiler, extracted with the latest version of … | |
| eRTL.ml | 25.0 KB | 2997 | 8 years | New extraction. | |
| eRTL.mli | 10.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTL_printer.ml | 1.3 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTL_printer.mli | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTL_semantics.ml | 11.3 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTL_semantics.mli | 3.2 KB | 2829 | 8 years | Semantics files committed. | |
| eRTLptr.ml | 11.9 KB | 2997 | 8 years | New extraction. | |
| eRTLptr.mli | 4.7 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTLptr_printer.ml | 1.3 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTLptr_printer.mli | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTLptr_semantics.ml | 6.0 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| eRTLptr_semantics.mli | 1.6 KB | 2829 | 8 years | Semantics files committed. | |
| eRTLptrToLTL.ml | 38.0 KB | 2997 | 8 years | New extraction. | |
| eRTLptrToLTL.mli | 8.7 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTLToERTLptr.ml | 4.6 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| eRTLToERTLptr.mli | 1.6 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| events.ml | 11.1 KB | 2997 | 8 years | New extraction. | |
| events.mli | 4.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| executions.ml | 658 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| executions.mli | 658 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| exp.ml | 268 bytes | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| exp.mli | 177 bytes | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| extra_bool.ml | 463 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| extra_bool.mli | 271 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| extraGlobalenvs.ml | 697 bytes | 2829 | 8 years | Semantics files committed. | |
| extraGlobalenvs.mli | 697 bytes | 2829 | 8 years | Semantics files committed. | |
| extralib.ml | 1.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| extralib.mli | 635 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| extraMonads.ml | 7.0 KB | 2829 | 8 years | Semantics files committed. | |
| extraMonads.mli | 3.6 KB | 2829 | 8 years | Semantics files committed. | |
| extranat.ml | 6.1 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| extranat.mli | 2.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| fetch.ml | 83.6 KB | 2997 | 8 years | New extraction. | |
| fetch.mli | 1.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| fixpoints.ml | 10.1 KB | 2997 | 8 years | New extraction. | |
| fixpoints.mli | 5.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| foldStuff.ml | 1.5 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| foldStuff.mli | 741 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| fresh.ml | 2.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| fresh.mli | 1.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| frontend_misc.ml | 6.1 KB | 2827 | 8 years | Everything extracted again. | |
| frontend_misc.mli | 2.2 KB | 2827 | 8 years | Everything extracted again. | |
| frontEndMem.ml | 3.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| frontEndMem.mli | 1.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| frontEndOps.ml | 56.8 KB | 2997 | 8 years | New extraction. | |
| frontEndOps.mli | 23.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| frontEndVal.ml | 4.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| frontEndVal.mli | 1.2 KB | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| genMem.ml | 9.7 KB | 2997 | 8 years | New extraction. | |
| genMem.mli | 4.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| globalenvs.ml | 26.2 KB | 2997 | 8 years | New extraction. | |
| globalenvs.mli | 11.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| graphs.ml | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| graphs.mli | 833 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| hide.ml | 81 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| hide.mli | 81 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| hints_declaration.ml | 162 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| hints_declaration.mli | 162 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| i8051.ml | 32.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| i8051.mli | 6.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| i8051bis.ml | 551 bytes | 2829 | 8 years | Semantics files committed. | |
| i8051bis.mli | 211 bytes | 2829 | 8 years | Semantics files committed. | |
| identifiers.ml | 17.7 KB | 2997 | 8 years | New extraction. | |
| identifiers.mli | 8.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| initialisation.ml | 5.5 KB | 2797 | 8 years | Extracted again after James's cleanup and the implementation of the … | |
| initialisation.mli | 1.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| integers.ml | 9.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| integers.mli | 3.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| interference.ml | 8.6 KB | 2997 | 8 years | New extraction. | |
| interference.mli | 4.4 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| interpret2.ml | 15.0 KB | 2997 | 8 years | New extraction. | |
| interpret2.mli | 2.6 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| interpret.ml | 245.5 KB | 2909 | 8 years | New extraction. | |
| interpret.mli | 2.5 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| iO.ml | 6.9 KB | 2997 | 8 years | New extraction. | |
| iO.mli | 2.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| iOMonad.ml | 18.6 KB | 2997 | 8 years | New extraction. | |
| iOMonad.mli | 9.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| jmeq.ml | 3.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| jmeq.mli | 1.7 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| joint.ml | 110.3 KB | 2997 | 8 years | New extraction. | |
| joint.mli | 54.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| joint_fullexec.ml | 3.2 KB | 2968 | 8 years | The initial status memory was not really initialized. Now it is. | |
| joint_fullexec.mli | 1.5 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| joint_LTL_LIN.ml | 13.4 KB | 2997 | 8 years | New extraction. | |
| joint_LTL_LIN.mli | 6.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| joint_LTL_LIN_semantics.ml | 7.7 KB | 2997 | 8 years | New extraction. | |
| joint_LTL_LIN_semantics.mli | 2.3 KB | 2997 | 8 years | New extraction. | |
| joint_printer.ml | 60.8 KB | 2996 | 8 years | Printing of graphs now starts from the entry point. | |
| joint_printer.mli | 25.8 KB | 2996 | 8 years | Printing of graphs now starts from the entry point. | |
| joint_semantics.ml | 112.8 KB | 2997 | 8 years | New extraction. | |
| joint_semantics.mli | 52.3 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| label.ml | 26.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| label.mli | 2.7 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| labelledObjects.ml | 2.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| labelledObjects.mli | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| lIN.ml | 2.0 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| lIN.mli | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lIN_printer.ml | 1.3 KB | 2995 | 8 years | The lIN_printer extracted. | |
| lIN_printer.mli | 1.0 KB | 2995 | 8 years | The lIN_printer extracted. | |
| lIN_semantics.ml | 1.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lIN_semantics.mli | 1.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| linearise.ml | 11.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| linearise.mli | 2.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lINToASM.ml | 62.8 KB | 2986 | 8 years | New extraction. | |
| lINToASM.mli | 9.2 KB | 2986 | 8 years | New extraction. | |
| list.ml | 9.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| list.mli | 3.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| listb.ml | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| listb.mli | 477 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| listb_extra.ml | 232 bytes | 2730 | 8 years | Exported again. | |
| listb_extra.mli | 232 bytes | 2730 | 8 years | Exported again. | |
| lists.ml | 2.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| lists.mli | 945 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| liveness.ml | 15.1 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| liveness.mli | 2.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| logic.ml | 6.3 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| logic.mli | 2.6 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| lTL.ml | 4.1 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| lTL.mli | 2.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTL_printer.ml | 1.3 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTL_printer.mli | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTL_semantics.ml | 1.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTL_semantics.mli | 1.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTLToLIN.ml | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| lTLToLIN.mli | 982 bytes | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| measurable.ml | 20.6 KB | 2997 | 8 years | New extraction. | |
| measurable.mli | 8.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| memoryInjections.ml | 5.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| memoryInjections.mli | 2.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| memProperties.ml | 1.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| memProperties.mli | 1016 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| MODIFIED_BY_HAND | 48 bytes | 2966 | 8 years | Modified by hand files (to improve a little bit the performance). | |
| monad.ml | 20.1 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| monad.mli | 9.5 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| nat.ml | 3.2 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| nat.mli | 1.2 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| option.ml | 1.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| option.mli | 366 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| order.ml | 2.6 KB | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| order.mli | 968 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| pointers.ml | 11.0 KB | 2997 | 8 years | New extraction. | |
| pointers.mli | 4.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| policy.ml | 4.7 KB | 2962 | 8 years | Most performant algorithm restored. | |
| policy.mli | 1.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| policyFront.ml | 27.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| policyFront.mli | 2.6 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| policyStep.ml | 7.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| policyStep.mli | 864 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| positive.ml | 12.1 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| positive.mli | 3.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| positiveMap.ml | 12.7 KB | 2827 | 8 years | Everything extracted again. | |
| positiveMap.mli | 4.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| preamble.ml | 64 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| preIdentifiers.ml | 6.7 KB | 2827 | 8 years | Everything extracted again. | |
| preIdentifiers.mli | 2.8 KB | 2649 | 8 years | … | |
| PROBLEMS | 499 bytes | 2836 | 8 years | … | |
| proper.ml | 97 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| proper.mli | 97 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| pts.ml | 35 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| pts.mli | 35 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| registers.ml | 645 bytes | 2649 | 8 years | … | |
| registers.mli | 564 bytes | 2649 | 8 years | … | |
| registerSet.ml | 11.6 KB | 2997 | 8 years | New extraction. | |
| registerSet.mli | 6.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| relations.ml | 324 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| relations.mli | 286 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| rTL.ml | 9.0 KB | 2977 | 8 years | New extraction after several bug fixes. | |
| rTL.mli | 3.4 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTL_printer.ml | 1.3 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTL_printer.mli | 1.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTL_semantics.ml | 28.0 KB | 2997 | 8 years | New extraction. | |
| rTL_semantics.mli | 7.7 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| rTLabs_abstract.ml | 19.2 KB | 2997 | 8 years | New extraction. | |
| rTLabs_abstract.mli | 7.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| rTLabs_classified_system.ml | 1.9 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTLabs_classified_system.mli | 1.2 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTLabs_semantics.ml | 85.0 KB | 2997 | 8 years | New extraction. | |
| rTLabs_semantics.mli | 9.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| rTLabs_syntax.ml | 29.5 KB | 2997 | 8 years | New extraction. | |
| rTLabs_syntax.mli | 18.2 KB | 2997 | 8 years | New extraction. | |
| rTLabs_traces.ml | 90.7 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTLabs_traces.mli | 34.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| rTLabsToRTL.ml | 49.2 KB | 2997 | 8 years | New extraction. | |
| rTLabsToRTL.mli | 10.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTLToERTL.ml | 17.8 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| rTLToERTL.mli | 3.9 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| russell.ml | 104 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| russell.mli | 104 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| semantics.ml | 9.5 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| semantics.mli | 5.0 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| semanticsUtils.ml | 28.3 KB | 2997 | 8 years | New extraction. | |
| semanticsUtils.mli | 13.7 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| setoids.ml | 2.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| setoids.mli | 1.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| sets.ml | 81 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| sets.mli | 81 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| simplifyCasts.ml | 28.4 KB | 2997 | 8 years | New extraction. | |
| simplifyCasts.mli | 4.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| smallstep.ml | 16.8 KB | 2997 | 8 years | New extraction. | |
| smallstep.mli | 7.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| smallstepExec.ml | 21.5 KB | 2997 | 8 years | New extraction. | |
| smallstepExec.mli | 10.2 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| stacksize.ml | 8.5 KB | 2997 | 8 years | New extraction. | |
| stacksize.mli | 3.7 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| star.ml | 97 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| star.mli | 97 bytes | 2601 | 8 years | Extraction to ocaml is now working, with a couple of bugs left. One … | |
| state.ml | 1.1 KB | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| state.mli | 539 bytes | 2717 | 8 years | Extracted code for the whole compiler. The space cost model is not … | |
| status.ml | 250.9 KB | 2997 | 8 years | New extraction. | |
| status.mli | 16.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| statusProofs.ml | 599 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| statusProofs.mli | 599 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| string.ml | 890 bytes | 2649 | 8 years | … | |
| string.mli | 350 bytes | 2649 | 8 years | … | |
| structuredTraces.ml | 80.4 KB | 2997 | 8 years | New extraction. | |
| structuredTraces.mli | 36.5 KB | 2873 | 8 years | Extracted again. | |
| switchRemoval.ml | 23.2 KB | 2997 | 8 years | New extraction. | |
| switchRemoval.mli | 7.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| toCminor.ml | 94.5 KB | 2997 | 8 years | New extraction. | |
| toCminor.mli | 15.2 KB | 2960 | 8 years | New extraction, it diverges in RTL execution now. | |
| toRTLabs.ml | 54.6 KB | 2997 | 8 years | New extraction. | |
| toRTLabs.mli | 22.0 KB | 2997 | 8 years | New extraction. | |
| traces.ml | 24.6 KB | 2997 | 8 years | New extraction. | |
| traces.mli | 9.7 KB | 2997 | 8 years | New extraction. | |
| translateUtils.ml | 29.0 KB | 2981 | 8 years | New extraction after code simplification. | |
| translateUtils.mli | 14.2 KB | 2981 | 8 years | New extraction after code simplification. | |
| typeComparison.ml | 7.8 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| typeComparison.mli | 1.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| types.ml | 14.1 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| types.mli | 5.9 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| uses.ml | 3.5 KB | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| uses.mli | 1022 bytes | 2951 | 8 years | New extraction. Novely: a pre-main is used in the back-end. … | |
| util.ml | 21.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| util.mli | 6.4 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| utilBranch.ml | 445 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| utilBranch.mli | 361 bytes | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| values.ml | 13.8 KB | 2997 | 8 years | New extraction. | |
| values.mli | 3.3 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| vector.ml | 14.8 KB | 2775 | 8 years | The compiler now computes also the stack cost model. | |
| vector.mli | 5.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
| z.ml | 7.6 KB | 2827 | 8 years | Everything extracted again. | |
| z.mli | 2.0 KB | 2773 | 8 years | 1. everything extracted again after all bugs in Matita's extraction … | |
Note: See TracBrowser
for help on using the repository browser.
