]> matita.cs.unibo.it Git - helm.git/blob - helm/fix_params/cicFindParameters.ml
.cvsignore added where useful
[helm.git] / helm / fix_params / 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.LetIn (_, s, t) -> aux s @@ aux t
68      | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
69      | C.Const (uri,_) ->
70         (* the parameters could be not exact but only possible *)
71         fix_params uri (Some (filename_of_uri uri)) ;
72         (* now the parameters are surely possible *)
73         (match CicCache.get_obj uri with
74             C.Definition (_, _, _, params) ->
75               List.fold_right
76                (fun (_,l) i ->
77                  List.fold_right
78                   (fun x i -> S.singleton x @@ i) l i
79                ) params S.empty
80           | C.Axiom (_, _, params) ->
81              List.fold_right
82               (fun (_,l) i ->
83                 List.fold_right
84                  (fun x i -> S.singleton x @@ i) l i
85               ) params S.empty
86           | C.CurrentProof _ -> S.empty (*CSC wrong *)
87           | _ -> raise WrongUriToConstant
88         )
89      | C.Abst _ -> S.empty
90      | C.MutInd (uri,_,_) ->
91         (match CicCache.get_obj uri with
92             C.InductiveDefinition (_, params, _) ->
93              List.fold_right
94               (fun (_,l) i ->
95                 List.fold_right
96                  (fun x i -> S.singleton x @@ i) l i
97               ) params S.empty
98           | _ -> raise WrongUriToInductiveDefinition
99         )
100      | C.MutConstruct (uri,_,_,_) ->
101         (match CicCache.get_obj uri with
102             C.InductiveDefinition (_, params, _) ->
103              List.fold_right
104               (fun (_,l) i ->
105                 List.fold_right
106                  (fun x i -> S.singleton x @@ i) l i
107               ) params S.empty
108           | _ -> raise WrongUriToInductiveDefinition
109         )
110      | C.MutCase (uri,_,_,outtype,term,patterns) ->
111         (*CSC cosa basta? Ci vuole anche uri? *)
112         (match CicCache.get_obj uri with
113             C.InductiveDefinition (_, params, _) ->
114             List.fold_right
115              (fun (_,l) i ->
116                List.fold_right
117                 (fun x i -> S.singleton x @@ i) l i
118              ) params S.empty
119           | _ -> raise WrongUriToInductiveDefinition
120         ) @@ aux outtype @@ aux term @@
121          List.fold_right (fun x i -> aux x @@ i) patterns S.empty
122      | C.Fix (_,fl) ->
123         List.fold_right
124          (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
125          fl S.empty
126      | C.CoFix (_,fl) ->
127         List.fold_right
128          (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
129          fl S.empty
130  in
131   let actual_params = aux te @@ aux ty in
132    (* sort_actual_params wants in input the ordered list of possible params *)
133    let rec sort_actual_params2 =
134     function
135        [] -> []
136      | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
137      | _::tl -> sort_actual_params2 tl
138    in
139     let rec sort_actual_params =
140      function
141         [] -> []
142       | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
143     in
144      sort_actual_params pparams
145
146 and fix_params uri filename =
147  let module C = Cic in
148   let ann = CicCache.get_annobj uri in
149    match ann with
150       C.ADefinition (xid, id, te, ty, C.Possible pparams) ->
151        let te' = Deannotate.deannotate_term te in
152        let ty' = Deannotate.deannotate_term ty in
153         let real_params = parameters_of te' ty' pparams in
154          let fixed =
155           C.ADefinition (xid,id,te,ty,C.Actual real_params)
156          in
157           Xml.pp (Cic2Xml.pp fixed uri) filename ;
158     | _ -> ()
159 ;;