This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / gTopLevel / logicalOperations.ml

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
deleted file mode 100644 (file)
index 93c511f..0000000
--- a/helm/gTopLevel/logicalOperations.ml
+++ /dev/null
@@ -1,117 +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/.
- *)
-
-let get_parent id ids_to_terms ids_to_father_ids =
- match Hashtbl.find ids_to_father_ids id with
-    None -> None
-  | Some id -> Some (id, Hashtbl.find ids_to_terms id)
-;;
-
-let get_context ids_to_terms ids_to_father_ids =
- let module C = Cic in
-  let rec aux id =
-   match get_parent id ids_to_terms ids_to_father_ids with
-      None -> []
-    | Some (parentid,parent) ->
-       let term = Hashtbl.find ids_to_terms id in
-       let binding =
-        match parent with
-           C.Rel _
-         | C.Var _
-         | C.Meta _
-         | C.Sort _
-         | C.Implicit _
-         | C.Cast _ -> []
-         | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
-         | C.Prod _ -> []
-         | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
-         | C.Lambda _ -> []
-         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def (s,None))]
-         | C.LetIn _ -> []
-         | C.Appl _
-         | C.Const _ -> []
-         | C.MutInd _
-         | C.MutConstruct _
-         | C.MutCase _ -> []
-(*CSC: sbagliato: manca il when *)
-         | C.Fix (_,ifl) ->
-            let counter = ref 0 in
-             List.rev_map
-              (function (name,_,ty,bo) ->
-                let res =
-                 Some (C.Name name, (C.Def ((C.Fix (!counter,ifl)), Some ty)))
-                in
-                 incr counter ;
-                 res
-              ) ifl
-         | C.CoFix (_,ifl) ->
-            let counter = ref 0 in
-             List.rev_map
-              (function (name,ty,bo) ->
-                let res =
-                 Some (C.Name name,(C.Def ((C.CoFix (!counter,ifl)), Some ty)))
-                in
-                 incr counter ;
-                 res
-              ) ifl
-       in
-        binding@(aux parentid)
-  in
-   aux
-;;
-
-exception NotImplemented;;
-
-(* A subterm is changed into a fresh meta *)
-let to_sequent id ids_to_terms ids_to_father_ids =
- let module P = ProofEngine in
-  let term = Hashtbl.find ids_to_terms id in
-  let context = get_context ids_to_terms ids_to_father_ids id in
-   let metasenv =
-    match P.get_proof () with
-       None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
-   in
-    let ty = CicTypeChecker.type_of_aux' metasenv context term in
-     P.perforate context term ty (* P.perforate also sets the goal *)
-;;
-
-exception FocusOnlyOnMeta;;
-
-(* If the current selection is a Meta, that Meta becomes the current goal *)
-let focus id ids_to_terms ids_to_father_ids =
- let module P = ProofEngine in
-  let term = Hashtbl.find ids_to_terms id in
-  let context = get_context ids_to_terms ids_to_father_ids id in
-   let metasenv =
-    match P.get_proof () with
-       None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
-   in
-    let ty = CicTypeChecker.type_of_aux' metasenv context term in
-     match term with
-        Cic.Meta (n,_) -> P.goal := Some n
-      | _ -> raise FocusOnlyOnMeta
-;;