]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cicFindParameters.ml
Main code clean-up.
[helm.git] / helm / interface / cicFindParameters.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 exception WrongUriToConstant;;
27 exception WrongUriToInductiveDefinition;;
28 exception CircularDependency of string;;
29
30 module OrderedUris =
31  struct
32   type t = UriManager.uri
33   let compare (s1 : t) (s2 : t) =
34    (* library function for = *)
35    compare s1 s2
36    (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
37  end
38 ;;
39
40 let filename_of_uri uri =
41  let uri' = UriManager.string_of_uri uri in
42   let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
43    fn ^ ".xml"
44 ;;
45
46 (* quite inefficient coding of a set of strings: the only operations  *)
47 (* performed are mem O(log n), and union O(n * log n?)                *)
48 (* Perhaps a better implementation would be an array of bits or a map *)
49 (* from uri to booleans                                               *)
50 module SetOfUris = Set.Make(OrderedUris);;
51
52 let (@@) = SetOfUris.union;;
53
54 let rec parameters_of te ty pparams=
55  let module S = SetOfUris in
56  let module C = Cic in
57    let rec aux =
58     function
59        C.Rel _ -> S.empty
60      | C.Var uri -> S.singleton uri
61      | C.Meta _ -> S.empty
62      | C.Sort _ -> S.empty
63      | C.Implicit -> S.empty
64      | C.Cast (te, ty) -> aux te @@ aux ty
65      | C.Prod (_, s, t) -> aux s @@ aux t
66      | C.Lambda (_, s, t) -> aux s @@ aux t
67      | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
68      | C.Const (uri,_) ->
69         (* the parameters could be not exact but only possible *)
70         fix_params uri (Some (filename_of_uri uri)) ;
71         (* now the parameters are surely possible *)
72         (match CicCache.get_obj uri with
73             C.Definition (_, _, _, params) ->
74               List.fold_right
75                (fun (_,l) i ->
76                  List.fold_right
77                   (fun x i -> S.singleton x @@ i) l i
78                ) params S.empty
79           | C.Axiom (_, _, params) ->
80              List.fold_right
81               (fun (_,l) i ->
82                 List.fold_right
83                  (fun x i -> S.singleton x @@ i) l i
84               ) params S.empty
85           | C.CurrentProof _ -> S.empty (*CSC wrong *)
86           | _ -> raise WrongUriToConstant
87         )
88      | C.Abst _ -> S.empty
89      | C.MutInd (uri,_,_) ->
90         (match CicCache.get_obj uri with
91             C.InductiveDefinition (_, params, _) ->
92              List.fold_right
93               (fun (_,l) i ->
94                 List.fold_right
95                  (fun x i -> S.singleton x @@ i) l i
96               ) params S.empty
97           | _ -> raise WrongUriToInductiveDefinition
98         )
99      | C.MutConstruct (uri,_,_,_) ->
100         (match CicCache.get_obj uri with
101             C.InductiveDefinition (_, params, _) ->
102              List.fold_right
103               (fun (_,l) i ->
104                 List.fold_right
105                  (fun x i -> S.singleton x @@ i) l i
106               ) params S.empty
107           | _ -> raise WrongUriToInductiveDefinition
108         )
109      | C.MutCase (uri,_,_,outtype,term,patterns) ->
110         (*CSC cosa basta? Ci vuole anche uri? *)
111         (match CicCache.get_obj uri with
112             C.InductiveDefinition (_, params, _) ->
113             List.fold_right
114              (fun (_,l) i ->
115                List.fold_right
116                 (fun x i -> S.singleton x @@ i) l i
117              ) params S.empty
118           | _ -> raise WrongUriToInductiveDefinition
119         ) @@ aux outtype @@ aux term @@
120          List.fold_right (fun x i -> aux x @@ i) patterns S.empty
121      | C.Fix (_,fl) ->
122         List.fold_right
123          (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
124          fl S.empty
125      | C.CoFix (_,fl) ->
126         List.fold_right
127          (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
128          fl S.empty
129  in
130   let actual_params = aux te @@ aux ty in
131    (* sort_actual_params wants in input the ordered list of possible params *)
132    let rec sort_actual_params2 =
133     function
134        [] -> []
135      | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
136      | _::tl -> sort_actual_params2 tl
137    in
138     let rec sort_actual_params =
139      function
140         [] -> []
141       | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
142     in
143      sort_actual_params pparams
144
145 and fix_params uri filename =
146  let module C = Cic in
147   let (ann, _, deann) = CicCache.get_annobj uri in
148    match ann, deann with
149       (C.ADefinition (xid, ann, id, te, ty, C.Possible pparams),
150        C.Definition (id', te', ty', _)) ->
151         (* let's freeze the object to avoid circular dependencies *)
152         CicCache.change_obj uri None ;
153         let real_params = parameters_of te' ty' pparams in
154          let fixed =
155           C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
156          in
157           Xml.pp (Cic2Xml.pp fixed uri) filename ;
158           (* unfreeze and fix the object *)
159           CicCache.change_obj uri
160            (Some (C.Definition (id', te', ty', real_params)))
161     | _ -> ()
162 ;;