|
|
@2855
|
8 years |
piccolo |
little bug fixed in TranslateUtils?.
|
|
|
@2851
|
8 years |
piccolo |
partial commit
|
|
|
@2849
|
8 years |
piccolo |
partial commit
|
|
|
@2845
|
8 years |
piccolo |
ERTLptr to LTL correctness proof started
|
|
|
@2844
|
8 years |
piccolo |
Stupid bug fixed
|
|
|
@2824
|
8 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
@2819
|
8 years |
sacerdot |
Proof obligation closed.
|
|
|
@2818
|
8 years |
sacerdot |
"Repaired", using non computational daemons.
|
|
|
@2808
|
8 years |
tranquil |
added local_stacksize to joint internal functions to accomodate for …
|
|
|
@2806
|
8 years |
tranquil |
new b_graph_translate obligations
|
|
|
@2796
|
8 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
@2783
|
8 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
@2774
|
8 years |
sacerdot |
1. the compiler now outputs both the stack cost model and the max …
|
|
|
@2741
|
8 years |
sacerdot |
File used only by untrusted code.
Implemented in Matita to exploit …
|
|
|
@2739
|
8 years |
sacerdot |
The graph colouring algorithm takes in input also the function.
|
|
|
@2700
|
8 years |
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
|
@2697
|
8 years |
sacerdot |
Compiler fixed to include the ERTLptrToLTL pass.
|
|
|
@2694
|
8 years |
tranquil |
completed ERTLptrToLTL
|
|
|
@2693
|
8 years |
sacerdot |
1. Stuff moved to correct places.
2. ERTLptr pass added
|
|
|
@2691
|
8 years |
sacerdot |
ERTLtoERTLptr* moved to the proper place
|
|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
@2675
|
8 years |
tranquil |
* a generic graph program transformation
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
@2666
|
8 years |
piccolo |
bug fixed in blocks.ma
|
|
|
@2663
|
8 years |
piccolo |
some minor modifications to ERTLtoERTLptr
|
|
|
@2662
|
8 years |
piccolo |
Towards a very generalized lemma that summarizes all of Paolo's results.
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
@2604
|
8 years |
piccolo |
ERTLtoERTLptr in place.
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
@2570
|
8 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
@2566
|
8 years |
piccolo |
ERTL to ERTLptr pass implemented up to a few things to be
left to the …
|