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