source: driver/extracted/labelledObjects.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.1 KB
Line 
1open Preamble
2
3open Setoids
4
5open Monad
6
7open Option
8
9open Div_and_mod
10
11open Jmeq
12
13open Russell
14
15open Util
16
17open Bool
18
19open Relations
20
21open Nat
22
23open Hints_declaration
24
25open Core_notation
26
27open Pts
28
29open Logic
30
31open Types
32
33open List
34
35open Lists
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Positive
52
53open Identifiers
54
55type '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 **)
61let 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 **)
69let 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 **)
78let 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 **)
87let 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 **)
96let 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 **)
102let index_of_label tag l =
103  index_of (instruction_matches_identifier tag l)
104
Note: See TracBrowser for help on using the repository browser.