source: src/RTLabs/RTLAbstoRTL.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @1296   8 years mulligan changes
(edit) @1293   8 years mulligan finished rtl abs to rtl transformation subject to closing some axioms …
(edit) @1292   8 years mulligan more added to rtlabs translation
(edit) @1290   8 years sacerdot One more function ported to new Joint.
(edit) @1288   8 years mulligan more added to rtlabs to rtl pass
(edit) @1287   8 years mulligan about 3/4 of the way through rtlabs to rtl now
(edit) @1286   8 years mulligan more changes to the rtl abs to rtl pass
(edit) @1285   8 years mulligan more implementation on maps, final push to get rtl abs to rtl working
(edit) @1283   8 years sacerdot Bad programming practice removed: change_label is no longer required …
(edit) @1282   8 years sacerdot Cosmetic change: names of joint statements/instructions shortened and …
(edit) @1281   8 years sacerdot Porting of all transformation to the joint syntax practically …
(edit) @1280   8 years sacerdot Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) …
(edit) @1239   8 years sacerdot RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is …
(edit) @1224   8 years sacerdot Type of programs in common/AST made more dependent. In particular, the …
(edit) @1149   8 years mulligan changes to get everything type checking again after changing names of …
(edit) @1138   8 years mulligan merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
(edit) @1077   8 years mulligan ack, dependent types are scary
(edit) @1073   8 years mulligan more changes from today
(edit) @1071   8 years mulligan changes the specific form that the added proofs take to use None, not …
(edit) @1068   8 years mulligan rtlabs translation complete subject to axioms
(edit) @1067   8 years mulligan more smaller changes
(edit) @1066   8 years mulligan changes from today
(edit) @1064   8 years mulligan changes from today, nearly complete rtlabs translation pass
(edit) @1063   8 years mulligan changes from today
(edit) @1062   8 years mulligan separated jmeq and coercions from foldstuff.ma in order to fix the …
(edit) @1061   8 years mulligan more work, bug found, ridiculous map3 function with dep. types added
(edit) @1060   8 years mulligan work from this morning and yesterday
(edit) @1059   8 years mulligan work from today, bit of a mess at the moment
(edit) @1057   8 years mulligan changes from today
(edit) @1053   8 years mulligan changes
(edit) @1052   8 years mulligan removed offsets after reading cerco mailing list
(edit) @1050   8 years mulligan adding dependent types to map datastructure to remove all option …
(edit) @1049   8 years mulligan more stuff added
(edit) @1047   8 years mulligan more work from today
(edit) @1046   8 years mulligan syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
(edit) @1045   8 years mulligan resolved conflict in rtlabs
(edit) @799   9 years mulligan more changes.
(edit) @795   9 years mulligan Changes from this morning.
(edit) @793   9 years mulligan Work from today on rtlabs -> rtl pass.
(add) @789   9 years mulligan More work on rtlabs -> rtl pass.
Note: See TracRevisionLog for help on using the revision log.