Email Gateway (Aug 22 2022 at 20:27): Email Gateway (Aug 22 2022 at 20:27):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I am trying to generate code from an inductive predicate that involves a
quotient type. The problem is that code_pred doesn't work for the mode that
I want the code for my predicate to be for. I think it is because mode
checking is not seeing the constructors for the quotient type as being real
constructors that pattern matching works on.
Code is below and also in the attached.
Mark
datatype foo = FInt int | FUnit
axiomatization rel :: "foo ⇒ foo ⇒ bool" where equivp_rel: "equivp rel"
quotient_type bar = "foo" / rel using equivp_rel by simp
quotient_definition "BUnit :: bar" is FUnit done
quotient_definition "BInt :: int ⇒ bar" is FInt done
inductive foop :: "foo ⇒ int ⇒ bool" where
unitI: "foop FUnit 0"
| intI: "foop (FInt n) n"
(* This works *)
code_pred (modes: i ⇒ o ⇒ bool) [show_steps, show_mode_inference,
show_invalid_clauses] foop .
inductive barp :: "bar ⇒ int ⇒ bool" where
unitI: "barp BUnit 0"
| intI : "barp (BInt n) n"
(* This fails but works without the intI case. Is this because BInt isn't
really a constructor
that pattern matching works on? *)
code_pred (modes: i ⇒ o ⇒ bool) [show_steps, show_mode_inference,
show_invalid_clauses] barp .
CodeGenQuestion.thy
Email Gateway (Aug 22 2022 at 20:27):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
If I recall correctly without looking again at the code base,
code_pred relies on the datatype package to tell if it is a
constructor and hence obtains the case constant for splitting.
You can probably register some new constant as constructor in the
datatype package and you would also need to provide a case constant
for splitting, and hopefully then code_pred knows everything to infer
the mode you want and generate the code equations.
Experts on the datatype package can possibly tell you how to register
your quotient type as datatype in more detail; I have not seen that
part in recent years.
If that does not work together as expected, let me know and I will
look at the details of the code_pred command.
Lukas
Email Gateway (Aug 22 2022 at 20:28):From: Mark Wassell <mpwassell@gmail.com>
Lukas,
Thank you for your reply.
The free_constructor command looks to be what I need however it presupposes
that the constructors are injective. As it stands they are not and so I
will need to rethink my definitions.
Cheers
Mark
Email Gateway (Aug 22 2022 at 20:28):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
For the mode analysis and code_pred, you actually do not need
injectivity of "functions" (I would not call them constructors anymore
if no injectivity holds; but I am not an expert of what makes a type a
"datatype") to employ them in the mode analysis, but the inverse image
should be computable, i.e., there is an executable definition for that
inverse image.
You would be moving towards the boundaries of code_pred, and there are
probably no user commands, but you can find some examples here:
http://isabelle.in.tum.de/repos/isabelle/file/b85a12c2e2bf/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
starting at line 64 section \<open>Arithmetic operations\<close>
The examples make the functions plus and minus invertable on nat and
int and then set up the mode analysis and compiler.
Maybe this helps,
Lukas
Last updated: Apr 26 2024 at 20:16 UTC