|
|
|
@1330
|
9 years |
campbell |
Evict obsolete file.
|
|
|
|
@1321
|
9 years |
sacerdot |
No longer/never implemented files removed.
|
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1296
|
9 years |
mulligan |
changes
|
|
|
|
@1285
|
9 years |
mulligan |
more implementation on maps, final push to get rtl abs to rtl working
|
|
|
|
@1274
|
9 years |
mulligan |
starting removing axioms from adts and giving them proper implementations
|
|
|
|
@1268
|
9 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
|
@1266
|
9 years |
sacerdot |
Added second projection.
|
|
|
|
@1260
|
9 years |
mulligan |
commit for csc
|
|
|
|
@1250
|
9 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
|
@1248
|
9 years |
mulligan |
deleted files that do not compile in utilities, changed ertl.ma to use …
|
|
|
|
@1229
|
9 years |
mulligan |
changes
|
|
|
|
@1227
|
9 years |
mulligan |
changes
|
|
|
|
@1223
|
9 years |
mulligan |
changes
|
|
|
|
@1219
|
9 years |
mulligan |
a little more added
|
|
|
|
@1218
|
9 years |
mulligan |
a lot added to interference graph calculation
|
|
|
|
@1212
|
9 years |
mulligan |
more added on interference graphs
|
|
|
|
@1211
|
9 years |
mulligan |
fixed interference file
|
|
|
|
@1210
|
9 years |
mulligan |
getting rid of typeclass-like records in favour of file-level axioms. …
|
|
|
|
@1209
|
9 years |
mulligan |
more work on int. graphs
|
|
|
|
@1208
|
9 years |
mulligan |
added adts for sets, tables and priority sets in order to make life …
|
|
|
|
@1196
|
9 years |
mulligan |
some more changes, need some additional datastructures
|
|
|
|
@1195
|
9 years |
campbell |
List find function.
|
|
|
|
@1193
|
9 years |
mulligan |
work on colouring algorithm halted as it can be axiomatised. now …
|
|
|
|
@1192
|
9 years |
mulligan |
some files that were missing / laying dormant on my computer
|
|
|
|
@1145
|
9 years |
mulligan |
changed naming in i8051 of classes of registers to make them consistent
|
|
|
|
@1127
|
9 years |
mulligan |
interference graphs axiomatised, more added to ertl
|
|
|
|
@1092
|
9 years |
campbell |
Some minor definitions for identifiers and lists.
|
|
|
|
@1075
|
10 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
|
@1066
|
10 years |
mulligan |
changes from today
|
|
|
|
@1052
|
10 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
|
@1050
|
10 years |
mulligan |
adding dependent types to map datastructure to remove all option …
|
|
|
|
@1049
|
10 years |
mulligan |
more stuff added
|
|
|
|
@1048
|
10 years |
mulligan |
added implementation of haskell associative maps to clean up the mess …
|
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
|
@891
|
10 years |
campbell |
Revise proofs affected by recent matita change.
|
|
|
|
@882
|
10 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
|
@782
|
10 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@780
|
10 years |
campbell |
Properly update set of registers that are used for pointers in Cminor …
|
|
|
|
@778
|
10 years |
mulligan |
moved register set into correct place
|
|
|
|
@766
|
10 years |
campbell |
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …
|
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@747
|
10 years |
campbell |
Merge the two AST files together (although some definitions still need …
|
|
|
|
@746
|
10 years |
mulligan |
Changes to bitvectortrieset: equality on sets. Added new file for …
|
|
|
|
@744
|
10 years |
campbell |
Evict Coq-style integers from common/Integers.ma.
Make more bitvector …
|
|
|
|
@735
|
10 years |
mulligan |
Changes from today
|
|
|
|
@733
|
10 years |
mulligan |
Fixed partial commit.
|
|
|
|
@711
|
10 years |
sacerdot |
…
|
|
|
|
@709
|
10 years |
sacerdot |
Notations should NOT be redefined. Just add a new interpretation.
|
|
|
|
@699
|
10 years |
mulligan |
More or less finished formalisation of LIN.
|
|
|
|
@698
|
10 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
|
@697
|
10 years |
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
|
|
@695
|
10 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
|
|
@691
|
10 years |
mulligan |
More movement of files within the repository.
|
|
copied from Deliverables/D4.2-4.3/utilities:
|
|
|
|
@491
|
10 years |
mulligan |
Initial commit of (part)-formalisation of LIN intermediate language.
|
