nCicElim.cmi:
nTactics.cmi: nTacStatus.cmi
zipTree.cmi:
+andOrTree.cmi:
nAuto.cmi: nTacStatus.cmi
nInversion.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.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
nCicElim.cmi:
nTactics.cmi: nTacStatus.cmi
zipTree.cmi:
+andOrTree.cmi:
nAuto.cmi: nTacStatus.cmi
nInversion.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.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
nCicElim.mli \
nTactics.mli \
zipTree.mli \
+ andOrTree.mli \
nAuto.mli \
nInversion.mli
--- /dev/null
+(*
+ ||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)
--- /dev/null
+(*
+ ||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
+
+
(* $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 =
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 -> "<f"^string_of_int 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 -> "<f"^string_of_int 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
(* $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
projects / helm.git / commitdiff