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