|
|
|
@2869
|
7 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
|
@2824
|
7 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
|
@2769
|
7 years |
mckinna |
Mistakenly commented out
both as_cost_get_label (needed; OK)
as well …
|
|
|
|
@2768
|
7 years |
mckinna |
Nightmare: file no longer typechecks,
because defn as_cost_get_labels …
|
|
|
|
@2760
|
7 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
|
@2757
|
7 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
|
@2756
|
7 years |
sacerdot |
WARNING: this commit breaks things, sorry, Paolo is going to fix …
|
|
|
|
@2755
|
7 years |
tranquil |
* changed primitives of abstract status (with stuf that is probably …
|
|
|
|
@2553
|
7 years |
tranquil |
as_classify changed to a partial function
added a status for tailcalls
|
|
|
|
@2531
|
7 years |
mckinna |
Trivial tweaks.
|
|
|
|
@2508
|
8 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
|
@2503
|
8 years |
mckinna |
tidied up, with new auxiliary defns, some refactoring, some code …
|
|
|
|
@2423
|
8 years |
tranquil |
as_classifier predicate → as_classify function
as_call predicate from …
|
|
|
|
@2417
|
8 years |
boender |
- reverted changes to StructuredTraces? (shouldn't have been committed …
|
|
|
|
@2413
|
8 years |
tranquil |
* tal_rel corrected to include cases where tal_base_call \approx …
|
|
|
|
@2398
|
8 years |
boender |
- committed start of stacksize
|
|
|
|
@2299
|
8 years |
campbell |
Soundly labelled RTLabs structured traces are "unrepeating".
|
|
|
|
@2186
|
8 years |
tranquil |
updated joint semantics
|
|
|
|
@2129
|
8 years |
mulligan |
Large changes from today trying to complete the main theorem. Again :(
|
|
|
|
@2044
|
8 years |
campbell |
PCs for RTLabs structured traces.
|
|
|
|
@1976
|
8 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
|
@1964
|
8 years |
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
|
|
@1949
|
8 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1944
|
8 years |
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
|
|
@1939
|
8 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
|
@1938
|
8 years |
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
|
|
@1935
|
8 years |
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
|
|
@1927
|
8 years |
mulligan |
Reduced complexity of good_program predicate, ported to new notion of …
|
|
|
|
@1926
|
8 years |
tranquil |
* added as_label to abstract status, with as_costed defined with it. …
|
|
|
|
@1921
|
8 years |
mulligan |
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
|
|
|
|
@1918
|
8 years |
tranquil |
using listb.ma now
|
|
|
|
@1917
|
8 years |
tranquil |
predicate for unrepeating traces, fused final_abstract_status with …
|
|
|
|
@1902
|
8 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
|
@1901
|
8 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
|
@1880
|
8 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@1812
|
8 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
|
@1808
|
8 years |
campbell |
Create a Prop version of the non-terminating structured traces so that …
|
|
|
|
@1806
|
8 years |
campbell |
Show that we could construct RTLabs non-terminating structured traces …
|
|
|
|
@1783
|
8 years |
campbell |
Remove junk from non-terminating structured traces.
|
|
|
|
@1709
|
8 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
|
@1658
|
8 years |
mulligan |
asm costs changes from today
|
|
|
|
@1654
|
8 years |
campbell |
Corrections to structured trace definitions (see the mailing list). …
|
|
|
|
@1652
|
8 years |
campbell |
Forgot to apply 1583 to non-terminating case.
|
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1583
|
8 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
|
@1574
|
9 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
|
@1544
|
9 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
|
@1536
|
9 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
|
@1532
|
9 years |
campbell |
Remove jump classification from structured traces.
|
|
|
|
@1531
|
9 years |
campbell |
A notion of abstract structured traces.
|
