X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Ftacticals.ml;fp=helm%2FgTopLevel%2Ftacticals.ml;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=f3cd13b44c8f9544d766d027ef837242a977fbc9;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml deleted file mode 100644 index f3cd13b44..000000000 --- a/helm/gTopLevel/tacticals.ml +++ /dev/null @@ -1,89 +0,0 @@ -(* Copyright (C) 2002, 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://cs.unibo.it/helm/. - *) - -open CicReduction -open PrimitiveTactics -open ProofEngineTypes -open UriManager - -(** DEBUGGING *) - - (** perform debugging output? *) -let debug = false - - (** debugging print *) -let warn s = - if debug then - prerr_endline ("TACTICALS WARNING: " ^ s) - -(** AUX TACTIC{,AL}S *) - - (** - naive implementation of ORELSE tactical, try a sequence of tactics in turn: - if one fails pass to the next one and so on, eventually raises (failure "no - tactics left") - TODO warning: not tail recursive due to "try .. with" boxing - *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Ring.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Ring.try_tactics IS TRYING " ^ descr); - (try - let res = tac ~status in - warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); - res - with - e -> - match e with - (Fail _) - | (CicTypeChecker.NotWellTyped _) - | (CicUnification.UnificationFailed) -> - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - | _ -> raise e (* [e] must not be caught ; let's re-raise it *) - ) - | [] -> raise (Fail "try_tactics: no tactics left") - -let thens ~start ~continuations ~status = - let (proof,new_goals) = start ~status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - -let then_ ~start ~continuation ~status = - let (proof,new_goals) = start ~status in - List.fold_left - (fun (proof,goals) goal -> - let (proof',new_goals') = continuation ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals