helm/software/helena/src/text/txtTxt.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 C = Cps
  13 module T = Txt
  14
  15 (* Interface functions ******************************************************)
  16
  17 let rec contract f = function
  18    | T.Inst (t, vs)           ->
  19       let tt = T.Appl (List.rev vs, t) in
  20       contract f tt
  21    | T.Impl (n, false, id, w, t) ->
  22       let tt = T.Bind (n, T.Abst [id, false, w], t) in
  23       contract f tt
  24    | T.Impl (n, true, id, w, t)  ->
  25       let f = function
  26          | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
  27             f (T.Bind (n, T.Abst (xw :: xws), tt))
  28          | tt                                            -> f tt
  29       in
  30       let tt = T.Impl (n, false, id, w, t) in
  31       contract f tt
  32    | T.Sort _
  33    | T.NSrt _
  34    | T.LRef _
  35    | T.NRef _ as t            -> f t
  36    | T.Cast (u, t)            ->
  37       let f tt uu = f (T.Cast (uu, tt)) in
  38       let f tt = contract (f tt) u in
  39       contract f t
  40     | T.Appl (vs, t)          ->
  41       let f tt vvs = f (T.Appl (vvs, tt)) in
  42       let f tt = C.list_map (f tt) contract vs in
  43       contract f t
  44    | T.Bind (n, b, t)            ->
  45       let f tt bb = f (T.Bind (n, bb, tt)) in
  46       let f tt = contract_binder (f tt) b in
  47       contract f t
  48
  49 and contract_binder f = function
  50    | T.Void n as b -> f b
  51    | T.Abbr xvs    ->
  52       let map f (id, v) =
  53          let f vv = f (id, vv) in contract f v
  54       in
  55       let f xvvs = f (T.Abbr xvvs) in
  56       C.list_map f map xvs
  57    | T.Abst xws    ->
  58       let map f (id, real, w) =
  59          let f ww = f (id, real, ww) in contract f w
  60       in
  61       let f xwws = f (T.Abst xwws) in
  62       C.list_map f map xws