Ok, I had browsed the issues a bit too fast it seems...
I'll follow up on this on github then. Thanks!
V.
Le 13/11/12 17:49, Michael Norrish a écrit :
No, there are known problems here unfortunately.
See our github issue about it ( https://github.com/mn200/HOL/issues/97 ) for
some discussion.
As per my comment there, I'm inclined to go with changing the order of arguments
to the case constants, and to then play parsing/printing tricks to retain
backwards compatibility.
Michael
On 14/11/12 09:33, Vincent Aravantinos wrote:
Hi,
I played a little bit with computeLib in order to see its capabilities
and got stuck with efficiency problems when dealing with "case ... of".
My problem is that all branches are necessarily evaluated thus yielding
huge efficiency wastes.
The standard way to control the evaluation order for parameters would be
lazyfy_thm.
However, it is of no use here since the argument which allows to decide
on which branch to follow is the last one.
For instance ``case x of T => 1 | F => 2`` is actually a shortcut for
``bool_case 1 2 x``: x is in the end so lazyfy_thm cannot do anything.
Did I misunderstand something or is there a standard workaround?
Regards,
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
