• Sylvain Dailler's avatar
    [WIP] This is ongoing experimental work. · 035a91c6
    Sylvain Dailler authored
    Change the way shapes are saved. The shape files is now organized as
    follow:
    - first, the shapes of all declarations that were converted to shape
    - second, checksum followed by a string representing the succession of
    variables declarations.
    Example:
    "(* Recording of all shape variable declarations *)
    left case
    a=axc0
    a=a+a+a+a+a+a+a+axaxaxaxaxaxaxaxc0
    Na=axc0Oa=axc0
    right case
    Na=axc0
    
    (* Checksum then concatenated variables representing a task shape *)
    956169bfb451ee6459ffdc4df18de7fd H3H2H3
    4dceea9c71fce658291b3212396973a6 H1H2H3
    566331d4fbc568133c5beace068734c6 H0H1H2H1
    bf3e0320b4b7af8d182c9aaa24ff2ee7 H5H2H3
    03fe7b1734fc43b78ef069c15b8ceef0 H4H5H2H5
    "
    
    Other changes:
    - Transform to shape only the local declarations
    - The shape size limit is now per declarations
    
    Effect:
    - It seems to reduce the size of the shapes a little
    
    TODO:
    - We read the session Xml twice just to be able to get the version of the
    shape before reading them
    - Data structure to record correspondence between shape and variable index
    seems inefficient (GShape)
    - At saving, the shapes need to be recomputed in order to not save useless
    shape variables (or temporary goals that were removed). This does not seem
    to be too inefficient: To be decided.
    - shapes should now be saved as a list of integer instead of strings
    - Pairing is under change. Proposed measure during brainstorming with
    Claude -> lcp measure replaced by the lexicographic order on:
    (number of same hypotheses, lcp on explanations, lcp on goal shape)
    - hyp_sep is "H". To be decided
    - all remaining TODO in the code
    035a91c6
Name
Last commit
Last update
..
compress.mli Loading commit data...
compress_none.ml Loading commit data...
compress_z.ml Loading commit data...
controller_itp.ml Loading commit data...
controller_itp.mli Loading commit data...
itp_communication.ml Loading commit data...
itp_communication.mli Loading commit data...
itp_server.ml Loading commit data...
itp_server.mli Loading commit data...
json_util.ml Loading commit data...
json_util.mli Loading commit data...
protocol.mli Loading commit data...
server_utils.ml Loading commit data...
server_utils.mli Loading commit data...
session_itp.ml Loading commit data...
session_itp.mli Loading commit data...
strategy.ml Loading commit data...
strategy.mli Loading commit data...
strategy_parser.mli Loading commit data...
strategy_parser.mll Loading commit data...
termcode.ml Loading commit data...
termcode.mli Loading commit data...
xml.mli Loading commit data...
xml.mll Loading commit data...