FormalDB/Table2.mli at master · CornellDataScience/FormalDB · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

type __ = Obj.t

val negb : bool -> bool

val length : 'a1 list -> int

module Nat :
 sig
  val eqb : int -> int -> bool
 end

val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list

val string_dec : char list -> char list -> bool

module Table2 :
 sig
  val string_eq : char list -> char list -> bool

  type entry =
  | Coq_string_entry of char list
  | Coq_nat_entry of float
  | Coq_nil_entry

  val entry_rect : (char list -> 'a1) -> (float -> 'a1) -> 'a1 -> entry -> 'a1

  val entry_rec : (char list -> 'a1) -> (float -> 'a1) -> 'a1 -> entry -> 'a1

  type row = entry list

  type header = char list list

  type table = row list * header

  val get_rowlist : table -> row list

  val get_header : table -> header

  val empty_table : table

  val add_header : header -> table -> row list * header

  val entry_type_match : entry -> entry -> bool

  val row_validity_2_3_bool : row -> row -> bool

  val row_validity_2_3_table : row -> row list -> bool

  val header_matches_first_row : header -> row -> row list -> bool

  val add_row : row -> table -> table

  val entry_eqb : entry -> entry -> bool

  val row_eqb : row -> row -> bool

  val remove_first_row_from_row_list : row -> row list -> row list

  val remove_all_row_from_row_list : row -> row list -> row list

  val remove_all_row_from_table : row -> table -> row list * header

  val remove_first_row_from_table : row -> table -> row list * header

  val filter_row_by_entry : (entry -> bool) -> char list -> header -> row -> bool

  val filter_table_by_entry_helper :
    (entry -> bool) -> char list -> row list -> header -> row list

  val filter_table_by_entry : (entry -> bool) -> char list -> table -> table

  val table_valid_rect : table -> (__ -> __ -> __ -> 'a1) -> 'a1

  val table_valid_rec : table -> (__ -> __ -> __ -> 'a1) -> 'a1

  val entry_is_haram : entry -> bool

  val entry_is_string : char list -> entry -> bool

  val print_table : table -> unit
 end