

@1601

9 years 
sacerdot 
Files ported to new version of the standard library.



@1596

9 years 
campbell 
RTLabs structured traces: sort out passing of termination proofs around.



@1595

9 years 
campbell 
We don't need an explicit termination count when building traces.



@1594

9 years 
campbell 
Rework handling of termination information in RTLabs structured traces …



@1586

9 years 
campbell 
RTLabs structured traces: cost labels after jumps.



@1583

9 years 
campbell 
More on RTLabs structured traces.
Fixed mistake in structure trace …



@1574

9 years 
campbell 
A little more progress on traces on RTLabs.



@1565

9 years 
campbell 
Note that RTLabs ought to classify branches as "jumps" (in the …



@1563

9 years 
campbell 
A little progress on constructing RTLabs structured traces.



@1559

9 years 
campbell 
Add a notion of flat traces with evidence for RTLabs.



@1552

9 years 
campbell 
Update RTLabs structured trace definition.



@1537

9 years 
campbell 
A preliminary definition of the abstract status record for RTLabs.



@1535

9 years 
campbell 
Make RTLabs semantics use knowledge that the next instruction always …



@1529

9 years 
campbell 
Update RTLabs to RTL with unary operation types.



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1408

9 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1369

9 years 
campbell 
Put type information into frontend unary ops.
Slight change to …



@1358

9 years 
mulligan 
got rtlabs to rtl compiling, foldi_strong needs examining



@1356

9 years 
mulligan 
deleted redundant directory. added outlines for both reports, and …



@1354

9 years 
sacerdot 
One axiom closed.



@1352

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1343

9 years 
mulligan 
fixed some bugs in the translation



@1331

9 years 
mulligan 
some changes, but i now have two contradictory proof obligations.



@1325

9 years 
mulligan 
finished implementing the translate constant function



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1315

9 years 
mulligan 
another move for the same reason. got rtlabs > rtl compiling again by …



@1314

9 years 
mulligan 
name changes so that bash tab completion actually works with some …



@1308

9 years 
mulligan 
changes to translate_cst



@1307

9 years 
mulligan 
adding translate_cst



@1306

9 years 
mulligan 
small changes to rtlabs. what axioms remain look hard to close. need …



@1296

9 years 
mulligan 
changes



@1293

9 years 
mulligan 
finished rtl abs to rtl transformation subject to closing some axioms …



@1292

9 years 
mulligan 
more added to rtlabs translation



@1290

9 years 
sacerdot 
One more function ported to new Joint.



@1288

9 years 
mulligan 
more added to rtlabs to rtl pass



@1287

9 years 
mulligan 
about 3/4 of the way through rtlabs to rtl now



@1286

9 years 
mulligan 
more changes to the rtl abs to rtl pass



@1285

9 years 
mulligan 
more implementation on maps, final push to get rtl abs to rtl working



@1283

9 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

9 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1281

9 years 
sacerdot 
Porting of all transformation to the joint syntax practically …



@1280

9 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …



@1239

9 years 
sacerdot 
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …



@1238

9 years 
campbell 
Update Cminor and RTLabs to fit SmallstepExec? changes.



@1226

9 years 
campbell 
Adjust pretty printers for change in program records, try a test of each.



@1224

9 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1157

9 years 
campbell 
Update pretty printers and examples.



@1149

9 years 
mulligan 
changes to get everything type checking again after changing names of …



@1147

9 years 
campbell 
Remove some obsolete commented out code, update a couple of comments.



@1139

9 years 
campbell 
Shift init_data out of generic program record so that it only appears …



@1138

9 years 
mulligan 
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other



@1123

9 years 
sacerdot 
Added comment about missing alignment of data in memory.



@1116

9 years 
sacerdot 
Some comments.



@1077

9 years 
mulligan 
ack, dependent types are scary



@1073

9 years 
mulligan 
more changes from today



@1072

9 years 
campbell 
Use not equals form of showing entry/exit labels.



@1071

9 years 
mulligan 
changes the specific form that the added proofs take to use None, not …



@1070

9 years 
campbell 
Show that entry and exit labels are in the RTLabs graph.



@1068

9 years 
mulligan 
rtlabs translation complete subject to axioms



@1067

9 years 
mulligan 
more smaller changes



@1066

9 years 
mulligan 
changes from today



@1064

9 years 
mulligan 
changes from today, nearly complete rtlabs translation pass



@1063

9 years 
mulligan 
changes from today



@1062

9 years 
mulligan 
separated jmeq and coercions from foldstuff.ma in order to fix the …



@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



@1059

9 years 
mulligan 
work from today, bit of a mess at the moment



@1057

9 years 
mulligan 
changes from today



@1056

9 years 
campbell 
Switch to delayed identifier error scheme.



@1053

9 years 
mulligan 
changes



@1052

9 years 
mulligan 
removed offsets after reading cerco mailing list



@1051

9 years 
mulligan 
removed superfluous addressing mode code from RTLabs/syntax.ma



@1050

9 years 
mulligan 
adding dependent types to map datastructure to remove all option …



@1049

9 years 
mulligan 
more stuff added



@1047

9 years 
mulligan 
more work from today



@1046

9 years 
mulligan 
syntax of rtlabs was wrong: cast not const. more added to rtlabs > …



@1045

9 years 
mulligan 
resolved conflict in rtlabs



@967

9 years 
campbell 
Update RTLabs pretty printer and examples.



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@898

9 years 
campbell 
Update pretty printers and examples.



@888

9 years 
campbell 
Use simplified conditionals in RTLabs, following the prototype.



@887

9 years 
campbell 
Start bringing RTLabs into line with the prototype compiler:
 a …



@882

9 years 
campbell 
Fix up fragile proofs for current version of matita.



@879

9 years 
campbell 
Refine "AST" types to include size/signedness information.



@878

9 years 
campbell 
Removal of manually inserted record projections.



@816

9 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …



@799

9 years 
mulligan 
more changes.



@797

9 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@795

9 years 
mulligan 
Changes from this morning.



@793

9 years 
mulligan 
Work from today on rtlabs > rtl pass.



@789

9 years 
mulligan 
More work on rtlabs > rtl pass.



@775

9 years 
campbell 
A few useful definitions for when RTLabs programs fail.



@774

9 years 
campbell 
Separate out the different forms of addition and subtraction in the …



@766

9 years 
campbell 
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …



@765

9 years 
campbell 
Remove superfluous register in RTLabs return statements.
Also fix up …



@764

9 years 
campbell 
Start Cminor to RTLabs phase.
Includes some syntax for matching …



@762

9 years 
campbell 
Make naming of RTLabs files more uniform



@761

9 years 
campbell 
Enforce the use of declared identifiers/registers in Cminor/RTLabs.



@751

9 years 
campbell 
Initial version of the Cminor syntax and semantics.


