matita/components/binaries/matex/ground.ml

   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 module L = List
  13 module P = Printf
  14 module S = String
  15
  16 exception Error of string
  17
  18 (* interface functions ******************************************************)
  19
  20 let id x = x
  21
  22 let id2 x y = x, y
  23
  24 let rec segments_of_string ss l s =
  25    match try Some (S.index s '/') with Not_found -> None with
  26       | None   -> s :: ss
  27       | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
  28
  29 let rec rev_map_concat map sep r = function
  30    | []                  -> r
  31    | s :: ss             ->
  32       if r = "" then rev_map_concat map sep (map s) ss else
  33       rev_map_concat map sep (map s ^ sep ^ r) ss
  34
  35 let fold_string map a s =
  36    let l = S.length s in
  37    let rec aux i a =
  38       if i >= l then a else aux (succ i) (map a s.[i])
  39    in
  40    aux 0 a
  41
  42 let rec rev_neg_filter filter r = function
  43    | []       -> r
  44    | hd :: tl ->
  45       if filter hd then rev_neg_filter filter r tl else rev_neg_filter filter (hd :: r) tl
  46
  47 let rec foldi_left mapi i a = function
  48    | []       -> a
  49    | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
  50
  51 let rec rev_mapi mapi i l =
  52    let map i a hd = mapi i hd :: a in
  53    foldi_left map i [] l
  54
  55 let rec rev_map_append map l r = match l with
  56    | []       -> r
  57    | hd :: tl -> rev_map_append map tl (map hd :: r)
  58
  59 let rec split_at x = function
  60    | l when x <= 0 -> [], l
  61    | []       -> [], []
  62    | hd :: tl ->
  63       let l1, l2 = split_at (pred x) tl in
  64       hd :: l1, l2
  65
  66 let error s = raise (Error s)
  67
  68 let log s = P.eprintf "MaTeX: %s\n%!" s