|
|
|
@1295
|
8 years |
sacerdot |
More progress.
|
|
|
|
@1294
|
8 years |
sacerdot |
RTL semantics: porting to joint semantics started.
|
|
|
|
@1284
|
8 years |
sacerdot |
Bugs fixed: fresh_label changes the label universe, but this was not …
|
|
|
|
@1283
|
8 years |
sacerdot |
Bad programming practice removed: change_label is no longer required …
|
|
|
|
@1282
|
8 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@1280
|
8 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
|
|
|
@1278
|
8 years |
sacerdot |
oppargs requires two more arguments. RTLtoERTL to be fixed since it …
|
|
|
|
@1275
|
8 years |
sacerdot |
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …
|
|
|
|
@1270
|
8 years |
sacerdot |
Making RTL syntax an instance of Joint.
|
|
|
|
@1262
|
8 years |
sacerdot |
RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …
|
|
|
|
@1259
|
8 years |
sacerdot |
More progress towards new Joint data type.
|
|
|
|
@1258
|
8 years |
sacerdot |
More progress towards porting to joint syntax.
|
|
|
|
@1257
|
8 years |
sacerdot |
More progress in porting to joint datatype.
|
|
|
|
@1254
|
8 years |
sacerdot |
More progress towards porting of RTLtoERTL to joint syntax.
|
|
|
|
@1252
|
8 years |
sacerdot |
graph_params added to joint/Joint.ma, together with useful common …
|
|
|
|
@1250
|
8 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
|
@1245
|
8 years |
sacerdot |
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
|
|
|
|
@1240
|
8 years |
sacerdot |
Ported to common definitions.
|
|
|
|
@1239
|
8 years |
sacerdot |
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …
|
|
|
|
@1237
|
8 years |
sacerdot |
Wrong commit repaired.
|
|
|
|
@1233
|
8 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
|
@1149
|
8 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
|
@1141
|
8 years |
sacerdot |
Comment (about a bug) added.
|
|
|
|
@1138
|
8 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
|
@1131
|
8 years |
mulligan |
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
|
|
|
|
@1126
|
8 years |
sacerdot |
Semantics completed up to initial state creation.
|
|
|
|
@1122
|
8 years |
sacerdot |
Internal function call implemented too.
|
|
|
|
@1121
|
8 years |
sacerdot |
External function calls implemented (but look at the new comment on …
|
|
|
|
@1120
|
8 years |
sacerdot |
All operations implemented.
|
|
|
|
@1118
|
8 years |
sacerdot |
All derivatives of St_const implemented (up to axioms to match the two …
|
|
|
|
@1117
|
8 years |
sacerdot |
More operations implemented.
|
|
|
|
@1115
|
8 years |
sacerdot |
Some comments.
|
|
|
|
@1114
|
8 years |
sacerdot |
some more operations implemented
|
|
|
|
@1113
|
8 years |
sacerdot |
Semantics (interpreter) of RTL.
The file does not compile yet. I am …
|
|
|
|
@1107
|
8 years |
mulligan |
got rtl-ertl pass working again
|
|
|
|
@1106
|
8 years |
mulligan |
changes necessary to get RTLabs->RTL to compile
|
|
|
|
@1089
|
8 years |
mulligan |
more changes from earlier in the week
|
|
|
|
@1081
|
9 years |
mulligan |
completed rtl-ertl pass
|
|
|
|
@1080
|
9 years |
mulligan |
more added
|
|
|
|
@1079
|
9 years |
mulligan |
finished rtl to ertl pass modulo conversion of tailcall simplification code
|
|
|
|
@1077
|
9 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1076
|
9 years |
mulligan |
small changes
|
|
|
|
@1075
|
9 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
|
@1071
|
9 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
@1068
|
9 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
|
@1066
|
9 years |
mulligan |
changes from today
|
|
|
|
@1064
|
9 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
|
@1061
|
9 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
|
@1060
|
9 years |
mulligan |
work from this morning and yesterday
|
|
|
|
@878
|
9 years |
campbell |
Removal of manually inserted record projections.
|
|
|
|
@784
|
9 years |
mulligan |
Added missing tailcall simplification file.
|
|
|
|
@783
|
9 years |
mulligan |
rtl to ertl pass complete (modulo some straightforward axioms that …
|
|
|
|
@782
|
9 years |
mulligan |
More work on rtl-ertl pass from today, plus resolved conflict.
|
|
|
|
@777
|
9 years |
mulligan |
Lots of work on RTL to ERTL pass from today.
|
|
|
|
@763
|
9 years |
mulligan |
Changes to RTL-ERTL pass.
|
|
|
|
@759
|
9 years |
mulligan |
More work on the RTL to ERTL pass.
|
|
|
|
@756
|
9 years |
mulligan |
Made a start on RTL. Renaming in ERTL and below to move closer to …
|
|
|
|
@754
|
9 years |
mulligan |
Syntax of RTL.
|
