Katherine Kosaian (Jan 23 2024 at 16:38): Katherine Kosaian (Jan 23 2024 at 16:38):Hi all, I am trying to write some executable code, but am running into an issue when importing certain files. In particular, I want to be able to import some files that depend on "Containers.Set_Impl", but importing "Containers.Set_Impl" changes which definitions are executable. It looks like Containers.Set_Impl uses "code drop", which might be contributing to or causing the problem. In any case, I have attached MWEs for two of the definitions that are executable until loading this file. Any thoughts on what exactly is causing the issue and how I can fix it would be greatly appreciated.
Mathias Fleury (Jan 23 2024 at 21:17):So, the idea of Containers.Set_Impl is to implement a more efficient replacement for sets (assuming that some type classes are there).
Solution 1: you actually do not care about the more efficient efficient. Then remove the import.
Solution 2: you want the more efficient implementation. Then you actually need to get the right type-classes. There are already various instantiation in Factor_Algebraic_Polynomial, so either you use derive too or you import those theories
Mathias Fleury (Jan 23 2024 at 21:20):By copy-pasting and doing a lot of grep:
derive (eq) ceq poly_mapping
derive (no) ccompare poly_mapping
derive (dlist) set_impl poly_mapping
derive (eq) ceq real
derive (compare) ccompare real
derive (dlist) set_impl complex real
(* This is executable without loading Containers.Set_Impl*)
value "vars (Var 0::real mpoly)"
For Test1 the problem is different and due to a faulty code equation. You can remove the code equation lemmas [code del] = prod.set_conv_list, but then there is no equation to execute the code.
Mathias Fleury (Jan 23 2024 at 21:25):I think that this would require to extend Set_impl properly to support the product operation
Katherine Kosaian (Jan 25 2024 at 13:06):This was very useful; thank you!!
Last updated: Apr 27 2024 at 16:16 UTC