|
|
|
@334
|
10 years |
mulligan |
More added.
|
|
|
|
@333
|
10 years |
mulligan |
Work on execute_1 function.
|
|
|
|
@332
|
10 years |
sacerdot |
Code of fetch greatly simplified because of better behaviour of Matita.
|
|
|
|
@331
|
10 years |
mulligan |
More changes to get everything to typecheck.
|
|
|
|
@330
|
10 years |
mulligan |
Fixed segmentation fault in Nat.ma, added get_index and renamed …
|
|
|
|
@329
|
10 years |
mulligan |
Commit to restore deleted file.
|
|
|
|
@328
|
10 years |
mulligan |
Got fold_right_i to type check. Moved eq_rect_Type0 into …
|
|
|
|
@327
|
10 years |
sacerdot |
Completed!
|
|
|
|
@326
|
10 years |
sacerdot |
Almost compiling.
|
|
|
|
@325
|
10 years |
sacerdot |
Almost finished.
|
|
|
|
@324
|
10 years |
sacerdot |
It starts working…
|
|
|
|
@323
|
10 years |
sacerdot |
…
|
|
|
|
@322
|
10 years |
sacerdot |
More work on fetch.
|
|
|
|
@320
|
10 years |
mulligan |
Added fold_right_i, equivalent of O'Caml's fold_right2.
|
|
|
|
@319
|
10 years |
sacerdot |
…
|
|
|
|
@318
|
10 years |
sacerdot |
First version: to be debugged.
|
|
|
|
@317
|
10 years |
mulligan |
Fixed problems with arguments of register change.
|
|
|
|
@316
|
10 years |
sacerdot |
REGISTER now takes a BitVector? 3
|
|
|
|
@315
|
10 years |
mulligan |
Decidable equality on vectors and its specialisation to bitvectors.
|
|
|
|
@314
|
10 years |
mulligan |
Finished all get_ and set_arg_* functions.
|
|
|
|
@313
|
10 years |
mulligan |
Added axioms for addition for claudio.
|
|
|
|
@312
|
10 years |
sacerdot |
arguments of split reversed
|
|
|
|
@311
|
10 years |
mulligan |
get_arg_16 complete.
|
|
|
|
@310
|
10 years |
mulligan |
Most of get_arg_16 done.
|
|
|
|
@309
|
10 years |
sacerdot |
assembly1 is finally compiling in about 37s!
|
|
|
|
@308
|
10 years |
sacerdot |
More explicit typing solves one of the points.
|
|
|
|
@307
|
10 years |
sacerdot |
assembly1 completed, but two cases commented out since they require …
|
|
|
|
@306
|
10 years |
sacerdot |
…
|
|
|
|
@305
|
10 years |
sacerdot |
…
|
|
|
|
@304
|
10 years |
sacerdot |
…
|
|
|
|
@303
|
10 years |
sacerdot |
…
|
|
|
|
@302
|
10 years |
sacerdot |
…
|
|
|
|
@301
|
10 years |
sacerdot |
…
|
|
|
|
@300
|
10 years |
sacerdot |
…
|
|
|
|
@299
|
10 years |
sacerdot |
…
|
|
|
|
@298
|
10 years |
sacerdot |
…
|
|
|
|
@297
|
10 years |
sacerdot |
…
|
|
|
|
@296
|
10 years |
sacerdot |
…
|
|
|
|
@294
|
10 years |
mulligan |
get and set_arg_16 implemented.
|
|
|
|
@293
|
10 years |
sacerdot |
…
|
|
|
|
@290
|
10 years |
mulligan |
Moved definitions around so related are grouped together.
|
|
|
|
@289
|
10 years |
mulligan |
Writing at stack pointer implemented.
|
|
|
|
@288
|
10 years |
mulligan |
Set flags implemented.
|
|
|
|
@287
|
10 years |
mulligan |
Reading at stack pointer added.
|
|
|
|
@286
|
10 years |
mulligan |
Added bit address lookup for registers.
|
|
|
|
@285
|
10 years |
mulligan |
Get and set for bitaddressable SFRs now completed.
|
|
|
|
@284
|
10 years |
sacerdot |
…
|
|
|
|
@283
|
10 years |
sacerdot |
Bug fixed in type declaration of BIT/N_BIT.
|
|
|
|
@282
|
10 years |
sacerdot |
…
|
|
|
|
@281
|
10 years |
mulligan |
Resolved conflicts.
|
|
|
|
@280
|
10 years |
sacerdot |
Bug fixed in assemblying AJMP.
|
|
|
|
@279
|
10 years |
sacerdot |
Notation moved to Cartesian.
|
|
|
|
@278
|
10 years |
sacerdot |
More curryfication.
|
|
|
|
@277
|
10 years |
sacerdot |
Bugs fixed in definition of sub8_with_carrier.
|
|
|
|
@276
|
10 years |
mulligan |
Messed up a file.
|
|
|
|
@275
|
10 years |
mulligan |
Removed all axioms from Arithmetic.ma and replaced them with …
|
|
|
|
@274
|
10 years |
mulligan |
First attempt at sub8_with_c complete.
|
|
|
|
@273
|
10 years |
mulligan |
Some fault functions were rewritten.
|
|
|
|
@272
|
10 years |
mulligan |
Changes from this morning.
|
|
|
|
@271
|
10 years |
sacerdot |
assembly1 defined on ACALL and ADD: it seems it will become too slow…
|
|
|
|
@270
|
10 years |
mulligan |
More added.
|
|
|
|
@269
|
10 years |
sacerdot |
- …
|
|
|
|
@268
|
10 years |
sacerdot |
- notation moved to proper places
- new function split on Vectors
|
|
|
|
@267
|
10 years |
mulligan |
Renamed Interpret to Status.
|
|
|
|
@266
|
10 years |
mulligan |
Changes to bitvector.
|
|
|
|
@265
|
10 years |
mulligan |
Test commit.
|
|
|
|
@264
|
10 years |
sacerdot |
- new axiomatic data type for Strings
- new file for Assembly
|
|
|
|
@263
|
10 years |
sacerdot |
- use standard notation for exponential
- Bit is now Bool
|
|
|
|
@262
|
10 years |
sacerdot |
- new notation ...? for vectors to reduce ambiguity
- …
|
|
|
|
@261
|
10 years |
mulligan |
Strengthened typings of get_ and set_index in Vector file.
|
|
|
|
@260
|
10 years |
sacerdot |
- Minimal changes to make it compile with the standard distribution of …
|
|
|
|
@259
|
10 years |
mulligan |
Need stronger set_ and get_index functions on vectors (current ones …
|
|
|
|
@258
|
10 years |
mulligan |
Forgotten files.
|
|
|
|
@257
|
10 years |
mulligan |
Added exponential functions for nats. Working on operational …
|
|
|
|
@256
|
10 years |
mulligan |
Work on ASM.ma file.
|
|
|
|
@249
|
10 years |
mulligan |
More work on defining fundamental datatypes.
|
|
|
|
@248
|
10 years |
mulligan |
More changes. Added datatype for addressing modes.
|
|
|
|
@247
|
10 years |
mulligan |
Changes to get directory to compile.
|
|
|
|
@246
|
10 years |
mulligan |
Added physical file (Arithmetic) for arithmetic on bit vectors, and …
|
|
|
|
@244
|
10 years |
mulligan |
Vector.ma now compiles.
|
|
|
|
@243
|
10 years |
mulligan |
Updated Util.ma too.
|
|
|
|
@242
|
10 years |
mulligan |
Got List to compile.
|
|
|
|
@241
|
10 years |
mulligan |
Also needed an updated List.ma.
|
|
|
|
@240
|
10 years |
mulligan |
Updated Vector / BitVector? files taken from my Matita library.
|
|
|
|
@238
|
10 years |
mulligan |
More work on bitvectors.
|
|
|
|
@237
|
10 years |
mulligan |
More functions on bitvectors written.
|
|
|
|
@236
|
10 years |
mulligan |
Strange problem with matita and the Maybe file? Cannot find Maybe.ng.
|
|
|
|
@235
|
10 years |
mulligan |
More work on bitvectors.
|
|
|
|
@234
|
10 years |
mulligan |
Division and modulus implemented. All necessary orders on naturals …
|
|
|
|
@233
|
10 years |
mulligan |
Changes from this morning: Bool / Prop division = nightmare.
|
|
|
|
@232
|
10 years |
mulligan |
Lots of work from today. Writing bitvector library is harder than it …
|
|
|
|
@231
|
10 years |
mulligan |
BitVector? stuff from this morning: need further development of Nat …
|
|
|
|
@230
|
10 years |
mulligan |
Lots of work from today.
|
|
|
|
@229
|
10 years |
mulligan |
More changes.
|
|
|
|
@228
|
10 years |
mulligan |
Conjunction, disjunction and 'xorjunction' implemented on bitvectors. …
|
|
|
|
@224
|
10 years |
mulligan |
Changes to bit vectors and vectors.
|
|
|
|
@223
|
10 years |
mulligan |
File for bitvector specific stuff added.
|
|
|
|
@222
|
10 years |
mulligan |
Datatype for fixed length lists (vectors) as well as some recursive …
|
|
|
|
@221
|
10 years |
mulligan |
Starting formalisation in Matita
|
|
|
|
@220
|
10 years |
mulligan |
Started on timer 2 capture mode.
|
|
|
|
