val merge (#a: eqtype) (#b: Type u#b) (m1: map a b) (m2: map a b)
  : map a b
let merge (#a: eqtype) (#b: Type u#b) (m1: map a b) (m2: map a b) : map a b =
  let keys' = FSet.union (domain m1) (domain m2) in
  let f' = on_domain a (fun key -> if FSet.mem key (domain m2) then (elements m2) key else (elements m1) key) in
  (| keys', f' |)
val merge (#a: eqtype) (#b: Type u#b) (m1: map a b) (m2: map a b)
  : map a b
let merge (#a: eqtype) (#b: Type u#b) (m1 m2: map a b) : map a b =
let keys' = FSet.union (domain m1) (domain m2) in
let f' =
  on_domain a (fun key -> if FSet.mem key (domain m2) then (elements m2) key else (elements m1) key)
in
(| keys', f' |)
FStar.FiniteMap.Base.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.FiniteSet.Base.fsti.checked FStar.FiniteSet.Ambient.fst.checked FStar.Classical.Sugar.fsti.checked
FStar.FiniteMap.Base.fst
Prims.eqtype FStar.FiniteMap.Base.map Prims.Mkdtuple2 FStar.FiniteSet.Base.set FStar.FiniteMap.Base.setfun_t FStar.Pervasives.Native.option FStar.FunctionalExtensionality.on_domain FStar.FiniteSet.Base.mem FStar.FiniteMap.Base.domain FStar.FiniteMap.Base.elements Prims.bool FStar.FiniteSet.Base.union
(*
   Copyright 2008-2021 John Li, Jay Lorch, Rustan Leino, Alex Summers,
   Dan Rosen, Nikhil Swamy, Microsoft Research, and contributors to
   the Dafny Project

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Includes material from the Dafny project
   (https://github.com/dafny-lang/dafny) which carries this license
   information:

     Created 9 February 2008 by Rustan Leino.
     Converted to Boogie 2 on 28 June 2008.
     Edited sequence axioms 20 October 2009 by Alex Summers.
     Modified 2014 by Dan Rosen.
     Copyright (c) 2008-2014, Microsoft.
     Copyright by the contributors to the Dafny Project
     SPDX-License-Identifier: MIT
*)

(**
This module declares a type and functions used for modeling
finite maps as they're modeled in Dafny.

@summary Type and functions for modeling finite maps
*)
module FStar.FiniteMap.Base

open FStar.FunctionalExtensionality
module FLT = FStar.List.Tot
module FSet = FStar.FiniteSet.Base
open FStar.FiniteSet.Ambient
module T = FStar.Tactics.V2

// Finite maps
type map (a: eqtype) (b: Type u#b) = (keys: FSet.set a) & (setfun_t a b keys)

let domain (#a: eqtype) (#b: Type u#b) (m: map a b) : FSet.set a =
  let (| keys, _ |) = m in 
  keys


let elements (#a: eqtype) (#b: Type u#b) (m: map a b) : (setfun_t a b (domain m)) =
  let (| _, f |) = m in
  f
  
let rec key_list_to_item_list
  (#a: eqtype)
  (#b: Type u#b)
  (m: map a b)
  (keys: list a{FSet.list_nonrepeating keys /\ (forall key. FLT.mem key keys ==> FSet.mem key (domain m))})
: GTot (items: list (a * b){item_list_doesnt_repeat_keys items /\ (forall key. FLT.mem key keys <==> key_in_item_list key items)})
       (decreases keys) =
  match keys with
  | [] -> []
  | key :: remaining_keys -> (key, Some?.v ((elements m) key)) :: key_list_to_item_list m remaining_keys

let map_as_list (#a: eqtype) (#b: Type u#b) (m: map a b)
: GTot (items: list (a * b){item_list_doesnt_repeat_keys items /\ (forall key. key_in_item_list key items <==> mem key m)}) =
  key_list_to_item_list m (FSet.set_as_list (domain m))

/// We represent the Dafny function `Map#Card` with `cardinality`:
///
/// function Map#Card<U,V>(Map U V) : int;

let cardinality (#a: eqtype) (#b: Type u#b) (m: map a b) : GTot nat =
  FSet.cardinality (domain m)

/// We represent the Dafny function `Map#Values` with `values`:
///
/// function Map#Values<U,V>(Map U V) : Set V;

let values (#a: eqtype) (#b: Type u#b) (m: map a b) : GTot (b -> prop) =
  fun value -> exists key. ((elements m) key == Some value)

/// We represent the Dafny function `Map#Items` with `items`:
///
/// function Map#Items<U,V>(Map U V) : Set Box;

let items (#a: eqtype) (#b: Type u#b) (m: map a b) : GTot ((a * b) -> prop) =
  fun item -> ((elements m) (fst item) == Some (snd item))

/// We represent the Dafny function `Map#Empty` with `emptymap`:
///
/// function Map#Empty<U, V>(): Map U V;

let emptymap (#a: eqtype) (#b: Type u#b) : (map a b) =
  (| FSet.emptyset, on_domain a (fun key -> None) |)

/// We represent the Dafny function `Map#Glue` with `glue`.
///
/// function Map#Glue<U, V>([U]bool, [U]V, Ty): Map U V;

let glue (#a: eqtype) (#b: Type u#b) (keys: FSet.set a) (f: setfun_t a b keys) : map a b =
  (| keys, f |)
  
/// We represent the Dafny function `Map#Build` with `build`:
///
/// function Map#Build<U, V>(Map U V, U, V): Map U V;

let insert (#a: eqtype) (#b: Type u#b) (k: a) (v: b) (m: map a b) : map a b =
  let keys' = FSet.insert k (domain m) in
  let f' = on_domain a (fun key -> if key = k then Some v else (elements m) key) in
  (| keys', f' |)

/// We represent the Dafny function `Map#Merge` with `merge`:
///
/// function Map#Merge<U, V>(Map U V, Map U V): Map U V;
val merge (#a: eqtype) (#b: Type u#b) (m1: map a b) (m2: map a b)
  : map a b
m1: FStar.FiniteMap.Base.map a b -> m2: FStar.FiniteMap.Base.map a b -> FStar.FiniteMap.Base.map a b