(* $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 =
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 -> "<f"^string_of_int 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 -> "<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 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
projects / helm.git / blobdiff