bench/check-ce/maps_mono.mlw

   1 module MapIntInt
   2
   3   type mapintint = int -> int
   4
   5   let function get (f: mapintint) (x: int) : int = f x
   6
   7   let ghost function set (f: mapintint) (x: int) (v: int) : mapintint =
   8     fun y -> if pure {y = x} then v else f y
   9
  10 end
  11
  12 module MapIntBool
  13
  14   type mapintbool = int -> bool
  15
  16   let function get (f: mapintbool) (x: int) : bool = f x
  17
  18   let ghost function set (f: mapintbool) (x: int) (v: bool) : mapintbool =
  19     fun y -> if pure {y = x} then v else f y
  20
  21 end
  22
  23 module MapMulti
  24
  25   use MapIntInt
  26
  27   type mapmulti = int -> mapintint
  28
  29   let function get (f: mapmulti) (x: int) : mapintint = f x
  30
  31   let ghost function set (f: mapmulti) (x: int) (v: mapintint) : mapmulti =
  32     fun y -> if pure {y = x} then v else f y
  33
  34 end
  35
  36 module M
  37
  38   use int.Int
  39   use ref.Ref
  40   use MapIntInt
  41   use MapIntBool
  42   use MapMulti
  43
  44   let ghost test_map (ghost x : ref mapintint) : unit
  45     ensures { MapIntInt.get !x 0 <> MapIntInt.get !x 1 }
  46   =
  47     x := MapIntInt.set !x 0 3
  48
  49   (* Multi-dimensional maps *)
  50   let ghost test_map_multidim1 (ghost x : ref mapmulti) : unit
  51     ensures { MapIntInt.get (MapMulti.get !x 0) 0 <> MapIntInt.get (MapMulti.get !x 1) 1 }
  52   =
  53     x := MapMulti.set !x 0 (MapMulti.get !x 1)
  54
  55   let ghost test_map_multidim2 (ghost x : ref mapmulti) : unit
  56     ensures { MapIntInt.get (MapMulti.get !x 0) 0 <> MapIntInt.get (MapMulti.get !x 1) 1 }
  57   =
  58     let x0 = MapMulti.get !x 0 in
  59     let x0 = MapIntInt.set x0 0 3 in
  60     x := MapMulti.set !x 0 x0
  61
  62   let ghost proj_map_test1 (ghost x : ref mapintint) : unit
  63     ensures { MapIntInt.get !x 0 <> MapIntInt.get !x 1 }
  64   =
  65     x := MapIntInt.set !x 0 3
  66
  67   let ghost proj_map_test2 (ghost x : ref mapintbool) : unit
  68     ensures { MapIntBool.get !x 0 <> MapIntBool.get !x 1 }
  69   =
  70     x := MapIntBool.set !x 0 true
  71
  72 end
  73
  74 theory ModelMap
  75
  76 use MapIntInt
  77
  78 goal t1 : forall t:mapintint, i : int.
  79    get (set t 0 42) i = get t i
  80
  81 end