

@2991

8 years 
piccolo 
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …



@2968

8 years 
sacerdot 
The initial status memory was not really initialized. Now it is.



@2967

8 years 
sacerdot 
Semantics changed so that a terminating joint program that returns an …



@2952

8 years 
tranquil 
* corrected all backend premains to not pass any arguments to the …



@2946

8 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2932

8 years 
sacerdot 
Same comment as previous commit on this file: the previous commit was …



@2929

8 years 
sacerdot 
Bug fixed: the coercion mechanism made you think that the CALL case …



@2824

8 years 
tranquil 
* moved sum on lists notation to extranat
* used sum on lists to …



@2821

8 years 
tranquil 
* implemented preclassified system for joint (in joint/joint_fullexec.ma)



@2796

8 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2785

8 years 
piccolo 
Traces.ma repaired



@2783

8 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2757

8 years 
tranquil 
many things are still broken, but there is a partial backtrack on …



@2688

8 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2681

8 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2645

8 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2642

8 years 
piccolo 
fixed joint/Traces after having posed block 0 to be Code



@2638

8 years 
piccolo 
Backend fixes for last Garnier's commit that removes the regions from …



@2601

8 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2590

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



@2562

8 years 
piccolo 
linearise modified



@2561

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



@2556

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



@2553

8 years 
tranquil 
as_classify changed to a partial function
added a status for tailcalls



@2538

8 years 
tranquil 
fixed Traces.ma after changes in joint/semantics.ma



@2529

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



@2484

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



@2481

8 years 
piccolo 
corrected some inconsistencies
fixed some of lineariseProof



@2477

8 years 
tranquil 
status_simulation reformulated
definition of joint_classify split up …



@2473

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



@2470

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



@2457

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



@2443

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



@2442

8 years 
piccolo 
Traces repaired. (By Paolo)
Statement of lineariseProof in place.



@2422

8 years 
tranquil 
adapted joint to cl_call f



@2286

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



@2186

8 years 
tranquil 
updated joint semantics


copied from src/joint/as_semantics.ma:



@1976

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