-
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