diff --git a/test/good/convolutions.ept b/test/good/convolutions.ept new file mode 100644 index 0000000..a20bbe6 --- /dev/null +++ b/test/good/convolutions.ept @@ -0,0 +1,47 @@ +(* Deal with matrix of size n*m, apply coeff : + kt + kl k kr + kb + centered on [>i<][>j<]. *) +fun kernel_1 << n,m,k,kl,kt,kr,kb :int>> (t :int^n^m; i,x,j :int) returns (r :int) +let + r = k*t[>i<][>j<] + kl*t[>i<][>j-1<] + kt*t[>i-1<][>j<] + kr*t[>i<][>j+1<] + kb*t[>i+1<][>j<] +tel + +fun convol_1_h <> (t:int^n^m; line : int^m; i :int) returns (r :int^m) +let + r = mapi<> (kernel_1<>)<(t,i)> (line) +tel + +fun convol_1 <> (t:int^n^m) returns (r :int^n^m) +let + r = mapi<> ( convol_1_h<> ) <(t)> (t) +tel + + +(* Deal with matrix of size n*m, apply coeff : + ktt + klt kt ktr + kll kl k kr krr + kbl kb krb + kbb + centered on [>i<][>j<]. *) +fun kernel_2 <> (t :int^n^m; i,x,j :int) returns (r :int) +let + r = ktt*t[>i-2<][>j<]+ + klt*t[>i-1<][>j-1<]+ kt*t[>i-1<][>j<]+ ktr*t[>i-1<][>j+1<]+ + kll*t[>i<][>j-2<]+ kl*t[>i<][>j-1<]+ k*t[>i<][>j<]+ kr*t[>i<][>j+1<]+ krr*t[>i<][>j+2<]+ + kbl*t[>i+1<][>j-1<]+ kb*t[>i+1<][>j<]+ krb*t[>i+1<][>j+1<]+ + kbb*t[>i+2<][>j<]; +tel + +fun convol_2_h<> (t:int^n^m; line : int^m; i :int) returns (r :int^m) +let + r = mapi<> (kernel_2<>) <(t,i)> (line) +tel + +fun convol_2<>(t:int^n^m) returns (r :int^n^m) +let + r = mapi<> (convol_2_h<>) <(t)> (t) +tel + diff --git a/test/good/downscale.ept b/test/good/downscale.ept new file mode 100644 index 0000000..4fc1c9f --- /dev/null +++ b/test/good/downscale.ept @@ -0,0 +1,152 @@ + +type pixel = float^3 + +node nat() returns (n :int) +let + n = 0 fby n+1 +tel + +fun pix_sum(x1,x2 :pixel) returns (r :pixel) +let + r = map<<3>> (+.) (x1,x2); +tel + +fun pix_div(x :pixel; c :float) returns (r :pixel) +let + r = map<<3>> (/.) (x, c^3); +tel + +const pix_zero :pixel = 0.0^3 +const pix_o :pixel = [1.0,1.0,1.0] + +node counter() returns (cpt :int) +let + cpt = (0 fby cpt) + 1 +tel + +node counter_r(res :bool) returns (cpt :int) +let + reset + cpt = inlined counter() + every res +tel + +(* count from 1 to m included, reset to 1 when [res] *) +node mod_counter_r<>(res :bool) returns (cpt :int) +let + reset + cpt = (0 fby cpt) + 1 + every (res or (0 fby cpt = m)) +tel + +(* count from 1 to m included *) +node mod_counter<>() returns (cpt :int) +let + cpt = inlined mod_counter_r<>(false) +tel + + +node current(x :int; ck :bool) returns (c :int) +let + c = merge ck x ((0 fby c) whenot ck) +tel +node current_bool(x :bool; ck :bool) returns (c :bool) +let + c = merge ck x ((false fby c) whenot ck) +tel + +fun flatten_clock(x :pixel ::.on ck on ck2; ck :bool ::.; ck2 :bool ::.on ck) returns (y :pixel; ck2_flat :bool :: .) +var x_ck, x_base : pixel; +let + x_ck = merge ck2 x pix_o; + x_base = merge ck x_ck pix_o; + ck2_flat = merge ck ck2 false; + y = x_base when ck2_flat; +tel + + +node transpose<>(i :pixel) returns (o :pixel) +var store :pixel^x^y^2; (*This is the double buffer*) + i_x, i_y, o_x, o_y :int; (*These are current buffer indexes*) + i_line, o_line, i_img :bool; (*These define line and img beginning*) + i_buff, o_buff :int; (*These are used to control the double buffering*) +let + i_x = mod_counter<>() - 1; + i_line = i_x = 0; + i_y = current (mod_counter<>() - 1, i_line); + i_img = (i_x = 0) & (i_y = 0); + i_buff = current(mod_counter<<2>>() - 1, i_img); + o_buff = (i_buff + 1) % 2; + o_y = mod_counter<>() -1; + o_line = o_y = 0; + o_x = current (mod_counter<>()-1, o_line); + store = (pix_zero^x^y^2) fby [store with [i_buff][i_y][i_x] = i]; + o = store[>o_buff<][>o_y<][>o_x<]; +tel + + +(* a fby-n would be nice to allow average of the last n pixels *) +(* returns the average of the last 3 pixels when asked *) +node down(x :pixel; out :bool) returns (r :pixel :: . on out) +var x1, x2 : pixel; +let + x1 = x fby x; + x2 = x fby x1; + r = pix_div(pix_sum(x when out, pix_sum(x1 when out, x2 when out)), 3.0 ); +tel + +node down_line<>(x :pixel) returns (r :pixel; r_clock :bool) +let + r_clock = mod_counter<>() = ratio; + r = down(x,r_clock); +tel + + +node down_img <> (x :pixel :: .) +returns (y_flat :pixel; y_clock :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool + ) +var + x_line, y_dh_t_line :bool; + +let + x_line = mod_counter<>() = 1; + reset + (y_dh, ck_y_dh) = down_line<>(x) + every x_line; + y_dh_t = transpose<>(y_dh); + y_dh_t_line = current_bool(mod_counter<>() = 1, ck_y_dh); + reset + (y_dhv_t, ck_y_dhv) = down_line<>(y_dh_t) + every y_dh_t_line; + y = transpose<>(y_dhv_t); + (*flatten clock of y, in order to return only one, instead of ck_y_dh on ck_y_dhv*) + (y_flat, y_clock) = flatten_clock(y, ck_y_dh, ck_y_dhv); +tel + + +(*node main () returns (img, out : pixel; ck_out, ck_out_2 :bool) +(*var img : pixel;*) +let + img = pix_o; + (out, ck_out, ck_out_2) = down_img<<2,2,2,2>>(img); +tel*) + +node mainp<> () returns (img, out : pixel; ck_out :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool) +(*var img : pixel;*) +let + (*ck_out = true fby false fby not ck_out;*) + img = pix_o fby pix_sum(img, pix_o); + (out, ck_out, y, y_dh, y_dh_t, y_dhv_t, ck_y_dh, ck_y_dhv) = down_img<>(img); +tel + +node main() returns (img, out : pixel; ck_out :bool; + y, y_dh, y_dh_t, y_dhv_t :pixel; + ck_y_dh, ck_y_dhv :bool) +let + (img, out, ck_out, y, y_dh, y_dh_t, y_dhv_t, ck_y_dh, ck_y_dhv) = mainp<<640,480>>(); +tel + diff --git a/test/good/foldi_arrays.ept b/test/good/foldi_arrays.ept new file mode 100644 index 0000000..1046546 --- /dev/null +++ b/test/good/foldi_arrays.ept @@ -0,0 +1,24 @@ + +type t = A | B | C + +const n:int = 10 + +type couple = { t1 : int^n; t2 : int^n } + +fun f (a:t;b:float;i:int;acc_in:couple) = (acc_out:couple) +let + switch a + | A do acc_out = { t1 = [ acc_in.t1 with [1] = acc_in.t1[1] + 1 ]; t2 = acc_in.t2 } + | B do acc_out = acc_in + | C do acc_out = { acc_in with .t2 = map<> (+)(acc_in.t1,acc_in.t2) } + end +tel + + +node main() returns (o:couple) +var a:t^n; b:float^n; +let + a = [A, B, C, A, B, C, A, B, C, A]; + b = 0.001^n; + o = foldi<> f (a, b, { t1 = 0^n; t2 = 0^n }); +tel diff --git a/test/good/mapnot.ept b/test/good/mapnot.ept new file mode 100644 index 0000000..cbf0724 --- /dev/null +++ b/test/good/mapnot.ept @@ -0,0 +1,15 @@ +type s = bool^10 +type t = { x : s } + +node g() returns (c : t) +var + b : s; +let + c = {x = false^10}; + b = map <<10>> (not) (true^10); +tel + +node main() returns (c:t) +let + c = g(); +tel diff --git a/test/good/pip.ept b/test/good/pip.ept new file mode 100644 index 0000000..c93f11b --- /dev/null +++ b/test/good/pip.ept @@ -0,0 +1,19 @@ +fun pip_line<> (line1 :int^m1; line2 :int^m2) returns (r :int^m1) +let + r = line1[0 .. y-1] @ line2 @ line1[y+m2 .. m1-1] +tel + +fun pip<> (t1 :int^n1^m1; t2 :int^n2^m2) returns (r :int^n1^m1) +var t12 :int^m1^n2; +let + t12 = map<> (pip_line<>) (t1[x..x+n2-1], t2); + r = t1[0 .. x-1] @ t12 @ t1[x+n2 .. n1-1]; +tel + +node main() returns (r :int^10^10) +var x,y:int; +let + x = 0 fby x+1; + y = x*x; + r = pip<<10,10,2,2,3,3>>(x^10^10,y^2^2); +tel diff --git a/test/good/pip_slice.ept b/test/good/pip_slice.ept new file mode 100644 index 0000000..c93f11b --- /dev/null +++ b/test/good/pip_slice.ept @@ -0,0 +1,19 @@ +fun pip_line<> (line1 :int^m1; line2 :int^m2) returns (r :int^m1) +let + r = line1[0 .. y-1] @ line2 @ line1[y+m2 .. m1-1] +tel + +fun pip<> (t1 :int^n1^m1; t2 :int^n2^m2) returns (r :int^n1^m1) +var t12 :int^m1^n2; +let + t12 = map<> (pip_line<>) (t1[x..x+n2-1], t2); + r = t1[0 .. x-1] @ t12 @ t1[x+n2 .. n1-1]; +tel + +node main() returns (r :int^10^10) +var x,y:int; +let + x = 0 fby x+1; + y = x*x; + r = pip<<10,10,2,2,3,3>>(x^10^10,y^2^2); +tel diff --git a/test/good/quasi.ept b/test/good/quasi.ept new file mode 100644 index 0000000..617ea7d --- /dev/null +++ b/test/good/quasi.ept @@ -0,0 +1,51 @@ +(* include "notsameperiod2.lus" *) + +type data = int + +const v:data = 0 + +node current (v : data; c : bool; u : data) +returns (o : data) +let + o = merge c u ((v fby o) whenot c) +tel + +node mem (v : data; cw : bool; u : data) +returns (o : data) +let + o = v fby (current (v, cw, u)) +tel + +node mcounter (start, limit : int) +returns (o : int) +let + o = (start -> (pre o + 1)) % limit; +tel + +node twonodes (cw, cr : bool) +returns (ok : bool) +var uw, ur : int; +let + uw = mcounter((0, 5) when cw); + ur = mem(v, cw, uw) when cr; + ok = (mem(v, cr, ur) = mem(v, cw, uw)) + or (mem(v, cr, ur)= mem(v, cw, v fby uw)) + or (mem(v, cr, ur) = mem(v, cw, v fby v fby uw)); +tel + +(* +node verify (cw, cr : bool) +returns (ok : bool) +let + ok = twonodes(cw, cr); + assert(not notsameperiod2(cw, cr)); +tel +*) + +node main() returns (ok:bool) + var cw, cr : bool; +let + cw = false fby not cw; + cr = not cw; + ok = twonodes(cw,cr); +tel