From: Andrea Asperti Date: Wed, 6 Oct 2010 14:12:55 +0000 (+0000) Subject: removed zipTree and andOrTree. X-Git-Tag: make_still_working~2802 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a788e3d51daff7846b555fbe8e4a0e912a56b6f7;p=helm.git removed zipTree and andOrTree. --- diff --git a/matita/components/ng_tactics/Makefile b/matita/components/ng_tactics/Makefile index 2e35685e7..a1b5e0205 100644 --- a/matita/components/ng_tactics/Makefile +++ b/matita/components/ng_tactics/Makefile @@ -5,8 +5,6 @@ INTERFACE_FILES = \ nTacStatus.mli \ nCicElim.mli \ nTactics.mli \ - zipTree.mli \ - andOrTree.mli \ nnAuto.mli \ nDestructTac.mli \ nInversion.mli diff --git a/matita/components/ng_tactics/andOrTree.ml b/matita/components/ng_tactics/andOrTree.ml deleted file mode 100644 index 57be10271..000000000 --- a/matita/components/ng_tactics/andOrTree.ml +++ /dev/null @@ -1,98 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - - -type andT -type orT - -type ('s,'g) tree = ([ `And of 's | `Or ], 'g) ZipTree.tree -type ('a,'s,'g) position = ('a,[ `And of 's | `Or ], 'g) ZipTree.position - -type ('s,'g) subtreeA = - Solution of 's | Todo of (andT,'s,'g) position - -type ('s,'g) subtreeO = - Unexplored | Alternatives of (orT,'s,'g) position - -open ZipTree - -(* fails if Nil *) - -let start t = - match down (start t) with - | None -> assert false - | Some pos -> pos - -let setO x = set `Or x -let setA x y = set (`And x) y - -let getO x = match get x with `And _,_ -> assert false | `Or, x -> x -let getA x = match get x with `And x,y -> x,y | `Or, _ -> assert false - -let root = root - -let upA p = - match up p with - | None -> None - | Some p -> if is_top p then None else Some p - -let upO p = match up p with None -> assert false | Some x -> x - -let downA p = - match down p with - | Some x -> Alternatives x - | None -> assert(eject p = Nil); Unexplored - -let downO p = - match down p with - | Some x -> Todo x - | None -> - match eject p with - | Node(`And s,[]) -> Solution s - | _ -> assert false - -let downOr p = - match downr p with - | Some x -> Todo x - | None -> - match eject p with - | Node(`And s,[]) -> Solution s - | _ -> assert false - -let left = left -let right = right - -let is_top = is_top -let is_nil p = - match eject p with - | Nil -> true - | _ -> false -let is_solved_leaf p = - match eject p with - | Node(`And _,[]) -> true - | _ -> false -let get_leaf_solution p = - match eject p with - | Node(`And x,[]) -> x - | _ -> assert false - - -let inject = inject -let eject = eject - -let dump f = - dump f (function - | `And _ -> fun _ _ -> () - | `Or -> fun node fmt -> - GraphvizPp.Dot.node node ~attrs:["style","rounded"] - fmt) diff --git a/matita/components/ng_tactics/andOrTree.mli b/matita/components/ng_tactics/andOrTree.mli deleted file mode 100644 index 2a8eea24d..000000000 --- a/matita/components/ng_tactics/andOrTree.mli +++ /dev/null @@ -1,57 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -type andT -type orT - -type ('s,'g) tree = ([ `And of 's | `Or ], 'g) ZipTree.tree -type ('a,'s,'g) position = ('a,[ `And of 's | `Or ], 'g) ZipTree.position - -type ('s,'g) subtreeA = - Solution of 's | Todo of (andT,'s,'g) position - -type ('s,'g) subtreeO = - Unexplored | Alternatives of (orT,'s,'g) position - -(* fails if Nil *) -val start : ('s,'g) tree -> (andT,'s,'g) position - -val upA : (andT,'s,'g) position -> (orT,'s,'g) position option -val upO : (orT,'s,'g) position -> (andT,'s,'g) position -val downA : (andT,'s,'g) position -> ('s,'g) subtreeO -val downO : (orT,'s,'g) position -> ('s,'g) subtreeA -val downOr : (orT,'s,'g) position -> ('s,'g) subtreeA - -val left : ('a,'s,'g) position -> ('a,'s,'g) position option -val right : ('a,'s,'g) position -> ('a,'s,'g) position option - -val is_top : (orT,'s,'g) position -> bool -val is_nil : (andT,'s,'g) position -> bool -val is_solved_leaf : (orT,'s,'g) position -> bool - -val get_leaf_solution : (orT,'s,'g) position -> 's - -val root: ('a,'s,'g) position -> ('s,'g) tree - -val getA: (andT,'s,'g) position -> 's * 'g -val getO: (orT,'s,'g) position -> 'g -val setA: 's -> 'g -> (andT,'s,'g) position -> (andT,'s,'g) position -val setO: 'g -> (orT,'s,'g) position -> (orT,'s,'g) position - -val inject: ('s,'g) tree -> ('a,'s,'g) position -> ('a,'s,'g) position -val eject: ('a,'s,'g) position -> ('s,'g) tree - -val dump: ('g -> string) -> - ('a,'s,'g) position -> Format.formatter -> unit - - diff --git a/matita/components/ng_tactics/zipTree.ml b/matita/components/ng_tactics/zipTree.ml deleted file mode 100644 index 30f09940e..000000000 --- a/matita/components/ng_tactics/zipTree.ml +++ /dev/null @@ -1,132 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -let rec repeat f l = match f l with None -> l | Some l -> repeat f l;; - -type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil - -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 ('a,'s,'g) position = Loc of ('s,'g) tree_ctx * ('s,'g) tree - -let start (t : ('s,'g) tree) : ('a,'s,'g) position = Loc (Top, t);; - -let down = function - | 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,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,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,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(_,s,_,x,_),_) -> s,x -;; - -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,s,l,x,r),t) -;; - -let root t = - match repeat up t with - | Loc(Top,t) -> t - | _ -> assert false -;; - -let eject (Loc (_,t)) = t ;; - -let inject t (Loc (c,_)) = Loc(c,t) ;; - -let dump ppg pps pos fmt = - let module Pp = GraphvizPp.Dot in - let c = ref 0 in - 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 - 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 -;; - diff --git a/matita/components/ng_tactics/zipTree.mli b/matita/components/ng_tactics/zipTree.mli deleted file mode 100644 index 751d3720d..000000000 --- a/matita/components/ng_tactics/zipTree.mli +++ /dev/null @@ -1,38 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil -type ('a,'s,'g) position - -val start : ('s,'g) tree -> ('a,'s,'g) position - -val up : ('a,'s,'g) position -> ('b,'s,'g) position option -val down : ('a,'s,'g) position -> ('b,'s,'g) position option -val downr : ('a,'s,'g) position -> ('b,'s,'g) position option -val left : ('a,'s,'g) position -> ('b,'s,'g) position option -val right : ('a,'s,'g) position -> ('b,'s,'g) position option - -val is_top : ('a,'s,'g) position -> bool - -val root: ('a,'s,'g) position -> ('s,'g) tree - -val get: ('a,'s,'g) position -> 's * 'g -val set: 's -> 'g -> ('a,'s,'g) position -> ('a,'s,'g) position - -val inject: ('s,'g) tree -> ('a,'s,'g) position -> ('a,'s,'g) position -val eject: ('a,'s,'g) position -> ('s,'g) tree - -val dump: ('g -> string) -> ('s -> string -> Format.formatter -> unit) -> - ('a,'s,'g) position -> Format.formatter -> unit - -