[guru-lang] r528 committed - implemented qwarray; instead of tracking the checked-out item through ...
guru...@googlecode.com
Author: kain.nomad
Date: Sun Aug 7 05:34:30 2011
Log: implemented qwarray; instead of tracking the checked-out item
through its type, the item is taken out permanently and a place holder
fills the spot (qwarray_swap)
http://code.google.com/p/guru-lang/source/detail?r=528
Added:
/branches/1.0/tests/test-qwarray.g
Modified:
/branches/1.0/guru/Expr.java
/branches/1.0/lib/qwarray.g
/branches/1.0/tests/Makefile
=======================================
--- /dev/null
+++ /branches/1.0/tests/test-qwarray.g Sun Aug 7 05:34:30 2011
@@ -0,0 +1,43 @@
+Include "../lib/uwarray.g".
+Include "../lib/qwarray.g".
+
+Set "no_expand_vars"
+
+Define T := <uwarray word 0x4>
+Define g := fun(u:Unit):#unique T. (uwarray_new word 0x4 0x0).
+
+Define main :=
+ let arr = (qwarray_new T 0x10 g)
+
+ % testing "get"
+ let iarr = (inspect_unique <qwarray T 0x10> arr)
+ cabbrev p = join (ltword 0x0 0x10) tt
+ let x = (qwarray_get T 0x10 iarr 0x0 p)
+ do
+ (consume_unique_owned T x)
+ (consume_unique_owned <qwarray T 0x10> iarr)
+
+ % testing "set"
+ let x1 = (uwarray_new word 0x4 0x1)
+ let arr = (qwarray_set T 0x10 arr 0x0 x1 p)
+
+ % testing "swap"
+ let x2 = (uwarray_new word 0x4 0x1)
+ let arr =
+ match (qwarray_swap T 0x10 arr 0x0 x2 p) with qwarray_swap_v _ x3 n' arr
=>
+ do
+ % free to access x3
+ (uwarray_free word 0x4 x3)
+ cast arr by cong <qwarray T *> join n' 0x10
+ end
+ end % match
+
+ % testing "free"
+ (qwarray_free T 0x10 arr)
+ end % do
+
+%Set "debug_eta_expand".
+%Set "debug_to_carraway".
+%Set "debug_stages".
+
+Compile main to "test-qwarray.c".
=======================================
--- /branches/1.0/guru/Expr.java Thu May 12 14:49:12 2011
+++ /branches/1.0/guru/Expr.java Sun Aug 7 05:34:30 2011
@@ -209,7 +209,7 @@
// to x will be replaced with e.
final public Expr rewrite(Context ctxt, Expr e, Expr x, Stack
boundVars)
{
- if(defEq(ctxt, x, 0, true) &&
+ if(defEq(ctxt, x, NO_APPROX, true) &&
!x.containsVars(boundVars) &&
!e.containsVars(boundVars))
{
@@ -230,7 +230,7 @@
}
public Expr classify(Context ctxt, int approx, boolean spec) {
- if (approx > 0) {
+ if (approx > NO_APPROX) {
System.out.println("Approximate classification for this construct "
+"unimplemented: "
+(new Integer(construct)));
@@ -243,7 +243,7 @@
a stack overflow. We will treat this as specificational (use the
other classify() method to specify non-specificational). */
public Expr classify(Context ctxt) {
- return classify(ctxt,0,true);
+ return classify(ctxt,NO_APPROX,true);
}
// is e definitionally equal to this expr in the given ctxt.
@@ -264,12 +264,12 @@
}
final public boolean defEq(Context ctxt, Expr e, boolean spec) {
- return defEq(ctxt,e,0,spec);
+ return defEq(ctxt,e,NO_APPROX,spec);
}
// specificational by default
final public boolean defEq(Context ctxt, Expr e) {
- return defEq(ctxt,e,0,true);
+ return defEq(ctxt,e,NO_APPROX,true);
}
/* approx level 2 means all types are considered equal; 1 means we
@@ -308,7 +308,7 @@
ctxt.w.println("");
ctxt.w.flush();
}
- if (approx == 1)
+ if (approx == APPROX_NO_INDICES)
return e1.defEqNoAnnoApprox(ctxt,e2,spec);
return e1.defEqNoAnno(ctxt,e2,spec);
}
=======================================
--- /branches/1.0/lib/qwarray.g Wed Jul 27 07:32:57 2011
+++ /branches/1.0/lib/qwarray.g Sun Aug 7 05:34:30 2011
@@ -1,7 +1,7 @@
%=============================================================================
% word-indexed arrays of unique data
%=============================================================================
-
+Include trusted "unit.g".
Include trusted "word.g".
Include trusted "unique_owned.g".
@@ -12,17 +12,29 @@
END.
Define primitive qwarray_new
- : Fun(spec A:type)(n:word)(f:Fun(i:word).#unique A).#unique <qwarray A
n> :=
- fun(spec A:type)(n:word)(f:Fun(i:word).A). (mkvec A (f word0)
(word_to_nat n)) <<END
-void *gqwarray_new(int n, void* (*f)(int), void *a) {
+ : Fun(spec A:type)(n:word)(f:Fun(u:Unit).#unique A).#unique <qwarray A
n> :=
+ fun(A:type)(n:word)(f:Fun(u:Unit).A). (mkvec A (f unit) (word_to_nat n))
<<END
+void *gqwarray_new(unsigned n, void* (*f)(void*)) {
void **h = (void **)guru_malloc(sizeof(void *)*n);
- int c;
+ unsigned c;
for (c = 0; c < n; c++)
- h[c] = f(0); // f is a generator function.
+ h[c] = f(gunit()); // f is a generator function.
return h;
}
END.
+Define primitive qwarray_free : Fun(A:type)(n:word)(^ #unique l:<qwarray A
n>).void :=
+ fun(A:type)(n:word)(l:<qwarray A n>).voidi <<END
+void gqwarray_free(int A, unsigned n, void *l) {
+ unsigned c;
+ // fprintf(stdout,"gwarray_free(%x).\n", l);
+ for (c = 0; c < n; c++)
+ gconsume_unique(A,((void **)l)[c]);
+ carraway_free(l);
+}
+END.
+
+% read-only access
Define primitive qwarray_get
: Fun(spec A:type)(spec n:word)(! #unique_owned l:<qwarray A n>)
(i:word)
@@ -33,26 +45,40 @@
inline void* gqwarray_get(void **l, int i) { return l[i]; }
END.
+% replace an item
Define primitive qwarray_set
- : Fun(A:type)(i:word)(#unique a:A)(spec n:word)(#unique l:<qwarray A n>)
- (u:{(ltword i n) = tt}). #unique <qwarray A n> :=
- fun(A:type)(i:word)(a:A)(spec n:word)(l:<qwarray A n>)(u:{(ltword i n) =
tt}).
+ : Fun(A:type)(spec n:word)(#unique l:<qwarray A n>)
+ (i:word)(#unique a:A)(u:{(ltword i n) = tt}). #unique <qwarray A n> :=
+ fun(A:type)(spec n:word)(l:<qwarray A n>)(i:word)(a:A)(u:{(ltword i n) =
tt}).
abbrev p = hypjoin (lt (to_nat i) (to_nat n)) tt by u end in
(vec_update A (to_nat wordlen n) l (to_nat wordlen i) a p) <<END
-void *gqwarray_set(int A, int c, void *d, void *l) {
+void *gqwarray_set(int A, void *l, unsigned c, void *d) {
gconsume_unique(A,((void **)l)[c]);
((void **)l)[c] = d;
return l;
}
END.
-Define primitive qwarray_free : Fun(A:type)(n:word)(^ #unique l:<qwarray A
n>).void :=
- fun(A:type)(n:word)(l:<qwarray A n>).voidi <<END
-void gwarray_free(int A, int n, void *l) {
- int c;
- // fprintf(stdout,"gwarray_free(%x).\n", l);
- for (c = 0; c < n; c++)
- gconsume_unique(A,((void **)l)[c]);
- carraway_free(l);
+% take out and replace an item
+Inductive qwarray_swap_t : Fun(A:type)(n:word).type :=
+ qwarray_swap_v : Fun(A:type)(#unique a:A)
+ (spec n:word)(#unique l:<qwarray A n>)
+ .#unique <qwarray_swap_t A n>.
+
+Define primitive qwarray_swap : Fun
+ (A:type)(spec n:word)(#unique l:<qwarray A n>)
+ (i:word)(#unique a:A)
+ (u:{(ltword i n) = tt}). #unique <qwarray_swap_t A n> :=
+ fun(A:type)(spec n:word)(l:<qwarray A n>)(i:word)(a:A)(u:{(ltword i n) =
tt})
+ .
+ cabbrev p = hypjoin (lt (to_nat i) (to_nat n)) tt by u end in
+ cabbrev a' = (vec_get A (to_nat wordlen n) l (to_nat wordlen i) p)
+ cabbrev l' = (vec_update A (to_nat wordlen n) l (to_nat wordlen i) a p)
+ (qwarray_swap_v A a' n l')
+ <<END
+void *gqwarray_swap(int A, void *l, unsigned c, void *d) {
+ void* tmp = ((void **)l)[c];
+ ((void **)l)[c] = d;
+ return gqwarray_swap_v(A,tmp,l);
}
END.
=======================================
--- /branches/1.0/tests/Makefile Wed Jul 27 02:45:43 2011
+++ /branches/1.0/tests/Makefile Sun Aug 7 05:34:30 2011
@@ -333,3 +333,9 @@
test_qappend: test_qappend.g
guru $<
gcc -m32 -DDEBUG=1 -w -o $@ test_qappend.c
+
+test-qwarray: test-qwarray.g
+ guru $<
+ gcc -m32 -DDEBUG=1 -w -o $@ test-qwarray.c
+ ./test-qwarray
+