helm/software/components/ng_tactics/andOrTree.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
  15 type andT
  16 type orT
  17
  18 type ('s,'g) tree = ([ `And of 's | `Or ], 'g) ZipTree.tree
  19 type ('a,'s,'g) position = ('a,[ `And of 's | `Or ], 'g) ZipTree.position
  20
  21 type ('s,'g) subtreeA =
  22   Solution of 's | Todo of (andT,'s,'g) position
  23
  24 type ('s,'g) subtreeO =
  25   Unexplored | Alternatives of (orT,'s,'g) position
  26
  27 open ZipTree
  28
  29 (* fails if Nil *)
  30
  31 let start t =
  32   match down (start t) with
  33   | None -> assert false
  34   | Some pos -> pos
  35
  36 let setO x = set `Or x
  37 let setA x y = set (`And x) y
  38
  39 let getO x = match get x with `And _,_ -> assert false | `Or, x -> x
  40 let getA x = match get x with `And x,y -> x,y | `Or, _ -> assert false
  41
  42 let root = root
  43
  44 let upA p =
  45   match up p with
  46   | None -> None
  47   | Some p -> if is_top p then None else Some p
  48
  49 let upO p = match up p with None -> assert false | Some x -> x
  50
  51 let downA p =
  52  match down p with
  53  | Some x -> Alternatives x
  54  | None -> assert(eject p = Nil); Unexplored
  55
  56 let downO p =
  57  match down p with
  58  | Some x -> Todo x
  59  | None ->
  60     match eject p with
  61     | Node(`And s,[]) -> Solution s
  62     | _ -> assert false
  63
  64 let downOr p =
  65  match downr p with
  66  | Some x -> Todo x
  67  | None ->
  68     match eject p with
  69     | Node(`And s,[]) -> Solution s
  70     | _ -> assert false
  71
  72 let left = left
  73 let right = right
  74
  75 let is_top = is_top
  76 let is_nil p =
  77   match eject p with
  78   | Nil -> true
  79   | _ -> false
  80 let is_solved_leaf p =
  81   match eject p with
  82   | Node(`And _,[]) -> true
  83   | _ -> false
  84 let get_leaf_solution p =
  85   match eject p with
  86   | Node(`And x,[]) -> x
  87   | _ -> assert false
  88
  89
  90 let inject = inject
  91 let eject = eject
  92
  93 let dump f =
  94   dump f (function
  95           | `And _ -> fun _ _ -> ()
  96           | `Or -> fun node fmt ->
  97                           GraphvizPp.Dot.node node ~attrs:["style","rounded"]
  98                           fmt)