23 open Hints_declaration
55 type 'a labelled_obj =
56 (PreIdentifiers.identifier Types.option, 'a) Types.prod
58 (** val instruction_matches_identifier :
59 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
60 labelled_obj -> Bool.bool **)
61 let instruction_matches_identifier tag y x =
62 match x.Types.fst with
63 | Types.None -> Bool.False
64 | Types.Some x0 -> Identifiers.eq_identifier tag x0 y
66 (** val does_not_occur :
67 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
68 labelled_obj List.list -> Bool.bool **)
69 let rec does_not_occur tag id = function
70 | List.Nil -> Bool.True
71 | List.Cons (x, l0) ->
72 Bool.andb (Bool.notb (instruction_matches_identifier tag id x))
73 (does_not_occur tag id l0)
75 (** val occurs_exactly_once :
76 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
77 labelled_obj List.list -> Bool.bool **)
78 let rec occurs_exactly_once tag id = function
79 | List.Nil -> Bool.False
80 | List.Cons (x, l0) ->
81 (match instruction_matches_identifier tag id x with
82 | Bool.True -> does_not_occur tag id l0
83 | Bool.False -> occurs_exactly_once tag id l0)
85 (** val index_of_internal :
86 ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> Nat.nat **)
87 let rec index_of_internal test l acc =
89 | List.Nil -> assert false (* absurd case *)
90 | List.Cons (x, tl) ->
93 | Bool.False -> index_of_internal test tl (Nat.S acc))
95 (** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
97 index_of_internal test l Nat.O
99 (** val index_of_label :
100 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
101 labelled_obj List.list -> Nat.nat **)
102 let index_of_label tag l =
103 index_of (instruction_matches_identifier tag l)