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 Make (E:Engine) =
  59 struct
  60   type goal_switch = Open of E.goal | Closed of E.goal
  61   type 'a stack = 'a list
  62   type status =
  63     E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
  64
  65   type tactical =
  66     | Tactic of E.tactic
  67     | Skip
  68
  69   type t =
  70     | Dot
  71     | Semicolon
  72     | Branch
  73     | Shift of int option
  74     | Merge
  75     | Select of E.goal list
  76     | End_select
  77     | Tactical of tactical
  78     | Qed
  79
  80   let goal_of = function _, Open g -> g | _, Closed g -> g
  81   let is_open = function _, Open _ -> true | _, Closed _ -> false
  82   let open_all = List.map (fun p, g -> p, Open g)
  83
  84   let union a b = a @ b
  85
  86   let complementary part full = (* not really efficient *)
  87     List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
  88       full []
  89
  90   let close to_close =
  91     List.map
  92       (function
  93       | p, Open g when List.mem g to_close -> p, Closed g
  94       | g -> g)
  95
  96   let map_stack f g h = List.map (fun (a,b,c) -> f a, g b, h c)
  97
  98   let dummy_pos = ~-1
  99   let add_dummy_pos g = dummy_pos, g
 100   let map_dummy_pos = List.map add_dummy_pos
 101
 102   let map_open_pos =
 103     let rec aux pos =
 104       function
 105       | [] -> []
 106       | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
 107     in
 108     aux 1
 109
 110   let eval_tactical tactical proof switch =
 111     match tactical, switch with
 112     | Tactic tac, Open n -> E.apply_tactic tac proof n
 113     | Skip, Closed n -> proof, [], [n]
 114     | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal"
 115     | Skip, Open _ -> fail "can't skip an open goal"
 116
 117   let eval continuational status =
 118     match continuational, status with
 119     | _, (_, []) -> assert false
 120     | Tactical t, (proof, (env, todo, left)::tail) ->
 121         assert (List.length env > 1);
 122         let proof, opened, closed =
 123           List.fold_left
 124             (fun (proof, opened, closed) cur_goal ->
 125               if List.exists ((=) (goal_of cur_goal)) closed then
 126                 proof, opened, closed
 127               else
 128                 let proof, newopened, newclosed =
 129                   eval_tactical t proof (snd cur_goal)
 130                 in
 131                 proof,
 132                 union (complementary newclosed opened) newopened,
 133                 union closed newclosed
 134             ) (proof, [],[]) env
 135         in
 136         let pos = ref 0 in
 137         let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
 138         proof,
 139         (open_all stack_opened,
 140          complementary closed todo,
 141          complementary opened left)
 142         :: map_stack
 143             (close closed) (complementary closed) (complementary opened) tail
 144     | Semicolon, (proof, stack) -> proof, stack
 145     | Dot, (proof, (env, todo, left)::tail) ->
 146         let env, left =
 147           match List.filter is_open env, left with
 148           | [], [] -> fail "There is nothig to do for '.'"
 149           | g::env,left -> [g], union (List.map goal_of env) left
 150           | [], g::left -> [dummy_pos, Open g], left
 151         in
 152         proof, (env, todo, left)::tail
 153     | Branch, (proof, (g1::tl, todo, left)::tail) ->
 154         assert (List.length tl >= 1);
 155         proof, ([g1], [], [])::(tl, todo, left)::tail
 156     | Branch, (_, _) -> fail "can't branch on a singleton context"
 157     | Shift opt_pos, (proof, (leftopen, t, l)::(goals, todo, left)::tail) ->
 158         let next_goal, rem_goals =
 159           match opt_pos, goals with
 160           | None, g1 :: tl -> g1, tl
 161           | Some pos, _ ->
 162               (try
 163                 list_assoc_extract pos goals
 164               with Not_found -> fail (sprintf "position %d not found" pos))
 165           | None, [] -> fail "no more goals to shift"
 166         in
 167         let t =
 168           union t (union (List.map goal_of (List.filter is_open leftopen)) l)
 169         in
 170         proof, ([next_goal], t, [])::(rem_goals, todo,left)::tail
 171     | Shift _, (_, _) -> fail "no more goals to shift"
 172     | Merge, (proof, (leftopen,t,l)::(not_processed,todo,left)::tail) ->
 173         let env =
 174           (union (open_all (map_dummy_pos t))
 175             (union (open_all (map_dummy_pos l))
 176               (union not_processed (List.filter is_open leftopen))))
 177         in
 178         proof, (env,todo,left)::tail
 179     | Merge, (_, [_]) -> fail "can't merge here"
 180     | Select gl, (proof, stack) ->
 181         List.iter
 182           (fun g ->
 183             if not (E.is_goal_closed g proof) then
 184               fail "you can't select a closed goal")
 185           gl;
 186         (proof, (open_all (map_dummy_pos gl),[],[])::stack)
 187     | End_select, (proof, stack) ->
 188         (match stack with
 189         | ([], [], [])::tail -> proof, tail
 190         | _ -> fail "select left some goals open")
 191     | Qed, (proof, [[], [], []]) -> status
 192     | Qed, _ -> fail "can't qed an unfinished proof"
 193
 194   let init proof =
 195     proof,
 196     [ map_open_pos (E.goals_of_proof proof),  [], [] ]
 197 end
 198