|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1424
|
9 years |
sacerdot |
1. fold function over BitVectorTries? moved from ERTLToLTL to …
|
|
|
|
@1423
|
9 years |
sacerdot |
- spill no longer used
- BUG IN Interference: generating the destruct …
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1282
|
9 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@1281
|
9 years |
sacerdot |
Porting of all transformation to the joint syntax practically …
|
|
|
|
@1275
|
9 years |
sacerdot |
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …
|
|
|
|
@1274
|
9 years |
mulligan |
starting removing axioms from adts and giving them proper implementations
|
|
|
|
@1271
|
9 years |
mulligan |
finished, kind of
|
|
|
|
@1263
|
9 years |
mulligan |
changes
|
|
|
|
@1260
|
9 years |
mulligan |
commit for csc
|
|
|
|
@1256
|
9 years |
mulligan |
changes: added a mapi for graphs
|
|
|
|
@1251
|
9 years |
mulligan |
changes to get things compiling again after yet another CSC rearrangement!
|
|
|
|
@1250
|
9 years |
sacerdot |
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …
|
|
|
|
@1249
|
9 years |
mulligan |
changes to get everything to typecheck again
|
|
|
|
@1241
|
9 years |
mulligan |
changes for claudio
|
|
|
|
@1232
|
9 years |
mulligan |
big changes: got what was implemented in the ertl to ltl pass type …
|
|
|
|
@1230
|
9 years |
mulligan |
more changes
|
|
|
|
@1229
|
9 years |
mulligan |
changes
|
|
|
|
@1192
|
9 years |
mulligan |
some files that were missing / laying dormant on my computer
|
|
|
|
@1191
|
9 years |
mulligan |
ertl to ertl pass back where it was before the changes to joint
|
|
|
|
@1179
|
9 years |
mulligan |
changes to ertl, ltl and lin to use new notion of joint params. ertl …
|
|
|
|
@1175
|
9 years |
mulligan |
changes to ertl pass
|
|
|
|
@1172
|
9 years |
mulligan |
ertltoltl.ma half complete
|
|
|
|
@1171
|
9 years |
mulligan |
changes made on claudio's request: changed order of nesting in the …
|
|
|
|
@1170
|
9 years |
mulligan |
changes to ertl > ltl pass
|
|
|
|
@1168
|
9 years |
sacerdot |
Joint statements parameterized over a record.
|
|
|
|
@1166
|
9 years |
mulligan |
moved joint ltl lin files into their own directory. more changes to …
|
|
|
|
@1165
|
9 years |
mulligan |
more changes
|
|
|
|
@1163
|
9 years |
mulligan |
even more streamlining and fixes to get things type checking
|
|
|
|
@1161
|
9 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
|
@1160
|
9 years |
mulligan |
changes to unfunctorised code in ertltoltl.ma
|
|
|
|
@1154
|
9 years |
mulligan |
changes to ertl files: in process of removing ertltoltli.ma in favour …
|
|
|
|
@1152
|
9 years |
mulligan |
more added
|
|
|
|
@1144
|
9 years |
mulligan |
added build.ma file. matita bug found
|
|
|
|
@1128
|
9 years |
mulligan |
fixed ERTLtoLTLI so it type checks again
|
|
|
|
@1124
|
9 years |
mulligan |
finished off liveness analysis by axiomatising properties
|
|
|
|
@1110
|
9 years |
mulligan |
changes to get ltl to lin pass to work properly
|
|
|
|
@1088
|
10 years |
mulligan |
work on liveness analysis: an imperative nightmare
|
|
|
|
@1084
|
10 years |
mulligan |
more added on ertl pass: not sure how much should be axiomatised wrt …
|
|
|
|
@1082
|
10 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
|
@759
|
10 years |
mulligan |
More work on the RTL to ERTL pass.
|
|
|
|
@757
|
10 years |
mulligan |
Lots more fixing to get both front and backends using same conventions …
|
|
|
|
@753
|
10 years |
mulligan |
Work from today.
|
|
|
|
@752
|
10 years |
mulligan |
Fixed error in BitVectorTrieSet? file.
|
|
|
|
@745
|
10 years |
mulligan |
Changes from yesterday. Slowly implementing the functorized …
|
|
|
|
@733
|
10 years |
mulligan |
Fixed partial commit.
|
