]> matita.cs.unibo.it Git - helm.git/blob - helm/mathql/mathql_generator/cGSearchPattern.ml
reorganization continues ...
[helm.git] / helm / mathql / mathql_generator / cGSearchPattern.ml
1 (* Copyright (C) 2000, 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 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 02/12/2002                                 *)
32 (*                                                                            *)
33 (*                            Missing description                             *)
34 (*                                                                            *)
35 (******************************************************************************)
36
37 (* $Id$ *)
38
39 module T = MQGTypes
40 module U = MQGUtil
41
42 type classification =
43    Backbone of int
44  | Branch of int
45  | InConclusion
46  | InHypothesis
47 ;;
48
49 let soften_classification =
50  function
51     Backbone _ -> InConclusion
52   | Branch _ -> InHypothesis
53   | k -> k
54 ;;
55
56 let (!!) =
57  function
58     Backbone n -> `MainConclusion (Some n)
59   | Branch n -> `MainHypothesis (Some n)
60   | _        -> assert false
61 ;;
62
63 let (!!!) =
64  function
65     Backbone n -> `MainConclusion (Some n)
66   | Branch n -> `MainHypothesis (Some n)
67   | InConclusion -> `InConclusion
68   | InHypothesis -> `InHypothesis
69 ;;
70
71
72 let (@@) (l1,l2,l3) (l1',l2',l3') =
73  let merge l1 l2 =
74   List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
75  in
76   merge l1 l1', merge l2 l2', merge l3 l3'
77 ;;
78
79 let get_constraints term =
80  let module U = UriManager in
81  let module C = Cic in
82   let rec process_type_aux kind =
83    function
84       C.Var (uri,expl_named_subst) ->
85        (* andrea: this is a bug: variable are not indexedin the db 
86           ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ *)
87          (process_type_aux_expl_named_subst kind expl_named_subst)
88     | C.Rel _ ->
89        (match kind with
90          | InConclusion 
91          | InHypothesis -> [],[],[] 
92          | _            -> [],[!!kind],[])
93     | C.Sort s ->
94        (match kind with
95            Backbone _
96          | Branch _ ->
97             let s' =
98              match s with
99                 Cic.Prop -> T.Prop
100               | Cic.Set -> T.Set
101               | Cic.Type _ -> T.Type (* TASSI: ?? *)
102               | Cic.CProp -> T.CProp
103             in
104             [],[],[!!kind,s']
105          | _ -> [],[],[])
106     | C.Meta _ -> [],[],[] (* ???? To be understood *)
107     | C.Implicit _ -> assert false
108     | C.Cast (te,_) ->
109        (* type ignored *)
110        process_type_aux kind te
111     | C.Prod (_,sou,ta) ->
112        let (source_kind,target_kind) =
113         match kind with
114            Backbone n -> (Branch 0, Backbone (n+1))
115          | Branch n -> (InHypothesis, Branch (n+1))
116          | k -> (k,k)
117        in
118         process_type_aux source_kind sou @@
119         process_type_aux target_kind ta
120     | C.Lambda (_,sou,ta) ->
121         let kind' = soften_classification kind in
122          process_type_aux kind' sou @@
123          process_type_aux kind' ta
124     | C.LetIn (_,te,ta)->
125        let kind' = soften_classification kind in
126         process_type_aux kind' te @@
127         process_type_aux kind ta
128     | C.Appl (he::tl) ->
129        let kind' = soften_classification kind in
130         process_type_aux kind he @@
131         List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
132     | C.Appl _ -> assert false
133     | C.Const (uri,_) ->
134        [!!!kind, UriManager.string_of_uri uri],[],[]
135     | C.MutInd (uri,typeno,expl_named_subst) ->
136        ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ 
137         string_of_int (typeno + 1) ^ ")"],[],[]) @@
138          (process_type_aux_expl_named_subst kind expl_named_subst)
139     | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
140         ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
141          string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[])
142           @@ (process_type_aux_expl_named_subst kind expl_named_subst)
143     | C.MutCase (_,_,_,term,patterns) ->
144        (* outtype ignored *)
145        let kind' = soften_classification kind in
146         process_type_aux kind' term @@
147         List.fold_left (fun i t -> i @@ process_type_aux kind' t)
148          ([],[],[]) patterns
149     | C.Fix (_,funs) ->
150        let kind' = soften_classification kind in
151         List.fold_left
152          (fun i (_,_,bo,ty) ->
153            i @@
154             process_type_aux kind' bo @@
155             process_type_aux kind' ty
156          ) ([],[],[]) funs
157     | C.CoFix (_,funs) ->
158        let kind' = soften_classification kind in
159         List.fold_left
160          (fun i (_,bo,ty) ->
161            i @@
162             process_type_aux kind' bo @@
163             process_type_aux kind' ty
164          ) ([],[],[]) funs
165  and process_type_aux_expl_named_subst kind =
166   List.fold_left
167    (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
168    ([],[],[])
169 in
170  let obj_constraints,rel_constraints,sort_constraints =
171   process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
172  in
173   (obj_constraints,rel_constraints,sort_constraints)
174 ;;
175
176 (*CSC: Debugging only *)
177 (* 
178 let get_constraints term =
179  let res = get_constraints term in
180  let (objs,rels,sorts) = res in
181   let text_of_pos p =
182     U.text_of_position p ^ " " ^ U.text_of_depth p "NULL"
183   in
184   prerr_endline "Constraints on objs:" ;
185   List.iter
186    (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ;
187   prerr_endline "Constraints on Rels:" ;
188   List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ;
189   prerr_endline "Constraints on Sorts:" ;
190   List.iter
191    (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
192    ) sorts ;
193   res
194 ;; *)
195
196 let universe =
197    [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]