X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FzipTree.ml;h=30f09940ed7acc4229377de190e2b1d7a8eb2323;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=2259ae5283abab16d51803e6a7ffc2208d1bff1a;hpb=204600c93b7e4d0bbd8c414835c6d57917b1f1a0;p=helm.git diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml index 2259ae528..30f09940e 100644 --- a/helm/software/components/ng_tactics/zipTree.ml +++ b/helm/software/components/ng_tactics/zipTree.ml @@ -11,77 +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 - - val dump: position -> Format.formatter -> unit - -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 ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil -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 = @@ -94,40 +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) - in - aux acc (eject p) -;; - -let dump pos fmt = +let dump ppg pps pos fmt = let module Pp = GraphvizPp.Dot in - let tree = root pos in - let where = eject pos in let c = ref 0 in - let rec aux (Node l as orig) = - let j = !c in - Pp.node ("node"^string_of_int j) ~attrs:(["shape","record"; - "label",String.concat "|" - (HExtlib.list_mapi - (fun (x,_) i -> "" ^ T.pp x) - l)] @ if orig == where then ["style","rounded"] else []) fmt; - ignore(HExtlib.list_mapi - (fun (_,t) i -> - 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) - l) + 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 -> " " ^ 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 tree + 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