|
|
|
@2949
|
7 years |
sacerdot |
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …
|
|
|
|
@2897
|
7 years |
campbell |
Minor tidying.
|
|
|
|
@2824
|
7 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
|
@2800
|
7 years |
campbell |
Tidy up Measurable.ma a little, get rid of obsolete comments.
|
|
|
|
@2796
|
7 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
|
@2772
|
7 years |
sacerdot |
Useless code removed.
|
|
|
|
@2770
|
7 years |
mckinna |
WARNING: another big commit, touching many files in ASM/*.ma
This …
|
|
|
|
@2767
|
7 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|
|
@2732
|
7 years |
sacerdot |
Unused code removed.
|
|
|
|
@2728
|
7 years |
sacerdot |
listb.ma => listb_extra.ma for extraction
|
|
|
|
@2716
|
7 years |
sacerdot |
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
|
|
|
|
@2708
|
7 years |
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
|
|
|
@2700
|
7 years |
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
|
|
@2670
|
7 years |
campbell |
Clean up from recent commits.
|
|
|
|
@2601
|
7 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2529
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
|
@2453
|
8 years |
tranquil |
come changes in monad notation to
* avoid pretty printed monsters
* …
|
|
|
|
@2443
|
8 years |
tranquil |
changed joint's stack pointer and internal stack
|
|
|
|
@2440
|
8 years |
piccolo |
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)
|
|
|
|
@2314
|
8 years |
campbell |
Move generic definitions from recent commit to appropriate places.
|
|
|
|
@2310
|
8 years |
garnier |
Moved a lemma from switchRemoval to positive.
|
|
|
|
@2309
|
8 years |
garnier |
Removed the superfluous xorb definition and move some basic properties …
|
|
|
|
@2306
|
8 years |
campbell |
An insertion sort for testing purposes.
|
|
|
|
@2296
|
8 years |
campbell |
Tidy up some ill-placed definitions.
|
|
|
|
@2292
|
8 years |
campbell |
More RTLabs invariants.
|
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2200
|
8 years |
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
|
|
@2179
|
8 years |
campbell |
Dependent pair monad binding notation.
|
|
|
|
@2178
|
8 years |
campbell |
Shift some notation into utilities.
|
|
|
|
@2174
|
8 years |
tranquil |
* factored out script for (axiomatised) fixpoint computation
* ERTL → …
|
|
|
|
@2155
|
8 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2101
|
8 years |
boender |
- renamed medium to absolute jump
- revised proofs of policy, some …
|
|
|
|
@2006
|
8 years |
boender |
- added alias for bitvector zero
- changed extralib bounded …
|
|
|
|
@1976
|
8 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
|
@1949
|
8 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1930
|
8 years |
campbell |
Tidy up labelling simulation stuff a bit.
|
|
|
|
@1908
|
8 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1648
|
8 years |
mulligan |
new version of utilities/monad.ma with typecheck command comented out
|
|
|
|
@1647
|
8 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
|
@1640
|
8 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1636
|
8 years |
tranquil |
* added coercions to arguments (in RTL) and notation for ops (for the …
|
|
|
|
@1635
|
8 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1631
|
9 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1630
|
9 years |
campbell |
Remainder of freshness in Clight to Cminor pass.
|
|
|
|
@1628
|
9 years |
campbell |
Show that the universe generated by Clight/fresh.ma is good.
|
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1600
|
9 years |
sacerdot |
utilities and ASM ported to the new standard library
|
|
|
|
@1599
|
9 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1598
|
9 years |
mulligan |
changes over the last couple of days
|
|
|
|
@1593
|
9 years |
boender |
- cleaned up Assembly, moved some definitions elsewhere
|
|
|
|
@1587
|
9 years |
mulligan |
changes from today, including removing indexing of problematic …
|
|
|
|
@1551
|
9 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
|
@1528
|
9 years |
campbell |
Update most of Assembly.ma with new syntax and identifier maps.
Change …
|
|
|
|
@1523
|
9 years |
campbell |
Separate out positive and Z definitions from extralib.ma.
Minor syntax …
|
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1517
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1516
|
9 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1463
|
9 years |
mulligan |
added erasure for lin
|
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
|
@1351
|
9 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
|
@1350
|
9 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1341
|
9 years |
sacerdot |
Empty directory removed.
|
|
|
|
@1338
|
9 years |
sacerdot |
Automation is now stronger.
|
|
|
|
@1337
|
9 years |
sacerdot |
Automation is now stronger.
|
|
|
|
@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
|
9 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
|
@1066
|
9 years |
mulligan |
changes from today
|
|
|
|
@1052
|
9 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
|
@1050
|
9 years |
mulligan |
adding dependent types to map datastructure to remove all option …
|
|
|
|
@1049
|
9 years |
mulligan |
more stuff added
|
|
|
|
@1048
|
9 years |
mulligan |
added implementation of haskell associative maps to clean up the mess …
|
|
|
|
