|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
|
@2233
|
9 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
|
@2186
|
9 years |
tranquil |
updated joint semantics
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2174
|
9 years |
tranquil |
* factored out script for (axiomatised) fixpoint computation
* ERTL → …
|
|
|
|
@2162
|
9 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@2035
|
9 years |
sacerdot |
Fixed
|
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@1999
|
9 years |
campbell |
Make back-end use the main global envs.
|
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1644
|
9 years |
tranquil |
minor changes
|
|
|
|
@1643
|
9 years |
tranquil |
* some changes in everything
* separated extensions in sequential and …
|
|
|
|
@1641
|
9 years |
tranquil |
* semanticsUtils_paolo.ma contains code to generate both graph and …
|
|
|
|
@1640
|
9 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1636
|
9 years |
tranquil |
* added coercions to arguments (in RTL) and notation for ops (for the …
|
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1601
|
9 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 re-grouped 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
|
10 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
|
@1141
|
10 years |
sacerdot |
Comment (about a bug) added.
|
|
|
|
@1138
|
10 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
|
@1131
|
10 years |
mulligan |
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
|
|
|
|
@1126
|
10 years |
sacerdot |
Semantics completed up to initial state creation.
|
|
|
|
@1122
|
10 years |
sacerdot |
Internal function call implemented too.
|
|
|
|
@1121
|
10 years |
sacerdot |
External function calls implemented (but look at the new comment on …
|
|
|
|
@1120
|
10 years |
sacerdot |
All operations implemented.
|
|
|
|
@1118
|
10 years |
sacerdot |
All derivatives of St_const implemented (up to axioms to match the two …
|
|
|
|
@1117
|
10 years |
sacerdot |
More operations implemented.
|
|
|
|
@1115
|
10 years |
sacerdot |
Some comments.
|
|
|
|
@1114
|
10 years |
sacerdot |
some more operations implemented
|
|
|
|
@1113
|
10 years |
sacerdot |
Semantics (interpreter) of RTL.
The file does not compile yet. I am …
|
|
|
|
@1107
|
10 years |
mulligan |
got rtl-ertl pass working again
|
|
|
|
@1106
|
10 years |
mulligan |
changes necessary to get RTLabs->RTL to compile
|
|
|
|
@1089
|
10 years |
mulligan |
more changes from earlier in the week
|
|
|
|
@1081
|
10 years |
mulligan |
completed rtl-ertl pass
|
|
|
|
@1080
|
10 years |
mulligan |
more added
|
|
|
|
@1079
|
10 years |
mulligan |
finished rtl to ertl pass modulo conversion of tailcall simplification code
|
|
|
|
@1077
|
10 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1076
|
10 years |
mulligan |
small changes
|
|
|
|
@1075
|
10 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
|
@1071
|
10 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
|
