open Preamble

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Lists

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Positive

open Identifiers

type 'a labelled_obj =
  (PreIdentifiers.identifier Types.option, 'a) Types.prod

(** val instruction_matches_identifier :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
    labelled_obj -> Bool.bool **)
let instruction_matches_identifier tag y x =
  match x.Types.fst with
  | Types.None -> Bool.False
  | Types.Some x0 -> Identifiers.eq_identifier tag x0 y

(** val does_not_occur :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
    labelled_obj List.list -> Bool.bool **)
let rec does_not_occur tag id = function
| List.Nil -> Bool.True
| List.Cons (x, l0) ->
  Bool.andb (Bool.notb (instruction_matches_identifier tag id x))
    (does_not_occur tag id l0)

(** val occurs_exactly_once :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
    labelled_obj List.list -> Bool.bool **)
let rec occurs_exactly_once tag id = function
| List.Nil -> Bool.False
| List.Cons (x, l0) ->
  (match instruction_matches_identifier tag id x with
   | Bool.True -> does_not_occur tag id l0
   | Bool.False -> occurs_exactly_once tag id l0)

(** val index_of_internal :
    ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> Nat.nat **)
let rec index_of_internal test l acc =
  match l with
  | List.Nil -> assert false (* absurd case *)
  | List.Cons (x, tl) ->
    (match test x with
     | Bool.True -> acc
     | Bool.False -> index_of_internal test tl (Nat.S acc))

(** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
let index_of test l =
  index_of_internal test l Nat.O

(** val index_of_label :
    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
    labelled_obj List.list -> Nat.nat **)
let index_of_label tag l =
  index_of (instruction_matches_identifier tag l)