new syntax for parameter (similar to logic and let)

parent 0c051a6e
......@@ -17,49 +17,51 @@ module Array
logic ([]) (a: array 'a) (i: int) : 'a = get a i
logic ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
parameter ([]) : a:array 'a -> i:int ->
parameter ([]) (a:array 'a) (i:int) :
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter ([]<-) : a:array 'a -> i:int -> v:'a ->
parameter ([]<-) (a:array 'a) (i:int) (v:'a) :
{ 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
parameter length (a: array 'a) : {} int { result = a.length }
(* unsafe get/set operations with no precondition *)
exception OutOfBounds
parameter defensive_get: a:array 'a -> i:int ->
let defensive_get (a:array 'a) (i:int) =
{ }
'a reads a raises OutOfBounds
if i < 0 || i >= length a then raise OutOfBounds;
a[i]
{ 0 <= i < length a and result = a[i] }
| OutOfBounds -> { i < 0 or i >= length a }
parameter defensive_set : a:array 'a -> i:int -> v:'a ->
let defensive_set (a: array 'a) (i: int) (v: 'a) =
{ }
unit writes a raises OutOfBounds
if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
{ 0 <= i < length a and a = (old a)[i <- v] }
| OutOfBounds -> { i < 0 or i >= length a }
parameter length : a:array 'a -> {} int { result = a.length }
parameter make : n:int -> v:'a ->
parameter make (n:int) (v:'a) :
{}
array 'a
{ result = {| length = n; elts = M.const v |} }
(* { length result = n and forall i:int. 0 <= i < n -> result[i] = v} *)
parameter append : a1:array 'a -> a2:array 'a ->
parameter append (a1: array 'a) (a2: array 'a) :
{}
array 'a
{ length result = length a1 + length a2 and
(forall i:int. 0 <= i < length a1 -> result[i] = a1[i]) and
(forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]) }
parameter sub : a:array 'a -> ofs:int -> len:int ->
parameter sub (a:array 'a) (ofs:int) (len:int) :
{ 0 <= ofs and ofs + len <= length a }
array 'a
{ length result = len and
forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
parameter copy : a:array 'a ->
parameter copy (a:array 'a) :
{}
array 'a
{ length result = length a and
......@@ -83,17 +85,16 @@ module Array
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
parameter blit :
a1:array 'a -> ofs1:int -> a2:array 'a -> ofs2:int -> len:int ->
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
parameter blit (a1:array 'a) (ofs1:int) (a2:array 'a) (ofs2:int) (len:int) :
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
(* TODO?
- concat : 'a array list -> 'a array
......
......@@ -976,6 +976,9 @@ program_decl:
{ Dletrec $3 }
| PARAMETER lident_rich_pgm labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
| PARAMETER lident_rich_pgm labels list1_type_v_param COLON type_c
{ let tv = Tarrow ($4, $6) in
Dparam (add_lab $2 $3, tv) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, None) }
| EXCEPTION uident labels pure_type
......@@ -1276,6 +1279,20 @@ type_v:
/*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
;
type_v_param:
/* TODO
| simple_type_v
{ [id_anonymous (), Some $1] }
*/
| LEFTPAR lidents_lab COLON type_v RIGHTPAR
{ List.map (fun i -> (i, Some $4)) $2 }
;
list1_type_v_param:
| type_v_param { $1 }
| type_v_param list1_type_v_param { $1 @ $2 }
;
simple_type_v:
| pure_type
{ Tpure $1 }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment