The Coq mailing list

[Anton Tayanovskyy <anton.tayanovskyy AT gmail.com>]

You can perhaps write a few axioms defining the interface for
immutable arrays (vectors), and then implement them in OCaml, say:

Parameter vec : forall (a : Type), Type.
Parameter nth : forall {a}, vec a -> nat -> option a.
Parameter init : forall {a}, nat -> (nat -> a) -> vec a.

Definition test :=
  let x := init 3 (fun x => x + 1) in
  nth x 2.

Extraction test.

Thanks,

--A


On Sat, Aug 3, 2013 at 5:34 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> For ints,
>
> there are:
>
>   (1)  "nat" which consists of:
>     O = 0
>     S(n) = n+1
>
>   (2) Z, which consists of:
>     Zpos, Zneg, Z0; where Zpos/Zneg use binary representations (xH, xO, xI).
>
>
> For arrays, texts I've read suggested representing "T arr[];" as "f: nat ->
> T"
>
> However, in practice, I found it (for the sake of eval compute and proving
> things) easier if I represented arrays as an associative list. [Of course,
> you will have to do some black magic (beyond my abilities) for telling Coq
> to map the associative list operations to array ops rather than actual
> associative list ops.]
>
>
>
>
> On Sat, Aug 3, 2013 at 1:24 PM, Helmut Brandl 
> <helmut.luis.brandl AT gmail.com>
> wrote:
>>
>> Hello all,
>>
>> I am writing a verifying compiler and I use ocaml as the implementation
>> language. I would like to use coq to verify some critical algorithms.
>>
>> I have already read some documentation on program extraction. With
>> inductive types I don't see any problems, because inductive types and
>> functions on inductive types are translated one to one (with some
>> lexical adaptions and proof deletion) from coq to ocaml.
>>
>> However I need arrays and I need to index arrays with ints in my
>> program. The algorithms I am trying to verify do not use the mutability
>> of ocaml arrays but they use the contents.
>>
>> Can anybody give me hints (or links to any documentation) on how to
>> represent arrays and ints in coq?
>>
>> Thanks
>> Helmut
>
>



-- 
Kind Regards,
Anton Tayanovskyy

WebSharper™ - type-safe JavaScript in F#
http://intellifactory.com