

@2595

9 years 
tranquil 
* dropped locals and exit from definition of joint_if_function
* new …



@2592

9 years 
piccolo 
main lemma of ERTLptr in place



@2590

9 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2570

9 years 
piccolo 
ERTLtoERTLptr in place



@2564

9 years 
piccolo 
ERTL fully repaired, useless part of return value of pop_ra
removed.



@2562

9 years 
piccolo 
linearise modified



@2561

9 years 
tranquil 
* moved CALL as different case than joint_seq: lots of broken code now …



@2556

9 years 
tranquil 
in joint semantics and traces: added a last popped calling address to …



@2551

9 years 
piccolo 
completed isFinal and fetchStatementSigmaCommute. Fixed exit …



@2537

9 years 
tranquil 
rolled back changes on calls in joint. Now the save_frame parameter …



@2532

9 years 
tranquil 
added FCOND in LIN, and rewritten linearise so that it never adds a …



@2529

9 years 
tranquil 
rewritten function handling in joint
swapped call_rel with ret_rel in …



@2491

9 years 
tranquil 
fixed wrt change of list member definition



@2484

9 years 
piccolo 
fixed Traces and semantics
added commutation record (not yet finished) …



@2481

9 years 
piccolo 
corrected some inconsistencies
fixed some of lineariseProof



@2473

9 years 
tranquil 
put some generic stuff we need in the back end in extraGlobalenvs …



@2470

9 years 
tranquil 
completely separated program counters from code pointers in joint …



@2462

9 years 
tranquil 
separated in back end values program counters from code pointers …



@2457

9 years 
tranquil 
rewritten function handling in joint
swapped call_rel with ret_rel in …



@2443

9 years 
tranquil 
changed joint's stack pointer and internal stack



@2437

9 years 
tranquil 
generalised calls to calls with pointers



@2422

9 years 
tranquil 
adapted joint to cl_call f



@2286

9 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2185

9 years 
campbell 
Use bitvectors for offsets.



@2176

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



@1999

9 years 
campbell 
Make backend use the main global envs.



@1601

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



@1457

10 years 
sacerdot 
Bug fixed: when calling an internal function, the pc block is now set …



@1451

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



@1430

10 years 
sacerdot 
Bug fixed: push/pop must work on the isp (now added).
Note: the sp is …



@1415

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



@1411

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



@1408

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



@1395

10 years 
sacerdot 
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …



@1390

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



@1387

10 years 
sacerdot 
Further simplification *params1 no longer used.



@1386

10 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

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



@1384

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



@1383

10 years 
sacerdot 
Potential bug fixed and bug found: the way pointers and labels are put …



@1382

10 years 
sacerdot 
 succ_pc generalized to return a res (necessary for LIN semantics)
 …



@1377

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



@1376

10 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@1372

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



@1371

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



@1359

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



@1352

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



@1329

10 years 
sacerdot 
1. Definition of addresses moved to BEMem
2. Basic functions on …



@1324

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



@1312

10 years 
sacerdot 
Type of frame operations (pop_frame/save_frame) generalized to take in …



@1303

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



@1298

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



@1294

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



@1289

10 years 
sacerdot 
semantics ported to latest Joint version



@1281

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



@1250

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



@1247

10 years 
sacerdot 
Code (almost) ported to latest joint/Joint.ma datatype.
I still need …



@1246

10 years 
sacerdot 
Yet another change to Joint.ma to accomodate all passes.
The concrete …



@1233

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



@1220

10 years 
sacerdot 
ERTL ported to the new joint syntax.



@1217

10 years 
sacerdot 
Only one axiom left.



@1215

10 years 
sacerdot 
1) Added shifting directly on pointers
2) More temporary axioms closed.



@1214

10 years 
sacerdot 
res_to_opt function added to common/Errors and used in joint/semantics …



@1213

10 years 
sacerdot 
1) New values (joint/BEValues.ma) and memory model for the backends
…



@1186

10 years 
sacerdot 
Spurious code removed.
joint_fullexec implemented up to …



@1182

10 years 
mulligan 
changes to semantics: removing parameterised "next" element in joint …



@1177

10 years 
sacerdot 
Almost finished. Some functions still to be implemented, but I suspect …



@1176

10 years 
sacerdot 
…



@1174

10 years 
sacerdot 
Semantics of most instructions completed.



@1173

10 years 
sacerdot 
Unified semantics for ERTL/LTL/LIN (in progress).
I hope to include …
