

@1882

8 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1644

8 years 
tranquil 
minor changes



@1643

8 years 
tranquil 
* some changes in everything
* separated extensions in sequential and …



@1641

8 years 
tranquil 
* semanticsUtils_paolo.ma contains code to generate both graph and …



@1640

8 years 
tranquil 
* finished fork of semantics.ma
* unification of Errors under the …



@1636

8 years 
tranquil 
* added coercions to arguments (in RTL) and notation for ops (for the …



@1635

8 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1601

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



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1481

9 years 
sacerdot 
Proof fixed. The new standard library does not index any longer the …



@1451

9 years 
sacerdot 
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …



@1450

9 years 
sacerdot 
Disambiguation problem avoided.



@1415

9 years 
sacerdot 
1. hwreg_store/retrieve no longer returns a res (but it is still …



@1412

9 years 
sacerdot 
Tailcalls (via ids or pointers) to internal functions implemented. …



@1411

9 years 
sacerdot 
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …



@1408

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



@1396

9 years 
sacerdot 
Proof obligation closed.



@1390

9 years 
sacerdot 
All fetch_result implementations have been factorized out, leaving …



@1388

9 years 
sacerdot 
fetch_result implemented for ERTL. This required a different …



@1386

9 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

9 years 
sacerdot 
1. fetch_result and pop_frame now takes the genv in input
2. …



@1384

9 years 
sacerdot 
* fetch_ra taken out of pop_frame again since it is used uniformly and …



@1381

9 years 
sacerdot 
Old commented out code removed.



@1377

9 years 
sacerdot 
pop_frame now incorporates the fetch_result (that made sense only for …



@1376

9 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@1372

9 years 
sacerdot 
save_frame now takes the stacksize to allow RTL to allocate the stack frame



@1371

9 years 
sacerdot 
save_frame changed to accept also the formal/actual argument pairs, …



@1359

9 years 
sacerdot 
1. more work on the RTL semantics
2. changes to joint/semantics to …



@1352

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



@1348

9 years 
sacerdot 
…



@1326

9 years 
sacerdot 
Code improved (now it uses the high level functions from …



@1324

9 years 
sacerdot 
The semantics of extended statements must also consider the label …



@1322

9 years 
sacerdot 
address => stack_address



@1320

9 years 
sacerdot 
Frame operations implemented.



@1315

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



@1313

9 years 
sacerdot 
(E)RTL semantics ported to new data type for save/pop frame (but not …



@1303

9 years 
sacerdot 
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …



@1301

9 years 
sacerdot 
Axioms regrouped according to their use.



@1300

9 years 
sacerdot 
More (graph) axioms implemented. Look at the comments marked with XXX …



@1299

9 years 
sacerdot 
Functions from RTL/semantics.ma generalized to work on every graph …



@1298

9 years 
sacerdot 
 fetch_statement now takes in input the globalenv
 fetch_statement …



@1295

9 years 
sacerdot 
More progress.



@1294

9 years 
sacerdot 
RTL semantics: porting to joint semantics started.



@1284

9 years 
sacerdot 
Bugs fixed: fresh_label changes the label universe, but this was not …



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



@1280

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



@1278

9 years 
sacerdot 
oppargs requires two more arguments. RTLtoERTL to be fixed since it …



@1275

9 years 
sacerdot 
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …



@1270

9 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1262

9 years 
sacerdot 
RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …



@1259

9 years 
sacerdot 
More progress towards new Joint data type.



@1258

9 years 
sacerdot 
More progress towards porting to joint syntax.



@1257

9 years 
sacerdot 
More progress in porting to joint datatype.



@1254

9 years 
sacerdot 
More progress towards porting of RTLtoERTL to joint syntax.



@1252

9 years 
sacerdot 
graph_params added to joint/Joint.ma, together with useful common …



@1250

9 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1245

9 years 
sacerdot 
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …



@1240

9 years 
sacerdot 
Ported to common definitions.



@1239

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



@1237

9 years 
sacerdot 
Wrong commit repaired.



@1233

9 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1149

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



@1141

9 years 
sacerdot 
Comment (about a bug) added.



@1138

9 years 
mulligan 
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other



@1131

9 years 
mulligan 
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …



@1126

9 years 
sacerdot 
Semantics completed up to initial state creation.



@1122

9 years 
sacerdot 
Internal function call implemented too.



@1121

9 years 
sacerdot 
External function calls implemented (but look at the new comment on …



@1120

9 years 
sacerdot 
All operations implemented.



@1118

9 years 
sacerdot 
All derivatives of St_const implemented (up to axioms to match the two …



@1117

9 years 
sacerdot 
More operations implemented.



@1115

9 years 
sacerdot 
Some comments.



@1114

9 years 
sacerdot 
some more operations implemented



@1113

9 years 
sacerdot 
Semantics (interpreter) of RTL.
The file does not compile yet. I am …



@1107

9 years 
mulligan 
got rtlertl pass working again



@1106

9 years 
mulligan 
changes necessary to get RTLabs>RTL to compile



@1089

9 years 
mulligan 
more changes from earlier in the week



@1081

9 years 
mulligan 
completed rtlertl pass



@1080

9 years 
mulligan 
more added



@1079

9 years 
mulligan 
finished rtl to ertl pass modulo conversion of tailcall simplification code



@1077

9 years 
mulligan 
ack, dependent types are scary



@1076

9 years 
mulligan 
small changes



@1075

9 years 
mulligan 
nearly completed rtl > ertl pass removing all option types with dep. types



@1071

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



@1068

9 years 
mulligan 
rtlabs translation complete subject to axioms



@1066

9 years 
mulligan 
changes from today



@1064

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



@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



@878

9 years 
campbell 
Removal of manually inserted record projections.



@784

9 years 
mulligan 
Added missing tailcall simplification file.



@783

9 years 
mulligan 
rtl to ertl pass complete (modulo some straightforward axioms that …



@782

9 years 
mulligan 
More work on rtlertl pass from today, plus resolved conflict.



@777

9 years 
mulligan 
Lots of work on RTL to ERTL pass from today.



@763

9 years 
mulligan 
Changes to RTLERTL pass.



@759

9 years 
mulligan 
More work on the RTL to ERTL pass.



@756

9 years 
mulligan 
Made a start on RTL. Renaming in ERTL and below to move closer to …



@754

9 years 
mulligan 
Syntax of RTL.
