Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/labelledObjects.ml

    r2601 r2649  
    66
    77open Deqsets
     8
     9open ErrorMessages
    810
    911open PreIdentifiers
     
    2729open Util
    2830
     31open List
     32
    2933open Lists
    30 
    31 open Positive
    32 
    33 open Char
    3434
    3535open Bool
     
    3939open Nat
    4040
    41 open List
    42 
    43 open String
     41open Positive
    4442
    4543open Hints_declaration
     
    5957
    6058(** val instruction_matches_identifier :
    61     String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj ->
    62     Bool.bool **)
     59    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
     60    labelled_obj -> Bool.bool **)
    6361let instruction_matches_identifier tag y x =
    6462  match x.Types.fst with
     
    6765
    6866(** val does_not_occur :
    69     String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list
    70     -> Bool.bool **)
     67    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
     68    labelled_obj List.list -> Bool.bool **)
    7169let rec does_not_occur tag id = function
    7270| List.Nil -> Bool.True
     
    7674
    7775(** val occurs_exactly_once :
    78     String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list
    79     -> Bool.bool **)
     76    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
     77    labelled_obj List.list -> Bool.bool **)
    8078let rec occurs_exactly_once tag id = function
    8179| List.Nil -> Bool.False
     
    10098
    10199(** val index_of_label :
    102     String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list
    103     -> Nat.nat **)
     100    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> 'a1
     101    labelled_obj List.list -> Nat.nat **)
    104102let index_of_label tag l =
    105103  index_of0 (instruction_matches_identifier tag l)
Note: See TracChangeset for help on using the changeset viewer.