• 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
intro_projections_counterexmp.ml 12.5 KB