]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_tactics/zipTree.ml
auto snapshot
[helm.git] / helm / software / components / ng_tactics / zipTree.ml
index 45c7f02b94b595d4029be769afee73418fe0bf36..30f09940ed7acc4229377de190e2b1d7a8eb2323 100644 (file)
@@ -29,6 +29,15 @@ let down = function
   | 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,s,l,x,r),t) -> Some (Loc (ctx,Node (s,(List.rev l)@[x,t]@r)))
@@ -95,7 +104,7 @@ let dump ppg pps pos fmt =
     match pos with
     | Top -> ()
     | Ctx(ctx,s,l,x,r) ->
-        let t = Node(s,l@[x,skip]@r) in
+        let t = Node(s,(List.rev l)@[x,skip]@r) in
         let cur = !c in
         aux_t t;
         incr c;
@@ -107,10 +116,11 @@ let dump ppg pps pos fmt =
         aux ctx
   in
   let Loc (ctx, t) = pos in
-  let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->l 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