From 315f37e0c47d4af8c1767b4f836d74c7125ab736 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 15:31:55 +0000 Subject: [PATCH] first bits for the zipper --- helm/software/components/ng_tactics/.depend | 6 ++ .../components/ng_tactics/.depend.opt | 9 ++- helm/software/components/ng_tactics/Makefile | 1 + .../software/components/ng_tactics/zipTree.ml | 71 +++++++++++++++++++ .../components/ng_tactics/zipTree.mli | 14 ++++ 5 files changed, 98 insertions(+), 3 deletions(-) create mode 100644 helm/software/components/ng_tactics/zipTree.ml create mode 100644 helm/software/components/ng_tactics/zipTree.mli diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 8d46f1671..c2166601e 100644 --- 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 615a158e9..c2166601e 100644 --- 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 1db1ad6e7..3bc9fafcc 100644 --- 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 index 000000000..66cd99496 --- /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 index 000000000..04e9a7b7c --- /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 $ *) + + -- 2.39.2