• 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
bench Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
opam Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
stdlib Loading commit data...
tests Loading commit data...
.dockerignore Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
.ocp-indent Loading commit data...
AUTHORS Loading commit data...
CHANGES.md Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL.md Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README.md Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
autogen.sh Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...