matita/components/ng_tactics/continuationals.mli

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 exception Error of string Lazy.t
  27
  28 type goal = int
  29
  30 (** {2 Goal stack} *)
  31
  32 (* Key value pairs *)
  33 type parameters = (string * string) list
  34
  35 module Stack:
  36 sig
  37   type switch = Open of goal | Closed of goal
  38   type locator = int * switch
  39   type tag = [ `BranchTag | `FocusTag | `NoTag ]
  40   type entry = locator list * locator list * locator list * tag * parameters
  41   type t = entry list
  42
  43   val empty: t
  44
  45   val find_goal: t -> goal            (** find "next" goal *)
  46   val is_empty: t -> bool             (** a singleton empty level *)
  47   val of_nmetasenv: (goal * 'a) list -> t
  48   val head_switches: t -> switch list (** top level switches *)
  49   val head_goals: t -> goal list      (** top level goals *)
  50   val head_tag: t -> tag              (** top level tag *)
  51   val shift_goals: t -> goal list     (** second level goals *)
  52   val open_goals: t -> goal list      (** all (Open) goals *)
  53   val goal_of_switch: switch -> goal
  54   val filter_open : (goal * switch) list -> (goal * switch) list
  55   val is_open: goal * switch -> bool
  56   val is_fresh: goal * switch -> bool
  57   val init_pos: (goal * switch) list -> (goal * switch) list
  58   val goal_of_loc: goal * switch -> goal
  59   val switch_of_loc: goal * switch -> switch
  60   val zero_pos : goal list -> (goal * switch) list
  61   val deep_close: goal list -> t -> t
  62
  63
  64   val ( @+ ) : 'a list -> 'a list -> 'a list
  65   val ( @- ) : 'a list -> 'a list -> 'a list
  66   val ( @~- ) : ('a * switch) list -> goal list -> ('a * switch) list
  67
  68
  69
  70   (** @param int depth, depth 0 is the top of the stack *)
  71   val fold:
  72     env: ('a -> int -> tag -> locator -> 'a) ->
  73     cont:('a -> int -> tag -> locator -> 'a) ->
  74     todo:('a -> int -> tag -> locator -> 'a) ->
  75       'a  -> t -> 'a
  76
  77   val iter: (** @param depth as above *)
  78     env: (int -> tag -> locator -> unit) ->
  79     cont:(int -> tag -> locator -> unit) ->
  80     todo:(int -> tag -> locator -> unit) ->
  81       t -> unit
  82
  83   val map:  (** @param depth as above *)
  84     env: (int -> tag -> locator list -> locator list) ->
  85     cont:(int -> tag -> locator list -> locator list) ->
  86     todo:(int -> tag -> locator list -> locator list) ->
  87       t -> t
  88
  89   val pp: t -> string
  90 end
  91
  92 (** {2 Functorial interface} *)
  93
  94 module type Status =
  95 sig
  96   type input_status
  97   type output_status
  98
  99   type tactic
 100   val mk_tactic : (input_status -> output_status) -> tactic
 101   val apply_tactic : tactic -> input_status -> output_status
 102
 103   val goals : output_status -> goal list * goal list (** opened, closed goals *)
 104   val get_stack : input_status -> Stack.t
 105   val set_stack : Stack.t -> output_status -> output_status
 106
 107   val inject : input_status -> output_status
 108   val focus : goal -> output_status -> input_status
 109 end
 110
 111 module type C =
 112 sig
 113   type input_status
 114   type output_status
 115   type tactic
 116
 117   type tactical =
 118     | Tactic of tactic
 119     | Skip
 120
 121   type t =
 122     | Dot
 123     | Semicolon
 124
 125     | Branch
 126     | Shift
 127     | Pos of int list
 128     | Wildcard
 129     | Merge
 130
 131     | Focus of goal list
 132     | Unfocus
 133
 134     | Tactical of tactical
 135
 136   val eval: t -> input_status -> output_status
 137 end
 138
 139 module Make (S: Status) : C
 140   with type tactic = S.tactic
 141    and type input_status = S.input_status
 142    and type output_status = S.output_status
 143