source: extracted/assocList.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.
File size: 984 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 (hd0, tl) ->
35  Bool.orb (eq hd0.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 (hd0, tl) ->
43  (match eq hd0.Types.fst a with
44   | Bool.True -> Types.Some hd0.Types.snd
45   | Bool.False -> assoc_list_lookup a eq tl)
46
Note: See TracBrowser for help on using the repository browser.