Add deep map patch test

This commit is contained in:
John David Pressman 2019-10-14 10:19:18 -07:00
parent 5070ded5b9
commit 93b5a068b5
3 changed files with 15 additions and 0 deletions

View File

@ -33,6 +33,9 @@ function patch_empty (var m : foobar) : foobar is block {
patch m with map [] patch m with map []
} with m } with m
function patch_deep (var m: foobar * nat) : foobar * nat is
begin patch m.0 with map [1 -> 9]; end with m
function size_ (const m : foobar) : nat is function size_ (const m : foobar) : nat is
block {skip} with (size(m)) block {skip} with (size(m))

View File

@ -17,6 +17,9 @@ let patch_ (m : foobar) : foobar = Map.literal [ (0, 5) ; (1, 6) ; (2, 7) ]
(* Second dummy test, see above *) (* Second dummy test, see above *)
let patch_empty (m : foobar) : foobar = Map.literal [ (0, 0) ; (1, 1) ; (2, 2) ] let patch_empty (m : foobar) : foobar = Map.literal [ (0, 0) ; (1, 1) ; (2, 2) ]
(* Third dummy test, see above *)
let patch_deep (m: foobar * nat) : foobar * nat = (Map.literal [ (0, 0) ; (1, 9) ; (2, 2) ], 10p)
let size_ (m : foobar) : nat = Map.size m let size_ (m : foobar) : nat = Map.size m
let gf (m : foobar) : int = Map.find 23 m let gf (m : foobar) : int = Map.find 23 m

View File

@ -421,6 +421,15 @@ let map_ type_f path : unit result =
let expected = ez [(0,0) ; (1,1) ; (2,2)] in let expected = ez [(0,0) ; (1,1) ; (2,2)] in
expect_eq program "patch_empty" input expected expect_eq program "patch_empty" input expected
in in
let%bind () =
let input = (e_pair
(ez [(0,0) ; (1,1) ; (2,2)])
(e_nat 10)) in
let expected = (e_pair
(ez [(0,0) ; (1,9) ; (2,2)])
(e_nat 10)) in
expect_eq program "patch_deep" input expected
in
let%bind () = let%bind () =
let make_input = fun n -> ez List.(map (fun x -> (x, x)) @@ range n) in let make_input = fun n -> ez List.(map (fun x -> (x, x)) @@ range n) in
let make_expected = e_nat in let make_expected = e_nat in