The Coq mailing list

[Fritjof Bornebusch <fritjof AT uni-bremen.de>]

Hi,

thank you for your answers.

My current solution is:

  Definition minusone := Types.Signed32.repr (-1).
  Notation "-1" := minusone : my_scope. (* default value for List.nth_default 
*)

  Definition SignedVector := Vector.t Types.Signed32.int.
  Definition getAt (index : Types.Signed32.int) (vector: SignedVector(32)) : 
Types.Signed32.int :=
    List.nth_default (-1) (Vector.to_list vector) (Z.to_nat 
(Types.Signed32.unsigned index)).

  Compute (getAt (Types.Signed32.repr 0) initialRegisters). (* = {|
                                                                 
Types.Signed32.intval := 1;
                                                                 
Types.Signed32.intrange := Types.Signed32.Z_mod_modulus_range' 1 |}
                                                               : 
Types.Signed32.int
                                                            *)

  Compute (getAt (Types.Signed32.repr 64) initialRegisters). (* = {|
                                                                  
Types.Signed32.intval := 4294967295;
                                                                  
Types.Signed32.intrange := Types.Signed32.Z_mod_modulus_range' (-1) |}
                                                                : 
Types.Signed32.int
                                                             *)

The Signed32.int type comes from CompCerts integer library:
https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

Best Regards,
--f.

On Wed, May 20, 2020 at 08:23:33PM +0200, Dominique Larchey-Wendling wrote:
>    Vector.to_list ?
> 
>    Le 20 mai 2020 18:15:53 GMT+02:00, Fritjof Bornebusch
>    <fritjof AT uni-bremen.de> a écrit :
> 
> On Wed, May 20, 2020 at 05:29:19PM +0200, Dominique Larchey-Wendling wrote:
> 
>      Quick fix ... project your vector into a list ;-)
> 
>      Interessting, do you know any function that does that for me?
> 
>      ----- Mail original -----
> 
>      De: "Fritjof Bornebusch" <fritjof AT uni-bremen.de>
>      À: "coq-club" <coq-club AT inria.fr>
>      Envoyé: Mercredi 20 Mai 2020 17:15:33
>      Objet: [Coq-Club] nth element of a vector
> 
>      Hi there,
>      I'm looking for a function that iterates over a vector -
>      [1]https://coq.inria.fr/library/Coq.Vectors.Vector.html - and
>      returns
>      the Zth element, like the nth element of a list.
>      The library function only dealy with the Fin.t type, but I need Z.
>      Does anyone has a suggestion or hint?
>      Best Regards,
>      --f.
> 
>    --
>    Envoyé de mon appareil Android avec Courriel K-9 Mail. Veuillez excuser
>    ma brièveté.
> 
> References
> 
>    1. https://coq.inria.fr/library/Coq.Vectors.Vector.html