|
|
|
@2946
|
7 years |
tranquil |
main novelties:
* there is an in-built stack_usage nat in joint …
|
|
|
|
@2767
|
7 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|
|
@2763
|
7 years |
sacerdot |
All daemons in compiler.ma closed (i.e. proof obligations added
to the …
|
|
|
|
@2760
|
7 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
|
@2754
|
7 years |
sacerdot |
1. WARNING: I commented out one of James's function used in …
|
|
|
|
@2708
|
7 years |
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
|
|
|
@2490
|
7 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
|
@2443
|
7 years |
tranquil |
changed joint's stack pointer and internal stack
|
|
|
|
@2286
|
8 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@1995
|
8 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
|
@1522
|
8 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
|
@1520
|
8 years |
campbell |
Generate cost labels with correct type.
|
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1379
|
8 years |
sacerdot |
Invariant on LIN code removed. In Paris it was decided that a simpler …
|
|
|
|
@1282
|
9 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@1275
|
9 years |
sacerdot |
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …
|
|
|
|
@1270
|
9 years |
sacerdot |
Making RTL syntax an instance of Joint.
|
|
|
|
@1268
|
9 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
|
@1264
|
9 years |
sacerdot |
Almost ported to new Joint syntax.
|
|
|
|
@1245
|
9 years |
sacerdot |
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
|
|
|
|
@1179
|
9 years |
mulligan |
changes to ertl, ltl and lin to use new notion of joint params. ertl …
|
|
|
|
@1168
|
9 years |
sacerdot |
Joint statements parameterized over a record.
|
|
|
|
@1149
|
9 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
|
@1112
|
9 years |
mulligan |
got lin > asm stuff working
|
|
|
|
@757
|
9 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@734
|
9 years |
mulligan |
Fixed lin2asm.
|
|
|
|
@723
|
9 years |
mulligan |
Added dependent type internalising the invariant that LIN function …
|
|
|
|
@722
|
9 years |
mulligan |
Committing changes from today. Several files do not typecheck.
|
|
|
|
@699
|
9 years |
mulligan |
More or less finished formalisation of LIN.
|
|
|
|
@698
|
9 years |
mulligan |
Commit with changes to files to get our files to typecheck.
|
|
|
|
@696
|
9 years |
mulligan |
Added missing I8051 file and completed most of LIN formalisation.
|
|
|
|
@691
|
9 years |
mulligan |
More movement of files within the repository.
|
|
copied from Deliverables/D4.2-4.3/LINToASM.ma:
|
|
|
|
@687
|
9 years |
mulligan |
Renamed to enforce consistency of filenames
|
