extracted/labelledObjects.ml

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Div_and_mod
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Util
  16
  17 open Bool
  18
  19 open Relations
  20
  21 open Nat
  22
  23 open Hints_declaration
  24
  25 open Core_notation
  26
  27 open Pts
  28
  29 open Logic
  30
  31 open Types
  32
  33 open List
  34
  35 open Lists
  36
  37 open Proper
  38
  39 open PositiveMap
  40
  41 open Deqsets
  42
  43 open ErrorMessages
  44
  45 open PreIdentifiers
  46
  47 open Errors
  48
  49 open Extralib
  50
  51 open Positive
  52
  53 open Identifiers
  54
  55 type 'a labelled_obj =
  56   (PreIdentifiers.identifier Types.option, 'a) Types.prod
  57
  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
  65
  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)
  74
  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)
  84
  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 =
  88   match l with
  89   | List.Nil -> assert false (* absurd case *)
  90   | List.Cons (x, tl) ->
  91     (match test x with
  92      | Bool.True -> acc
  93      | Bool.False -> index_of_internal test tl (Nat.S acc))
  94
  95 (** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
  96 let index_of test l =
  97   index_of_internal test l Nat.O
  98
  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)
 104