matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 val raise_error: RolesTypes.error -> 'a
  13
  14 val list_apply: (int -> 'a -> bool) -> ('a -> unit) -> int -> 'a list -> bool
  15
  16 val list_nth: ('a -> unit) -> int -> 'a list -> unit
  17
  18 val list_split: ('a -> bool) -> ('a -> unit) -> 'a list -> 'a list * 'a list
  19
  20 val list_visit:
  21   (string -> string -> unit) -> (string -> bool -> string -> unit) ->
  22   (RolesTypes.pointer -> 'a -> unit) -> (unit -> unit) ->
  23   ('a -> bool) -> ('a -> string) -> RolesTypes.pointer -> 'a list -> unit
  24
  25 val string_of_stage: RolesTypes.stage -> string
  26
  27 val stage_of_string: string -> RolesTypes.stage
  28
  29 val stage_compare: RolesTypes.stage -> RolesTypes.stage -> int
  30
  31 val string_of_nobj: RolesTypes.nobj -> string
  32
  33 val nobj_of_string: string -> RolesTypes.nobj
  34
  35 val nobj_selected: RolesTypes.nobj -> bool
  36
  37 val nobj_select: RolesTypes.nobj -> unit
  38
  39 val nobj_union: RolesTypes.nobjs -> RolesTypes.nobjs -> RolesTypes.nobjs
  40
  41 val string_of_oobj: RolesTypes.oobj -> string
  42
  43 val oobj_of_string: string -> RolesTypes.oobj
  44
  45 val oobj_selected: RolesTypes.oobj -> bool
  46
  47 val oobj_select: RolesTypes.oobj -> unit
  48
  49 val oobj_union: RolesTypes.oobjs -> RolesTypes.oobjs -> RolesTypes.oobjs
  50
  51 val oobj_match: int -> int -> RolesTypes.oobjs -> RolesTypes.nobjs -> (int * int) option
  52
  53 val string_of_robj: RolesTypes.robj -> string
  54
  55 val robj_selected: RolesTypes.robj -> bool
  56
  57 val robj_select: RolesTypes.robj -> unit
  58
  59 val robj_expand: RolesTypes.robj -> unit
  60
  61 val robj_union: RolesTypes.robjs -> RolesTypes.robjs -> RolesTypes.robjs
  62
  63 val robj_tops: RolesTypes.stage -> RolesTypes.robjs -> RolesTypes.oobjs * RolesTypes.oobjs
  64
  65 val robj_split:
  66   RolesTypes.stage -> RolesTypes.robjs ->
  67   RolesTypes.robjs * RolesTypes.oobjs * RolesTypes.nobjs
  68
  69 val new_status: RolesTypes.status
  70
  71 val string_of_pointer: RolesTypes.pointer -> string
  72
  73 val pointer_of_string: string -> RolesTypes.pointer
  74
  75 val string_of_error: RolesTypes.error -> string