• Sylvain Dailler's avatar
    P419-017 counterex- Missing one liner with multidim array · bc0b6ca9
    Sylvain Dailler authored
    The one liner is missing because we did not project value of array
    elements in intro_projections_counterexmp. I changed the whole algorithm
    of projections to allow projecting values of multidim array. Also,
    moved local functions outside the main function. Added some trivial
    helping functions.
    
    * intro_projections_counterexmp
     (detect_map_types): Takes a type and return the list of successive types
      in the map and the return type. On map int (map int int) returns
      ([int; int], int).
     (last_type): Takes a list of proj_functions and returns the return type
      of the last projections_function that will be applied.
     (recreate_types): Recreates the type of the map with projected return
      type.
     (create_index_list): Returns a list of new well typed symbol for
      application in the axiom.
     (recreate_term_applications): Apply array to indices.
     (list_projection_until_base_type): Returns the list of all possible
      list of proj_functions applied to it.
     (projections_for_term): Changed the map part almost completely. We do
      not call this function recursively but we used other functions to get
      the recursive behavior.
    bc0b6ca9
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
opam Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
AUTHORS Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...