X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FzipTree.ml;h=30f09940ed7acc4229377de190e2b1d7a8eb2323;hb=8dbc4dcef7328f3ac84f847255e9be8d47c1de6d;hp=77a724f405bc7ee447d5ca8ad42e55452e897a68;hpb=a57b60bb92d8587ced8ef5e9e47cdc4daafa40fc;p=helm.git

diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml
index 77a724f40..30f09940e 100644
--- a/helm/software/components/ng_tactics/zipTree.ml
+++ b/helm/software/components/ng_tactics/zipTree.ml
@@ -11,75 +11,58 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-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 ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil
 
-type t = T.t
-
-type tree = Node of (T.t * tree) list
-
-type tree_ctx = 
-  | Ctx of tree_ctx *  (T.t * tree) list * T.t *  (T.t * tree) list 
+type ('s,'g) tree_ctx = 
+  | Ctx of ('s,'g) tree_ctx * 's * 
+             ('g * ('s,'g) tree) list * 'g *  ('g * ('s,'g) tree) list 
   | Top
 
-type position = Loc of tree_ctx * tree
+type ('a,'s,'g) position = Loc of ('s,'g) tree_ctx * ('s,'g) tree
 
-let start (t : tree) : position = Loc (Top, t);;
+let start (t : ('s,'g) tree) : ('a,'s,'g) position = Loc (Top, t);;
 
 let down = function 
-  | Loc (_,Node []) -> None
-  | Loc (ctx, Node ((x,t)::tl)) -> Some (Loc (Ctx (ctx,[],x,tl),t))
+  | Loc (_,(Nil|Node (_,[]))) -> None
+  | Loc (ctx, Node (s,(x,t)::tl)) -> Some (Loc (Ctx (ctx,s,[],x,tl),t))
+;;
+
+let downr = function 
+  | Loc (_,(Nil|Node (_,[]))) -> None
+  | Loc (ctx, Node (s,(_::_ as l))) -> 
+     match List.rev l with
+     | [] -> assert false
+     | (x,t) :: tl ->     
+         Some (Loc (Ctx (ctx,s,tl,x,[]),t))
 ;;
 
 let up = function
   | Loc (Top,_) -> None
-  | Loc (Ctx(ctx,l,x,r),t) -> Some (Loc (ctx,Node (l@[x,t]@r)))
+  | Loc (Ctx(ctx,s,l,x,r),t) -> Some (Loc (ctx,Node (s,(List.rev l)@[x,t]@r)))
 ;;
 
 let right = function
-  | Loc (Top,_) | Loc (Ctx(_,_,_,[]),_) -> None
-  | Loc (Ctx(ctx,l,x,(rx,rt)::tl),t) -> Some (Loc(Ctx(ctx,l@[x,t],rx,tl),rt))
+  | Loc (Top,_) | Loc (Ctx(_,_,_,_,[]),_) -> None
+  | Loc (Ctx(ctx,s,l,x,(rx,rt)::tl),t)-> Some (Loc(Ctx(ctx,s,(x,t)::l,rx,tl),rt))
 ;;
 
 let left = function
-  | Loc (Top,_) | Loc (Ctx(_,[],_,_),_) -> None
-  | Loc (Ctx(ctx,(lx,lt)::tl,x,r),t) -> Some (Loc(Ctx(ctx,tl,lx,(x,t)::r),lt))
+  | Loc (Top,_) | Loc (Ctx(_,_,[],_,_),_) -> None
+  | Loc (Ctx(ctx,s,(lx,lt)::tl,x,r),t)->Some (Loc(Ctx(ctx,s,tl,lx,(x,t)::r),lt))
 ;;
 
 let get = function
   | Loc(Top,_) -> assert false
-  | Loc(Ctx(_,_,x,_),_) -> x
+  | Loc(Ctx(_,s,_,x,_),_) -> s,x
 ;;
 
-let set x = function
+let is_top = function Loc(Top,_) -> true | _ -> false;;
+
+let set s x = function
   | Loc(Top,_) -> assert false
-  | Loc(Ctx(c,l,_,r),t) -> Loc(Ctx(c,l,x,r),t)
+  | Loc(Ctx(c,_,l,_,r),t) -> Loc(Ctx(c,s,l,x,r),t)
 ;;
 
 let root t =
@@ -92,16 +75,58 @@ 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) -> 
-       let acc = aux acc t in
-       let acc = f acc x in
-       aux acc (Node tl)
+let dump ppg pps pos fmt =
+  let module Pp = GraphvizPp.Dot in
+  let c = ref 0 in
+  let skip = Node (Obj.magic (),[]) in
+  let rec aux_t = function 
+    | Nil -> 
+        Pp.node ("node"^string_of_int !c) ~attrs:["shape","point"] fmt
+    | Node (s,l) ->
+        let j = !c in
+        Pp.node ("node"^string_of_int j) ~attrs:["shape","record"; 
+          "label",String.concat "|"
+            (HExtlib.list_mapi 
+              (fun (x,_) i -> "<f"^string_of_int i^"> " ^ ppg x)
+            l)] fmt;
+        pps s ("node"^string_of_int j) fmt;
+        ignore(HExtlib.list_mapi 
+          (fun (_,t) i -> if t != skip then begin 
+             incr c;
+             let k = !c in
+             Pp.edge 
+               ("node"^string_of_int j^":f"^string_of_int i)
+               ("node"^string_of_int k) fmt;
+               aux_t t end)
+          l)
+  in
+  let rec aux pos = 
+    match pos with
+    | Top -> ()
+    | Ctx(ctx,s,l,x,r) ->
+        let t = Node(s,(List.rev l)@[x,skip]@r) in
+        let cur = !c in
+        aux_t t;
+        incr c;
+        if ctx <> Top then
+          Pp.edge 
+            ("node"^string_of_int !c)
+            ("node"^string_of_int cur^":f"^string_of_int( List.length l))
+            fmt; 
+        aux ctx
   in
-   aux acc (eject p)
+  let Loc (ctx, t) = pos in
+  let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->List.rev l in
+  let cur = !c in
+  Pp.node ("node"^string_of_int !c) 
+    ~attrs:["style","filled";"fillcolor","red";"color","red"] fmt;
+  Pp.edge  ("node"^string_of_int !c)  ("node"^string_of_int !c) fmt;
+  aux_t t;
+  incr c;
+  Pp.edge 
+    ("node"^string_of_int !c^":f"^string_of_int (List.length l))
+    ("node"^string_of_int cur)
+    fmt; 
+  aux ctx
 ;;
 
-
-end