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 type ZipTree = sig
  17   type t
  18   type tree = Node of (t * tree) list
  19   type position
  20
  21   val start : tree -> position
  22
  23   val up    : position -> position option
  24   val down  : position -> position option
  25   val left  : position -> position option
  26   val right : position -> position option
  27
  28   val root: position -> tree
  29   val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
  30
  31   val get: position -> t
  32   val set: t -> position -> position
  33
  34   val inject: tree -> position -> position
  35   val eject: position -> tree
  36
  37 end
  38
  39 let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
  40
  41 module Make(T : Elem) = struct
  42
  43 type t = T.t
  44
  45 type tree = Node of (T.t * tree) list
  46
  47 type tree_ctx =
  48   | Ctx of tree_ctx *  (T.t * tree) list * T.t *  (T.t * tree) list
  49   | Top
  50
  51 type position = Loc of tree_ctx * tree
  52
  53 let start (t : tree) : position = Loc (Top, t);;
  54
  55 let down = function
  56   | Loc (_,Node []) -> None
  57   | Loc (ctx, Node ((x,t)::tl)) -> Some (Loc (Ctx (ctx,[],x,tl),t))
  58 ;;
  59
  60 let up = function
  61   | Loc (Top,_) -> None
  62   | Loc (Ctx(ctx,l,x,r),t) -> Some (Loc (ctx,Node (l@[x,t]@r)))
  63 ;;
  64
  65 let right = function
  66   | Loc (Top,_) | Loc (Ctx(_,_,_,[]),_) -> None
  67   | Loc (Ctx(ctx,l,x,(rx,rt)::tl),t) -> Some (Loc(Ctx(ctx,l@[x,t],rx,tl),rt))
  68 ;;
  69
  70 let left = function
  71   | Loc (Top,_) | Loc (Ctx(_,[],_,_),_) -> None
  72   | Loc (Ctx(ctx,(lx,lt)::tl,x,r),t) -> Some (Loc(Ctx(ctx,tl,lx,(x,t)::r),lt))
  73 ;;
  74
  75 let get = function
  76   | Loc(Top,_) -> assert false
  77   | Loc(Ctx(_,_,x,_),_) -> x
  78 ;;
  79
  80 let set x = function
  81   | Loc(Top,_) -> assert false
  82   | Loc(Ctx(c,l,_,r),t) -> Loc(Ctx(c,l,x,r),t)
  83 ;;
  84
  85 let root t =
  86   match repeat up t with
  87   | Loc(Top,t) -> t
  88   | _ -> assert false
  89 ;;
  90
  91 let eject (Loc (_,t)) = t ;;
  92
  93 let inject t (Loc (c,_)) = Loc(c,t) ;;
  94
  95 let previsit f acc (p : position) =
  96   let rec aux acc = function
  97     | Node [] -> acc
  98     | Node ((x,t)::tl) ->
  99        let acc = aux acc t in
 100        let acc = f acc x in
 101        aux acc (Node tl)
 102   in
 103    aux acc (eject p)
 104 ;;
 105
 106
 107 end