source: src/common/Identifiers.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2420   7 years campbell Tidy away generic results about folds on positive/identifier maps.
(edit) @2418   7 years campbell Add a checking function for the uniqueness of cost labels in RTLabs …
(edit) @2415   7 years campbell Add the ability to map blocks to symbols in preparation for stack space.
(edit) @2335   7 years campbell Deal with goto labels in RTLabs to Cminor by fixing up goto statements …
(edit) @2314   7 years campbell Move generic definitions from recent commit to appropriate places.
(edit) @2307   7 years campbell Half the proofs for sound cost labelling check.
(edit) @2305   7 years campbell RTLabs cost spec checking function implemented (lacks proof, or much …
(edit) @2303   7 years campbell Some preliminary checking of cost labelling properties in RTLabs.
(edit) @2222   7 years sacerdot More robust to possible future changes to the "in match" semantics …
(edit) @2182   7 years tranquil updated linearisation pass
(edit) @2155   7 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2111   7 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
(edit) @1949   8 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
(edit) @1928   8 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
(edit) @1908   8 years fguidi notation fixup following last commit of matita we shifted the levels …
(edit) @1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1635   8 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1631   8 years campbell Use fact that type environments in Cminor have distinct variables to …
(edit) @1627   8 years campbell Add some notions of freshness, and start using them for temporary …
(edit) @1601   8 years sacerdot Files ported to new version of the standard library.
(edit) @1562   8 years mulligan new version of assembly, fixed conflict in positivemap.ma, changed …
(edit) @1535   8 years campbell Make RTLabs semantics use knowledge that the next instruction always …
(edit) @1516   8 years sacerdot Ported to syntax of Matita 0.99.1.
(edit) @1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1316   8 years campbell Merge in id-lookup-branch to trunk.
(edit) @1092   8 years campbell Some minor definitions for identifiers and lists.
(edit) @1077   8 years mulligan ack, dependent types are scary
(edit) @1072   8 years campbell Use not equals form of showing entry/exit labels.
(edit) @1070   8 years campbell Show that entry and exit labels are in the RTLabs graph.
(edit) @1068   8 years mulligan rtlabs translation complete subject to axioms
(edit) @1058   8 years campbell Evict CompCert? Maps interface in favour of BitVectorTries?.
(edit) @1057   8 years mulligan changes from today
(edit) @1056   8 years campbell Switch to delayed identifier error scheme.
(edit) @1055   8 years mulligan changes to how identifiers are generated
(edit) @1053   8 years mulligan changes
(edit) @816   9 years campbell Clight to Cminor compilation, modulo switch statements, temporary …
(edit) @797   9 years campbell Add error messages wherever the error monad is used. Sticks to …
(edit) @782   9 years mulligan More work on rtl-ertl pass from today, plus resolved conflict.
(edit) @779   9 years campbell Add merging of tries and identifier sets (based on Dominic's earlier …
(edit) @761   9 years campbell Enforce the use of declared identifiers/registers in Cminor/RTLabs.
(edit) @757   9 years mulligan Lots more fixing to get both front and backends using same conventions …
(edit) @753   9 years mulligan Work from today.
(edit) @738   9 years campbell Use lower case names for identifiers for consistency with CompCert?
(edit) @737   9 years campbell Use more abstract identifiers in Clight / RTLabs.
(add) @736   9 years campbell Extra type safety for identifiers.
Note: See TracRevisionLog for help on using the revision log.