

@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.



@750

9 years 
campbell 
Track some of the changes to the prototype in RTLabs.
Just one …



@747

9 years 
campbell 
Merge the two AST files together (although some definitions still need …



@744

9 years 
campbell 
Evict Coqstyle integers from common/Integers.ma.
Make more bitvector …



@738

9 years 
campbell 
Use lower case names for identifiers for consistency with CompCert? …



@737

9 years 
campbell 
Use more abstract identifiers in Clight / RTLabs.



@736

9 years 
campbell 
Extra type safety for identifiers.



@731

9 years 
campbell 
Common definition for animation semantics, and factor out IO definitions.



@729

9 years 
campbell 
Pretty ugly printer for RTLabs programs.



@727

9 years 
campbell 
Enough fixes to let an RTLabs program run.



@726

9 years 
campbell 
Change identifiers to Words in Clight and RTLabs semantics.



@720

9 years 
campbell 
Sort out cost labels.



@718

9 years 
campbell 
Add an AST type (i.e., intermediate language type) for pointers.



@710

9 years 
campbell 
Start of way to import RTLabs from prototype compiler.



@702

9 years 
campbell 
Refine smallstep executable semantics abstraction a little.
Some …



@695

9 years 
campbell 
Rearrange Clight files a bit  will try to make them work again soon…


copied from src/Clight/RTLabs:



@694

9 years 
campbell 
Start moving Clight into common directory.
