--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception Error of string
+
+module L = List
+
+module type Engine =
+sig
+ type goal
+ type conjecture
+ type metasenv = conjecture list
+ type tactic
+
+ val goal_of_conjecture: conjecture -> goal
+ val is_goal_in_metasenv: metasenv -> goal -> bool
+
+ val apply_tactic:
+ tactic -> metasenv -> goal ->
+ metasenv * goal list * goal list
+end
+
+(** like List.assoc returning a pair: binding matching the given key,
+ * associative list without the returned binding
+ * @raise Not_found *)
+let list_assoc_extract key =
+ let rec aux acc =
+ function
+ | [] -> raise Not_found
+ | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl)
+ | hd :: tl -> aux (hd :: acc) tl
+ in
+ aux []
+
+module Make (E:Engine) =
+struct
+ type goal_switch = Open of E.goal | Closed of E.goal
+ type 'a stack = 'a list
+ type status =
+ E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+
+ type tactical =
+ | Tactic of E.tactic
+ | Skip
+
+ type t =
+ | Dot
+ | Semicolon
+ | Branch
+ | Shift of int option
+ | Merge
+ | Select of E.goal list
+ | End_select
+ | Tactical of tactical
+
+ let goal_of = function _, Open g -> g | _, Closed g -> g
+ let is_open = function _, Open _ -> true | _, Closed _ -> false
+ let open_all = L.map (fun p, g -> p, Open g)
+
+ let union a b = a @ b
+
+ let complementary part full = (* not really efficient *)
+ L.fold_left (fun acc g -> if L.mem g part then acc else g::acc) full []
+
+ let close to_close l =
+ L.map (function p, Open g when L.mem g to_close -> p, Closed g | g -> g) l
+
+ let stack_map f g h stack =
+ L.map (fun (a,b,c) -> f a, g b, h c) stack
+
+ let dummy_pos = ~-1
+ let add_dummy_pos g = dummy_pos, g
+ let map_dummy_pos = List.map add_dummy_pos
+
+ let eval_tactical tactical metasenv switch =
+ match tactical, switch with
+ | Tactic tac, Open n -> E.apply_tactic tac metasenv n
+ | Skip, Closed n -> metasenv, [], [n]
+ | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal")
+ | Skip, Open _ -> raise (Error "can't skip an open goal")
+
+ let eval continuational (status: status) =
+ match continuational, status with
+ | Tactical t, (metasenv, (env, todo, left)::tail) ->
+ assert (L.length env > 1);
+ let metasenv, opened, closed =
+ L.fold_left
+ (fun (metasenv, opened, closed) cur_goal ->
+ if L.exists ((=) (goal_of cur_goal)) closed then
+ metasenv, opened, closed
+ else
+ let metasenv, newopened, newclosed =
+ eval_tactical t metasenv (snd cur_goal)
+ in
+ metasenv,
+ union (complementary newclosed opened) newopened,
+ union closed newclosed
+ ) (metasenv, [],[]) env
+ in
+ let pos = ref 0 in
+ let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
+ metasenv,
+ (open_all stack_opened,
+ complementary closed todo,
+ complementary opened left)
+ :: stack_map
+ (close closed) (complementary closed) (complementary opened) tail
+ | Tactical _, (_, []) -> assert false
+ | Semicolon, (metasenv, stack) -> metasenv, stack
+ | Dot, (metasenv, (env, todo, left)::tail) ->
+ let env, left =
+ match L.filter is_open env, left with
+ | [], [] -> raise (Error "There is nothig to do for '.'")
+ | g::env,left -> [g], union (L.map goal_of env) left
+ | [], g::left -> [dummy_pos, Open g], left
+ in
+ metasenv, (env, todo, left)::tail
+ | Dot, (_, []) -> assert false
+ | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
+ assert (L.length tl >= 1);
+ metasenv, ([g1], [], [])::(tl, todo, left)::tail
+ | Branch, (_, _) -> raise (Error "can't branch on a singleton context")
+ | Shift opt_pos, (metasenv, (leftopen, t, l)::(goals, todo, left)::tail) ->
+ let next_goal, rem_goals =
+ match opt_pos, goals with
+ | None, g1 :: tl -> g1, tl
+ | Some pos, _ ->
+ (try
+ list_assoc_extract pos goals
+ with Not_found ->
+ raise (Error (Printf.sprintf "position %d not found" pos)))
+ | None, [] -> raise (Error "no more goals to shift")
+ in
+ let t = union t (union (L.map goal_of (L.filter is_open leftopen)) l) in
+ metasenv, ([next_goal], t, [])::(rem_goals, todo,left)::tail
+ | Shift _, (_, _) -> raise (Error "no more goals to shift")
+ | Merge, (metasenv, (leftopen,t,l)::(not_processed,todo,left)::tail) ->
+ let env =
+ (union (open_all (map_dummy_pos t))
+ (union (open_all (map_dummy_pos l))
+ (union not_processed (L.filter is_open leftopen ))))
+ in
+ metasenv, (env,todo,left)::tail
+ | Merge, (_, [])
+ | Merge, (_, [_]) -> raise (Error "can't merge here")
+ | Select gl, (metasenv, stack) ->
+ List.iter
+ (fun g -> if not (E.is_goal_in_metasenv metasenv g) then
+ raise (Error "you can't select a closed goal")) gl;
+ (metasenv, (open_all (map_dummy_pos gl),[],[])::stack)
+ | End_select, (metasenv, stack) ->
+ (match stack with
+ | ([], [], [])::tail -> metasenv, tail
+ | _ -> raise (Error "select left some goals open"))
+end
+
projects / helm.git / blobdiff