From 3c77b701737ef41c39a5d08d76ca9071e5b1bdd7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2009 12:20:50 +0000 Subject: [PATCH 1/1] new data structures for auto --- helm/software/components/ng_tactics/.depend | 7 +- .../components/ng_tactics/.depend.opt | 7 +- helm/software/components/ng_tactics/Makefile | 1 + .../components/ng_tactics/andOrTree.ml | 90 +++++++++++ .../components/ng_tactics/andOrTree.mli | 56 +++++++ .../software/components/ng_tactics/zipTree.ml | 145 ++++++++---------- .../components/ng_tactics/zipTree.mli | 37 ++--- 7 files changed, 239 insertions(+), 104 deletions(-) create mode 100644 helm/software/components/ng_tactics/andOrTree.ml create mode 100644 helm/software/components/ng_tactics/andOrTree.mli diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index c2166601e..2e709a0af 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -3,6 +3,7 @@ nTacStatus.cmi: nCicElim.cmi: nTactics.cmi: nTacStatus.cmi zipTree.cmi: +andOrTree.cmi: nAuto.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi @@ -15,7 +16,9 @@ nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi zipTree.cmo: zipTree.cmi zipTree.cmx: zipTree.cmi -nAuto.cmo: nTactics.cmi nTacStatus.cmi nAuto.cmi -nAuto.cmx: nTactics.cmx nTacStatus.cmx nAuto.cmi +andOrTree.cmo: zipTree.cmi andOrTree.cmi +andOrTree.cmx: zipTree.cmx andOrTree.cmi +nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi +nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index c2166601e..2e709a0af 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -3,6 +3,7 @@ nTacStatus.cmi: nCicElim.cmi: nTactics.cmi: nTacStatus.cmi zipTree.cmi: +andOrTree.cmi: nAuto.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nCicTacReduction.cmo: nCicTacReduction.cmi @@ -15,7 +16,9 @@ nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi zipTree.cmo: zipTree.cmi zipTree.cmx: zipTree.cmi -nAuto.cmo: nTactics.cmi nTacStatus.cmi nAuto.cmi -nAuto.cmx: nTactics.cmx nTacStatus.cmx nAuto.cmi +andOrTree.cmo: zipTree.cmi andOrTree.cmi +andOrTree.cmx: zipTree.cmx andOrTree.cmi +nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi +nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index 3bc9fafcc..f05c75e94 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -6,6 +6,7 @@ INTERFACE_FILES = \ nCicElim.mli \ nTactics.mli \ zipTree.mli \ + andOrTree.mli \ nAuto.mli \ nInversion.mli diff --git a/helm/software/components/ng_tactics/andOrTree.ml b/helm/software/components/ng_tactics/andOrTree.ml new file mode 100644 index 000000000..22d36844f --- /dev/null +++ b/helm/software/components/ng_tactics/andOrTree.ml @@ -0,0 +1,90 @@ +(* + ||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 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/helm/software/components/ng_tactics/andOrTree.mli b/helm/software/components/ng_tactics/andOrTree.mli new file mode 100644 index 000000000..9570c62d9 --- /dev/null +++ b/helm/software/components/ng_tactics/andOrTree.mli @@ -0,0 +1,56 @@ +(* + ||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 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/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml index 2259ae528..45c7f02b9 100644 --- a/helm/software/components/ng_tactics/zipTree.ml +++ b/helm/software/components/ng_tactics/zipTree.ml @@ -11,77 +11,49 @@ (* $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 ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil -type t = T.t - -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 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 = @@ -94,40 +66,57 @@ let eject (Loc (_,t)) = 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 -> "" ^ 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 -> " " ^ 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,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,_,_)->l in + let cur = !c in + Pp.node ("node"^string_of_int !c) + ~attrs:["style","filled";"fillcolor","red";"color","red"] 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 diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli index 6a6c4d67f..bed576157 100644 --- a/helm/software/components/ng_tactics/zipTree.mli +++ b/helm/software/components/ng_tactics/zipTree.mli @@ -11,34 +11,27 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val repeat : ('a -> 'a option) -> 'a -> 'a +type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil +type ('a,'s,'g) position -module type Elem = sig type t val pp : t -> string end ;; +val start : ('s,'g) tree -> ('a,'s,'g) position -module type ZipTree = sig - type t - type tree = Node of (t * tree) list - type position +val up : ('a,'s,'g) position -> ('b,'s,'g) position option +val down : ('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 start : tree -> position +val is_top : ('a,'s,'g) position -> bool - val up : position -> position option - val down : position -> position option - val left : position -> position option - val right : position -> position option +val root: ('a,'s,'g) position -> ('s,'g) tree - val root: position -> tree - val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a +val get: ('a,'s,'g) position -> 's * 'g +val set: 's -> 'g -> ('a,'s,'g) position -> ('a,'s,'g) position - val get: position -> t - val set: t -> position -> position +val inject: ('s,'g) tree -> ('a,'s,'g) position -> ('a,'s,'g) position +val eject: ('a,'s,'g) position -> ('s,'g) tree - val inject: tree -> position -> position - val eject: position -> tree +val dump: ('g -> string) -> ('s -> string -> Format.formatter -> unit) -> + ('a,'s,'g) position -> Format.formatter -> unit - val dump: position -> Format.formatter -> unit - -end - -module Make(T : Elem) : ZipTree with type t = T.t -- 2.39.2