GitLab

The type of syntax_arguments_typed is unnecessarily specific,
so that it is not applicable to patterns.

          fix: recompute_all_shapes forgot to iter on metas

thanks to Johannes Kanig

Certain modifications in Why3 change tasks but not the propositional
structure of the goal. In this case, it is sometimes easier to use
"optimistic pairing": as long as the number of subgoals is the same
as in the old session, match them in the existing order, without
comparing shapes. This should be used only for repairing sessions
after changes in Why3.

Submitted by Johannes Kanig

Submitted by Johannes Kanig

lskept: the old selection check required at least one non-variable
non-closed type in the lsymbol's signature. This is too permissive,
because (list_match : list 'a -> 'b -> 'b) is allowed and will produce
an instance for every type in the "inst" set. The new check requires
that all freely standing type variables occur under a type constructor
elsewhere in the lsymbol's signature.

lsinst: accept any monomorphic instance of any polymorphic symbol
except equality. The old procedure applied the same restrictions
as for the "lskept" set which serve no real purpose for "lsinst".

Best of three runs on a bench for Gappa transformations:
- before: 34.98user 0.09system 0:35.13elapsed 99%CPU (0avgtext+0avgdata 241492maxresident)k
- after:  29.68user 0.08system 0:29.80elapsed 99%CPU (0avgtext+0avgdata 241820maxresident)k
Speed-up: +18%.

Sharing is caring, right?

this is useful to declare on-the-fly a new sort which replaces
a complex type. Otherwise, the printer has to traverse any term
twice: first, to detect complex types, second, to print the term.

also, avoid the "encoding_sort" transformation, if it can be done
directly in the printer.

On the same example as in the previous commits, this gives 5x
acceleration together with some memory usage reduction.