

@2103

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



@2043

7 years 
sacerdot 
Broken code commented out.



@2042

7 years 
sacerdot 
Repaired (Type => DeqSet?)



@1999

7 years 
campbell 
Make backend use the main global envs.



@1995

7 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1993

7 years 
campbell 
Make frontend memory model only depend on the general definitions by …



@1988

7 years 
campbell 
Abstraction of the memory contents in the memory models is no longer …



@1987

7 years 
campbell 
Move BEValues to common to reflect their use in the memory model for …



@1976

7 years 
tranquil 
* monads: just changed some defs, which had to be propagated in some …



@1949

7 years 
tranquil 
* lemma trace rel to eq flatten trace
* some more properties of …



@1908

7 years 
fguidi 
notation fixup following last commit of matita
we shifted the levels …



@1882

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



@1874

7 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1709

8 years 
mulligan 
Changes to the execution of the MOVC instruction



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



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



@1599

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



@1521

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



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1472

8 years 
mulligan 
moved proof utils to erasure.ma



@1471

8 years 
mulligan 
finished erasure and generalised so as to work on arbitrary joint programs



@1470

8 years 
mulligan 
finished, pretty ugly though as matita's disambiguation is a …



@1469

8 years 
mulligan 
finished new relabelling for graphs subject to one axiom closed



@1467

8 years 
mulligan 
small change, adding entry and exit labels into the internal function, …



@1466

8 years 
mulligan 
erasure for graph based joint languages almost complete



@1463

8 years 
mulligan 
added erasure for lin



@1458

8 years 
mulligan 
added skeleton file for erasure function for joint languages



@1457

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



@1452

8 years 
sacerdot 
Bug fixed: labels MUST be represented as pointers whose block is the …



@1451

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



@1430

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



@1419

8 years 
sacerdot 
All axioms closed.



@1416

8 years 
sacerdot 
Maps from hardware registers to beval now implemented in ASM/I8051 (in …



@1415

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



@1411

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



@1408

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



@1395

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



@1390

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



@1387

8 years 
sacerdot 
Further simplification *params1 no longer used.



@1386

8 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

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



@1384

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



@1383

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



@1382

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



@1380

8 years 
sacerdot 
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …



@1377

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



@1376

8 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@1372

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



@1371

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



@1359

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



@1352

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



@1329

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



@1324

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



@1312

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



@1303

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



@1302

8 years 
sacerdot 
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)



@1300

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



@1299

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



@1298

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



@1294

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



@1289

8 years 
sacerdot 
semantics ported to latest Joint version



@1284

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



@1283

8 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

8 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1281

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



@1280

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



@1275

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



@1271

8 years 
mulligan 
finished, kind of



@1270

8 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1260

8 years 
mulligan 
commit for csc



@1255

8 years 
sacerdot 
Major mistake fixed: op1 and op2 were assuming the source and dest …



@1254

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



@1252

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



@1250

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



@1247

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



@1246

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



@1245

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



@1236

8 years 
sacerdot 
LTLToLin.ma completed (up to a couple of daemons used to provide dead …



@1233

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



@1228

8 years 
mulligan 
some more changes



@1220

8 years 
sacerdot 
ERTL ported to the new joint syntax.



@1217

8 years 
sacerdot 
Only one axiom left.



@1215

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



@1214

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



@1213

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



@1186

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



@1182

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



@1177

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



@1176

8 years 
sacerdot 
…



@1174

8 years 
sacerdot 
Semantics of most instructions completed.



@1173

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



@1171

8 years 
mulligan 
changes made on claudio's request: changed order of nesting in the …



@1169

8 years 
sacerdot 
JointRTLtoLIN moved to Joint



@1167

8 years 
mulligan 
…



@1166

8 years 
mulligan 
moved joint ltl lin files into their own directory. more changes to …
