Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fixing modes for all predicates in mutually re...


view this post on Zulip Email Gateway (Aug 22 2022 at 19:26):

From: Mark Wassell <mpwassell@gmail.com>
Hello,

I am finding that mode checking on a block of mutually recursive predicates
is taking a long time (5+ minutes) and this is hindering any sort of
iterative development.

I know the mode I want for each predicate in the block and although I can
fix the mode for one of the predicates in the code_pred command, it looks
like all modes are being checked for the other predicates.

Is there a way to fix the modes for all of the predicates so that the mode
checking doesn't waste time exploring modes I have no interest in?

Cheers

Mark

view this post on Zulip Email Gateway (Aug 22 2022 at 19:26):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mark,

You can specify the modes for each predicate with the code_pred command. The syntax is as
follows:

Given two mutually recursive predicates

inductive P1 :: "... => bool"
and P2 :: "... => bool" where ...

you can write

code_pred (modes: P1: i => ... => o => bool and P2: o => ... => i => bool) P1

and the predicate compiler should no longer try all possible modes for P2.

Is this what you are looking for?

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 19:26):

From: Mark Wassell <mpwassell@gmail.com>
Yes it is and thank you.

Mark


Last updated: Nov 21 2024 at 12:39 UTC