• 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
..
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
isabelle-client Loading commit data...
jessie Loading commit data...
mlw Loading commit data...
parser Loading commit data...
printer Loading commit data...
server Loading commit data...
session Loading commit data...
tools Loading commit data...
transform Loading commit data...
trywhy3 Loading commit data...
util Loading commit data...
why3doc Loading commit data...
why3session Loading commit data...
config.sh.in Loading commit data...