|
|
@1612
|
9 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
@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
|
10 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
@1358
|
10 years |
mulligan |
got rtlabs to rtl compiling, foldi_strong needs examining
|
|
|
@1356
|
10 years |
mulligan |
deleted redundant directory. added outlines for both reports, and …
|
|
|
@1354
|
10 years |
sacerdot |
One axiom closed.
|
|
|
@1352
|
10 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
@1343
|
10 years |
mulligan |
fixed some bugs in the translation
|
|
|
@1331
|
10 years |
mulligan |
some changes, but i now have two contradictory proof obligations.
|
|
|
@1325
|
10 years |
mulligan |
finished implementing the translate constant function
|
|
|
@1316
|
10 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
@1315
|
10 years |
mulligan |
another move for the same reason. got rtlabs > rtl compiling again by …
|
|
|
@1314
|
10 years |
mulligan |
name changes so that bash tab completion actually works with some …
|
|
|
@1308
|
10 years |
mulligan |
changes to translate_cst
|
|
|
@1307
|
10 years |
mulligan |
adding translate_cst
|
|
|
@1306
|
10 years |
mulligan |
small changes to rtlabs. what axioms remain look hard to close. need …
|
|
|
@1296
|
10 years |
mulligan |
changes
|
|
|
@1293
|
10 years |
mulligan |
finished rtl abs to rtl transformation subject to closing some axioms …
|
|
|
@1292
|
10 years |
mulligan |
more added to rtlabs translation
|
|
|
@1290
|
10 years |
sacerdot |
One more function ported to new Joint.
|
|
|
@1288
|
10 years |
mulligan |
more added to rtlabs to rtl pass
|
|
|
@1287
|
10 years |
mulligan |
about 3/4 of the way through rtlabs to rtl now
|
|
|
@1286
|
10 years |
mulligan |
more changes to the rtl abs to rtl pass
|
|
|
@1285
|
10 years |
mulligan |
more implementation on maps, final push to get rtl abs to rtl working
|
|
|
@1283
|
10 years |
sacerdot |
Bad programming practice removed: change_label is no longer required …
|
|
|
@1282
|
10 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
@1281
|
10 years |
sacerdot |
Porting of all transformation to the joint syntax practically …
|
|
|
@1280
|
10 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
|
|
@1239
|
10 years |
sacerdot |
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …
|
|
|
@1238
|
10 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
@1226
|
10 years |
campbell |
Adjust pretty printers for change in program records, try a test of each.
|
|
|
@1224
|
10 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
@1157
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
@1149
|
10 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
@1147
|
10 years |
campbell |
Remove some obsolete commented out code, update a couple of comments.
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
@1138
|
10 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
@1123
|
10 years |
sacerdot |
Added comment about missing alignment of data in memory.
|
|
|
@1116
|
10 years |
sacerdot |
Some comments.
|
|
|
@1077
|
10 years |
mulligan |
ack, dependent types are scary
|
|
|
@1073
|
10 years |
mulligan |
more changes from today
|
|
|
@1072
|
10 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
@1070
|
10 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
@1068
|
10 years |
mulligan |
rtlabs translation complete subject to axioms
|
|
|
@1067
|
10 years |
mulligan |
more smaller changes
|
|
|
@1066
|
10 years |
mulligan |
changes from today
|
|
|
@1064
|
10 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
@1063
|
10 years |
mulligan |
changes from today
|
|
|
@1062
|
10 years |
mulligan |
separated jmeq and coercions from foldstuff.ma in order to fix the …
|
|
|
@1061
|
10 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
@1060
|
10 years |
mulligan |
work from this morning and yesterday
|
|
|
@1059
|
10 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
@1057
|
10 years |
mulligan |
changes from today
|
|
|
@1056
|
10 years |
campbell |
Switch to delayed identifier error scheme.
|
|
|
@1053
|
10 years |
mulligan |
changes
|
|
|
@1052
|
10 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
@1051
|
10 years |
mulligan |
removed superfluous addressing mode code from RTLabs/syntax.ma
|
|
|
@1050
|
10 years |
mulligan |
adding dependent types to map datastructure to remove all option …
|
|
|
@1049
|
10 years |
mulligan |
more stuff added
|
|
|
@1047
|
10 years |
mulligan |
more work from today
|
|
|
@1046
|
10 years |
mulligan |
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
|
|
|
@1045
|
10 years |
mulligan |
resolved conflict in rtlabs
|
|
|
@967
|
10 years |
campbell |
Update RTLabs pretty printer and examples.
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@898
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
@888
|
10 years |
campbell |
Use simplified conditionals in RTLabs, following the prototype.
|
|
|
@887
|
10 years |
campbell |
Start bringing RTLabs into line with the prototype compiler:
- a …
|
|
|
@882
|
10 years |
campbell |
Fix up fragile proofs for current version of matita.
|
|
|
@879
|
10 years |
campbell |
Refine "AST" types to include size/signedness information.
|
|
|
@878
|
10 years |
campbell |
Removal of manually inserted record projections.
|
|
|
@816
|
10 years |
campbell |
Clight to Cminor compilation, modulo switch statements, temporary …
|
|
|
@799
|
10 years |
mulligan |
more changes.
|
|
|
@797
|
10 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
@795
|
10 years |
mulligan |
Changes from this morning.
|
|
|
@793
|
10 years |
mulligan |
Work from today on rtlabs -> rtl pass.
|
|
|
@789
|
10 years |
mulligan |
More work on rtlabs -> rtl pass.
|
|
|
@775
|
10 years |
campbell |
A few useful definitions for when RTLabs programs fail.
|
|
|
@774
|
10 years |
campbell |
Separate out the different forms of addition and subtraction in the …
|
|
|
@766
|
10 years |
campbell |
Most of the Cminor to RTLabs stage.
Is buggy, generates inefficient …
|
|
|
@765
|
10 years |
campbell |
Remove superfluous register in RTLabs return statements.
Also fix up …
|
|
|
@764
|
10 years |
campbell |
Start Cminor to RTLabs phase.
Includes some syntax for matching …
|
|
|
@762
|
10 years |
campbell |
Make naming of RTLabs files more uniform
|
|
|
@761
|
10 years |
campbell |
Enforce the use of declared identifiers/registers in Cminor/RTLabs.
|
|
|