helm/software/components/ng_tactics/zipTree.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 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 module type Elem = sig type t val pp : t -> string end ;;
  15
  16 module Make(T : Elem) = struct
  17
  18 type tree = Node of (T.t * tree) list
  19
  20 type tree_ctx =
  21   | Ctx of tree_ctx *  (T.t * tree) list * T.t *  (T.t * tree) list
  22   | Top
  23
  24 type position = Loc of tree_ctx * tree
  25
  26
  27 let start (t : tree) : position = Loc (Top, t);;
  28
  29 let down = function
  30   | Loc (_,Node []) -> None
  31   | Loc (ctx, Node ((x,t)::tl)) -> Some (Loc (Ctx (ctx,[],x,tl),t))
  32 ;;
  33
  34 let up = function
  35   | Loc (Top,_) -> None
  36   | Loc (Ctx(ctx,l,x,r),t) -> Some (Loc (ctx,Node (l@[x,t]@r)))
  37 ;;
  38
  39 let right = function
  40   | Loc (Top,_) | Loc (Ctx(_,_,_,[]),_) -> None
  41   | Loc (Ctx(ctx,l,x,(rx,rt)::tl),t) -> Some (Loc(Ctx(ctx,l@[x,t],rx,tl),rt))
  42 ;;
  43
  44 let left = function
  45   | Loc (Top,_) | Loc (Ctx(_,[],_,_),_) -> None
  46   | Loc (Ctx(ctx,(lx,lt)::tl,x,r),t) -> Some (Loc(Ctx(ctx,tl,lx,(x,t)::r),lt))
  47 ;;
  48
  49 let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
  50
  51 let root t =
  52   match repeat up t with
  53   | Loc(Top,t) -> t
  54   | _ -> assert false
  55 ;;
  56
  57 let previsit f acc (t : position) =
  58   let rec aux acc = function
  59     | Node [] -> acc
  60     | Node ((x,t)::tl) ->
  61        let acc = aux acc t in
  62        let acc = f acc x in
  63        aux acc (Node tl)
  64   in
  65    aux acc (root t)
  66 ;;
  67
  68
  69
  70
  71 end