+%%%% Array (without IO, but they could be added easily)
[...]
+Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a;
[...]
+let array_set loc depth args_val = match args_val with
- | [Vint idx; v; Varray a] -> if (a = (Array.make 0 Vundefined))
- then
let a = (Array.make 0 v) in
let copy = (Array.map (fun v -> v) a) in
(Array.set copy idx v; Varray copy)
- else
let copy = (Array.map (fun v -> v) a) in
(Array.set copy idx v; Varray copy)
Aha: Une opération Array.set avec O(n)! Je ne comprends pas le besoin du `if (a = (Array.make 0 Vundefined))`, pourrais-tu ajouter un commentaire pour expliquer?
+let array_get loc depth args_val = match args_val with
- | [Vint idx; Varray a] -> if (a = (Array.make 0 Vundefined))
- || (idx > (Array.length a))
- || (idx < 0)
- then
error loc "Array.get index out of bounds"
Hmm... dans un langage comme Coq/Typer, les fonctions doivent être pures et totales, sinon il y a un risque de casser la cohérence.
Pour prendre l'exemple de la fonction `head` qui renvoie le premier élément d'une liste:
head : List ?a -> ?a;
foo : List False; foo = nil;
boom : False; boom = head foo;
Je crois que dans le cas ci-dessus la cohérence n'est en fait pas cassée, parce que si on a un `Array a`, il devait y avoir qqch de type `a` au moment de la construction du tableau (même si le tableau a taille 0).
Stefan