nTacStatus.mli \
nCicElim.mli \
nTactics.mli \
- zipTree.mli \
- andOrTree.mli \
nnAuto.mli \
nDestructTac.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 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)
+++ /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 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
-
-
+++ /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 $ *)
-
-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 -> "<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,(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
-;;
-
+++ /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 ('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
-
-
projects / helm.git / commitdiff