]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/proofEngineHelpers.ml
removed ancient lablgtk, lablgtk_gtkmathview
[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 (* mk_fresh_name context name typ                      *)
27 (* returns an identifier which is fresh in the context *)
28 (* and that resembles [name] as much as possible.      *)
29 (* [typ] will be the type of the variable              *)
30 let mk_fresh_name context name ~typ =
31  let module C = Cic in
32   let basename =
33    match name with
34       C.Anonymous ->
35        (*CSC: great space for improvements here *)
36        (try
37          (match CicTypeChecker.type_of_aux' [] context typ with
38              C.Sort C.Prop -> "H"
39            | C.Sort C.CProp -> "H"
40            | C.Sort C.Set -> "x"
41            | _ -> "H"
42          )
43         with CicTypeChecker.TypeCheckerFailure _ -> "H"
44        )
45     | C.Name name ->
46        Str.global_replace (Str.regexp "[0-9]*$") "" name
47   in
48    let already_used name =
49     List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
50    in
51     if not (already_used basename) then
52      C.Name basename
53     else
54      let rec try_next n =
55       let name' = basename ^ string_of_int n in
56        if already_used name' then
57         try_next (n+1)
58        else
59         C.Name name'
60      in
61       try_next 1
62 ;;
63
64 (* identity_relocation_list_for_metavariable i canonical_context         *)
65 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
66 (* where n = List.length [canonical_context]                             *)
67 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
68 let identity_relocation_list_for_metavariable canonical_context =
69  let canonical_context_length = List.length canonical_context in
70   let rec aux =
71    function
72       (_,[]) -> []
73     | (n,None::tl) -> None::(aux ((n+1),tl))
74     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
75   in
76    aux (1,canonical_context)
77
78 (* Returns the first meta whose number is above the *)
79 (* number of the higher meta.                       *)
80 let new_meta ~proof =
81  let (_,metasenv,_,_) = proof in
82   let rec aux =
83    function
84       None,[] -> 1
85     | Some n,[] -> n
86     | None,(n,_,_)::tl -> aux (Some n,tl)
87     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
88   in
89    1 + aux (None,metasenv)
90
91 let subst_meta_in_proof proof meta term newmetasenv =
92  let uri,metasenv,bo,ty = proof in
93   let subst_in = CicUnification.apply_subst [meta,term] in
94    let metasenv' =
95     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
96    in
97     let metasenv'' =
98      List.map
99       (function i,canonical_context,ty ->
100         let canonical_context' =
101          List.map
102           (function
103               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
104             | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
105             | None -> None
106             | Some (_,Cic.Def (_,Some _)) -> assert false
107           ) canonical_context
108         in
109          i,canonical_context',(subst_in ty)
110       ) metasenv'
111     in
112      let bo' = subst_in bo in
113       let newproof = uri,metasenv'',bo',ty in
114        (newproof, metasenv'')
115
116 (*CSC: commento vecchio *)
117 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
118 (* This (heavy) function must be called when a tactic can instantiate old *)
119 (* metavariables (i.e. existential variables). It substitues the metasenv *)
120 (* of the proof with the result of removing [meta] from the domain of     *)
121 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
122 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
123 (*  current proof.                                                        *)
124 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
125 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
126 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
127 (*CSC: [newmetasenv].                                             *)
128 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
129  let (uri,_,bo,ty) = proof in
130   let bo' = subst_in bo in
131   let metasenv' =
132    List.fold_right
133     (fun metasenv_entry i ->
134       match metasenv_entry with
135          (m,canonical_context,ty) when m <> meta ->
136            let canonical_context' =
137             List.map
138              (function
139                  None -> None
140                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
141                | Some (i,Cic.Def (t,None))  ->
142                   Some (i,Cic.Def ((subst_in t),None))
143                | Some (_,Cic.Def (_,Some _))  -> assert false
144              ) canonical_context
145            in
146             (m,canonical_context',subst_in ty)::i
147        | _ -> i
148     ) newmetasenv []
149   in
150    let newproof = uri,metasenv',bo',ty in
151     (newproof, metasenv')
152