1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* Missing description *)
35 (******************************************************************************)
44 let soften_classification =
46 Backbone _ -> InConclusion
47 | Branch _ -> InHypothesis
54 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
56 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
58 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
60 "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
63 let (@@) (l1,l2,l3) (l1',l2',l3') =
65 List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
67 merge l1 l1', merge l2 l2', merge l3 l3'
70 let get_constraints term =
71 let module U = UriManager in
73 let rec process_type_aux kind =
75 C.Var (uri,expl_named_subst) ->
76 let kind',depth = !!kind in
77 ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
78 (process_type_aux_expl_named_subst kind expl_named_subst)
80 let kind',depth = !!kind in
83 | Some d -> [],[kind',Some d],[])
91 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
93 "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
95 "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
97 let kind',depth = !!kind in
100 | Some d -> [],[],[kind',Some d,s'])
103 | C.Implicit -> assert false
106 process_type_aux kind te
107 | C.Prod (_,sou,ta) ->
108 let (source_kind,target_kind) =
110 Backbone n -> (Branch 0, Backbone (n+1))
111 | Branch n -> (InHypothesis, Branch (n+1))
114 process_type_aux source_kind sou @@
115 process_type_aux target_kind ta
116 | C.Lambda (_,sou,ta) ->
117 let kind' = soften_classification kind in
118 process_type_aux kind' sou @@
119 process_type_aux kind' ta
120 | C.LetIn (_,te,ta)->
121 let kind' = soften_classification kind in
122 process_type_aux kind' te @@
123 process_type_aux kind ta
125 let kind' = soften_classification kind in
126 process_type_aux kind he @@
127 List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
128 | C.Appl _ -> assert false
130 let kind',depth = !!kind in
131 [UriManager.string_of_uri uri,kind',depth],[],[]
132 | C.MutInd (uri,typeno,expl_named_subst) ->
133 let kind',depth = !!kind in
134 ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
135 ")", kind', depth],[],[]) @@
136 (process_type_aux_expl_named_subst kind expl_named_subst)
137 | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
138 let kind',depth = !!kind in
139 ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
140 "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
141 (process_type_aux_expl_named_subst kind expl_named_subst)
142 | C.MutCase (_,_,_,term,patterns) ->
143 (* outtype ignored *)
144 let kind' = soften_classification kind in
145 process_type_aux kind' term @@
146 List.fold_left (fun i t -> i @@ process_type_aux kind' t)
149 let kind' = soften_classification kind in
151 (fun i (_,_,bo,ty) ->
153 process_type_aux kind' bo @@
154 process_type_aux kind' ty
156 | C.CoFix (_,funs) ->
157 let kind' = soften_classification kind in
161 process_type_aux kind' bo @@
162 process_type_aux kind' ty
164 and process_type_aux_expl_named_subst kind =
166 (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
169 let obj_constraints,rel_constraints,sort_constraints =
170 process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
172 (obj_constraints,rel_constraints,sort_constraints)
175 (*CSC: Debugging only *)
176 let get_constraints term =
177 let res = get_constraints term in
178 let (objs,rels,sorts) = res in
179 prerr_endline "Constraints on objs:" ;
181 (function (s1,s2,n) ->
183 (s1 ^ " " ^ s2 ^ " " ^
184 match n with None -> "NULL" | Some n -> string_of_int n)
186 prerr_endline "Constraints on Rels:" ;
190 (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
192 prerr_endline "Constraints on Sorts:" ;
194 (function (s1,n,s2) ->
196 (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^