Re: [isabelle] about longer computation syntax sugar



Dear Liu Jian,

> When you simply change it as following, a error occurs.
> 
>   range :: "index => seed => index => seed"
> where
>   "range k = (do
>      v <- range_aux (log 2147483561 k) 1;
>      if True return (v mod k) else return (v mod k)
>    done)"

The reason for this failure is the HOL if syntax: it demands a "then",
an in most cases has to be put in brackets:

>   "range k = (do
>      v <- range_aux (log 2147483561 k) 1;
>      (if True then return (v mod k) else return (v mod k))
>    done)"

> what's the meaning of following lines. Here, I can not understand the
> meaning of "CONST" and the difference between "=>" and "==" in a
> translation
> 
> translations
>   "_do f" => "CONST run f"

The "CONST" is a technical detail - for historical reasons, there are
two syntactic classes of constants: constants which are represented with
their proper qualified names in the syntax layer ("authentic constants")
and constants which are represented just by their base name
("non-authentic constants").  New-style definition tools (definition,
inductive, function, primrec with new "where"-syntax ...) yield
authentic constants, whereas older devices do not (consts, constdefs,
...).  The "CONST" marker states that "run" is an authentic constant.

The difference between "=>" and "==" in first approximation is that "=>"
is only applied in input direction, whereas "==" is applied during input
and reversely during output.  For a detailed description on how the
syntax layer work I have to redirect you to the old Isabelle Reference
Manual http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf which is
outdated in huge passages but the chapter on syntax still represents the
current implementation fairly well.

Hope this helps
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.