

@2869

8 years 
tranquil 
some reorganization of definitions, and a new taaf_append_taaf



@2824

8 years 
tranquil 
* moved sum on lists notation to extranat
* used sum on lists to …



@2769

8 years 
mckinna 
Mistakenly commented out
both as_cost_get_label (needed; OK)
as well …



@2768

8 years 
mckinna 
Nightmare: file no longer typechecks,
because defn as_cost_get_labels …



@2760

8 years 
sacerdot 
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …



@2757

8 years 
tranquil 
many things are still broken, but there is a partial backtrack on …



@2756

8 years 
sacerdot 
WARNING: this commit breaks things, sorry, Paolo is going to fix …



@2755

8 years 
tranquil 
* changed primitives of abstract status (with stuf that is probably …



@2553

8 years 
tranquil 
as_classify changed to a partial function
added a status for tailcalls



@2531

8 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

9 years 
campbell 
Soundly labelled RTLabs structured traces are "unrepeating".



@2186

9 years 
tranquil 
updated joint semantics



@2129

9 years 
mulligan 
Large changes from today trying to complete the main theorem. Again :(



@2044

9 years 
campbell 
PCs for RTLabs structured traces.



@1976

9 years 
tranquil 
* monads: just changed some defs, which had to be propagated in some …



@1964

9 years 
tranquil 
introduced as_label_of_cost and adapted accordingly. Equality of cost …



@1949

9 years 
tranquil 
* lemma trace rel to eq flatten trace
* some more properties of …



@1944

9 years 
sacerdot 
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)



@1939

9 years 
mulligan 
Changes to get things to compile and to avoid the dependency …



@1938

9 years 
sacerdot 
Definitions moved to the right places, now everything compiles again.



@1935

9 years 
mulligan 
Generalized some lemma in ASM/CostsProof.ma to work on abstract …



@1927

9 years 
mulligan 
Reduced complexity of good_program predicate, ported to new notion of …



@1926

9 years 
tranquil 
* added as_label to abstract status, with as_costed defined with it. …



@1921

9 years 
mulligan 
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).



@1918

9 years 
tranquil 
using listb.ma now



@1917

9 years 
tranquil 
predicate for unrepeating traces, fused final_abstract_status with …



@1902

9 years 
mulligan 
Reverted needless changes to StructuredTraces?



@1901

9 years 
mulligan 
Slight changes to StructuredTraces?: should not change too much



@1880

9 years 
campbell 
Show that RTLabs flat traces are determined by their starting state, …



@1812

9 years 
campbell 
Provide a combined type for terminating and nonterminating structured …



@1808

9 years 
campbell 
Create a Prop version of the nonterminating structured traces so that …



@1806

9 years 
campbell 
Show that we could construct RTLabs nonterminating structured traces …



@1783

9 years 
campbell 
Remove junk from nonterminating structured traces.



@1709

9 years 
mulligan 
Changes to the execution of the MOVC instruction



@1658

9 years 
mulligan 
asm costs changes from today



@1654

9 years 
campbell 
Corrections to structured trace definitions (see the mailing list). …



@1652

9 years 
campbell 
Forgot to apply 1583 to nonterminating case.



@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1583

9 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.
