2011-03-17 17:12:16 +01:00
|
|
|
const n:int = 10
|
|
|
|
const m:int = 10
|
2010-07-09 10:35:54 +02:00
|
|
|
|
|
|
|
node concatenate(a:int^n; b:int^m) returns (o1, o2: int^(n+m))
|
|
|
|
let
|
|
|
|
o1 = a @ b;
|
|
|
|
o2 = b @ a;
|
|
|
|
tel
|
2010-07-28 12:34:07 +02:00
|
|
|
|
2010-07-09 10:35:54 +02:00
|
|
|
node slicing (a:int^n) returns (u1,u2 : int^3)
|
|
|
|
let
|
|
|
|
u1 = a[0 .. 2];
|
|
|
|
u2 = a[3 .. 5];
|
|
|
|
tel
|
|
|
|
|
|
|
|
node elt (a:int^m) returns (o:int^m)
|
|
|
|
var x : int;
|
|
|
|
let
|
|
|
|
x = a[2] + 1;
|
|
|
|
o = [ a with [1] = x ];
|
|
|
|
tel
|
|
|
|
|
2010-07-28 12:34:07 +02:00
|
|
|
node upd_dyn(a:int^m; i:int) returns (o:int^m)
|
|
|
|
let
|
|
|
|
o = [ a with [i] = a[0] ];
|
|
|
|
tel
|
|
|
|
|
2010-07-09 10:35:54 +02:00
|
|
|
node elt_dyn (a:int^m; i:int) returns (o:int^m)
|
|
|
|
var x : int;
|
|
|
|
let
|
|
|
|
x = a.[i] default 3;
|
|
|
|
o = [ a with [1] = x ];
|
|
|
|
tel
|
|
|
|
|
|
|
|
node ten (i: int) returns (o:int^m)
|
|
|
|
let
|
|
|
|
o = i^m;
|
|
|
|
tel
|
|
|
|
|
|
|
|
node constant(a,b:int) returns (o:int^4)
|
|
|
|
let
|
|
|
|
o = [a,b,a,b];
|
|
|
|
tel
|
2011-03-17 17:12:16 +01:00
|
|
|
|
|
|
|
|
|
|
|
node test1() returns (r1,r2: int^3)
|
|
|
|
var x,y : int^10; z,t : int^20;
|
|
|
|
let
|
|
|
|
x = ten(3);
|
|
|
|
y = ten(4);
|
|
|
|
(z,t) = concatenate(x,y);
|
|
|
|
(r1,r2) = slicing(x);
|
|
|
|
tel
|
2011-03-22 22:12:59 +01:00
|
|
|
|
|
|
|
node elt_trunc (a:int^m^m; i,j:int) returns (o : int)
|
|
|
|
let
|
|
|
|
o = a[>i<][>j<];
|
|
|
|
tel
|