]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic/cicUtil.ml
removed spurious "
[helm.git] / helm / software / components / cic / cicUtil.ml
1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 module C  = Cic
29 module UM = UriManager
30
31 exception Meta_not_found of int
32 exception Subst_not_found of int
33
34 let lookup_meta index metasenv =
35   try
36     List.find (fun (index', _, _) -> index = index') metasenv
37   with Not_found -> raise (Meta_not_found index)
38
39 let lookup_subst n subst =
40   try
41     List.assoc n subst
42   with Not_found -> raise (Subst_not_found n)
43
44 let exists_meta index = List.exists (fun (index', _, _) -> (index = index'))
45
46 (* clean_up_meta take a substitution, a metasenv a meta_inex and a local
47 context l and clean up l with respect to the hidden hipothesis in the 
48 canonical context *)
49
50 let clean_up_local_context subst metasenv n l =
51   let cc =
52     (try
53        let (cc,_,_) = lookup_subst n subst in cc
54      with Subst_not_found _ ->
55        try
56          let (_,cc,_) = lookup_meta n metasenv in cc
57        with Meta_not_found _ -> assert false) in
58   (try 
59      List.map2
60        (fun t1 t2 ->
61           match t1,t2 with 
62               None , _ -> None
63             | _ , t -> t) cc l
64    with 
65        Invalid_argument _ -> 
66          assert false)
67
68 let is_closed =
69  let module C = Cic in
70  let rec is_closed k =
71   function
72       C.Rel m when m > k -> false
73     | C.Rel m -> true
74     | C.Meta (_,l) ->
75        List.fold_left
76         (fun i t -> i && (match t with None -> true | Some t -> is_closed k t)
77         ) true l
78     | C.Sort _ -> true
79     | C.Implicit _ -> assert false
80     | C.Cast (te,ty) -> is_closed k te && is_closed k ty
81     | C.Prod (name,so,dest) -> is_closed k so && is_closed (k+1) dest
82     | C.Lambda (_,so,dest) -> is_closed k so && is_closed (k+1) dest
83     | C.LetIn (_,so,ty,dest) ->
84        is_closed k so && is_closed k ty && is_closed (k+1) dest
85     | C.Appl l ->
86        List.fold_right (fun x i -> i && is_closed k x) l true
87     | C.Var (_,exp_named_subst)
88     | C.Const (_,exp_named_subst)
89     | C.MutInd (_,_,exp_named_subst)
90     | C.MutConstruct (_,_,_,exp_named_subst) ->
91        List.fold_right (fun (_,x) i -> i && is_closed k x)
92         exp_named_subst true
93     | C.MutCase (_,_,out,te,pl) ->
94        is_closed k out && is_closed k te &&
95         List.fold_right (fun x i -> i && is_closed k x) pl true
96     | C.Fix (_,fl) ->
97        let len = List.length fl in
98         let k_plus_len = k + len in
99          List.fold_right
100           (fun (_,_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
101           ) fl true
102     | C.CoFix (_,fl) ->
103        let len = List.length fl in
104         let k_plus_len = k + len in
105          List.fold_right
106           (fun (_,ty,bo) i -> i && is_closed k ty && is_closed k_plus_len bo
107           ) fl true
108 in 
109  is_closed 0
110 ;;
111
112 let rec is_meta_closed =
113   function
114       C.Rel _ -> true
115     | C.Meta _ -> false
116     | C.Sort _ -> true
117     | C.Implicit _ -> assert false
118     | C.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
119     | C.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
120     | C.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
121     | C.LetIn (_,so,ty,dest) ->
122        is_meta_closed so &&
123        is_meta_closed ty &&
124        is_meta_closed dest
125     | C.Appl l ->
126        not (List.exists (fun x -> not (is_meta_closed x)) l)
127     | C.Var (_,exp_named_subst)
128     | C.Const (_,exp_named_subst)
129     | C.MutInd (_,_,exp_named_subst)
130     | C.MutConstruct (_,_,_,exp_named_subst) ->
131        not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst)
132     | C.MutCase (_,_,out,te,pl) ->
133        is_meta_closed out && is_meta_closed te &&
134         not (List.exists (fun x -> not (is_meta_closed x)) pl)
135     | C.Fix (_,fl) ->
136         not (List.exists 
137               (fun (_,_,ty,bo) -> 
138                   not (is_meta_closed ty) || not (is_meta_closed bo)) 
139               fl)
140     | C.CoFix (_,fl) ->
141         not (List.exists 
142               (fun (_,ty,bo) -> 
143                   not (is_meta_closed ty) || not (is_meta_closed bo)) 
144               fl)
145 ;;
146
147 let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
148 let slash_RE = Str.regexp "/"
149
150 let term_of_uri uri =
151   let s = UriManager.string_of_uri uri in
152   try
153     (if UriManager.uri_is_con uri then
154       C.Const (uri, [])
155     else if UriManager.uri_is_var uri then
156       C.Var (uri, [])
157     else if not (Str.string_match xpointer_RE s 0) then
158       raise (UriManager.IllFormedUri s)
159     else
160       let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in
161       let baseuri = UriManager.uri_of_string baseuri in
162       (match Str.split slash_RE xpointer with
163       | [_; tyno] -> C.MutInd (baseuri, int_of_string tyno - 1, [])
164       | [_; tyno; consno] ->
165           C.MutConstruct
166             (baseuri, int_of_string tyno - 1, int_of_string consno, [])
167       | _ -> raise Exit))
168   with
169   | Exit
170   | Failure _
171   | Not_found -> raise (UriManager.IllFormedUri s)
172
173 let uri_of_term = function
174   | C.Const (uri, _)
175   | C.Var (uri, _) -> uri
176   | C.MutInd (baseuri, tyno, _) ->
177      UriManager.uri_of_string
178       (Printf.sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
179   | C.MutConstruct (baseuri, tyno, consno, _) ->
180      UriManager.uri_of_string
181       (Printf.sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
182         (tyno + 1) consno)
183   | _ -> raise (Invalid_argument "uri_of_term")
184
185
186 (*
187 let pack terms =
188   List.fold_right
189     (fun term acc -> C.Prod (C.Anonymous, term, acc))
190     terms (C.Sort (C.Type (CicUniv.fresh ())))
191
192 let rec unpack = function
193   | C.Prod (C.Anonymous, term, C.Sort (C.Type _)) -> [term]
194   | C.Prod (C.Anonymous, term, tgt) -> term :: unpack tgt
195   | _ -> assert false
196 *)
197
198 let rec strip_prods n = function
199   | t when n = 0 -> t
200   | C.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
201   | _ -> failwith "not enough prods"
202
203 let params_of_obj = function
204   | C.Constant (_, _, _, params, _)
205   | C.Variable (_, _, _, params, _)
206   | C.CurrentProof (_, _, _, _, params, _)
207   | C.InductiveDefinition (_, params, _, _) ->
208       params
209
210 let attributes_of_obj = function
211   | C.Constant (_, _, _, _, attributes)
212   | C.Variable (_, _, _, _, attributes)
213   | C.CurrentProof (_, _, _, _, _, attributes)
214   | C.InductiveDefinition (_, _, _, attributes) ->
215       attributes
216
217 let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
218
219 let projections_of_record obj uri =
220   let attrs = attributes_of_obj obj in
221   try
222     let tag=List.find (function `Class (`Record _) -> true|_->false) attrs in
223     match tag with
224     |  `Class (`Record l) -> 
225          List.map (fun (name,_,_) ->
226            let buri = UriManager.buri_of_uri uri in
227            let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
228            puri) l
229     | _-> assert false 
230   with Not_found -> []
231 ;;
232       
233 let rec mk_rels howmany from =
234   match howmany with 
235   | 0 -> []
236   | _ -> (C.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
237
238 let id_of_annterm =
239   function
240   | C.ARel (id,_,_,_)
241   | C.AVar (id,_,_)
242   | C.AMeta (id,_,_)
243   | C.ASort (id,_)
244   | C.AImplicit (id,_)
245   | C.ACast (id,_,_)
246   | C.AProd (id,_,_,_)
247   | C.ALambda (id,_,_,_)
248   | C.ALetIn (id,_,_,_,_)
249   | C.AAppl (id,_)
250   | C.AConst (id,_,_)
251   | C.AMutInd (id,_,_,_)
252   | C.AMutConstruct (id,_,_,_,_)
253   | C.AMutCase (id,_,_,_,_,_)
254   | C.AFix (id,_,_)
255   | C.ACoFix (id,_,_) -> id
256
257
258 let rec rehash_term =
259   let module C = Cic in
260   let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
261   function
262    | (C.Rel _) as t -> t
263    | C.Var (uri,exp_named_subst) ->
264       let uri' = recons uri in
265       let exp_named_subst' =
266        List.map
267         (function (uri,t) ->(recons uri,rehash_term t)) 
268          exp_named_subst
269       in
270        C.Var (uri',exp_named_subst')
271    | C.Meta (i,l) ->
272       let l' =
273        List.map
274         (function
275             None -> None
276           | Some t -> Some (rehash_term t)
277         ) l
278       in
279        C.Meta(i,l')
280    | C.Sort (C.Type u) -> 
281        CicUniv.assert_univ u;
282        C.Sort (C.Type (CicUniv.recons_univ u))
283    | C.Sort _ as t -> t
284    | C.Implicit _ as t -> t
285    | C.Cast (te,ty) -> C.Cast (rehash_term te, rehash_term ty)
286    | C.Prod (n,s,t) -> C.Prod (n, rehash_term s, rehash_term t)
287    | C.Lambda (n,s,t) -> C.Lambda (n, rehash_term s, rehash_term t)
288    | C.LetIn (n,s,ty,t) ->
289       C.LetIn (n, rehash_term s, rehash_term ty, rehash_term t)
290    | C.Appl l -> C.Appl (List.map rehash_term l)
291    | C.Const (uri,exp_named_subst) ->
292       let uri' = recons uri in
293       let exp_named_subst' = 
294        List.map
295         (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
296       in
297        C.Const (uri',exp_named_subst')
298    | C.MutInd (uri,tyno,exp_named_subst) ->
299       let uri' = recons uri in
300       let exp_named_subst' = 
301        List.map
302         (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
303       in
304        C.MutInd (uri',tyno,exp_named_subst')
305    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
306       let uri' = recons uri in
307       let exp_named_subst' = 
308        List.map
309         (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst
310       in
311        C.MutConstruct (uri',tyno,consno,exp_named_subst')
312    | C.MutCase (uri,i,outty,t,pl) ->
313       C.MutCase (recons uri, i, rehash_term outty, rehash_term t,
314        List.map rehash_term pl)
315    | C.Fix (i, fl) ->
316       let liftedfl =
317        List.map
318         (fun (name, i, ty, bo) ->
319           (name, i, rehash_term ty, rehash_term bo))
320          fl
321       in
322        C.Fix (i, liftedfl)
323    | C.CoFix (i, fl) ->
324       let liftedfl =
325        List.map
326         (fun (name, ty, bo) -> (name, rehash_term ty, rehash_term bo))
327          fl
328       in
329        C.CoFix (i, liftedfl)
330
331 let rehash_obj =
332  let module C = Cic in
333  let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
334  function 
335    C.Constant (name,bo,ty,params,attrs) ->
336      let bo' =
337        match bo with
338          None -> None
339        | Some bo -> Some (rehash_term bo)
340      in
341      let ty' = rehash_term ty in
342      let params' = List.map recons params in
343      C.Constant (name, bo', ty', params',attrs)
344  | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
345      let conjs' =
346        List.map
347          (function (i,hyps,ty) ->
348            (i,
349            List.map (function
350                None -> None
351              | Some (name,C.Decl t) ->
352                  Some (name,C.Decl (rehash_term t))
353              | Some (name,C.Def (bo,ty)) ->
354                  Some (name,C.Def (rehash_term bo, rehash_term ty))) hyps,
355            rehash_term ty))
356          conjs
357      in
358      let bo' = rehash_term bo in
359      let ty' = rehash_term ty in
360      let params' = List.map recons params in
361      C.CurrentProof (name, conjs', bo', ty', params',attrs)
362  | C.Variable (name,bo,ty,params,attrs) ->
363      let bo' =
364        match bo with
365          None -> None
366        | Some bo -> Some (rehash_term bo)
367      in
368      let ty' = rehash_term ty in
369      let params' = List.map recons params in
370      C.Variable (name, bo', ty', params',attrs)
371  | C.InductiveDefinition (tl,params,paramsno,attrs) ->
372      let params' = List.map recons params in
373      let tl' =
374        List.map (function (name, inductive, ty, constructors) ->
375          name,
376          inductive,
377          rehash_term ty,
378          (List.map
379            (function (name, ty) -> name, rehash_term ty)
380            constructors))
381          tl
382      in
383      C.InductiveDefinition (tl', params', paramsno, attrs)
384
385 let rec metas_of_term = function
386   | C.Meta (i, c) -> [i,c]
387   | C.Var (_, ens) 
388   | C.Const (_, ens) 
389   | C.MutInd (_, _, ens) 
390   | C.MutConstruct (_, _, _, ens) ->
391       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
392   | C.Cast (s, t)
393   | C.Prod (_, s, t)
394   | C.Lambda (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
395   | C.LetIn (_, s, ty, t) ->
396      (metas_of_term s) @ (metas_of_term ty) @ (metas_of_term t)
397   | C.Appl l -> List.flatten (List.map metas_of_term l)
398   | C.MutCase (uri, i, s, t, l) ->
399       (metas_of_term s) @ (metas_of_term t) @
400         (List.flatten (List.map metas_of_term l))
401   | C.Fix (i, il) ->
402       List.flatten
403         (List.map (fun (s, i, t1, t2) ->
404                      (metas_of_term t1) @ (metas_of_term t2)) il)
405   | C.CoFix (i, il) ->
406       List.flatten
407         (List.map (fun (s, t1, t2) ->
408                      (metas_of_term t1) @ (metas_of_term t2)) il)
409   | _ -> []
410 ;;      
411
412 module MetaOT = struct
413   type t = int * C.term option list
414   let compare = Pervasives.compare
415 end
416
417 module S = Set.Make(MetaOT)
418
419 let rec metas_of_term_set = function
420   | C.Meta (i, c) -> S.singleton (i,c)
421   | C.Var (_, ens) 
422   | C.Const (_, ens) 
423   | C.MutInd (_, _, ens) 
424   | C.MutConstruct (_, _, _, ens) ->
425       List.fold_left 
426         (fun s (_,t) -> S.union s (metas_of_term_set t)) 
427         S.empty ens
428   | C.Cast (s, t)
429   | C.Prod (_, s, t)
430   | C.Lambda (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
431   | C.LetIn (_, s, ty, t) ->
432      S.union (metas_of_term_set s)
433       (S.union (metas_of_term_set ty) (metas_of_term_set t))
434   | C.Appl l -> 
435       List.fold_left 
436         (fun s t -> S.union s (metas_of_term_set t)) 
437         S.empty l
438   | C.MutCase (uri, i, s, t, l) ->
439       S.union 
440         (S.union (metas_of_term_set s)  (metas_of_term_set t))
441         (List.fold_left 
442           (fun s t -> S.union s (metas_of_term_set t)) 
443           S.empty l)
444   | C.Fix (_, il) ->
445       (List.fold_left 
446         (fun s (_,_,t1,t2) -> 
447           S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
448         S.empty il
449   | C.CoFix (i, il) ->
450       (List.fold_left 
451         (fun s (_,t1,t2) -> 
452           S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
453         S.empty il
454   | _ -> S.empty
455 ;;      
456
457 let metas_of_term_set t = 
458   let s = metas_of_term_set t in
459   S.elements s
460 ;;
461
462 (* syntactic_equality up to the                 *)
463 (* distinction between fake dependent products  *)
464 (* and non-dependent products, alfa-conversion  *)
465 let alpha_equivalence =
466   let rec aux t t' =
467    if t = t' then true
468    else
469     match t,t' with
470        C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
471         UriManager.eq uri1 uri2 &&
472          aux_exp_named_subst exp_named_subst1 exp_named_subst2
473      | C.Cast (te,ty), C.Cast (te',ty') ->
474         aux te te' && aux ty ty'
475      | C.Prod (_,s,t), C.Prod (_,s',t') ->
476         aux s s' && aux t t'
477      | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
478         aux s s' && aux t t'
479      | C.LetIn (_,s,ty,t), C.LetIn(_,s',ty',t') ->
480         aux s s' && aux ty ty' && aux t t'
481      | C.Appl l, C.Appl l' when List.length l = List.length l' ->
482         (try
483           List.fold_left2
484            (fun b t1 t2 -> b && aux t1 t2) true l l'
485          with
486           Invalid_argument _ -> false)
487      | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
488         UriManager.eq uri uri' &&
489          aux_exp_named_subst exp_named_subst1 exp_named_subst2
490      | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
491         UriManager.eq uri uri' && i = i' &&
492          aux_exp_named_subst exp_named_subst1 exp_named_subst2
493      | C.MutConstruct (uri,i,j,exp_named_subst1),
494        C.MutConstruct (uri',i',j',exp_named_subst2) ->
495         UriManager.eq uri uri' && i = i' && j = j' &&
496          aux_exp_named_subst exp_named_subst1 exp_named_subst2
497      | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
498         UriManager.eq sp sp' && i = i' &&
499          aux outt outt' && aux t t' &&
500           (try
501             List.fold_left2
502              (fun b t1 t2 -> b && aux t1 t2) true pl pl'
503            with
504             Invalid_argument _ -> false)
505      | C.Fix (i,fl), C.Fix (i',fl') ->
506         i = i' &&
507         (try
508           List.fold_left2
509            (fun b (_,i,ty,bo) (_,i',ty',bo') ->
510              b && i = i' && aux ty ty' && aux bo bo'
511            ) true fl fl'
512          with
513           Invalid_argument _ -> false)
514      | C.CoFix (i,fl), C.CoFix (i',fl') ->
515         i = i' &&
516         (try
517           List.fold_left2
518            (fun b (_,ty,bo) (_,ty',bo') ->
519              b && aux ty ty' && aux bo bo'
520            ) true fl fl'
521          with
522           Invalid_argument _ -> false)
523      | C.Meta (i, subst), C.Meta (i', subst') ->
524         i = i' &&
525         (try
526           List.fold_left2
527            (fun b xt xt' -> match xt,xt' with
528              | Some t, Some t' -> b && aux t t'
529              | _               -> b
530            ) true subst subst'
531          with
532           Invalid_argument _ -> false)
533      | C.Appl [t], t' | t, C.Appl [t'] -> assert false
534 (* FG: are we _really_ sure of these?      
535      | C.Sort (C.Type u), C.Sort (C.Type u') -> u = u' 
536      | C.Implicit a, C.Implicit a' -> a = a'
537    we insert an unused variable below to genarate a warning at compile time
538 *)     
539      | _,_ -> false (* we already know that t != t' *)
540   and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
541    try
542      List.fold_left2
543       (fun b (uri1,t1) (uri2,t2) ->
544         b && UriManager.eq uri1 uri2 && aux t1 t2
545       ) true exp_named_subst1 exp_named_subst2
546     with
547      Invalid_argument _ -> false
548   in
549    aux
550
551 let is_sober c t =
552    let rec sober_term c g = function
553       | C.Rel _ 
554       | C.Sort _  
555       | C.Implicit _                    -> g      
556       | C.Const (_, xnss) 
557       | C.Var (_, xnss) 
558       | C.MutConstruct (_, _, _, xnss)
559       | C.MutInd (_, _, xnss)           -> sober_xnss c g xnss
560       | C.Meta (_, xss)                 -> sober_xss c g xss
561       | C.Lambda (_, v, t)
562       | C.Prod (_, v, t)
563       | C.Cast (t, v)                   ->
564          sober_term c (sober_term c g t) v
565       | C.LetIn (_, v, ty, t)           ->
566          sober_term c (sober_term c (sober_term c g t) ty) v
567       | C.Appl []                       
568       | C.Appl [_]                      -> fun b -> false
569       | C.Appl ts                       -> sober_terms c g ts
570       | C.MutCase (_, _, t, v, ts)      -> 
571          sober_terms c (sober_term c (sober_term c g t) v) ts
572       | C.Fix (_, ifs)                  -> sober_ifs c g ifs
573       | C.CoFix (_, cifs)               -> sober_cifs c g cifs
574    and sober_terms c g = List.fold_left (sober_term c) g
575    and sober_xnss c g =
576       let map g (_, t) = sober_term c g t in
577       List.fold_left map g
578    and sober_xss c g =
579       let map g = function 
580          | None   -> g
581          | Some t -> sober_term c g t
582       in
583       List.fold_left map g
584    and sober_ifs c g =
585       let map g (_, _, t, v) = sober_term c (sober_term c g t) v in
586       List.fold_left map g
587    and sober_cifs c g =
588       let map g (_, t, v) = sober_term c (sober_term c g t) v in
589       List.fold_left map g
590    in 
591    sober_term c (fun b -> b) t true
592
593 (* raw cic prettyprinter ****************************************************)
594
595 let xiter out so ss sc map l =
596    let rec aux = function
597       | hd :: tl when tl <> [] -> map hd; out ss; aux tl
598       | hd :: tl               -> map hd; aux tl
599       | []                     -> ()
600    in
601    out so; aux l; out sc
602
603 let abst s w = Some (s, C.Decl w)
604
605 let abbr s v w = Some (s, C.Def (v, w))
606
607 let pp_sort out = function
608    | C.Type _  -> out "*Type"
609    | C.Prop    -> out "*Prop"
610    | C.CProp _ -> out "*CProp"
611    | C.Set     -> out "*Set"
612
613 let pp_name out = function
614    | C.Name s    -> out s
615    | C.Anonymous -> out "_"
616
617 let pp_rel out c i =
618    try match List.nth c (pred i) with
619       | None           -> out (Printf.sprintf "%u[?]" i)
620       | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
621    with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
622
623 let pp_implict out = function
624    | None         -> out "?"
625    | Some `Closed -> out "?[Closed]" 
626    | Some `Type   -> out "?[Type]"
627    | Some `Hole   -> out "?[Hole]"
628
629 let pp_uri out a =
630    out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
631
632 let rec pp_term out e c = function
633    | C.Sort h                      -> pp_sort out h
634    | C.Rel i                       -> pp_rel out c i
635    | C.Implicit x                  -> pp_implict out x
636    | C.Meta (i, iss)               ->
637       let map = function None   -> out "_" | Some v -> pp_term out e c v in
638       out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
639    | C.Var (a, xss)              ->
640       pp_uri out a; pp_xss out e c xss
641    | C.Const (a, xss)              ->
642       pp_uri out a; pp_xss out e c xss
643    | C.MutInd (a, m, xss)          ->
644       pp_uri out a; out (Printf.sprintf "/%u" m);
645       pp_xss out e c xss
646    | C.MutConstruct (a, m, n, xss) ->
647       pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
648       pp_xss out e c xss
649    | C.Cast (v, w)                 ->
650       out "type "; pp_term out e c w; out " contains "; pp_term out e c v
651    | C.Appl vs                     ->
652       xiter out "(" " @ " ")" (pp_term out e c) vs
653    | C.MutCase (a, m, w, v, vs)    ->
654       out "match "; pp_term out e c v;
655       out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
656       out " to "; pp_term out e c w;
657       xiter out " cases " " | " "" (pp_term out e c) vs
658    | C.Prod (s, w, t)             ->
659       out "forall "; pp_name out s; out " of "; pp_term out e c w;
660       out " in "; pp_term out e (abst s w :: c) t
661    | C.Lambda (s, w, t)            ->
662       out "fun "; pp_name out s; out " of "; pp_term out e c w;
663       out " in "; pp_term out e (abst s w :: c) t
664    | C.LetIn (s, v, w, t)          ->
665       out "let "; pp_name out s; 
666       out " def "; pp_term out e c v; out " of "; pp_term out e c w;
667       out " in "; pp_term out e (abbr s v w :: c) t
668    | C.Fix (i, fs)                 ->
669       let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
670       let c' = List.fold_left map c fs in
671       let map (s, i, w, v) =
672          out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v; 
673          out " of "; pp_term out e c w;
674       in
675       xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
676    | C.CoFix (i, fs)                 ->
677       let map c (s, w, v) = abbr (C.Name s) v w :: c in
678       let c' = List.fold_left map c fs in
679       let map (s, w, v) =
680          out s; pp_term out e c' v; 
681          out " of "; pp_term out e c w;
682       in
683       xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
684
685 and pp_xss out e c xss = 
686    let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
687    xiter out "[" "; " "]" map xss 
688
689 let pp_int out i =
690    out (Printf.sprintf "%u" i)
691
692 let pp_attrs out attrs = 
693    let map = function
694       | _ -> ()
695    in
696    xiter out "[" "; " "] " map attrs 
697    
698 let pp_pars out pars = 
699    xiter out " (" ", " ")\n" (pp_uri out) pars 
700
701 let pp_point out point =
702    if point then out "ind " else out "coind "
703
704 let pp_constructor out (s, w) =
705    out s; out " of "; pp_term out [] [] w
706
707 let pp_definition out (s, point, w, ts) =
708    out "let "; pp_point out point; out s; out " of "; pp_term out [] [] w;  
709    xiter out "\ndef " "\nor " "" (pp_constructor out) ts
710
711 let pp_obj out = function
712    | C.Constant (s, None, u, pars, attrs)           ->
713       out "fun "; pp_attrs out attrs; out s; pp_pars out pars;
714       out " of "; pp_term out [] [] u
715    | C.Constant (s, Some t, u, pars, attrs)         ->
716       out "let "; pp_attrs out attrs; out s; pp_pars out pars;
717       out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
718    | C.Variable (s, None, u, pars, attrs)           ->
719       out "local fun "; pp_attrs out attrs; out s; pp_pars out pars;
720       out " of "; pp_term out [] [] u
721    | C.Variable (s, Some t, u, pars, attrs)         ->
722       out "local let "; pp_attrs out attrs; out s; pp_pars out pars;
723       out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
724    | C.InductiveDefinition (us, pars, lpsno, attrs) ->
725       out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars;
726       xiter out "" "\n" "" (pp_definition out) us
727    | C.CurrentProof (s, e, t, u, pars, attrs)       ->
728       out "Current Proof" 
729