X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;fp=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=0000000000000000000000000000000000000000;hp=16be77edb443c84c3c7845182564dacfb1601cce;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
deleted file mode 100644
index 16be77edb..000000000
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ /dev/null
@@ -1,148 +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/.
- *)
-
-(* mk_fresh_name context name typ                      *)
-(* returns an identifier which is fresh in the context *)
-(* and that resembles [name] as much as possible.      *)
-(* [typ] will be the type of the variable              *)
-let mk_fresh_name context name ~typ =
- let module C = Cic in
-  let basename =
-   match name with
-      C.Anonymous ->
-       (*CSC: great space for improvements here *)
-       (try
-         (match CicTypeChecker.type_of_aux' [] context typ with
-             C.Sort C.Prop -> "H"
-           | C.Sort C.Set -> "x"
-           | _ -> "H"
-         )
-        with CicTypeChecker.TypeCheckerFailure _ -> "H"
-       )
-    | C.Name name ->
-       Str.global_replace (Str.regexp "[0-9]*$") "" name
-  in
-   let already_used name =
-    List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
-   in
-    if not (already_used basename) then
-     C.Name basename
-    else
-     let rec try_next n =
-      let name' = basename ^ string_of_int n in
-       if already_used name' then
-        try_next (n+1)
-       else
-        C.Name name'
-     in
-      try_next 1
-;;
-
-(* identity_relocation_list_for_metavariable i canonical_context         *)
-(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
-(* where n = List.length [canonical_context]                             *)
-(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
- let canonical_context_length = List.length canonical_context in
-  let rec aux =
-   function
-      (_,[]) -> []
-    | (n,None::tl) -> None::(aux ((n+1),tl))
-    | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
-  in
-   aux (1,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta.                       *)
-let new_meta ~proof =
- let (_,metasenv,_,_) = proof in
-  let rec aux =
-   function
-      None,[] -> 1
-    | Some n,[] -> n
-    | None,(n,_,_)::tl -> aux (Some n,tl)
-    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
-  in
-   1 + aux (None,metasenv)
-
-let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty = proof in
-  let subst_in = CicUnification.apply_subst [meta,term] in
-   let metasenv' =
-    newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
-   in
-    let metasenv'' =
-     List.map
-      (function i,canonical_context,ty ->
-        let canonical_context' =
-         List.map
-          (function
-              Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
-            | None -> None
-          ) canonical_context
-        in
-         i,canonical_context',(subst_in ty)
-      ) metasenv'
-    in
-     let bo' = subst_in bo in
-      let newproof = uri,metasenv'',bo',ty in
-       (newproof, metasenv'')
-
-(*CSC: commento vecchio *)
-(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
-(* This (heavy) function must be called when a tactic can instantiate old *)
-(* metavariables (i.e. existential variables). It substitues the metasenv *)
-(* of the proof with the result of removing [meta] from the domain of     *)
-(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
-(* in the current proof. Finally it applies [apply_subst_replacing] to    *)
-(*  current proof.                                                        *)
-(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
-(*CSC: ci ripasso sopra apply_subst!!!                                     *)
-(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
-(*CSC: [newmetasenv].                                             *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty) = proof in
-  let bo' = subst_in bo in
-  let metasenv' =
-   List.fold_right
-    (fun metasenv_entry i ->
-      match metasenv_entry with
-         (m,canonical_context,ty) when m <> meta ->
-           let canonical_context' =
-            List.map
-             (function
-                 None -> None
-               | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
-               | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
-             ) canonical_context
-           in
-            (m,canonical_context',subst_in ty)::i
-       | _ -> i
-    ) newmetasenv []
-  in
-   let newproof = uri,metasenv',bo',ty in
-    (newproof, metasenv')
-