source: driver/extracted/assocList.ml @ 3106

Last change on this file since 3106 was 2842, checked in by sacerdot, 7 years ago

The compiler can now show all back-end traces too (assembly and object code
are excluded ATM).

File size: 979 bytes
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21type ('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 **)
26let 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 **)
32let 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 **)
40let 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
Note: See TracBrowser for help on using the repository browser.