]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_exportation/cicExportation.ml
more pps
[helm.git] / helm / software / components / cic_exportation / cicExportation.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 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
27
28 exception CicExportationInternalError;;
29 exception NotEnoughElements;;
30
31 (* *)
32
33 let is_mcu_type u = 
34   UriManager.eq (UriManager.uri_of_string
35   "cic:/matita/freescale/opcode/mcu_type.ind") u
36 ;;
37
38 (* Utility functions *)
39
40 let analyze_term context t =
41  match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
42   | Cic.Sort _ -> `Type
43   | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
44   | ty -> 
45      match
46       fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
47      with
48      | Cic.Sort Cic.Prop -> `Proof
49      | _ -> `Term
50 ;;
51
52 let analyze_type context t =
53  let rec aux =
54   function
55      Cic.Sort s -> `Sort s
56    | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
57    | Cic.Prod (_,_,t) -> aux t
58    | _ -> `SomethingElse
59  in
60  match aux t with
61     `Sort _ | `Optimize as res -> res
62   | `SomethingElse ->
63       match
64        fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
65       with
66           Cic.Sort Cic.Prop -> `Statement
67        | _ -> `Type
68 ;;
69
70 let ppid =
71  let reserved =
72   [ "to";
73     "mod";
74     "val";
75     "in";
76     "function"
77   ]
78  in
79   function n ->
80    let n = String.uncapitalize n in
81     if List.mem n reserved then n ^ "_" else n
82 ;;
83
84 let ppname =
85  function
86     Cic.Name s     -> ppid s
87   | Cic.Anonymous  -> "_"
88 ;;
89
90 (* get_nth l n   returns the nth element of the list l if it exists or *)
91 (* raises NotEnoughElements if l has less than n elements             *)
92 let rec get_nth l n =
93  match (n,l) with
94     (1, he::_) -> he
95   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
96   | (_,_) -> raise NotEnoughElements
97 ;;
98
99 let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
100  let name =
101   if capitalize then
102    String.capitalize (UriManager.name_of_uri uri)
103   else
104    ppid (UriManager.name_of_uri uri) in
105   let filename =
106    let suri = UriManager.buri_of_uri uri in
107    let s = String.sub suri 5 (String.length suri - 5) in
108    let s = Pcre.replace ~pat:"/" ~templ:"_" s in
109     String.uncapitalize s in
110   if current_module_uri = UriManager.buri_of_uri uri then
111    name
112   else
113    String.capitalize filename ^ "." ^ name
114 ;;
115
116 let current_go_up = ref "(.!(";;
117 let at_level2 f x = 
118   try 
119     current_go_up := "(.~(";
120     let rc = f x in 
121     current_go_up := "(.!("; 
122     rc
123   with exn -> 
124     current_go_up := "(.!("; 
125     raise exn
126 ;;
127
128 let pp current_module_uri ?metasenv ~in_type =
129 let rec pp ~in_type t context =
130  let module C = Cic in
131    match t with
132       C.Rel n ->
133        begin
134         try
135          (match get_nth context n with
136              Some (C.Name s,_) -> ppid s
137            | Some (C.Anonymous,_) -> "__" ^ string_of_int n
138            | None -> "_hidden_" ^ string_of_int n
139          )
140         with
141          NotEnoughElements -> string_of_int (List.length context - n)
142        end
143     | C.Var (uri,exp_named_subst) ->
144         qualified_name_of_uri current_module_uri uri ^
145          pp_exp_named_subst exp_named_subst context
146     | C.Meta (n,l1) ->
147        (match metasenv with
148            None ->
149             "?" ^ (string_of_int n) ^ "[" ^ 
150              String.concat " ; "
151               (List.rev_map
152                 (function
153                     None -> "_"
154                   | Some t -> pp ~in_type:false t context) l1) ^
155              "]"
156          | Some metasenv ->
157             try
158              let _,context,_ = CicUtil.lookup_meta n metasenv in
159               "?" ^ (string_of_int n) ^ "[" ^ 
160                String.concat " ; "
161                 (List.rev
162                   (List.map2
163                     (fun x y ->
164                       match x,y with
165                          _, None
166                        | None, _ -> "_"
167                        | Some _, Some t -> pp ~in_type:false t context
168                     ) context l1)) ^
169                "]"
170             with
171               CicUtil.Meta_not_found _ 
172             | Invalid_argument _ ->
173               "???" ^ (string_of_int n) ^ "[" ^ 
174                String.concat " ; "
175                 (List.rev_map (function None -> "_" | Some t ->
176                   pp ~in_type:false t context) l1) ^
177                "]"
178        )
179     | C.Sort s ->
180        (match s with
181            C.Prop  -> "Prop"
182          | C.Set   -> "Set"
183          | C.Type _ -> "Type"
184          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
185          | C.CProp _ -> "CProp" 
186        )
187     | C.Implicit (Some `Hole) -> "%"
188     | C.Implicit _ -> "?"
189     | C.Prod (b,s,t) ->
190        (match b with
191           C.Name n ->
192            let n = "'" ^ String.uncapitalize n in
193             "(" ^ pp ~in_type:true s context ^ " -> " ^
194             pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
195         | C.Anonymous ->
196            "(" ^ pp ~in_type:true s context ^ " -> " ^
197            pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
198     | C.Cast (v,t) -> pp ~in_type v context
199     | C.Lambda (b,s,t) ->
200        (match analyze_type context s with
201            `Sort _
202          | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
203          | `Optimize -> prerr_endline "XXX lambda";assert false
204          | `Type ->
205             "(function " ^ ppname b ^ " -> " ^
206              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
207     | C.LetIn (b,s,ty,t) ->
208        (match analyze_term context s with
209          | `Type
210          | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
211          | `Optimize 
212          | `Term ->
213             "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
214             " = " ^ pp ~in_type:false s context ^ " in " ^
215              pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
216     | C.Appl (he::tl) when in_type ->
217        let hes = pp ~in_type he context in
218        let stl = String.concat "," (clean_args_for_ty context tl) in
219         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
220     | C.Appl (C.MutInd _ as he::tl) ->
221        let hes = pp ~in_type he context in
222        let stl = String.concat "," (clean_args_for_ty context tl) in
223         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
224     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
225        let nparams =
226         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
227            C.InductiveDefinition (_,_,nparams,_) -> nparams
228          | _ -> assert false in
229        let hes = pp ~in_type he context in
230        let stl = String.concat "," (clean_args_for_constr nparams context tl) in
231         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
232     | C.Appl li ->
233        "(" ^ String.concat " " (clean_args context li) ^ ")"
234     | C.Const (uri,exp_named_subst) ->
235        qualified_name_of_uri current_module_uri uri ^
236         pp_exp_named_subst exp_named_subst context
237     | C.MutInd (uri,n,exp_named_subst) ->
238        (try
239          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
240             C.InductiveDefinition (dl,_,_,_) ->
241              let (name,_,_,_) = get_nth dl (n+1) in
242               qualified_name_of_uri current_module_uri
243                (UriManager.uri_of_string
244                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
245               pp_exp_named_subst exp_named_subst context
246           | _ -> raise CicExportationInternalError
247         with
248            Sys.Break as exn -> raise exn
249          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
250        )
251     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
252        (try
253          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
254             C.InductiveDefinition (dl,_,_,_) ->
255              let _,_,_,cons = get_nth dl (n1+1) in
256               let id,_ = get_nth cons n2 in
257                qualified_name_of_uri current_module_uri ~capitalize:true
258                 (UriManager.uri_of_string
259                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
260                pp_exp_named_subst exp_named_subst context
261           | _ -> raise CicExportationInternalError
262         with
263            Sys.Break as exn -> raise exn
264          | _ ->
265           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
266            string_of_int n2
267        )
268     | C.MutCase (uri,n1,ty,te,patterns) ->
269        if in_type then
270         "unit (* TOO POLYMORPHIC TYPE *)"
271        else (
272        let rec needs_obj_magic ty =
273         match CicReduction.whd context ty with
274          | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
275          | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
276          | _ -> false (* it can be a Rel, e.g. in *_rec *)
277        in
278        let needs_obj_magic = needs_obj_magic ty in
279        (match analyze_term context te with
280            `Type -> assert false
281          | `Proof ->
282              (match patterns with
283                  [] -> "assert false"   (* empty type elimination *)
284                | [he] ->
285                   pp ~in_type:false he context  (* singleton elimination *)
286                | _ -> assert false)
287          | `Optimize 
288          | `Term ->
289             if patterns = [] then "assert false"
290             else
291              (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
292                (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
293                    C.InductiveDefinition (dl,_,paramsno,_) ->
294                     let (_,_,_,cons) = get_nth dl (n1+1) in
295                     let rc = 
296                      List.map
297                       (fun (id,ty) ->
298                         (* this is just an approximation since we do not have
299                            reduction yet! *)
300                         let rec count_prods toskip =
301                          function
302                             C.Prod (_,_,bo) when toskip > 0 ->
303                              count_prods (toskip - 1) bo
304                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
305                           | _ -> 0
306                         in
307                          qualified_name_of_uri current_module_uri
308                           ~capitalize:true
309                           (UriManager.uri_of_string
310                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
311                          count_prods paramsno ty
312                       ) cons
313                     in
314                     if not (is_mcu_type uri) then rc, "","","",""
315                     else rc, !current_go_up, "))", "( .< (", " ) >.)"
316                  | _ -> raise CicExportationInternalError
317                )
318               in
319                let connames_and_argsno_and_patterns =
320                 let rec combine =
321                    function
322                       [],[] -> []
323                     | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
324                     | _,_ -> assert false
325                 in
326                  combine (connames_and_argsno,patterns)
327                in
328                 go_up ^
329                 "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
330                  (String.concat "\n | "
331                   (List.map
332                    (fun (x,argsno,y) ->
333                      let rec aux argsno context =
334                       function
335                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
336                           let name =
337                            match name with
338                               Cic.Anonymous -> Cic.Anonymous
339                             | Cic.Name n -> Cic.Name (ppid n) in
340                           let args,res =
341                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
342                             bo
343                           in
344                            (match analyze_type context ty with
345                              | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
346                              | `Statement
347                              | `Sort _ -> args,res
348                              | `Type ->
349                                  (match name with
350                                      C.Anonymous -> "_"
351                                    | C.Name s -> s)::args,res)
352                        | t when argsno = 0 -> [],pp ~in_type:false t context
353                        | t ->
354                           ["{" ^ string_of_int argsno ^ " args missing}"],
355                            pp ~in_type:false t context
356                      in
357                       let pattern,body =
358                        if argsno = 0 then x,pp ~in_type:false y context
359                        else
360                         let args,body = aux argsno context y in
361                         let sargs = String.concat "," args in
362                          x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
363                           body
364                       in
365                        pattern ^ " -> " ^ go_down ^
366                         (if needs_obj_magic then
367                          "Obj.magic (" ^ body ^ ")"
368                         else
369                          body) ^ go_nwod
370                    ) connames_and_argsno_and_patterns)) ^
371                  ")\n"^go_pu)))
372     | C.Fix (no, funs) ->
373        let names,_ =
374         List.fold_left
375          (fun (types,len) (n,_,ty,_) ->
376             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
377              len+1)
378          ) ([],0) funs
379        in
380          "let rec " ^
381          List.fold_right
382           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
383             pp ~in_type:false bo (names@context) ^ i)
384           funs "" ^
385          " in " ^
386          (match get_nth names (no + 1) with
387              Some (Cic.Name n,_) -> n
388            | _ -> assert false)
389     | C.CoFix (no,funs) ->
390        let names,_ =
391         List.fold_left
392          (fun (types,len) (n,ty,_) ->
393             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
394              len+1)
395          ) ([],0) funs
396        in
397          "\nCoFix " ^ " {" ^
398          List.fold_right
399           (fun (name,ty,bo) i -> "\n" ^ name ^ 
400             " : " ^ pp ~in_type:true ty context ^ " := \n" ^
401             pp ~in_type:false bo (names@context) ^ i)
402           funs "" ^
403          "}\n"
404 and pp_exp_named_subst exp_named_subst context =
405  if exp_named_subst = [] then "" else
406   "\\subst[" ^
407    String.concat " ; " (
408     List.map
409      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
410      exp_named_subst
411    ) ^ "]"
412 and clean_args_for_constr nparams context =
413  let nparams = ref nparams in
414  HExtlib.filter_map
415   (function t ->
416     decr nparams;
417     match analyze_term context t with
418        `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
419      | `Optimize 
420      | `Term
421      | `Type
422      | `Proof -> None)
423 and clean_args context =
424  function
425  | [] | [_] -> assert false
426  | he::arg1::tl as l ->
427     let head_arg1, rest = 
428        match analyze_term context arg1 with
429       | `Optimize -> 
430          !current_go_up :: pp ~in_type:false he context :: 
431                  pp ~in_type:false arg1 context :: ["))"], tl
432       | _ -> [], l
433     in
434     head_arg1 @ 
435     HExtlib.filter_map
436      (function t ->
437        match analyze_term context t with
438         | `Term -> Some (pp ~in_type:false t context)
439         | `Optimize -> 
440             prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
441         | `Type
442         | `Proof -> None) rest
443 and clean_args_for_ty context =
444  HExtlib.filter_map
445   (function t ->
446     match analyze_term context t with
447        `Type -> Some (pp ~in_type:true t context)
448      | `Optimize -> None
449      | `Proof -> None
450      | `Term -> None)
451 in
452  pp ~in_type
453 ;;
454
455 let ppty current_module_uri =
456  (* nparams is the number of left arguments
457     left arguments should either become parameters or be skipped altogether *)
458  let rec args nparams context =
459   function
460      Cic.Prod (n,s,t) ->
461       let n =
462        match n with
463           Cic.Anonymous -> Cic.Anonymous
464         | Cic.Name n -> Cic.Name (String.uncapitalize n)
465       in
466        (match analyze_type context s with
467          | `Optimize
468          | `Statement
469          | `Sort Cic.Prop ->
470              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
471          | `Type when nparams > 0 ->
472              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
473          | `Type ->
474              let abstr,args =
475               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
476                abstr,pp ~in_type:true current_module_uri s context::args
477          | `Sort _ when nparams <= 0 ->
478              let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
479               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
480          | `Sort _ ->
481              let n =
482               match n with
483                  Cic.Anonymous -> Cic.Anonymous
484                | Cic.Name name -> Cic.Name ("'" ^ name) in
485              let abstr,args =
486               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
487              in
488               (match n with
489                   Cic.Anonymous -> abstr
490                 | Cic.Name name -> name::abstr),
491               args)
492    | _ -> [],[]
493  in
494   args
495 ;;
496
497 exception DoNotExtract;;
498
499 let pp_abstracted_ty current_module_uri =
500  let rec args context =
501   function
502      Cic.Lambda (n,s,t) ->
503       let n =
504        match n with
505           Cic.Anonymous -> Cic.Anonymous
506         | Cic.Name n -> Cic.Name (String.uncapitalize n)
507       in
508        (match analyze_type context s with
509          | `Optimize 
510          | `Statement
511          | `Type
512          | `Sort Cic.Prop ->
513              args ((Some (n,Cic.Decl s))::context) t
514          | `Sort _ ->
515              let n =
516               match n with
517                  Cic.Anonymous -> Cic.Anonymous
518                | Cic.Name name -> Cic.Name ("'" ^ name) in
519              let abstr,res =
520               args ((Some (n,Cic.Decl s))::context) t
521              in
522               (match n with
523                   Cic.Anonymous -> abstr
524                 | Cic.Name name -> name::abstr),
525               res)
526    | ty ->
527      match analyze_type context ty with
528       | `Optimize ->
529            prerr_endline "XXX abstracted l2 ty"; assert false
530       | `Sort _
531       | `Statement -> raise DoNotExtract
532       | `Type ->
533           (* BUG HERE: this can be a real System F type *)
534           let head = pp ~in_type:true current_module_uri ty context in
535           [],head
536  in
537   args
538 ;;
539
540
541 (* ppinductiveType (typename, inductive, arity, cons)                       *)
542 (* pretty-prints a single inductive definition                              *)
543 (* (typename, inductive, arity, cons)                                       *)
544 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
545 =
546  match analyze_type [] arity with
547     `Sort Cic.Prop -> ""
548   | `Optimize 
549   | `Statement
550   | `Type -> assert false
551   | `Sort _ ->
552     if cons = [] then
553      "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
554     else (
555      let abstr,scons =
556       List.fold_right
557        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
558           let abstr',sargs = ppty current_module_uri nparams [] ty in
559           let sargs = String.concat " * " sargs in
560            abstr',
561            String.capitalize id ^
562             (if sargs = "" then "" else " of " ^ sargs) ^
563             (if i = "" then "" else "\n | ") ^ i)
564        cons ([],"")
565       in
566        let abstr =
567         let s = String.concat "," abstr in
568         if s = "" then "" else "(" ^ s ^ ") "
569        in
570        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
571 ;;
572
573 let ppobj current_module_uri obj =
574  let module C = Cic in
575  let module U = UriManager in
576   let pp ~in_type = pp ~in_type current_module_uri in
577   match obj with
578     C.Constant (name, Some t1, t2, params, _) ->
579       (match analyze_type [] t2 with
580         | `Sort Cic.Prop
581         | `Statement -> ""
582         | `Optimize 
583         | `Type -> 
584             (match t1 with
585             | Cic.Lambda (Cic.Name arg, s, t) ->
586                             (match analyze_type [] s with
587                 | `Optimize -> 
588
589                     "let " ^ ppid name ^ "__1 = function " ^ ppid arg 
590                     ^ " -> .< " ^ 
591                     at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)] 
592                     ^ " >. ;;\n"
593                     ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
594                     ^ "let " ^ ppid name ^ " = function " ^ ppid arg
595                     ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic  !"^ppid name
596                     ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
597                     ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
598                     ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
599                     ^ppid name^"__2)) >.\n;;\n"
600                     ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
601                     name^" Matita_freescale_opcode.HCS08)"
602                 | _ -> 
603                    "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
604             | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
605         | `Sort _ ->
606             match analyze_type [] t1 with
607                `Sort Cic.Prop -> ""
608              | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
609              | _ ->
610                (try
611                  let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
612                  let abstr =
613                   let s = String.concat "," abstr in
614                   if s = "" then "" else "(" ^ s ^ ") "
615                  in
616                   "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
617                 with
618                  DoNotExtract -> ""))
619    | C.Constant (name, None, ty, params, _) ->
620       (match analyze_type [] ty with
621           `Sort Cic.Prop
622         | `Optimize -> prerr_endline "XXX axiom l2"; assert false
623         | `Statement -> ""
624         | `Sort _ -> "type " ^ ppid name ^ "\n"
625         | `Type -> "let " ^ ppid name ^ " = assert false\n")
626    | C.Variable (name, bo, ty, params, _) ->
627       "Variable " ^ name ^
628        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
629        ")" ^ ":\n" ^
630        pp ~in_type:true ty [] ^ "\n" ^
631        (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
632    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
633       "Current Proof of " ^ name ^
634        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
635        ")" ^ ":\n" ^
636       let separate s = if s = "" then "" else s ^ " ; " in
637        List.fold_right
638         (fun (n, context, t) i -> 
639           let conjectures',name_context =
640                  List.fold_right 
641                   (fun context_entry (i,name_context) ->
642                     (match context_entry with
643                         Some (n,C.Decl at) ->
644                          (separate i) ^
645                            ppname n ^ ":" ^
646                             pp ~in_type:true ~metasenv:conjectures
647                             at name_context ^ " ",
648                             context_entry::name_context
649                       | Some (n,C.Def (at,aty)) ->
650                          (separate i) ^
651                            ppname n ^ ":" ^
652                             pp ~in_type:true ~metasenv:conjectures
653                             aty name_context ^
654                            ":= " ^ pp ~in_type:false
655                             ~metasenv:conjectures at name_context ^ " ",
656                             context_entry::name_context
657                       | None ->
658                          (separate i) ^ "_ :? _ ", context_entry::name_context)
659             ) context ("",[])
660           in
661            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
662             pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
663         ) conjectures "" ^
664         "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
665           pp ~in_type:true ~metasenv:conjectures ty [] 
666    | C.InductiveDefinition (l, params, nparams, _) ->
667       List.fold_right
668        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
669 ;;
670
671 let ppobj current_module_uri obj =
672  let res = ppobj current_module_uri obj in
673   if res = "" then "" else res ^ ";;\n\n"
674 ;;