extracted/assocList.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 type ('a, 'b) assoc_list = ('a, 'b) Types.prod List.list
  22
  23 (** val assoc_list_add :
  24     ('a1, 'a2) Types.prod -> ('a1, 'a2) assoc_list -> ('a1, 'a2) Types.prod
  25     List.list **)
  26 let assoc_list_add el al =
  27   List.Cons (el, al)
  28
  29 (** val assoc_list_exists :
  30     'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
  31     Bool.bool **)
  32 let rec assoc_list_exists a eq = function
  33 | List.Nil -> Bool.False
  34 | List.Cons (hd, tl) ->
  35   Bool.orb (eq hd.Types.fst a) (assoc_list_exists a eq tl)
  36
  37 (** val assoc_list_lookup :
  38     'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
  39     'a2 Types.option **)
  40 let rec assoc_list_lookup a eq = function
  41 | List.Nil -> Types.None
  42 | List.Cons (hd, tl) ->
  43   (match eq hd.Types.fst a with
  44    | Bool.True -> Types.Some hd.Types.snd
  45    | Bool.False -> assoc_list_lookup a eq tl)
  46