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