tests/test-eval.why

   1
   2
   3 theory T
   4
   5   use int.Int
   6
   7   constant i1 : int = 42
   8
   9   constant i2 : int = 2+2
  10
  11 (* test of the 'let' *)
  12
  13   constant let1 : int = let x = 42 in x * x - 1
  14
  15 (* test of the 'if' *)
  16
  17   constant c2 : int = if true then 1 else 2
  18
  19   constant c3 : int = if true /\ false then 1 else 2
  20
  21   constant c4 : int = if 2 = 2 then 1 else 2
  22
  23   constant c5 : int = if 2 = 3 then 1 else 2
  24
  25   constant c5a : int = if 2 <> 3 then 1 else 2
  26
  27   constant c6 : int = if 2 < 3 /\ 5 >= 6 /\ 7 > 8 \/ 9 <= 10 then 1 else 0
  28
  29   use int.Abs
  30
  31   constant c7 : int = abs 42 + abs (-12)
  32
  33   use list.List
  34
  35 (* test of the 'match' *)
  36
  37   constant l1 : list int = Cons 5 Nil
  38
  39   constant l2 : int = match Cons 5 Nil with Nil -> 1 | Cons _ _ -> 2 end
  40
  41   constant l3 : int = match Cons 5 Nil with Nil -> 1 | Cons x _ -> x end
  42
  43   constant l4 : list int = match Cons 5 (Cons 8 Nil) with
  44     | Nil -> Nil
  45     | Cons x Nil -> Nil
  46     | Cons x (Cons y l) -> Cons y (Cons x l)
  47     end
  48
  49   use list.Append
  50
  51   constant l5 : list 'a = Nil ++ Nil
  52
  53   constant l5a : list int = (Nil : list int) ++ Nil
  54
  55   constant l5b : list int = Nil ++ (Nil : list int)
  56
  57   constant l5c : list int = (Cons 5 Nil) ++ Nil
  58
  59   constant l6 : list int =
  60     Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)
  61
  62   constant l6a : int = match (Nil : list int) ++ Nil with Nil -> 1 | Cons _ _ -> 2 end
  63
  64   constant l6b : int = match (Cons 5 Nil) ++ Nil with Nil -> 1 | Cons _ _ -> 2 end
  65
  66   function prod (l:list int) : int =
  67     match l with
  68     | Nil -> 1
  69     | Cons x r -> x * prod r
  70     end
  71
  72   constant l7 : int = prod (Cons 12 (Cons 34 (Cons 56 Nil)))
  73
  74
  75   function puiss (n:int) (l:list int) : int =
  76     match l with
  77     | Nil -> 1
  78     | Cons _ r -> n * puiss n r
  79     end
  80
  81   constant l8 : int = puiss 2 (Cons 12 (Cons 34 (Cons 56 Nil)))
  82
  83   constant l9 : int = puiss l7 (Cons 12 (Cons 34 (Cons 56 Nil)))
  84
  85   constant l10 : int = puiss l9 (Cons 12 (Cons 34 (Cons 56 Nil)))
  86
  87   constant l11 : int = puiss l10 (Cons 12 (Cons 34 (Cons 56 Nil)))
  88
  89   use map.Map
  90
  91   constant t0 : map int int = (const 42)
  92
  93   constant a0 : int = t0[0]
  94   constant a1 : int = t0[1]
  95
  96   constant t1 : map int int = (const 0)[1<-42]
  97
  98   constant x0 : int = t1[0]
  99   constant x1 : int = t1[1]
 100
 101   constant t2 : map int int = t1[2<-37]
 102
 103   constant y0 : int = t2[0] (* should be 0 *)
 104   constant y1 : int = t2[1] (* should be 42 *)
 105   constant y2 : int = t2[2] (* should be 37 *)
 106
 107   constant t3 : map int int = t2[1<-12]
 108
 109   constant z0 : int = t3[0]
 110   constant z1 : int = t3[1]
 111   constant z2 : int = t3[2]
 112
 113 end
 114
 115
 116 theory Records
 117
 118   use int.Int
 119
 120   type pt = { x : int ; y : int }
 121
 122   constant pt1 : pt = { x = 3 ; y = 4 }
 123
 124   constant t1 : int = pt1.x + pt1.y
 125
 126 end