• Andrei Paskevich's avatar
    fix #17137 · 573870e0
    Andrei Paskevich authored
    Currently, clones "ts -> ty" are represented as "ts -> ts[=ty]",
    where the second type symbol is an alias created on the fly
    for the desired type. The problem comes when we want to clone
    a theory that contains such a cloning declaration. Since these
    aliases are "non-citizens" -- they are not properly declared,
    they are not put in the known_map, and they are not listed as
    locally declared symbols of the theory -- cloning of the cloning
    declaration mistakes them for external symbols and ignores them.
    Thus, the aliased type goes into the cloned theory as is, which
    provokes the error.
    
    The fix consists in an additional test for non-local type symbols.
    If such a symbol is an alias for a type that is actually cloneable,
    we conclude that the symbol is not external, but is a mere proxy
    for the aliased type, and so we clone the type and create a fresh
    type alias for it.
    
    A proper fix would be to always clone type symbols into types and
    never introduce the proxy type aliases. This is a more intrusive
    change, however, so let's start with a bandage.
    573870e0
theory.ml 27.8 KB