- added Ring tactic on reals

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

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
new file mode 100644 (file)
index 0000000..7e5f3a4
--- /dev/null
+++ b/helm/gTopLevel/proofEngineHelpers.ml
@@ -0,0 +1,123 @@
+(* 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/.
+ *)
+
+(* 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 =
+  match proof with
+     None -> assert false
+   | Some (_,metasenv,_,_) -> metasenv
+ 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) =
+  match proof with
+     None -> assert false
+   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ 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 = Some (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) =
+  match proof with
+     None -> assert false
+   | Some (uri,_,bo,ty) -> uri,bo,ty
+ 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 = Some (uri,metasenv',bo',ty) in
+    (newproof, metasenv')
+