

@2645

8 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2599

8 years 
tranquil 
* map_opt and map on positive maps are now clean (erase empty …



@2541

9 years 
tranquil 
adapted size notation to last matita lib update (01/12/2012)
that …



@2439

9 years 
campbell 
Get a proper reverse mapping of function blocks to identifiers by …



@2420

9 years 
campbell 
Tidy away generic results about folds on positive/identifier maps.



@2418

9 years 
campbell 
Add a checking function for the uniqueness of cost labels in RTLabs …



@2415

9 years 
campbell 
Add the ability to map blocks to symbols in preparation for stack space.



@2335

9 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2314

9 years 
campbell 
Move generic definitions from recent commit to appropriate places.



@2307

9 years 
campbell 
Half the proofs for sound cost labelling check.



@2305

9 years 
campbell 
RTLabs cost spec checking function implemented (lacks proof, or much …



@2303

9 years 
campbell 
Some preliminary checking of cost labelling properties in RTLabs.



@2222

9 years 
sacerdot 
More robust to possible future changes to the "in match" semantics …



@2182

9 years 
tranquil 
updated linearisation pass



@2155

9 years 
tranquil 
updates to blocks and RTLabs to RTL translation (which sidesteps …



@2111

9 years 
sacerdot 
Cleanup: lemmas/theorems/axioms moved to the right places.



@1949

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



@1928

9 years 
mulligan 
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …



@1908

9 years 
fguidi 
notation fixup following last commit of matita
we shifted the levels …



@1882

9 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1635

9 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1631

10 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1627

10 years 
campbell 
Add some notions of freshness, and start using them for temporary …



@1601

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



@1562

10 years 
mulligan 
new version of assembly, fixed conflict in positivemap.ma, changed …



@1535

10 years 
campbell 
Make RTLabs semantics use knowledge that the next instruction always …



@1516

10 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

10 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1092

10 years 
campbell 
Some minor definitions for identifiers and lists.



@1077

10 years 
mulligan 
ack, dependent types are scary



@1072

10 years 
campbell 
Use not equals form of showing entry/exit labels.



@1070

10 years 
campbell 
Show that entry and exit labels are in the RTLabs graph.



@1068

10 years 
mulligan 
rtlabs translation complete subject to axioms



@1058

10 years 
campbell 
Evict CompCert? Maps interface in favour of BitVectorTries?.



@1057

10 years 
mulligan 
changes from today



@1056

10 years 
campbell 
Switch to delayed identifier error scheme.



@1055

10 years 
mulligan 
changes to how identifiers are generated



@1053

10 years 
mulligan 
changes



@816

10 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …



@797

10 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@782

10 years 
mulligan 
More work on rtlertl pass from today, plus resolved conflict.



@779

10 years 
campbell 
Add merging of tries and identifier sets (based on Dominic's earlier …



@761

10 years 
campbell 
Enforce the use of declared identifiers/registers in Cminor/RTLabs.



@757

10 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@753

10 years 
mulligan 
Work from today.



@738

10 years 
campbell 
Use lower case names for identifiers for consistency with CompCert? …



@737

10 years 
campbell 
Use more abstract identifiers in Clight / RTLabs.



@736

10 years 
campbell 
Extra type safety for identifiers.
