Commit a9e7f3c8 authored by Robbert Krebbers's avatar Robbert Krebbers

Make the types of the finite map operational type classes explicit, and make some more specific.

parent 884299ba
...@@ -161,10 +161,11 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope. ...@@ -161,10 +161,11 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x X) (only parsing) : C_scope. Notation "(∉ X )" := (λ x, x X) (only parsing) : C_scope.
(** ** Operations on maps *) (** ** Operations on maps *)
(** In this file we will only define operational type classes for the (** In this section we define operational type classes for the operations
operations on maps. In the file [fin_maps] we will axiomatize finite maps. on maps. In the file [fin_maps] we will axiomatize finite maps.
The function lookup [m !! k] should yield the element at key [k] in [m]. *) The function lookup [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup K M := lookup: {A}, K M A option A. Class Lookup (K : Type) (M : Type Type) :=
lookup: {A}, K M A option A.
Instance: Params (@lookup) 4. Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope. Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
...@@ -174,43 +175,43 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope. ...@@ -174,43 +175,43 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with (** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *) value [a] in [m]. *)
Class Insert K M := Class Insert (K : Type) (M : Type Type) :=
insert: {A}, K A M A M A. insert: {A}, K A M A M A.
Instance: Params (@insert) 4. Instance: Params (@insert) 4.
Notation "<[ k := a ]>" := (insert k a) Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : C_scope. (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
(** The function delete [delete k m] should deletes the value at key [k] in (** The function delete [delete k m] should delete the value at key [k] in
[m]. *) [m]. If the key [k] is not a member of [m], the original map should be
Class Delete K M := returned. *)
delete: K M M. Class Delete (K : Type) (M : Type Type) :=
Instance: Params (@delete) 3. delete: {A}, K M A M A.
Instance: Params (@delete) 4.
(** The function [alter f k m] should update the value at key [k] using the (** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k]. When [k] is function [f], which is called with the original value. *)
not a member of [m], the original map should be returned. *) Class Alter (K : Type) (M : Type Type) :=
Class Alter K M :=
alter: {A}, (A A) K M A M A. alter: {A}, (A A) K M A M A.
Instance: Params (@alter) 4. Instance: Params (@alter) 4.
(** The function [alter f k m] should update the value at key [k] using the (** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None] if function [f], which is called with the original value at key [k] or [None]
[k] is not a member of [m]. The value at [k] should be deleted if [f] yields if [k] is not a member of [m]. The value at [k] should be deleted if [f]
[None]. *) yields [None]. *)
Class PartialAlter K M := Class PartialAlter (K : Type) (M : Type Type) :=
partial_alter: {A}, (option A option A) K M A M A. partial_alter: {A}, (option A option A) K M A M A.
Instance: Params (@partial_alter) 4. Instance: Params (@partial_alter) 4.
(** The function [dom C m] should yield the domain of [m]. That is a finite (** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *) collection of type [C] that contains the keys that are a member of [m]. *)
Class Dom K M := Class Dom (K : Type) (M : Type Type) :=
dom: C `{Empty C} `{Union C} `{Singleton K C}, M C. dom: {A} C `{Empty C} `{Union C} `{Singleton K C}, M A C.
Instance: Params (@dom) 7. Instance: Params (@dom) 8.
(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)] constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]
provided that [k] is a member of either [m1] or [m2].*) provided that [k] is a member of either [m1] or [m2].*)
Class Merge M := Class Merge (M : Type Type) :=
merge: {A}, (option A option A option A) M A M A M A. merge: {A}, (option A option A option A) M A M A M A.
Instance: Params (@merge) 3. Instance: Params (@merge) 3.
...@@ -218,22 +219,22 @@ Instance: Params (@merge) 3. ...@@ -218,22 +219,22 @@ Instance: Params (@merge) 3.
Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A := Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
fold_right (λ p, <[ fst p := snd p ]>) m l. fold_right (λ p, <[ fst p := snd p ]>) m l.
Instance: Params (@insert_list) 4. Instance: Params (@insert_list) 4.
Definition delete_list `{Delete K M} (l : list K) (m : M) : M := Definition delete_list `{Delete K M} {A} (l : list K) (m : M A) : M A :=
fold_right delete m l. fold_right delete m l.
Instance: Params (@delete_list) 3. Instance: Params (@delete_list) 4.
(** The function [union_with f m1 m2] should yield the union of [m1] and [m2] (** The function [union_with f m1 m2] should yield the union of [m1] and [m2]
using the function [f] to combine values of members that are in both [m1] and using the function [f] to combine values of members that are in both [m1] and
[m2]. *) [m2]. *)
Class UnionWith M := Class UnionWith (M : Type Type) :=
union_with: {A}, (A A A) M A M A M A. union_with: {A}, (A A A) M A M A M A.
Instance: Params (@union_with) 3. Instance: Params (@union_with) 3.
(** Similarly for the intersection and difference. *) (** Similarly for the intersection and difference. *)
Class IntersectionWith M := Class IntersectionWith (M : Type Type) :=
intersection_with: {A}, (A A A) M A M A M A. intersection_with: {A}, (A A A) M A M A M A.
Instance: Params (@intersection_with) 3. Instance: Params (@intersection_with) 3.
Class DifferenceWith M := Class DifferenceWith (M : Type Type) :=
difference_with: {A}, (A A option A) M A M A M A. difference_with: {A}, (A A option A) M A M A M A.
Instance: Params (@difference_with) 3. Instance: Params (@difference_with) 3.
......
...@@ -8,11 +8,11 @@ Require Export prelude. ...@@ -8,11 +8,11 @@ Require Export prelude.
(** * Axiomatization of finite maps *) (** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of (** We require Leibniz equality to be extensional on finite maps. This of
course limits the class of finite map implementations, but since we are mainly course limits the space of finite map implementations, but since we are mainly
interested in finite maps with numbers or paths as indexes, we do not consider interested in finite maps with numbers as indexes, we do not consider this to
this a serious limitation. The main application of finite maps is to implement be a serious limitation. The main application of finite maps is to implement
the memory, where extensionality of Leibniz equality becomes very important for the memory, where extensionality of Leibniz equality is very important for a
a convenient use in assertions of our axiomatic semantics. *) convenient use in the assertions of our axiomatic semantics. *)
(** Finiteness is axiomatized by requiring each map to have a finite domain. (** Finiteness is axiomatized by requiring each map to have a finite domain.
Since we may have multiple implementations of finite sets, the [dom] function is Since we may have multiple implementations of finite sets, the [dom] function is
parametrized by an implementation of finite sets over the map's key type. *) parametrized by an implementation of finite sets over the map's key type. *)
...@@ -20,7 +20,7 @@ parametrized by an implementation of finite sets over the map's key type. *) ...@@ -20,7 +20,7 @@ parametrized by an implementation of finite sets over the map's key type. *)
which enables us to give a generic implementation of [union_with], which enables us to give a generic implementation of [union_with],
[intersection_with], and [difference_with]. *) [intersection_with], and [difference_with]. *)
Class FinMap K M `{ A, Empty (M A)} `{Lookup K M} `{FMap M} Class FinMap K M `{ A, Empty (M A)} `{Lookup K M} `{FMap M}
`{PartialAlter K M} `{ A, Dom K (M A)} `{Merge M} := { `{PartialAlter K M} `{Dom K M} `{Merge M} := {
finmap_eq {A} (m1 m2 : M A) : finmap_eq {A} (m1 m2 : M A) :
( i, m1 !! i = m2 !! i) m1 = m2; ( i, m1 !! i = m2 !! i) m1 = m2;
lookup_empty {A} i : lookup_empty {A} i :
...@@ -46,7 +46,7 @@ Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f, ...@@ -46,7 +46,7 @@ Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f,
partial_alter (fmap f). partial_alter (fmap f).
Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x, Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x,
partial_alter (λ _, Some x) k. partial_alter (λ _, Some x) k.
Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) := Instance finmap_delete `{PartialAlter K M} : Delete K M := λ A,
partial_alter (λ _, None). partial_alter (λ _, None).
Instance finmap_singleton `{PartialAlter K M} {A} Instance finmap_singleton `{PartialAlter K M} {A}
`{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>. `{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>.
......
...@@ -27,7 +27,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t, ...@@ -27,7 +27,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
| N0, Build_Nmap o t => Build_Nmap (f o) t | N0, Build_Nmap o t => Build_Nmap (f o) t
| Npos p, Build_Nmap o t => Build_Nmap o (partial_alter f p t) | Npos p, Build_Nmap o t => Build_Nmap o (partial_alter f p t)
end. end.
Global Instance Ndom {A} : Dom N (Nmap A) := λ A _ _ _ t, Global Instance Ndom: Dom N Nmap := λ C _ _ _ _ t,
match t with match t with
| Build_Nmap o t => option_case (λ _, {[ 0 ]}) o (Pdom_raw Npos (`t)) | Build_Nmap o t => option_case (λ _, {[ 0 ]}) o (Pdom_raw Npos (`t))
end. end.
......
...@@ -281,7 +281,7 @@ Section dom. ...@@ -281,7 +281,7 @@ Section dom.
Qed. Qed.
End dom. End dom.
Global Instance Pdom {A} : Dom positive (Pmap A) := λ C _ _ _ t, Global Instance Pdom : Dom positive Pmap := λ C _ _ _ _ t,
Pdom_raw id (`t). Pdom_raw id (`t).
Fixpoint Pmerge_aux `(f : option A option B) (t : Pmap_raw A) : Pmap_raw B := Fixpoint Pmerge_aux `(f : option A option B) (t : Pmap_raw A) : Pmap_raw B :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment