reference.cd 858 Bytes
Newer Older
1
2
(* In CDuce the expression  "ref T exp" returns a reference  *)
(* to the result of "exp" and has type "ref T" provided that *)
3
4
5
(* "exp" is of type "T". References come equipped with three *)
(* operators: ":=" (assignment), "!" (dereferencing), and ";"*) 
(* (sequencing).                                             *)
6

7

8
let stack = ref [Int*] []
9
10

let fun push(x : Int) : []  = 
11
  stack := [x; !stack]
12
13

let fun pop ([] : []) : Int = 
14
  match !stack with [x; y] -> stack := y; x | _ -> raise "Empty stack"
15

16
17

(* In a pattern [ ... ; y] the variable y captures the tail of the *)
18
(* sequence. It is equivalent to [ ... y::_*].                     *)
19
20
21
(* In an expression [ ... ; e ] the expression e denotes the tail  *)
(* of the sequence. It is equivalent to [ ... ] @ e                *)

22
23
24
25
26
27
28
29
30
31

;;

push 1;;
push 2;;
push 3;;
pop [];;
pop [];;
pop [];;
pop [];;