]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/proofEngineHelpers.ml
coercion application
[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml
1 (* Copyright (C) 2002, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
27   CicMkImplicit.new_meta metasenv []
28
29 let subst_meta_in_proof proof meta term newmetasenv =
30  let uri,metasenv,bo,ty = proof in
31    (* empty context is ok for term since it wont be used by apply_subst *)
32    (* hack: since we do not know the context and the type of term, we
33       create a substitution with cc =[] and type = Implicit; they will be
34       in  any case dropped by apply_subst, but it would be better to rewrite
35       the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
36   let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
37    let metasenv' =
38     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
39    in
40     let metasenv'' =
41      List.map
42       (function i,canonical_context,ty ->
43         let canonical_context' =
44          List.map
45           (function
46               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
47             | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
48             | None -> None
49             | Some (_,Cic.Def (_,Some _)) -> assert false
50           ) canonical_context
51         in
52          i,canonical_context',(subst_in ty)
53       ) metasenv'
54     in
55      let bo' = subst_in bo in
56      (* Metavariables can appear also in the *statement* of the theorem
57       * since the parser does not reject as statements terms with
58       * metavariable therein *)
59      let ty' = subst_in ty in
60       let newproof = uri,metasenv'',bo',ty' in
61        (newproof, metasenv'')
62
63 (*CSC: commento vecchio *)
64 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
65 (* This (heavy) function must be called when a tactic can instantiate old *)
66 (* metavariables (i.e. existential variables). It substitues the metasenv *)
67 (* of the proof with the result of removing [meta] from the domain of     *)
68 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
69 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
70 (*  current proof.                                                        *)
71 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
72 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
73 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
74 (*CSC: [newmetasenv].                                             *)
75 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
76  let (uri,_,bo,ty) = proof in
77   let bo' = subst_in bo in
78   (* Metavariables can appear also in the *statement* of the theorem
79    * since the parser does not reject as statements terms with
80    * metavariable therein *)
81   let ty' = subst_in ty in
82   let metasenv' =
83    List.fold_right
84     (fun metasenv_entry i ->
85       match metasenv_entry with
86          (m,canonical_context,ty) when m <> meta ->
87            let canonical_context' =
88             List.map
89              (function
90                  None -> None
91                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
92                | Some (i,Cic.Def (t,None))  ->
93                   Some (i,Cic.Def ((subst_in t),None))
94                | Some (_,Cic.Def (_,Some _))  -> assert false
95              ) canonical_context
96            in
97             (m,canonical_context',subst_in ty)::i
98        | _ -> i
99     ) newmetasenv []
100   in
101    let newproof = uri,metasenv',bo',ty' in
102     (newproof, metasenv')
103
104 let compare_metasenvs ~oldmetasenv ~newmetasenv =
105  List.map (function (i,_,_) -> i)
106   (List.filter
107    (function (i,_,_) ->
108      not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
109 ;;