From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 23 Oct 2009 11:44:13 +0000 (+0000)
Subject: more functions
X-Git-Tag: make_still_working~3258
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a57b60bb92d8587ced8ef5e9e47cdc4daafa40fc;p=helm.git

more functions
---

diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml
index 66cd99496..77a724f40 100644
--- a/helm/software/components/ng_tactics/zipTree.ml
+++ b/helm/software/components/ng_tactics/zipTree.ml
@@ -13,8 +13,35 @@
 
 module type Elem = sig type t val pp : t -> string end ;;
 
+module type ZipTree = sig
+  type t
+  type tree = Node of (t * tree) list
+  type position
+
+  val start : tree -> position
+
+  val up    : position -> position option
+  val down  : position -> position option
+  val left  : position -> position option
+  val right : position -> position option
+
+  val root: position -> tree
+  val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
+
+  val get: position -> t
+  val set: t -> position -> position
+
+  val inject: tree -> position -> position
+  val eject: position -> tree
+
+end
+
+let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
+
 module Make(T : Elem) = struct
 
+type t = T.t
+
 type tree = Node of (T.t * tree) list
 
 type tree_ctx = 
@@ -23,7 +50,6 @@ type tree_ctx =
 
 type position = Loc of tree_ctx * tree
 
-
 let start (t : tree) : position = Loc (Top, t);;
 
 let down = function 
@@ -46,7 +72,15 @@ let left = function
   | Loc (Ctx(ctx,(lx,lt)::tl,x,r),t) -> Some (Loc(Ctx(ctx,tl,lx,(x,t)::r),lt))
 ;;
 
-let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
+let get = function
+  | Loc(Top,_) -> assert false
+  | Loc(Ctx(_,_,x,_),_) -> x
+;;
+
+let set x = function
+  | Loc(Top,_) -> assert false
+  | Loc(Ctx(c,l,_,r),t) -> Loc(Ctx(c,l,x,r),t)
+;;
 
 let root t =
   match repeat up t with
@@ -54,7 +88,11 @@ let root t =
   | _ -> assert false
 ;;
 
-let previsit f acc (t : position) =
+let eject (Loc (_,t)) = t ;;
+
+let inject t (Loc (c,_)) = Loc(c,t) ;;
+
+let previsit f acc (p : position) =
   let rec aux acc = function
     | Node [] -> acc
     | Node ((x,t)::tl) -> 
@@ -62,10 +100,8 @@ let previsit f acc (t : position) =
        let acc = f acc x in
        aux acc (Node tl)
   in
-   aux acc (root t)
+   aux acc (eject p)
 ;;
 
 
-
-
 end
diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli
index 04e9a7b7c..a74206cc3 100644
--- a/helm/software/components/ng_tactics/zipTree.mli
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -11,4 +11,32 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val repeat : ('a -> 'a option) -> 'a -> 'a
+
+module type Elem = sig type t val pp : t -> string end ;;
+
+module type ZipTree = sig
+  type t
+  type tree = Node of (t * tree) list
+  type position
+
+  val start : tree -> position
+
+  val up    : position -> position option
+  val down  : position -> position option
+  val left  : position -> position option
+  val right : position -> position option
+
+  val root: position -> tree
+  val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
+
+  val get: position -> t
+  val set: t -> position -> position
+
+  val inject: tree -> position -> position
+  val eject: position -> tree
+
+end
+
+module Make(T : Elem) : ZipTree with type t = T.t