From: Stefano Zacchiroli Date: Thu, 6 Oct 2005 11:19:35 +0000 (+0000) Subject: first check in of continuationals implementation X-Git-Tag: V_0_7_2_3~239 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68bff6f299e9022d6a54c007dea90dc829998c9b;p=helm.git first check in of continuationals implementation --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 1ef89807d..7c915b4c5 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -116,3 +116,5 @@ tactics.cmx: variousTactics.cmx tacticals.cmx ring.cmx reductionTactics.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi +continuationals.cmo: continuationals.cmi +continuationals.cmx: continuationals.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 0f902c47e..1b27678fb 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -14,7 +14,8 @@ INTERFACE_FILES = \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ - fourierR.mli fwdSimplTactic.mli history.mli statefulProofEngine.mli tactics.mli + fourierR.mli fwdSimplTactic.mli history.mli statefulProofEngine.mli \ + tactics.mli continuationals.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml new file mode 100644 index 000000000..f5a747720 --- /dev/null +++ b/helm/ocaml/tactics/continuationals.ml @@ -0,0 +1,178 @@ +(* 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 + diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli new file mode 100644 index 000000000..4b2632e56 --- /dev/null +++ b/helm/ocaml/tactics/continuationals.mli @@ -0,0 +1,66 @@ +(* 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 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 + +module Make (E:Engine) : +sig + 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 + + val eval: t -> status -> status +end + diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index be235a2c1..72639efb9 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -21,7 +21,9 @@ \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}} \newcommand{\SKIP}{\ensuremath{\mathtt{skip}}} \newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}} -\newcommand{\SELECT}[2]{\ensuremath{\mathtt{select} ~ #1 ~ #2}} +\newcommand{\OLDTACTICAL}[1]{\ensuremath{\mathtt{old\_tactical}~\mathit{#1}}} +\newcommand{\SELECT}[1]{\ensuremath{\mathtt{select} ~ #1}} +\newcommand{\ENDSELECT}[1]{\ensuremath{\mathtt{end}}} \newcommand{\GOAL}{\ensuremath{\mathit{goal}}} \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}} @@ -54,18 +56,28 @@ \[ \begin{array}{rcll} - C & ::= & & \mbox{(\textbf{continuationals})} \\ - & & C ~ \DOT & \mbox{(dot)} \\ - & | & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\ - & | & \BRANCH & \mbox{(branch)} \\ - & | & \SHIFT & \mbox{(shift)} \\ - & | & \MERGE & \mbox{(merge)} \\ - & | & \SELECT{n_1,\dots,n_k}{C} & \mbox{(select)} \\ - & | & \TACTICAL{T} & \mbox{(tactical)} \\[2ex] + S & ::= & & \mbox{(\textbf{toplevel grammar})}\\ + & & \varepsilon & \\ + & | & T~ P~ S & \\[2ex] - T & ::= & & \mbox{(\textbf{tacticals})} \\ + T & ::= & & \mbox{(\textbf{tactical})} \\ & & \APPLY{tac} & \mbox{(tactic application)} \\ & | & \SKIP & \mbox{(closed goal skipping)} \\ + & | & \OLDTACTICAL{tcl} & \mbox{(non step-by-step tactical)} \\ + & | & \SELECT{n_1,\dots,n_k}{S} & \mbox{(select)} \\[2ex] + + P & ::= & & \mbox{(\textbf{punctuation})} \\ + & & \DOT & \mbox{(dot)} \\ + & | & \SEMICOLON & \mbox{(semicolon)} \\ + & | & \BRANCH & \mbox{(branch)} \\ + & | & \SHIFT & \mbox{(shift)} \\ + & | & \MERGE ~ M & \mbox{(merge)} \\[2ex] + + M & ::= & & \mbox{(\textbf{merge-punctuation})} \\ + & & \varepsilon & \\ + & | & \MERGE ~ M& \mbox{(multi-merge)} \\ + & | & \DOT & \mbox{(merge and choose)} \\[2ex] + \end{array} \]