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
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
From: Mark Wassell <mpwassell@gmail.com>
Yes it is and thank you.
Mark
Last updated: Nov 21 2024 at 12:39 UTC