1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
30 exception Meta_not_found of int
31 exception Subst_not_found of int
33 let lookup_meta index metasenv =
35 List.find (fun (index', _, _) -> index = index') metasenv
36 with Not_found -> raise (Meta_not_found index)
38 let lookup_subst n subst =
41 with Not_found -> raise (Subst_not_found n)
43 let exists_meta index = List.exists (fun (index', _, _) -> (index = index'))
45 (* clean_up_meta take a substitution, a metasenv a meta_inex and a local
46 context l and clean up l with respect to the hidden hipothesis in the
49 let clean_up_local_context subst metasenv n l =
52 let (cc,_,_) = lookup_subst n subst in cc
53 with Subst_not_found _ ->
55 let (_,cc,_) = lookup_meta n metasenv in cc
56 with Meta_not_found _ -> assert false) in
71 C.Rel m when m > k -> false
75 (fun i t -> i && (match t with None -> true | Some t -> is_closed k t)
78 | C.Implicit _ -> assert false
79 | C.Cast (te,ty) -> is_closed k te && is_closed k ty
80 | C.Prod (name,so,dest) -> is_closed k so && is_closed (k+1) dest
81 | C.Lambda (_,so,dest) -> is_closed k so && is_closed (k+1) dest
82 | C.LetIn (_,so,dest) -> is_closed k so && is_closed (k+1) dest
84 List.fold_right (fun x i -> i && is_closed k x) l true
85 | C.Var (_,exp_named_subst)
86 | C.Const (_,exp_named_subst)
87 | C.MutInd (_,_,exp_named_subst)
88 | C.MutConstruct (_,_,_,exp_named_subst) ->
89 List.fold_right (fun (_,x) i -> i && is_closed k x)
91 | C.MutCase (_,_,out,te,pl) ->
92 is_closed k out && is_closed k te &&
93 List.fold_right (fun x i -> i && is_closed k x) pl true
95 let len = List.length fl in
96 let k_plus_len = k + len in
98 (fun (_,_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
101 let len = List.length fl in
102 let k_plus_len = k + len in
104 (fun (_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
110 let rec is_meta_closed =
113 | Cic.Meta _ -> false
115 | Cic.Implicit _ -> assert false
116 | Cic.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
117 | Cic.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
118 | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
119 | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
121 not (List.exists (fun x -> not (is_meta_closed x)) l)
122 | Cic.Var (_,exp_named_subst)
123 | Cic.Const (_,exp_named_subst)
124 | Cic.MutInd (_,_,exp_named_subst)
125 | Cic.MutConstruct (_,_,_,exp_named_subst) ->
126 not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst)
127 | Cic.MutCase (_,_,out,te,pl) ->
128 is_meta_closed out && is_meta_closed te &&
129 not (List.exists (fun x -> not (is_meta_closed x)) pl)
133 not (is_meta_closed ty) || not (is_meta_closed bo))
135 | Cic.CoFix (_,fl) ->
138 not (is_meta_closed ty) || not (is_meta_closed bo))
142 let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
143 let slash_RE = Str.regexp "/"
145 let term_of_uri uri =
146 let s = UriManager.string_of_uri uri in
148 (if UriManager.uri_is_con uri then
150 else if UriManager.uri_is_var uri then
152 else if not (Str.string_match xpointer_RE s 0) then
153 raise (UriManager.IllFormedUri s)
155 let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in
156 let baseuri = UriManager.uri_of_string baseuri in
157 (match Str.split slash_RE xpointer with
158 | [_; tyno] -> Cic.MutInd (baseuri, int_of_string tyno - 1, [])
159 | [_; tyno; consno] ->
161 (baseuri, int_of_string tyno - 1, int_of_string consno, [])
166 | Not_found -> raise (UriManager.IllFormedUri s)
168 let uri_of_term = function
170 | Cic.Var (uri, _) -> uri
171 | Cic.MutInd (baseuri, tyno, _) ->
172 UriManager.uri_of_string
173 (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
174 | Cic.MutConstruct (baseuri, tyno, consno, _) ->
175 UriManager.uri_of_string
176 (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
178 | _ -> raise (Invalid_argument "uri_of_term")
184 (fun term acc -> Cic.Prod (Cic.Anonymous, term, acc))
185 terms (Cic.Sort (Cic.Type (CicUniv.fresh ())))
187 let rec unpack = function
188 | Cic.Prod (Cic.Anonymous, term, Cic.Sort (Cic.Type _)) -> [term]
189 | Cic.Prod (Cic.Anonymous, term, tgt) -> term :: unpack tgt
193 let rec strip_prods n = function
195 | Cic.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
196 | _ -> failwith "not enough prods"
198 let params_of_obj = function
199 | Cic.Constant (_, _, _, params, _)
200 | Cic.Variable (_, _, _, params, _)
201 | Cic.CurrentProof (_, _, _, _, params, _)
202 | Cic.InductiveDefinition (_, params, _, _) ->
205 let attributes_of_obj = function
206 | Cic.Constant (_, _, _, _, attributes)
207 | Cic.Variable (_, _, _, _, attributes)
208 | Cic.CurrentProof (_, _, _, _, _, attributes)
209 | Cic.InductiveDefinition (_, _, _, attributes) ->
212 let arity_of_composed_coercion obj =
213 let attrs = attributes_of_obj obj in
215 let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
217 | `Class (`Coercion n) -> n
222 let rec mk_rels howmany from =
225 | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
229 | Cic.ARel (id,_,_,_)
233 | Cic.AImplicit (id,_)
235 | Cic.AProd (id,_,_,_)
236 | Cic.ALambda (id,_,_,_)
237 | Cic.ALetIn (id,_,_,_)
239 | Cic.AConst (id,_,_)
240 | Cic.AMutInd (id,_,_,_)
241 | Cic.AMutConstruct (id,_,_,_,_)
242 | Cic.AMutCase (id,_,_,_,_,_)
244 | Cic.ACoFix (id,_,_) -> id
247 let rec rehash_term =
248 let module C = Cic in
249 let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
251 | (C.Rel _) as t -> t
252 | C.Var (uri,exp_named_subst) ->
253 let uri' = recons uri in
254 let exp_named_subst' =
256 (function (uri,t) ->(recons uri,rehash_term t))
259 C.Var (uri',exp_named_subst')
265 | Some t -> Some (rehash_term t)
269 | C.Sort (C.Type u) ->
270 CicUniv.assert_univ u;
271 C.Sort (C.Type (CicUniv.recons_univ u))
273 | C.Implicit _ as t -> t
274 | C.Cast (te,ty) -> C.Cast (rehash_term te, rehash_term ty)
275 | C.Prod (n,s,t) -> C.Prod (n, rehash_term s, rehash_term t)
276 | C.Lambda (n,s,t) -> C.Lambda (n, rehash_term s, rehash_term t)
277 | C.LetIn (n,s,t) -> C.LetIn (n, rehash_term s, rehash_term t)
278 | C.Appl l -> C.Appl (List.map rehash_term l)
279 | C.Const (uri,exp_named_subst) ->
280 let uri' = recons uri in
281 let exp_named_subst' =
283 (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
285 C.Const (uri',exp_named_subst')
286 | C.MutInd (uri,tyno,exp_named_subst) ->
287 let uri' = recons uri in
288 let exp_named_subst' =
290 (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
292 C.MutInd (uri',tyno,exp_named_subst')
293 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
294 let uri' = recons uri in
295 let exp_named_subst' =
297 (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
299 C.MutConstruct (uri',tyno,consno,exp_named_subst')
300 | C.MutCase (uri,i,outty,t,pl) ->
301 C.MutCase (recons uri, i, rehash_term outty, rehash_term t,
302 List.map rehash_term pl)
306 (fun (name, i, ty, bo) ->
307 (name, i, rehash_term ty, rehash_term bo))
314 (fun (name, ty, bo) -> (name, rehash_term ty, rehash_term bo))
317 C.CoFix (i, liftedfl)
320 let module C = Cic in
321 let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
323 C.Constant (name,bo,ty,params,attrs) ->
327 | Some bo -> Some (rehash_term bo)
329 let ty' = rehash_term ty in
330 let params' = List.map recons params in
331 C.Constant (name, bo', ty', params',attrs)
332 | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
335 (function (i,hyps,ty) ->
339 | Some (name,C.Decl t) ->
340 Some (name,C.Decl (rehash_term t))
341 | Some (name,C.Def (bo,ty)) ->
345 | Some ty'' -> Some (rehash_term ty'')
347 Some (name,C.Def (rehash_term bo, ty'))) hyps,
351 let bo' = rehash_term bo in
352 let ty' = rehash_term ty in
353 let params' = List.map recons params in
354 C.CurrentProof (name, conjs', bo', ty', params',attrs)
355 | C.Variable (name,bo,ty,params,attrs) ->
359 | Some bo -> Some (rehash_term bo)
361 let ty' = rehash_term ty in
362 let params' = List.map recons params in
363 C.Variable (name, bo', ty', params',attrs)
364 | C.InductiveDefinition (tl,params,paramsno,attrs) ->
365 let params' = List.map recons params in
367 List.map (function (name, inductive, ty, constructors) ->
372 (function (name, ty) -> name, rehash_term ty)
376 C.InductiveDefinition (tl', params', paramsno, attrs)
378 let rec metas_of_term = function
379 | Cic.Meta (i, c) -> [i,c]
382 | Cic.MutInd (_, _, ens)
383 | Cic.MutConstruct (_, _, _, ens) ->
384 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
387 | Cic.Lambda (_, s, t)
388 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
389 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
390 | Cic.MutCase (uri, i, s, t, l) ->
391 (metas_of_term s) @ (metas_of_term t) @
392 (List.flatten (List.map metas_of_term l))
395 (List.map (fun (s, i, t1, t2) ->
396 (metas_of_term t1) @ (metas_of_term t2)) il)
397 | Cic.CoFix (i, il) ->
399 (List.map (fun (s, t1, t2) ->
400 (metas_of_term t1) @ (metas_of_term t2)) il)
404 module MetaOT = struct
405 type t = int * Cic.term option list
406 let compare = Pervasives.compare
409 module S = Set.Make(MetaOT)
411 let rec metas_of_term_set = function
412 | Cic.Meta (i, c) -> S.singleton (i,c)
415 | Cic.MutInd (_, _, ens)
416 | Cic.MutConstruct (_, _, _, ens) ->
418 (fun s (_,t) -> S.union s (metas_of_term_set t))
422 | Cic.Lambda (_, s, t)
423 | Cic.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
426 (fun s t -> S.union s (metas_of_term_set t))
428 | Cic.MutCase (uri, i, s, t, l) ->
430 (S.union (metas_of_term_set s) (metas_of_term_set t))
432 (fun s t -> S.union s (metas_of_term_set t))
436 (fun s (_,_,t1,t2) ->
437 S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
439 | Cic.CoFix (i, il) ->
442 S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
447 let metas_of_term_set t =
448 let s = metas_of_term_set t in