matita/components/ng_tactics/continuationals.ml

   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 (* $Id$ *)
  27
  28 open Printf
  29
  30 let debug = false
  31 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  32
  33 exception Error of string lazy_t
  34 let fail msg = raise (Error msg)
  35
  36 type goal = int
  37
  38 type parameters = (string * string) list
  39
  40 module Stack =
  41 struct
  42   type switch = Open of goal | Closed of goal
  43   type locator = int * switch
  44   type tag = [ `BranchTag | `FocusTag | `NoTag ]
  45   type entry = locator list * locator list * locator list * tag * parameters
  46   type t = entry list
  47
  48   let empty = [ [], [], [], `NoTag , []]
  49
  50   let fold ~env ~cont ~todo init stack =
  51     let rec aux acc depth =
  52       function
  53       | [] -> acc
  54       | (locs, todos, conts, tag, p) :: tl ->
  55           let acc = List.fold_left (fun acc -> env acc depth tag)  acc locs in
  56           let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
  57           let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
  58           aux acc (depth + 1) tl
  59     in
  60     assert (stack <> []);
  61     aux init 0 stack
  62
  63   let iter ~env ~cont ~todo =
  64     fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) ()
  65
  66   let map ~env ~cont ~todo =
  67     let depth = ref ~-1 in
  68     List.map
  69       (fun (s, t, c, tag, p) ->
  70         incr depth;
  71         let d = !depth in
  72         env d tag s, todo d tag t, cont d tag c, tag, p)
  73
  74   let is_open = function _, Open _ -> true | _ -> false
  75   let close = function n, Open g -> n, Closed g | l -> l
  76   let filter_open = List.filter is_open
  77   let is_fresh =
  78     function n, Open _ when n > 0 -> true | _,Closed _ -> true | _ -> false
  79   let goal_of_loc = function _, Open g | _, Closed g -> g
  80   let goal_of_switch = function Open g | Closed g -> g
  81   let switch_of_loc = snd
  82
  83   let zero_pos = List.map (fun g -> 0, Open g)
  84
  85   let init_pos locs =
  86     let pos = ref 0 in  (* positions are 1-based *)
  87     List.map (function _, sw -> incr pos; !pos, sw) locs
  88
  89   let extract_pos i =
  90     let rec aux acc =
  91       function
  92       | [] -> fail (lazy (sprintf "relative position %d not found" i))
  93       | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl
  94       | hd :: tl -> aux (hd :: acc) tl
  95     in
  96     aux []
  97
  98   let deep_close gs =
  99     let close _ _ =
 100       List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l)
 101     in
 102     let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in
 103     map ~env:close ~cont:rm ~todo:rm
 104
 105   let rec find_goal =
 106     function
 107     | [] -> raise (Failure "Continuationals.find_goal")
 108     | (l :: _,   _   ,   _   , _, _) :: _ -> goal_of_loc l
 109     | (  _   ,   _   , l :: _, _, _) :: _ -> goal_of_loc l
 110     | (  _   , l :: _,   _   , _, _) :: _ -> goal_of_loc l
 111     | _ :: tl -> find_goal tl
 112
 113   let is_empty =
 114     function
 115     | [] -> assert false
 116     | [ [], [], [], `NoTag , _] -> true
 117     | _ -> false
 118
 119   let of_nmetasenv metasenv =
 120     let goals = List.map (fun (g, _) -> g) metasenv in
 121     [ zero_pos goals, [], [], `NoTag , []]
 122
 123   let head_switches =
 124     function
 125     | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs
 126     | [] -> assert false
 127
 128   let head_goals =
 129     function
 130     | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
 131     | [] -> assert false
 132
 133   let head_tag =
 134     function
 135     | (_, _, _, tag, _) :: _ -> tag
 136     | [] -> assert false
 137
 138   let shift_goals =
 139     function
 140     | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
 141     | [] -> assert false
 142     | _ -> []
 143
 144   let open_goals stack =
 145     let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in
 146     List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack)
 147
 148   let (@+) = (@)  (* union *)
 149
 150   let (@-) s1 s2 =  (* difference *)
 151     List.fold_right
 152       (fun e acc -> if List.mem e s2 then acc else e :: acc)
 153       s1 []
 154
 155   let (@~-) locs gs = (* remove some goals from a locators list *)
 156     List.fold_right
 157       (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc)
 158       locs []
 159
 160   let pp stack =
 161     let pp_goal = string_of_int in
 162     let pp_switch =
 163       function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g
 164     in
 165     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
 166     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
 167     let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
 168     let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in
 169     let pp_stack_entry (env, todo, cont, tag, parameters) =
 170       sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
 171         (pp_tag tag) (pp_par parameters)
 172     in
 173     String.concat " :: " (List.map pp_stack_entry stack)
 174 end
 175
 176 module type Status =
 177 sig
 178   type input_status
 179   type output_status
 180
 181   type tactic
 182   val mk_tactic : (input_status -> output_status) -> tactic
 183   val apply_tactic : tactic -> input_status -> output_status
 184
 185   val goals : output_status -> goal list * goal list (** opened, closed goals *)
 186   val get_stack : input_status -> Stack.t
 187   val set_stack : Stack.t -> output_status -> output_status
 188
 189   val inject : input_status -> output_status
 190   val focus : goal -> output_status -> input_status
 191 end
 192
 193 module type C =
 194 sig
 195   type input_status
 196   type output_status
 197   type tactic
 198
 199   type tactical =
 200     | Tactic of tactic
 201     | Skip
 202
 203   type t =
 204     | Dot
 205     | Semicolon
 206
 207     | Branch
 208     | Shift
 209     | Pos of int list
 210     | Wildcard
 211     | Merge
 212
 213     | Focus of goal list
 214     | Unfocus
 215
 216     | Tactical of tactical
 217
 218   val eval: t -> input_status -> output_status
 219 end
 220
 221 module Make (S: Status) =
 222 struct
 223   open Stack
 224
 225   type input_status = S.input_status
 226   type output_status = S.output_status
 227   type tactic = S.tactic
 228
 229   type tactical =
 230     | Tactic of tactic
 231     | Skip
 232
 233   type t =
 234     | Dot
 235     | Semicolon
 236     | Branch
 237     | Shift
 238     | Pos of int list
 239     | Wildcard
 240     | Merge
 241     | Focus of goal list
 242     | Unfocus
 243     | Tactical of tactical
 244
 245   let pp_t =
 246     function
 247     | Dot -> "Dot"
 248     | Semicolon -> "Semicolon"
 249     | Branch -> "Branch"
 250     | Shift -> "Shift"
 251     | Pos i -> "Pos " ^ (String.concat "," (List.map string_of_int i))
 252     | Wildcard -> "Wildcard"
 253     | Merge -> "Merge"
 254     | Focus gs ->
 255         sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
 256     | Unfocus -> "Unfocus"
 257     | Tactical _ -> "Tactical <abs>"
 258
 259   let eval_tactical tactical ostatus switch =
 260     match tactical, switch with
 261     | Tactic tac, Open n ->
 262         let ostatus = S.apply_tactic tac (S.focus n ostatus) in
 263         let opened, closed = S.goals ostatus in
 264         ostatus, opened, closed
 265     | Skip, Closed n -> ostatus, [], [n]
 266     | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal")
 267     | Skip, Open _ -> fail (lazy "can't skip an open goal")
 268
 269   let eval cmd istatus =
 270     let stack = S.get_stack istatus in
 271     debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack)));
 272     let new_stack stack = S.inject istatus, stack in
 273     let ostatus, stack =
 274       match cmd, stack with
 275       | _, [] -> assert false
 276       | Tactical tac, (g, t, k, tag, p) :: s ->
 277 (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A
 278  *   auto paramodulation.try assumption.
 279  * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.
 280
 281   if g = [] then fail (lazy "can't apply a tactic to zero goals");
 282
 283 *)
 284           debug_print (lazy ("context length " ^string_of_int (List.length g)));
 285           let rec aux s go gc =
 286             function
 287             | [] -> s, go, gc
 288             | loc :: loc_tl ->
 289                 debug_print (lazy "inner eval tactical");
 290                 let s, go, gc =
 291                   if List.exists ((=) (goal_of_loc loc)) gc then
 292                     s, go, gc
 293                   else
 294                     let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in
 295                     s, (go @- gc') @+ go', gc @+ gc'
 296                 in
 297                 aux s go gc loc_tl
 298           in
 299           let s0, go0, gc0 = S.inject istatus, [], [] in
 300           let sn, gon, gcn = aux s0 go0 gc0 g in
 301           debug_print (lazy ("opened: "
 302             ^ String.concat " " (List.map string_of_int gon)));
 303           debug_print (lazy ("closed: "
 304             ^ String.concat " " (List.map string_of_int gcn)));
 305           let stack =
 306             (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s
 307           in
 308           sn, stack
 309       | Dot, ([], _, [], _, _) :: _ ->
 310           (* backward compatibility: do-nothing-dot *)
 311           new_stack stack
 312       | Dot, (g, t, k, tag, p) :: s ->
 313           (match filter_open g, k with
 314           | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s)
 315           | [], loc :: k ->
 316               assert (is_open loc);
 317               new_stack (([ loc ], t, k, tag, p) :: s)
 318           | _ -> fail (lazy "can't use \".\" here"))
 319       | Semicolon, _ -> new_stack stack
 320       | Branch, (g, t, k, tag, p) :: s ->
 321           (match init_pos g with
 322           | [] | [ _ ] -> fail (lazy "too few goals to branch");
 323           | loc :: loc_tl ->
 324               new_stack
 325                 (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s))
 326       | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->
 327           (match g' with
 328           | [] -> fail (lazy "no more goals to shift")
 329           | loc :: loc_tl ->
 330               new_stack
 331                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
 332                 :: (loc_tl, t', k', tag, p') :: s))
 333       | Shift, _ -> fail (lazy "can't shift goals here")
 334       | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
 335         when is_fresh loc ->
 336           let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
 337           new_stack
 338             ((l_js, t , [],`BranchTag, p)
 339              :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
 340       | Pos _, _ -> fail (lazy "can't use relative positioning here")
 341       | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s
 342           when is_fresh loc ->
 343             new_stack
 344               (([loc] @+ g', t, [], `BranchTag, p)
 345                 :: ([], t', k', tag, p') :: s)
 346       | Wildcard, _ -> fail (lazy "can't use wildcard here")
 347       | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s ->
 348           new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s)
 349       | Merge, _ -> fail (lazy "can't merge goals here")
 350       | Focus [], _ -> assert false
 351       | Focus gs, s ->
 352           let stack_locs =
 353             let add_l acc _ _ l = if is_open l then l :: acc else acc in
 354             Stack.fold ~env:add_l ~cont:add_l ~todo:add_l [] s
 355           in
 356           List.iter
 357             (fun g ->
 358               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
 359                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
 360             gs;
 361           new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s)
 362       | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s
 363       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
 364     in
 365     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
 366     S.set_stack stack ostatus
 367 end
 368