Animation of RoboChart_ChemicalDetector_autonomous_maincontroller doesn't work

[RandallYe]

After changing to Isabelle 2023, now the animation of RoboChart_ChemicalDetector_autonomous_maincontroller doesn't work. The runtime error is shown below.

Starting ITree Simulation...
Simulation: Finite_Set.hs:21:1-52: Non-exhaustive patterns in function card

[RandallYe]

I suspect it might be due to the code generation of Number_Type. For example, now value "Chemical_Chem2_list" in RoboChart_ChemicalDetector_autonomous_general.thy cannot be evaluated. Similarly, mk_blist also cannot be evaluated. I had a look at the simulation code for Isabelle.

The definition of mk_built: "mk_blist _ xs = map (bmake TYPE('n)) (lseqn xs CARD('n))"

For the new Isabell 2023, it generates

mk_blist uu xs =  map (Bounded_List.Bmake HOL.Type)   (lseqn xs ((Finite_Set.card :: Set.Set a -> Arith.Nat) Set.top_set));
`
```

But for the old Isabelle/'2021, it generated.
```
mk_blist uu xs =  map (Bmake Type) (lseqn xs (of_phantom (card_UNIV :: Phantom a Nat)));
```

[RandallYe]

In Isabelle2021, the generated code for list_of_blist is

list_of_blist :: forall a b. (Card_UNIV b, Finite b) => Blist a b -> [a];
list_of_blist (Bmake Type xs) =
  take (of_phantom (card_UNIV :: Phantom b Nat)) xs;

Where other definitions are shown below

newtype Phantom a b = Phantom b deriving (Prelude.Read, Prelude.Show);

of_phantom :: forall a b. Phantom a b -> b;
of_phantom (Phantom x) = x;

class (Finite_UNIV a) => Card_UNIV a where {
  card_UNIVa :: Phantom a Nat;
};

card_UNIV :: forall a. (Card_UNIV a) => Phantom a Nat;
card_UNIV = card_UNIVa;

card_UNIV_bit0 :: forall a. (Card_UNIV a, Finite a) => Phantom (Bit0 a) Nat;
card_UNIV_bit0 =
  Phantom
    (times_nat (nat_of_num (Bit0 One))
      (of_phantom (card_UNIVa :: Phantom a Nat)));

instance (Finite a) => Finite_UNIV (Bit0 a) where {
  finite_UNIV = finite_UNIV_bit0;
};

instance (Card_UNIV a, Finite a) => Card_UNIV (Bit0 a) where {
  card_UNIVa = card_UNIV_bit0;
};

Please take a look at the file I've attached for more details.
RoboChart_ChemicalDetector.hs.txt

But in Isabelle2023, it is

list_of_blist :: forall a b. (Finite_Set.Finite b, Eq b) => Blist a b -> [a];
list_of_blist (Bmake HOL.Type xs) =
  List.take ((Finite_Set.card :: Set.Set b -> Arith.Nat) Set.top_set) xs;

where top_set is defined in Set.hs

top_set :: forall a. Set a;
top_set = Coset [];

but card is defined as

card :: forall a. (Eq a) => Set.Set a -> Arith.Nat;
card (Set.Set xs) = List.size_list (List.remdups xs);

That's why the error occurs. See the files below for more details.

Bounded_List.hs.txt
Finite_Set.hs.txt
Set.hs.txt

[RandallYe]

If we import "HOL-Library.Code_Cardinality" in the beginning of the theory, then the generated code for card will be

(Phantom_Type.of_phantom (Code_Cardinality.card_UNIV :: Phantom_Type.Phantom b Arith.Nat))

Haven't tested it yet and it might fix the problem.

[RandallYe]

The change will cause further problems, which might be related to performance. Waited for long time till an error was given.

Starting ITree Simulation...

Simulation: Stack space overflow: current size 33616 bytes.
Simulation: Relink with -rtsopts and use `+RTS -Ksize -RTS' to increase it.