[guru-lang] r221 committed - commented out line in Parser which calls the CharExpr constructor; jus...
codesite...@google.com
Author: aaron.stump
Date: Tue Sep 15 06:49:25 2009
Log: commented out line in Parser which calls the CharExpr constructor;
just waiting for Derek to add CharExpr.java
http://code.google.com/p/guru-lang/source/detail?r=221
Added:
/branches/1.0/talks/plpv09/beamerouterthemenoinfolines.sty
/branches/1.0/talks/plpv09/beamerthemeEdinburgh.sty
/branches/1.0/tests/test_queuec.ml
Deleted:
/branches/1.0/tests/test-queuec.ml
Modified:
/branches/1.0/guru/Parser.java
/branches/1.0/lib/heaplet.g
/branches/1.0/lib/queue2.g
/branches/1.0/lib/rheaplet_thms.g
/branches/1.0/talks/plpv09/talk.pdf
/branches/1.0/talks/plpv09/talk.tex
/branches/1.0/tests/Makefile
=======================================
--- /dev/null
+++ /branches/1.0/talks/plpv09/beamerouterthemenoinfolines.sty Tue Sep 15
06:49:25 2009
@@ -0,0 +1,38 @@
+\ProvidesPackageRCS $Header:
/project/cl/Root/CVS/talks/smtcomp05/beamerouterthemenoinfolines.sty,v 1.1
2005/07/09 11:37:42 stump Exp $
+
+% Copyright 2003 by Till Tantau <tan...@users.sourceforge.net>
+%
+% This program can be redistributed and/or modified under the terms
+% of the GNU Public License, version 2.
+
+\mode<presentation>
+
+%\setbeamercolor*{author in head/foot}{parent=palette tertiary}
+%\setbeamercolor*{title in head/foot}{parent=palette secondary}
+%\setbeamercolor*{date in head/foot}{parent=palette primary}
+
+%\setbeamercolor*{author in head/foot}{fg=blue,bg=white}
+%\setbeamercolor*{title in head/foot}{fg=blue,bg=white}
+%\setbeamercolor*{date in head/foot}{fg=blue,bg=white}
+
+%\setbeamercolor*{section in head/foot}{parent=palette tertiary}
+%\setbeamercolor*{subsection in head/foot}{parent=palette primary}
+
+
+\defbeamertemplate*{headline}{infolines theme}
+{
+ \leavevmode%
+ \hbox{%
+ \begin{beamercolorbox}[wd=.5\paperwidth,ht=2.25ex,dp=1ex,right]{section
in head/foot}%
+ \usebeamerfont{section in head/foot}\insertsectionhead\hspace*{2ex}
+ \end{beamercolorbox}%
+
\begin{beamercolorbox}[wd=.5\paperwidth,ht=2.25ex,dp=1ex,left]{subsection
in head/foot}%
+ \usebeamerfont{subsection in
head/foot}\hspace*{2ex}\insertsubsectionhead
+ \end{beamercolorbox}}%
+ \vskip0pt%
+}
+
+\setbeamersize{text margin left=1em,text margin right=1em}
+
+\mode
+<all>
=======================================
--- /dev/null
+++ /branches/1.0/talks/plpv09/beamerthemeEdinburgh.sty Tue Sep 15 06:49:25
2009
@@ -0,0 +1,37 @@
+\ProvidesPackageRCS $Header:
/project/cl/Root/CVS/talks/smtcomp05/beamerthemeEdinburgh.sty,v 1.1
2005/07/09 11:37:43 stump Exp $
+
+% Copyright 2004 by Manuel Carro <mca...@fi.upm.es>
+%
+% This program can be redistributed and/or modified under the terms
+% of the GNU Public License, version 2.
+
+\mode<presentation>
+
+\newif\ifbeamer@secheader
+\beamer@secheaderfalse
+
+\DeclareOptionBeamer{secheader}{\beamer@secheadertrue}
+\ProcessOptionsBeamer
+
+\usecolortheme{rose}
+\useinnertheme[shadow]{rounded}
+\usecolortheme{dolphin}
+\useoutertheme{noinfolines}
+
+\setbeamertemplate{navigation symbols}{}
+
+% Tills' opinion: should be done in an inner theme, not here.
+
+\usesubitemizeitemtemplate{%
+ \tiny\raise1.5pt\hbox{\color{beamerstructure}$\blacktriangleright$}%
+}
+\usesubsubitemizeitemtemplate{%
+ \tiny\raise1.5pt\hbox{\color{beamerstructure}$\bigstar$}%
+}
+
+\setbeamersize{text margin left=1em,text margin right=1em}
+
+\ifbeamer@secheader\else\setbeamertemplate{headline}[default]\fi
+
+\mode
+<all>
=======================================
--- /dev/null
+++ /branches/1.0/tests/test_queuec.ml Tue Sep 15 06:49:25 2009
@@ -0,0 +1,49 @@
+open Queue;;
+
+let rec read_until_space() =
+ try
+ let c = (input_char stdin) in
+ if (c = ' ') then
+ (false,[])
+ else
+ let (eof,s) = (read_until_space()) in
+ (eof, c ::s)
+ with End_of_file -> (true,[])
+;;
+
+let rec enqueue_all q =
+ let (eof,s) = read_until_space() in
+ add s q;
+ if eof then
+ q
+ else
+ enqueue_all q;;
+
+let rec shift_all q1 q2 =
+ if (is_empty q1) then q2
+ else
+ let s = (take q1) in
+ add s q2; shift_all q1 q2;;
+
+let rec print_charlist s =
+ match s with
+ [] -> ()
+ | c::s -> output_char stdout c; print_charlist s;;
+
+let rec dequeue_all q prev =
+ if (is_empty q) then
+ (print_charlist prev; print_newline())
+ else
+ dequeue_all q (pop q);;
+
+(* (enqueue_all (create()));; *)
+
+(* (dequeue_all (enqueue_all (create())) []);; *)
+
+
+ (dequeue_all (shift_all (enqueue_all (create())) (create())) []);;
+
+(*
+let rec loop() = loop();;
+loop();;
+*)
=======================================
--- /branches/1.0/tests/test-queuec.ml Tue Sep 8 12:58:02 2009
+++ /dev/null
@@ -1,49 +0,0 @@
-open Queue;;
-
-let rec read_until_space() =
- try
- let c = (input_char stdin) in
- if (c = ' ') then
- (false,[])
- else
- let (eof,s) = (read_until_space()) in
- (eof, c ::s)
- with End_of_file -> (true,[])
-;;
-
-let rec enqueue_all q =
- let (eof,s) = read_until_space() in
- add s q;
- if eof then
- q
- else
- enqueue_all q;;
-
-let rec shift_all q1 q2 =
- if (is_empty q1) then q2
- else
- let s = (take q1) in
- add s q2; shift_all q1 q2;;
-
-let rec print_charlist s =
- match s with
- [] -> ()
- | c::s -> output_char stdout c; print_charlist s;;
-
-let rec dequeue_all q prev =
- if (is_empty q) then
- (print_charlist prev; print_newline())
- else
- dequeue_all q (pop q);;
-
-(* (enqueue_all (create()));; *)
-
- (dequeue_all (enqueue_all (create())) []);;
-
-
-(* (dequeue_all (shift_all (enqueue_all (create())) (create())) []);; *)
-
-(*
-let rec loop() = loop();;
-loop();;
-*)
=======================================
--- /branches/1.0/guru/Parser.java Mon Sep 14 19:59:51 2009
+++ /branches/1.0/guru/Parser.java Tue Sep 15 06:49:25 2009
@@ -683,7 +683,7 @@
protected Expr readCharExpr() throws IOException {
ungetc('\'');
- return new CharExpr(readString(new Character('\'')));
+ return null; //new CharExpr(readString(new Character('\'')));
}
protected Include readInclude() throws IOException
=======================================
--- /branches/1.0/lib/heaplet.g Tue Jul 21 08:26:31 2009
+++ /branches/1.0/lib/heaplet.g Tue Sep 15 06:49:25 2009
@@ -1,87 +1,88 @@
-% A heaplet models a portion of heap-allocated memory.
-%
-% Heaplets are just specificational data, and do not
-% exist at runtime (we must just pass a dummy value
-% through for them everywhere).
-%
-% We statically reference count the data stored in the
-% heaplet, and deallocate data only when the reference
-% count is known (statically) to be zero.
-
Include trusted "list.g".
-Include "unique.g".
-
-Define natlist := <list nat>.
-Define natlistn := (nil nat).
-Define natlistc := (cons nat).
+Include "unit.g".
+Include "holder.g".
+Include "unique_owned.g".
% the functional model for heaplets.
-%
-% L is the list of static reference counts. An entry of Z there means the
corresponding entry
-% has been removed from the heaplet. An entry of (S n) means there are n
outstanding aliases.
-
-Inductive heaplist : Fun(A:type)(L:natlist).type :=
- heaplistn : Fun(A:type).<heaplist A natlistn>
-| heaplistc : Fun(A:type)(n:nat)(a:A)(L:natlist)(h:<heaplist A
L>).<heaplist A (natlistc (S n) L)>
-| heaplistg : Fun(A:type)(L:natlist)(h:<heaplist A L>).<heaplist A
(natlistc Z L)>.
-
-% <heaplet A I L> is the type for heaplets holding objects of type A, with
heaplet_id I,
-% and list of static reference counts L.
-%
-% heaplet_ids are used to connect aliases to the heaplet with which they
are associated.
-% heaplet_ids do not exist at runtime (again, a dummy value is passed
through for them).
-
-Define primitive type_family_abbrev heaplet :=
fun(A:type)(I:nat)(L:natlist).<heaplist A L> <<END
- #define gconsume_heaplet(x)
-END.
Define primitive heaplet_id := nat <<END
- #define gconsume_heaplet_id(x)
+ #define gdelete_heaplet_id(x)
END.
-Define primitive heaplet_id0 := Z <<END
+Define primitive heaplet_id0 : #unique heaplet_id := Z <<END
#define gheaplet_id0 1
END.
+% call this once per compiled program, just to have the compiler pull in
functions
+% we need in our C code.
+Define init_heaplets : Fun(u:Unit).Unit :=
+ fun(u:Unit).
+ let x = mk_holder in unit.
+
+
+<heaplet A I n> -- type for heaplets of As with id I and n aliases.
+Define primitive type_family_abbrev heaplet :=
fun(A:type)(I:heaplet_id)(n:nat).<list A> <<END
+ #define gdelete_heaplet(x)
+END.
+
Inductive new_heaplet_t : Fun(A:type)(I:heaplet_id).type :=
return_new_heaplet : Fun(spec A:type)(spec I : heaplet_id)
(#unique nextI:heaplet_id)
- (#unique h:<heaplet A I
natlistn>).<new_heaplet_t A I>.
-
-Define primitive new_heaplet : Fun(spec A:type)(#unique
I:heaplet_id).<new_heaplet_t A I> :=
- fun(A:type)(I:heaplet_id). (return_new_heaplet A I (S I) (heaplistn A))
<<END
+ (#unique h:<heaplet A I Z>).#unique
<new_heaplet_t A I>.
+
+Define primitive new_heaplet : Fun(spec A:type)(#unique
I:heaplet_id).#unique <new_heaplet_t A I> :=
+ fun(A:type)(I:heaplet_id). (return_new_heaplet A I (S I) (nil A)) <<END
void *gnew_heaplet(int I) {
return greturn_new_heaplet(I,0);
}
END.
-% <alias I> is the type for a pointer into the (unique) heaplet with
heaplet id I.
-%
-% In the functional model, p:<alias I> is the position in the heaplet,
starting from
-% the end, where the data pointed to by the pointer is stored.
-%
-% In the actual implementation, p:<alias I> is pointer directly to the
data.
-
-Define primitive type_family_abbrev alias := fun(I:heaplet_id).nat <<END
-#define gconsume_alias(x)
+Define primitive type_family_abbrev alias := fun(I:rheaplet_id).nat <<END
+void gdelete_alias(void *x) {
+ release(gholder,x,1); // this will decrement the refcount for the
data pointed to.
+}
+END.
+
+Inductive heaplet_in_t : Fun(A:type)(I:heaplet_id)(n:nat).type :=
+ return_heaplet_in : Fun(spec A:type)(spec I:heaplet_id)
+ (spec n:nat)
+ (#unique h:<heaplet A I (S n)>)
+ (#unique p:<alias I>).
+ #unique <heaplet_in_t A I n>.
+
+Define primitive heaplet_in : Fun(A:type)(spec I:heaplet_id)(spec n:nat)
+ (#unique h:<heaplet A I n>)(a:A).
+ #unique <heaplet_in_t A I n> :=
+ fun (A:type)(spec I:heaplet_id)(h:<heaplet A I>)(a:A).
+ (return_heaplet_in A I (append A h (cons A a (nil A))) (length A h))
<<END
+void *gheaplet_in(int A, int h, void *a) {
+ return greturn_heaplet_in(1,a);
+}
END.
-Inductive heaplet_alias_t : Fun(A:type)(I:heaplet_id)(L:natlist).type :=
- return_heaplet_alias : Fun(spec A:type)(spec I:heaplet_id)(spec
L:natlist)
- (#unique h:<heaplet A I L>)(#unique p:<alias
I>).<heaplet_in_t A I L>.
-
-Define primitive heaplet_in : Fun(spec A:type)(spec I:heaplet_id)(spec
L:natlist)
- (h:<heaplet A I L>)(a:A).
- <heaplet_alias_t A I (append nat L (natlistc
(S Z) natlistn))> :=
- fun r(A:type)(spec I:heaplet_id)(spec L:natlist)
- (h:<heaplet A I L>)(a:A):
- <heaplet_alias_t A I (append nat L (natlistc (S Z) natlistn))>.
- match h with
- heaplistn _ => cast (heaplistc A n a natlistn (heaplistn A))
- by cong <heaplist A *> join (natlist (S Z) natlistn
-
-void *gheaplet_in(void *h, void *a) {
- return greturn_heaplet_alias(h,a);
+Inductive heaplet_dup_t : Fun(A:type)(I:rheaplet_id)(n:nat).type :=
+ return_heaplet_dup : Fun(A:type)(spec I:rheaplet_id)(spec n:nat)
+ (#unique h:<heaplet A I (S n)>)
+ (#unique p:<alias I>).<heaplet_dup_t A I n>.
+
+Define primitive heaplet_dup : Fun(spec A:type)(spec I:rheaplet_id)(spec
n:nat)
+ (#unique h:<rheaplet A I n>)
+ (!#unique_owned p:<alias I>).
+ <heaplet_dup_t A I n> :=
+ fun(spec A:type)(spec I:rheaplet_id)(spec n:nat)
+ (h:<rheaplet A I n>)
+ (p:<alias I>). p <<END
+
+inline void *gheaplet_dup(int h, void *p) {
+ return p;
}
END.
-
+
+
+Define primitive rheaplet_get : Fun(spec A:type)(spec I:rheaplet_id)(spec
n:nat)(#unique_owned p:<alias I>)
+ (!#unique_owned h:<rheaplet A I>).
+ #<owned h> A :=
+ fun (A:type)(spec I:rheaplet_id)(spec n:nat)(p:<alias I>)(h:<rheaplet A
I>). (nth A p h) <<END
+#define grheaplet_get(p, h) select_holder_mk_holder_a(p)
+END.
+
=======================================
--- /branches/1.0/lib/queue2.g Tue Sep 8 07:28:12 2009
+++ /branches/1.0/lib/queue2.g Tue Sep 15 06:49:25 2009
@@ -37,13 +37,15 @@
(u2:{(lt bound1 bound2) = tt}).
[list_all_implies <queue_cell A I>
(queue_cell_inv A I bound1) (queue_cell_inv A I bound2)
- foralli(c:<queue_cell A I>).
+ foralli(c:<queue_cell A I>)(u:{(queue_cell_inv A I bound1 c) = tt}).
case c with
- queue_cellc _ _ a nextp => existsi (lt nextp bound1) {
(queue_cell_inv bound1 c) = * }
- trans cong (queue_cell_inv bound1
*) c_eq
- join (queue_cell_inv bound1
(queue_cellc a nextp)) (lt nextp bound1)
- | queue_celln _ _ a => existi tt { (queue_cell_inv bound1 c) = *}
-
+ queue_cellc _ _ a nextp => hypjoin (queue_cell_inv A I bound2 c)
tt
+ by c_eq u [lt_trans nextp bound1
bound2
+ hypjoin (lt nextp
bound1) tt by c_eq u end
+ u2]
+ end
+ | queue_celln _ _ a => truei
+ end].
Define queue_cell_has_next : Fun(A:type)(spec I:rheaplet_id)(c:<queue_cell
A I>).bool :=
fun(A:type)(spec I:rheaplet_id)(c:<queue_cell A I>):bool.
=======================================
--- /branches/1.0/lib/rheaplet_thms.g Tue Sep 8 07:28:12 2009
+++ /branches/1.0/lib/rheaplet_thms.g Tue Sep 15 06:49:25 2009
@@ -52,18 +52,18 @@
end.
Define rheaplet_set_list_all :
- Forall(A:type)(f:Fun(a:A).bool)(ftot : Forall(a:A).Exists(b:bool). {(f
a) = b})
+ Forall(A:type)(f:Fun(a:A).bool)
(I:rheaplet_id)(h:<rheaplet A I>)(a:A)(p:<alias I>)
(u1 : { (list_all f h) = tt })
(u2 : { (f a) = tt })
(u3 : { (lt p (length h)) = tt }).
{ (list_all f (rheaplet_set p h a)) = tt } :=
- foralli(A:type)(f:Fun(a:A).bool)(ftot : Forall(a:A).Exists(b:bool). {(f
a) = b})
+ foralli(A:type)(f:Fun(a:A).bool)
(I:rheaplet_id)(h:<rheaplet A I>)(a:A)(p:<alias I>)
(u1 : { (list_all f h) = tt })
(u2 : { (f a) = tt })
(u3 : { (lt p (length h)) = tt }).
trans cong (list_all f *) join (rheaplet_set p h a) (set_nth p h a)
- [list_all_set_nth A p h a f ftot u3 u1 u2].
+ [list_all_set_nth A p h a f u3 u1 u2].
=======================================
--- /branches/1.0/talks/plpv09/talk.pdf Tue Jan 20 05:50:35 2009
+++ /branches/1.0/talks/plpv09/talk.pdf Tue Sep 15 06:49:25 2009
Binary file, no diff available.
=======================================
--- /branches/1.0/talks/plpv09/talk.tex Tue Jan 20 05:50:35 2009
+++ /branches/1.0/talks/plpv09/talk.tex Tue Sep 15 06:49:25 2009
@@ -34,8 +34,8 @@
% or ...
%\usetheme{IowaCity}
-%\usetheme{Edinburgh}
-\usetheme{Savannah}
+\usetheme{Edinburgh}
+%\usetheme{Savannah}
% \setbeamercovered{transparent}
% or whatever (possibly just delete it)
=======================================
--- /branches/1.0/tests/Makefile Tue Sep 8 12:58:02 2009
+++ /branches/1.0/tests/Makefile Tue Sep 15 06:49:25 2009
@@ -36,6 +36,9 @@
test-queue2: test-queue2.hs Makefile
ghc -O2 -o test-queue2 --make test-queue2.hs
+test-queue3: test-queue.hs Makefile
+ ghc -O2 -o test-queue3 --make test-queue.hs
+
test-warray1a: test-warray.g Makefile
../bin/guru test-warray.g
gcc -O2 -w -o test-warray1a test-warray.c