first bits for the zipper

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 8d46f1671ec75706c805db0550e9191d1b2507bf..c2166601e246be716a256462c24633e9af39efc7 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,4 +1,8 @@
+nCicTacReduction.cmi: 
+nTacStatus.cmi: 
+nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
+zipTree.cmi: 
 nAuto.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
@@ -9,6 +13,8 @@ nCicElim.cmo: nCicElim.cmi
 nCicElim.cmx: nCicElim.cmi 
 nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
 nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
+zipTree.cmo: zipTree.cmi 
+zipTree.cmx: zipTree.cmi 
 nAuto.cmo: nTactics.cmi nTacStatus.cmi nAuto.cmi 
 nAuto.cmx: nTactics.cmx nTacStatus.cmx nAuto.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 

diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 615a158e92abe4180fbde0a74ad4bdfc2b0f6efe..c2166601e246be716a256462c24633e9af39efc7 100644 (file)
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,8 +1,9 @@
 nCicTacReduction.cmi: 
 nTacStatus.cmi: 
 nCicElim.cmi: 
-nAuto.cmi: nTacStatus.cmi 
 nTactics.cmi: nTacStatus.cmi 
+zipTree.cmi: 
+nAuto.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
 nCicTacReduction.cmx: nCicTacReduction.cmi 
@@ -10,9 +11,11 @@ nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nCicElim.cmo: nCicElim.cmi 
 nCicElim.cmx: nCicElim.cmi 
-nAuto.cmo: nTacStatus.cmi nAuto.cmi 
-nAuto.cmx: nTacStatus.cmx nAuto.cmi 
 nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
 nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
+zipTree.cmo: zipTree.cmi 
+zipTree.cmx: zipTree.cmi 
+nAuto.cmo: nTactics.cmi nTacStatus.cmi nAuto.cmi 
+nAuto.cmx: nTactics.cmx nTacStatus.cmx nAuto.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 

diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile
index 1db1ad6e76f975b9f4bc5340f86a39d4a77e1f05..3bc9fafcc17c654f3fc603edb5664ad2844b5b45 100644 (file)
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -5,6 +5,7 @@ INTERFACE_FILES = \
        nTacStatus.mli \
        nCicElim.mli \
        nTactics.mli \
+       zipTree.mli \
        nAuto.mli \
        nInversion.mli
 

diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml
new file mode 100644 (file)
index 0000000..66cd994
--- /dev/null
+++ b/helm/software/components/ng_tactics/zipTree.ml
@@ -0,0 +1,71 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+module type Elem = sig type t val pp : t -> string end ;;
+
+module Make(T : Elem) = struct
+
+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 
+  | Top
+
+type position = Loc of tree_ctx * tree
+
+
+let start (t : tree) : position = Loc (Top, t);;
+
+let down = function 
+  | Loc (_,Node []) -> None
+  | Loc (ctx, Node ((x,t)::tl)) -> Some (Loc (Ctx (ctx,[],x,tl),t))
+;;
+
+let up = function
+  | Loc (Top,_) -> None
+  | Loc (Ctx(ctx,l,x,r),t) -> Some (Loc (ctx,Node (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))
+;;
+
+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))
+;;
+
+let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
+
+let root t =
+  match repeat up t with
+  | Loc(Top,t) -> t
+  | _ -> assert false
+;;
+
+let previsit f acc (t : 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)
+  in
+   aux acc (root t)
+;;
+
+
+
+
+end

diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli
new file mode 100644 (file)
index 0000000..04e9a7b
--- /dev/null
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -0,0 +1,14 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+