]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/logicalOperations.ml
...
[helm.git] / helm / gTopLevel / logicalOperations.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 get_parent id ids_to_terms ids_to_father_ids =
27  match Hashtbl.find ids_to_father_ids id with
28     None -> None
29   | Some id -> Some (id, Hashtbl.find ids_to_terms id)
30 ;;
31
32 let get_context ids_to_terms ids_to_father_ids =
33  let module C = Cic in
34   let rec aux id =
35    match get_parent id ids_to_terms ids_to_father_ids with
36       None -> []
37     | Some (parentid,parent) ->
38        let term = Hashtbl.find ids_to_terms id in
39        let binding =
40         match parent with
41            C.Rel _
42          | C.Var _
43          | C.Meta _
44          | C.Sort _
45          | C.Implicit _
46          | C.Cast _ -> []
47          | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
48          | C.Prod _ -> []
49          | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
50          | C.Lambda _ -> []
51          | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def (s,None))]
52          | C.LetIn _ -> []
53          | C.Appl _
54          | C.Const _ -> []
55          | C.MutInd _
56          | C.MutConstruct _
57          | C.MutCase _ -> []
58 (*CSC: sbagliato: manca il when *)
59          | C.Fix (_,ifl) ->
60             let counter = ref 0 in
61              List.rev_map
62               (function (name,_,ty,bo) ->
63                 let res =
64                  Some (C.Name name, (C.Def ((C.Fix (!counter,ifl)), Some ty)))
65                 in
66                  incr counter ;
67                  res
68               ) ifl
69          | C.CoFix (_,ifl) ->
70             let counter = ref 0 in
71              List.rev_map
72               (function (name,ty,bo) ->
73                 let res =
74                  Some (C.Name name,(C.Def ((C.CoFix (!counter,ifl)), Some ty)))
75                 in
76                  incr counter ;
77                  res
78               ) ifl
79        in
80         binding@(aux parentid)
81   in
82    aux
83 ;;
84
85 exception NotImplemented;;
86
87 (* A subterm is changed into a fresh meta *)
88 let to_sequent id ids_to_terms ids_to_father_ids =
89  let module P = ProofEngine in
90   let term = Hashtbl.find ids_to_terms id in
91   let context = get_context ids_to_terms ids_to_father_ids id in
92    let metasenv =
93     match P.get_proof () with
94        None -> assert false
95      | Some (_,metasenv,_,_) -> metasenv
96    in
97     let ty,_ = (* TASSI: FIXME ehhmmmm *)
98       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
99     in
100       P.perforate context term ty (* P.perforate also sets the goal *)
101 ;;
102
103 exception FocusOnlyOnMeta;;
104
105 (* If the current selection is a Meta, that Meta becomes the current goal *)
106 let focus id ids_to_terms ids_to_father_ids =
107  let module P = ProofEngine in
108   let term = Hashtbl.find ids_to_terms id in
109   let context = get_context ids_to_terms ids_to_father_ids id in
110    let metasenv =
111     match P.get_proof () with
112        None -> assert false
113      | Some (_,metasenv,_,_) -> metasenv
114    in
115     let ty,_ = 
116       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
117     in
118       match term with
119           Cic.Meta (n,_) -> P.goal := Some n
120         | _ -> raise FocusOnlyOnMeta
121 ;;