source: src/joint/Traces.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2932   7 years sacerdot Same comment as previous commit on this file: the previous commit was …
(edit) @2929   7 years sacerdot Bug fixed: the coercion mechanism made you think that the CALL case …
(edit) @2824   7 years tranquil * moved sum on lists notation to extranat * used sum on lists to …
(edit) @2821   7 years tranquil * implemented preclassified system for joint (in joint/joint_fullexec.ma)
(edit) @2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2785   7 years piccolo Traces.ma repaired
(edit) @2783   7 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2757   7 years tranquil many things are still broken, but there is a partial backtrack on …
(edit) @2688   7 years tranquil * in Arithmeticcs.ma: commented include that breaks script in latest …
(edit) @2681   7 years tranquil * improvements to the graph translation function * fixed passes up to LTL
(edit) @2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
(edit) @2642   7 years piccolo fixed joint/Traces after having posed block 0 to be Code
(edit) @2638   7 years piccolo Back-end fixes for last Garnier's commit that removes the regions from …
(edit) @2601   7 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
(edit) @2590   7 years piccolo added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
(edit) @2562   7 years piccolo linearise modified
(edit) @2561   7 years tranquil * moved CALL as different case than joint_seq: lots of broken code now …
(edit) @2556   7 years tranquil in joint semantics and traces: added a last popped calling address to …
(edit) @2553   7 years tranquil as_classify changed to a partial function added a status for tailcalls
(edit) @2538   7 years tranquil fixed Traces.ma after changes in joint/semantics.ma
(edit) @2529   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2484   7 years piccolo fixed Traces and semantics added commutation record (not yet finished) …
(edit) @2481   7 years piccolo corrected some inconsistencies fixed some of lineariseProof
(edit) @2477   7 years tranquil status_simulation reformulated definition of joint_classify split up …
(edit) @2473   7 years tranquil put some generic stuff we need in the back end in extraGlobalenvs …
(edit) @2470   7 years tranquil completely separated program counters from code pointers in joint …
(edit) @2457   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2443   7 years tranquil changed joint's stack pointer and internal stack
(edit) @2442   7 years piccolo Traces repaired. (By Paolo) Statement of lineariseProof in place.
(edit) @2422   7 years tranquil adapted joint to cl_call f
(edit) @2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(copy) @2186   7 years tranquil updated joint semantics
copied from src/joint/as_semantics.ma:
(add) @1976   8 years tranquil * monads: just changed some defs, which had to be propagated in some …
Note: See TracRevisionLog for help on using the revision log.