]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_tactics/andOrTree.ml
the edges must be quoted as well (not only the nodes)
[helm.git] / 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)