helm/software/components/ng_tactics/zipTree.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
  15
  16 type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil
  17
  18 type ('s,'g) tree_ctx =
  19   | Ctx of ('s,'g) tree_ctx * 's *
  20              ('g * ('s,'g) tree) list * 'g *  ('g * ('s,'g) tree) list
  21   | Top
  22
  23 type ('a,'s,'g) position = Loc of ('s,'g) tree_ctx * ('s,'g) tree
  24
  25 let start (t : ('s,'g) tree) : ('a,'s,'g) position = Loc (Top, t);;
  26
  27 let down = function
  28   | Loc (_,(Nil|Node (_,[]))) -> None
  29   | Loc (ctx, Node (s,(x,t)::tl)) -> Some (Loc (Ctx (ctx,s,[],x,tl),t))
  30 ;;
  31
  32 let downr = function
  33   | Loc (_,(Nil|Node (_,[]))) -> None
  34   | Loc (ctx, Node (s,(_::_ as l))) ->
  35      match List.rev l with
  36      | [] -> assert false
  37      | (x,t) :: tl ->
  38          Some (Loc (Ctx (ctx,s,tl,x,[]),t))
  39 ;;
  40
  41 let up = function
  42   | Loc (Top,_) -> None
  43   | Loc (Ctx(ctx,s,l,x,r),t) -> Some (Loc (ctx,Node (s,(List.rev l)@[x,t]@r)))
  44 ;;
  45
  46 let right = function
  47   | Loc (Top,_) | Loc (Ctx(_,_,_,_,[]),_) -> None
  48   | Loc (Ctx(ctx,s,l,x,(rx,rt)::tl),t)-> Some (Loc(Ctx(ctx,s,(x,t)::l,rx,tl),rt))
  49 ;;
  50
  51 let left = function
  52   | Loc (Top,_) | Loc (Ctx(_,_,[],_,_),_) -> None
  53   | Loc (Ctx(ctx,s,(lx,lt)::tl,x,r),t)->Some (Loc(Ctx(ctx,s,tl,lx,(x,t)::r),lt))
  54 ;;
  55
  56 let get = function
  57   | Loc(Top,_) -> assert false
  58   | Loc(Ctx(_,s,_,x,_),_) -> s,x
  59 ;;
  60
  61 let is_top = function Loc(Top,_) -> true | _ -> false;;
  62
  63 let set s x = function
  64   | Loc(Top,_) -> assert false
  65   | Loc(Ctx(c,_,l,_,r),t) -> Loc(Ctx(c,s,l,x,r),t)
  66 ;;
  67
  68 let root t =
  69   match repeat up t with
  70   | Loc(Top,t) -> t
  71   | _ -> assert false
  72 ;;
  73
  74 let eject (Loc (_,t)) = t ;;
  75
  76 let inject t (Loc (c,_)) = Loc(c,t) ;;
  77
  78 let dump ppg pps pos fmt =
  79   let module Pp = GraphvizPp.Dot in
  80   let c = ref 0 in
  81   let skip = Node (Obj.magic (),[]) in
  82   let rec aux_t = function
  83     | Nil ->
  84         Pp.node ("node"^string_of_int !c) ~attrs:["shape","point"] fmt
  85     | Node (s,l) ->
  86         let j = !c in
  87         Pp.node ("node"^string_of_int j) ~attrs:["shape","record";
  88           "label",String.concat "|"
  89             (HExtlib.list_mapi
  90               (fun (x,_) i -> "<f"^string_of_int i^"> " ^ ppg x)
  91             l)] fmt;
  92         pps s ("node"^string_of_int j) fmt;
  93         ignore(HExtlib.list_mapi
  94           (fun (_,t) i -> if t != skip then begin
  95              incr c;
  96              let k = !c in
  97              Pp.edge
  98                ("node"^string_of_int j^":f"^string_of_int i)
  99                ("node"^string_of_int k) fmt;
 100                aux_t t end)
 101           l)
 102   in
 103   let rec aux pos =
 104     match pos with
 105     | Top -> ()
 106     | Ctx(ctx,s,l,x,r) ->
 107         let t = Node(s,(List.rev l)@[x,skip]@r) in
 108         let cur = !c in
 109         aux_t t;
 110         incr c;
 111         if ctx <> Top then
 112           Pp.edge
 113             ("node"^string_of_int !c)
 114             ("node"^string_of_int cur^":f"^string_of_int( List.length l))
 115             fmt;
 116         aux ctx
 117   in
 118   let Loc (ctx, t) = pos in
 119   let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->List.rev l in
 120   let cur = !c in
 121   Pp.node ("node"^string_of_int !c)
 122     ~attrs:["style","filled";"fillcolor","red";"color","red"] fmt;
 123   Pp.edge  ("node"^string_of_int !c)  ("node"^string_of_int !c) fmt;
 124   aux_t t;
 125   incr c;
 126   Pp.edge
 127     ("node"^string_of_int !c^":f"^string_of_int (List.length l))
 128     ("node"^string_of_int cur)
 129     fmt;
 130   aux ctx
 131 ;;
 132