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 open Printf
  27
  28 exception Error of string Lazy.t
  29
  30 module type Engine =
  31 sig
  32   type goal
  33   type proof
  34   type tactic
  35
  36   val is_goal_closed: goal -> proof -> bool
  37   val goals_of_proof: proof -> goal list
  38
  39   val apply_tactic:
  40     tactic -> proof -> goal ->
  41       proof * goal list * goal list
  42 end
  43
  44 (** like List.assoc returning a pair: binding matching the given key,
  45  * associative list without the returned binding
  46  * @raise Not_found *)
  47 let list_assoc_extract key =
  48   let rec aux acc =
  49     function
  50     | [] -> raise Not_found
  51     | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl)
  52     | hd :: tl -> aux (hd :: acc) tl
  53   in
  54   aux []
  55
  56 module type C =
  57 sig
  58   type goal
  59   type proof
  60   type tactic
  61
  62   type status
  63
  64   type tactical =
  65     | Tactic of tactic
  66     | Skip
  67
  68   type t =
  69     | Dot
  70     | Semicolon
  71
  72     | Branch
  73     | Shift of int option
  74     | Select of goal list
  75     | End
  76
  77     | Tactical of tactical
  78
  79   val eval: t -> status -> status
  80   val init: proof -> status
  81
  82   val get_proof: status -> proof
  83   val set_proof: proof -> status -> status
  84
  85   type goal_switch = Open of goal | Closed of goal
  86   val get_goals: status -> goal_switch list
  87
  88   val is_completed: status -> bool
  89 end
  90
  91 module Make (E:Engine) =
  92 struct
  93   type goal = E.goal
  94   type proof = E.proof
  95   type tactic = E.tactic
  96
  97   type goal_switch = Open of goal | Closed of goal
  98   type 'a stack = 'a list
  99   type stack_tag = BranchTag | SelectTag | NoTag
 100   type stack_entry =
 101     (int * goal_switch) list * goal list * goal list * stack_tag
 102   type status = proof * stack_entry stack
 103
 104   let get_proof = fst
 105   let set_proof p (_, s) = p, s
 106   let get_goals (_, stack) =
 107     match stack with
 108     | (goals, _, _, _) :: _ -> List.map snd goals
 109     | [] -> assert false
 110
 111   type tactical =
 112     | Tactic of tactic
 113     | Skip
 114
 115   type t =
 116     | Dot
 117     | Semicolon
 118     | Branch
 119     | Shift of int option
 120     | Select of goal list
 121     | End
 122     | Tactical of tactical
 123
 124   let goal_of = function _, Open g -> g | _, Closed g -> g
 125   let is_open = function _, Open _ -> true | _, Closed _ -> false
 126   let open_all = List.map (fun p, g -> p, Open g)
 127
 128   let union a b = a @ b
 129
 130   let complementary part full = (* not really efficient *)
 131     List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
 132       full []
 133
 134   let close to_close =
 135     List.map
 136       (function
 137       | p, Open g when List.mem g to_close -> p, Closed g
 138       | g -> g)
 139
 140   let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag)
 141
 142   let dummy_pos = ~-1
 143   let add_dummy_pos g = dummy_pos, g
 144   let map_dummy_pos = List.map add_dummy_pos
 145
 146   let map_open_pos =
 147     let rec aux pos =
 148       function
 149       | [] -> []
 150       | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
 151     in
 152     aux 1
 153
 154   let eval_tactical tactical proof switch =
 155     match tactical, switch with
 156     | Tactic tac, Open n -> E.apply_tactic tac proof n
 157     | Skip, Closed n -> proof, [], [n]
 158     | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal"))
 159     | Skip, Open _ -> raise (Error (lazy "can't skip an open goal"))
 160
 161   let eval continuational status =
 162     match continuational, status with
 163     | _, (_, []) -> assert false
 164     | Tactical t, (proof, (env, todo, left,tag)::tail) ->
 165         assert (List.length env > 1);
 166         let proof, opened, closed =
 167           List.fold_left
 168             (fun (proof, opened, closed) cur_goal ->
 169               if List.exists ((=) (goal_of cur_goal)) closed then
 170                 proof, opened, closed
 171               else
 172                 let proof, newopened, newclosed =
 173                   eval_tactical t proof (snd cur_goal)
 174                 in
 175                 proof,
 176                 union (complementary newclosed opened) newopened,
 177                 union closed newclosed
 178             ) (proof, [],[]) env
 179         in
 180         let pos = ref 0 in
 181         let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
 182         proof,
 183         (open_all stack_opened,
 184          complementary closed todo,
 185          complementary opened left, tag)
 186         :: map_stack
 187             (close closed) (complementary closed) (complementary opened) tail
 188     | Semicolon, (proof, stack) -> proof, stack
 189     | Dot, (proof, (env, todo, left, tag)::tail) ->
 190         let env, left =
 191           match List.filter is_open env, left with
 192           | [], [] -> raise (Error (lazy "There is nothig to do for '.'"))
 193           | g::env,left -> [g], union (List.map goal_of env) left
 194           | [], g::left -> [dummy_pos, Open g], left
 195         in
 196         proof, (env, todo, left, tag)::tail
 197     | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
 198         assert (List.length tl >= 1);
 199         proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
 200     | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
 201     | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
 202                              (goals, todo, left,tag)::tail) ->
 203         let next_goal, rem_goals =
 204           match opt_pos, goals with
 205           | None, g1 :: tl -> g1, tl
 206           | Some pos, _ ->
 207               (try
 208                 list_assoc_extract pos goals
 209               with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos))))
 210           | None, [] -> raise (Error (lazy "no more goals to shift"))
 211         in
 212         let t =
 213           union t (union (List.map goal_of (List.filter is_open leftopen)) l)
 214         in
 215         proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
 216     | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift"))
 217     | Select gl, (proof, stack) ->
 218         List.iter
 219           (fun g ->
 220             if E.is_goal_closed g proof then
 221               raise (Error (lazy "you can't select a closed goal")))
 222           gl;
 223         (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
 224     | End, (proof, stack) ->
 225         (match stack with
 226         | ([], [], [], SelectTag)::tail -> proof, tail
 227         | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail ->
 228             let env =
 229               (union (open_all (map_dummy_pos t))
 230                 (union (open_all (map_dummy_pos l))
 231                   (union not_processed (List.filter is_open leftopen))))
 232             in
 233             proof, (env,todo,left,tag)::tail
 234         | _ -> raise (Error (lazy "can't end here")))
 235
 236   let init proof =
 237     proof,
 238     [ map_open_pos (E.goals_of_proof proof),  [], [], NoTag ]
 239
 240   let is_completed =
 241     function
 242     | (_, [[],[],[],NoTag]) -> true
 243     | _ -> false
 244 end
 245