From e191cc298e684fa4231c97abf4f89ab0f1b3a42c Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 11 Feb 2015 19:33:46 +0100 Subject: More efficient initialization of an array --- src/versions/standard/Array/PArray_standard.v | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 069c159..eb43cb0 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -31,16 +31,12 @@ Local Open Scope int63_scope. Module Map := FMapAVL.Make(IntOrderedType). +(* An array is represented as a tuple of a finite map, the default + element, and the length *) Definition array (A:Type) : Type := (Map.t A * A * int)%type. -Definition make {A:Type} (l:int) (d:A) : array A := - let r := - if l == 0 then - Map.empty A - else - foldi (fun j m => Map.add j d m) 0 (l-1) (Map.empty A) in - (r, d, l). +Definition make {A:Type} (l:int) (d:A) : array A := (Map.empty A, d, l). Definition get {A:Type} (t:array A) (i:int) : A := let (td,_) := t in -- cgit