Functions in HOL are (total) functions in the mathematical sense. They
can't throw exceptions because they don't "do" anything; they are just a
map from the domain type to the range type.
If you want to model exceptions, you have various options, the simplest of
which is probably to use the option type.
I.e. define NTH_BIT_VAL : num -> num list -> num option, so that it returns
NONE if the index is too large, otherwise it returns SOME x, where x is the
desired element of the list.
You may as well just use the EL constant already defined in listTheory.
Define `NTH_BIT_VAL n ls = if n < LENGTH ls then SOME (EL n ls) else NONE`;
On Tue, May 14, 2013 at 4:46 AM, Yuntao Peng <[email protected]>wrote:
> A number list stored a set of numbers, the number value may be 0 or 1, no
> other case, now, I want to get the value of n-th element of the list. If n
> is greater than the length of the list,then fail. I don't know how to throw
> the exception which defined by myself.
>
> The function defined as follows:
> val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l
> >= SUC n) /\ (n >= 0)) then (if(n = 0) then (HD l) else NTH_BIT_VAL(n-1,TL
> l)) else (failwith "n is greater than list's LENGTH")`;
>
> Exception raised at TotalDefn.Define:
> between line 40, character 31 and frag 0 row 0 col 137:
> at TotalDefn.defnDefine:
> The following variables are free in the
> right hand side of the proposed definition: "failwith"
> ! Uncaught exception:
> ! HOL_ERR
>
> val NTH_BIT_VAL_def = Define `NTH_BIT_VAL(n:num,l:num list) = if((LENGTH l
> >= SUC n) /\ (n >= 0)) then (if(n = 0) then (HD l) else NTH_BIT_VAL(n-1,TL
> l)) else fail()`;
>
> Exception raised at TotalDefn.Define:
> on line 41, characters 30-159:
> at TotalDefn.defnDefine:
> The following variables are free in the
> right hand side of the proposed definition: "fail"
> ! Uncaught exception:
> ! HOL_ERR
>
> however, I define function using ML, done.
> - fun nth_bit_val n l = if(n=0) then fail() else l;
> > val 'a nth_bit_val = fn : int -> 'a -> 'a
>
> thx
>
>
> ------------------------------------------------------------------------------
> AlienVault Unified Security Management (USM) platform delivers complete
> security visibility with the essential security capabilities. Easily and
> efficiently configure, manage, and operate all of your security controls
> from a single console and one unified framework. Download a free trial.
> http://p.sf.net/sfu/alienvault_d2d
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
AlienVault Unified Security Management (USM) platform delivers complete
security visibility with the essential security capabilities. Easily and
efficiently configure, manage, and operate all of your security controls
from a single console and one unified framework. Download a free trial.
http://p.sf.net/sfu/alienvault_d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
