Commit 573870e0 authored by Andrei Paskevich's avatar Andrei Paskevich

fix #17137

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.
parent 09d37ec0
......@@ -502,7 +502,10 @@ let empty_clones s = {
(* populate the clone structure *)
let rec cl_find_ts cl ts =
if not (Sid.mem ts.ts_name cl.cl_local) then ts
if not (Sid.mem ts.ts_name cl.cl_local) then
let td = (cl_trans_ty cl) ts.ts_def in
if Opt.equal ty_equal ts.ts_def td then ts else
create_tysymbol (id_clone ts.ts_name) ts.ts_args td
else try Mts.find ts cl.ts_table
with Not_found ->
let td' = (cl_trans_ty cl) ts.ts_def in
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment