

@2601

8 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2390

8 years 
campbell 
Tidy up a corner case when generating RTLabs so that we generate
less …



@2335

8 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2319

8 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2292

8 years 
campbell 
More RTLabs invariants.



@2289

8 years 
campbell 
Update alias



@2287

8 years 
campbell 
RTLabs typing for loads and stores.



@2253

8 years 
campbell 
Cminor to RTLabs is now a total function.



@2252

8 years 
campbell 
Use the return statement invariant. Restructure the invariants for …



@2251

8 years 
campbell 
Add new invariant to Cminor that return typs should be respected.



@2232

8 years 
campbell 
Remove unused block structure in Cminor.



@2178

8 years 
campbell 
Shift some notation into utilities.



@2176

8 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2103

8 years 
campbell 
Make transform_*program take a more general transformation to make …



@2033

8 years 
sacerdot 
Daemon reverted.



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1884

8 years 
campbell 
Syntax changes to fit Paolo's commit.



@1878

8 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1680

9 years 
campbell 
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …



@1631

9 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1626

9 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1611

9 years 
sacerdot 
All of Cminor now compiles with the latest lib of Matita.



@1605

9 years 
sacerdot 
Porting to last standard library of Matita.



@1603

9 years 
sacerdot 
More proofs ported to new lib.



@1599

9 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1521

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



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1464

9 years 
campbell 
Use unification hints to simplify the graph monotonicity proofs.



@1410

9 years 
campbell 
Remove a few old workarounds.



@1369

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



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1224

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



@1139

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



@1072

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



@1070

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



@1056

9 years 
campbell 
Switch to delayed identifier error scheme.



@961

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



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



@881

9 years 
campbell 
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.



@880

9 years 
campbell 
Add type information into Cminor.
As a result, the Clight to Cminor …



@816

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



@797

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



@790

9 years 
campbell 
A little tidying: get rid of requirement for jmeq in Mem.ma, remove …



@780

9 years 
campbell 
Properly update set of registers that are used for pointers in Cminor …



@772

9 years 
campbell 
Implement proper support for RTLabs addressing modes.



@771

9 years 
campbell 
Implement switch statements in Cminor > RTLabs phase



@767

9 years 
campbell 
Use variable shadowing as a poor man's state monad in cminor to rtlabs …



@766

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



@764

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