]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_acic/cic2acic.ml
types2006 patch
[helm.git] / helm / software / components / cic_acic / cic2acic.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$ *)
27
28 type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
29
30 let string_of_sort = function
31   | `Prop -> "Prop"
32   | `Set -> "Set"
33   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
34   | `CProp -> "CProp"
35
36 let sort_of_sort = function
37   | Cic.Prop  -> `Prop
38   | Cic.Set   -> `Set
39   | Cic.Type u -> `Type u
40   | Cic.CProp -> `CProp
41
42 (* let hashtbl_add_time = ref 0.0;; *)
43
44 let xxx_add h k v =
45 (*  let t1 = Sys.time () in *)
46   Hashtbl.add h k v ;
47 (*   let t2 = Sys.time () in
48    hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 *)
49 ;;
50
51 (* let number_new_type_of_aux' = ref 0;;
52 let type_of_aux'_add_time = ref 0.0;; *)
53
54 let xxx_type_of_aux' m c t =
55 (*  let t1 = Sys.time () in *)
56  let res,_ =
57    try
58     CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
59    with
60    | CicTypeChecker.AssertFailure _
61    | CicTypeChecker.TypeCheckerFailure _ ->
62        Cic.Sort Cic.Prop, CicUniv.empty_ugraph
63   in
64 (*  let t2 = Sys.time () in
65  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
66  res
67 ;;
68
69 type anntypes =
70  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
71 ;;
72
73 let gen_id seed =
74  let res = "i" ^ string_of_int !seed in
75   incr seed ;
76   res
77 ;;
78
79 let fresh_id seed ids_to_terms ids_to_father_ids =
80  fun father t ->
81   let res = gen_id seed in
82    xxx_add ids_to_father_ids res father ;
83    xxx_add ids_to_terms res t ;
84    res
85 ;;
86
87 let source_id_of_id id = "#source#" ^ id;;
88
89 exception NotEnoughElements;;
90
91 (*CSC: cut&paste da cicPp.ml *)
92 (* get_nth l n   returns the nth element of the list l if it exists or *)
93 (* raises NotEnoughElements if l has less than n elements             *)
94 let rec get_nth l n =
95  match (n,l) with
96     (1, he::_) -> he
97   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
98   | (_,_) -> raise NotEnoughElements
99 ;;
100
101 let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
102   seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
103   metasenv context idrefs t expectedty
104 =
105  let module D = DoubleTypeInference in
106  let module C = Cic in
107   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
108 (*    let time1 = Sys.time () in *)
109    let terms_to_types =
110 (*
111      let time0 = Sys.time () in
112      let prova = CicTypeChecker.type_of_aux' metasenv context t in
113      let time1 = Sys.time () in
114      prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
115      let res = D.double_type_of metasenv context t expectedty in
116      let time2 = Sys.time () in
117    prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
118      res 
119 *)
120     if global_computeinnertypes then
121      D.double_type_of metasenv context t expectedty
122     else
123      Cic.CicHash.create 1 (* empty table *)
124    in
125 (*
126    let time2 = Sys.time () in
127    prerr_endline
128     ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
129 *)
130     let rec aux computeinnertypes father context idrefs tt =
131      let fresh_id'' = fresh_id' father tt in
132      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
133      let aux' = aux computeinnertypes (Some fresh_id'') in
134       (* First of all we compute the inner type and the inner sort *)
135       (* of the term. They may be useful in what follows.          *)
136       (*CSC: This is a very inefficient way of computing inner types *)
137       (*CSC: and inner sorts: very deep terms have their types/sorts *)
138       (*CSC: computed again and again.                               *)
139       let sort_of t =
140        match CicReduction.whd context t with 
141           C.Sort C.Prop  -> `Prop
142         | C.Sort C.Set   -> `Set
143         | C.Sort (C.Type u) -> `Type u
144         | C.Meta _       -> `Type (CicUniv.fresh())
145         | C.Sort C.CProp -> `CProp
146         | t              ->
147             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
148             assert false
149       in
150        let ainnertypes,innertype,innersort,expected_available =
151 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
152 (*CSC: (expected type + inferred type). Just for now we use the usual *)
153 (*CSC: type-inference, but the result is very poor. As a very weak    *)
154 (*CSC: patch, I apply whd to the computed type. Full beta             *)
155 (*CSC: reduction would be a much better option.                       *)
156 (*CSC: solo per testare i tempi *)
157 (*XXXXXXX *)
158         try
159 (* *)
160         let {D.synthesized = synthesized; D.expected = expected} =
161          if computeinnertypes then
162           Cic.CicHash.find terms_to_types tt
163          else
164           (* We are already in an inner-type and Coscoy's double *)
165           (* type inference algorithm has not been applied.      *)
166           { D.synthesized =
167 (***CSC: patch per provare i tempi
168             CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
169             (*if global_computeinnertypes then
170               Cic.Sort (Cic.Type (CicUniv.fresh()))
171             else*)
172               CicReduction.whd context (xxx_type_of_aux' metasenv context tt);
173           D.expected = None}
174         in
175 (*          incr number_new_type_of_aux' ; *)
176          let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
177           let ainnertypes,expected_available =
178            if computeinnertypes then
179             let annexpected,expected_available =
180                match expected with
181                   None -> None,false
182                 | Some expectedty' ->
183                    Some
184                     (aux false (Some fresh_id'') context idrefs expectedty'),
185                     true
186             in
187              Some
188               {annsynthesized =
189                 aux false (Some fresh_id'') context idrefs synthesized ;
190                annexpected = annexpected
191               }, expected_available
192            else
193             None,false
194           in
195            ainnertypes,synthesized, sort_of innersort, expected_available
196 (*XXXXXXXX *)
197         with
198          Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
199           (* CSC: Type or Set? I can not tell *)
200           let u = CicUniv.fresh() in
201           None,Cic.Sort (Cic.Type u),`Type u,false 
202           (* TASSI non dovrebbe fare danni *)
203 (* *)
204        in
205         let add_inner_type id =
206          match ainnertypes with
207             None -> ()
208           | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
209         in
210          match tt with
211             C.Rel n ->
212              let id =
213               match get_nth context n with
214                  (Some (C.Name s,_)) -> s
215                | _ -> "__" ^ string_of_int n
216              in
217               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
218               if innersort = `Prop  && expected_available then
219                add_inner_type fresh_id'' ;
220               C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
221           | C.Var (uri,exp_named_subst) ->
222              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
223              if innersort = `Prop  && expected_available then
224               add_inner_type fresh_id'' ;
225              let exp_named_subst' =
226               List.map
227                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
228              in
229               C.AVar (fresh_id'', uri,exp_named_subst')
230           | C.Meta (n,l) ->
231              let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
232              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
233              if innersort = `Prop  && expected_available then
234               add_inner_type fresh_id'' ;
235              C.AMeta (fresh_id'', n,
236               (List.map2
237                 (fun ct t ->
238                   match (ct, t) with
239                   | None, _ -> None
240                   | _, Some t -> Some (aux' context idrefs t)
241                   | Some _, None -> assert false (* due to typing rules *))
242                 canonical_context l))
243           | C.Sort s -> C.ASort (fresh_id'', s)
244           | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
245           | C.Cast (v,t) ->
246              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
247              if innersort = `Prop then
248               add_inner_type fresh_id'' ;
249              C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
250           | C.Prod (n,s,t) ->
251               xxx_add ids_to_inner_sorts fresh_id''
252                (sort_of innertype) ;
253                     let sourcetype = xxx_type_of_aux' metasenv context s in
254                      xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
255                       (sort_of sourcetype) ;
256               let n' =
257                match n with
258                   C.Anonymous -> n
259                 | C.Name n' ->
260                    if DoubleTypeInference.does_not_occur 1 t then
261                     C.Anonymous
262                    else
263                     C.Name n'
264               in
265                C.AProd
266                 (fresh_id'', n', aux' context idrefs s,
267                  aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
268           | C.Lambda (n,s,t) ->
269              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
270                    let sourcetype = xxx_type_of_aux' metasenv context s in
271                     xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
272                      (sort_of sourcetype) ;
273               if innersort = `Prop then
274                begin
275                 let father_is_lambda =
276                  match father with
277                     None -> false
278                   | Some father' ->
279                      match Hashtbl.find ids_to_terms father' with
280                         C.Lambda _ -> true
281                       | _ -> false
282                 in
283                  if (not father_is_lambda) || expected_available then
284                   add_inner_type fresh_id''
285                end ;
286               C.ALambda
287                (fresh_id'',n, aux' context idrefs s,
288                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
289           | C.LetIn (n,s,t) ->
290              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
291              if innersort = `Prop then
292               add_inner_type fresh_id'' ;
293              C.ALetIn
294               (fresh_id'', n, aux' context idrefs s,
295                aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
296           | C.Appl l ->
297              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
298              if innersort = `Prop then
299               add_inner_type fresh_id'' ;
300              C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
301           | C.Const (uri,exp_named_subst) ->
302              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
303              if innersort = `Prop  && expected_available then
304               add_inner_type fresh_id'' ;
305              let exp_named_subst' =
306               List.map
307                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
308              in
309               C.AConst (fresh_id'', uri, exp_named_subst')
310           | C.MutInd (uri,tyno,exp_named_subst) ->
311              let exp_named_subst' =
312               List.map
313                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
314              in
315               C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
316           | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
317              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
318              if innersort = `Prop  && expected_available then
319               add_inner_type fresh_id'' ;
320              let exp_named_subst' =
321               List.map
322                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
323              in
324               C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
325           | C.MutCase (uri, tyno, outty, term, patterns) ->
326              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
327              if innersort = `Prop then
328               add_inner_type fresh_id'' ;
329              C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
330               aux' context idrefs term, List.map (aux' context idrefs) patterns)
331           | C.Fix (funno, funs) ->
332              let fresh_idrefs =
333               List.map (function _ -> gen_id seed) funs in
334              let new_idrefs = List.rev fresh_idrefs @ idrefs in
335              let tys =
336               List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
337              in
338               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
339               if innersort = `Prop then
340                add_inner_type fresh_id'' ;
341               C.AFix (fresh_id'', funno,
342                List.map2
343                 (fun id (name, indidx, ty, bo) ->
344                   (id, name, indidx, aux' context idrefs ty,
345                     aux' (tys@context) new_idrefs bo)
346                 ) fresh_idrefs funs
347              )
348           | C.CoFix (funno, funs) ->
349              let fresh_idrefs =
350               List.map (function _ -> gen_id seed) funs in
351              let new_idrefs = List.rev fresh_idrefs @ idrefs in
352              let tys =
353               List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
354              in
355               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
356               if innersort = `Prop then
357                add_inner_type fresh_id'' ;
358               C.ACoFix (fresh_id'', funno,
359                List.map2
360                 (fun id (name, ty, bo) ->
361                   (id, name, aux' context idrefs ty,
362                     aux' (tys@context) new_idrefs bo)
363                 ) fresh_idrefs funs
364               )
365         in
366 (*
367          let timea = Sys.time () in
368          let res = aux true None context idrefs t in
369          let timeb = Sys.time () in
370           prerr_endline
371            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
372           res
373 *)
374         aux global_computeinnertypes None context idrefs t
375 ;;
376
377 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
378  let ids_to_terms = Hashtbl.create 503 in
379  let ids_to_father_ids = Hashtbl.create 503 in
380  let ids_to_inner_sorts = Hashtbl.create 503 in
381  let ids_to_inner_types = Hashtbl.create 503 in
382  let seed = ref 0 in
383    acic_of_cic_context' ~computeinnertypes seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
384     ids_to_inner_types metasenv context idrefs t,
385    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
386 ;;
387
388 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
389   ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
390   metasenv (metano,context,goal)
391
392   let computeinnertypes = false in
393   let acic_of_cic_context =
394     acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
395       ids_to_inner_types  metasenv in
396   let _, acontext,final_idrefs =
397     (List.fold_right
398       (fun binding (context, acontext,idrefs) ->
399          let hid = "h" ^ string_of_int !hypotheses_seed in
400            Hashtbl.add ids_to_hypotheses hid binding ;
401            incr hypotheses_seed ;
402            match binding with
403                Some (n,Cic.Def (t,_)) ->
404                  let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
405                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
406                   (Some hid);
407                  (binding::context),
408                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
409              | Some (n,Cic.Decl t) ->
410                  let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
411                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
412                   (Some hid);
413                  (binding::context),
414                    ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
415              | None ->
416                  (* Invariant: "" is never looked up *)
417                   (None::context),((hid,None)::acontext),""::idrefs
418          ) context ([],[],[])
419        )
420   in 
421   let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in
422   (metano,acontext,agoal)
423 ;;
424
425 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = 
426     let ids_to_terms = Hashtbl.create 503 in
427     let ids_to_father_ids = Hashtbl.create 503 in
428     let ids_to_inner_sorts = Hashtbl.create 503 in
429     let ids_to_inner_types = Hashtbl.create 503 in
430     let ids_to_hypotheses = Hashtbl.create 23 in
431     let hypotheses_seed = ref 0 in
432     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
433     let unsh_sequent =
434      let i,canonical_context,term = sequent in
435       let canonical_context' =
436        List.fold_right
437         (fun d canonical_context' ->
438           let d =
439            match d with
440               None -> None
441             | Some (n, Cic.Decl t)->
442                Some (n, Cic.Decl (Unshare.unshare t))
443             | Some (n, Cic.Def (t,None)) ->
444                Some (n, Cic.Def ((Unshare.unshare t),None))
445             | Some (n,Cic.Def (bo,Some ty)) ->
446                Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
447           in
448            d::canonical_context'
449         ) canonical_context []
450       in
451       let term' = Unshare.unshare term in
452        (i,canonical_context',term')
453     in
454     let (metano,acontext,agoal) = 
455       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
456       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
457       metasenv unsh_sequent in
458     (unsh_sequent,
459      (("i0",metano,acontext,agoal), 
460       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
461 ;;
462
463 let acic_object_of_cic_object ?(eta_fix=true) obj =
464  let module C = Cic in
465  let module E = Eta_fixing in
466   let ids_to_terms = Hashtbl.create 503 in
467   let ids_to_father_ids = Hashtbl.create 503 in
468   let ids_to_inner_sorts = Hashtbl.create 503 in
469   let ids_to_inner_types = Hashtbl.create 503 in
470   let ids_to_conjectures = Hashtbl.create 11 in
471   let ids_to_hypotheses = Hashtbl.create 127 in
472   let hypotheses_seed = ref 0 in
473   let conjectures_seed = ref 0 in
474   let seed = ref 0 in
475   let acic_term_of_cic_term_context' =
476    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
477     ids_to_inner_types in
478   let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
479   let aconjecture_of_conjecture' = aconjecture_of_conjecture seed 
480     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types 
481     ids_to_hypotheses hypotheses_seed in 
482    let eta_fix metasenv context t =
483     let t = if eta_fix then E.eta_fix metasenv context t else t in
484      Unshare.unshare t in
485    let aobj =
486     match obj with
487       C.Constant (id,Some bo,ty,params,attrs) ->
488        let bo' = eta_fix [] [] bo in
489        let ty' = eta_fix [] [] ty in
490        let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
491        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
492         C.AConstant
493          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
494     | C.Constant (id,None,ty,params,attrs) ->
495        let ty' = eta_fix [] [] ty in
496        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
497         C.AConstant
498          ("mettereaposto",None,id,None,aty,params,attrs)
499     | C.Variable (id,bo,ty,params,attrs) ->
500        let ty' = eta_fix [] [] ty in
501        let abo =
502         match bo with
503            None -> None
504          | Some bo ->
505             let bo' = eta_fix [] [] bo in
506              Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
507        in
508        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
509         C.AVariable
510          ("mettereaposto",id,abo,aty,params,attrs)
511     | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
512        let conjectures' =
513         List.map
514          (function (i,canonical_context,term) ->
515            let canonical_context' =
516             List.fold_right
517              (fun d canonical_context' ->
518                let d =
519                 match d with
520                    None -> None
521                  | Some (n, C.Decl t)->
522                     Some (n, C.Decl (eta_fix conjectures canonical_context' t))
523                  | Some (n, C.Def (t,None)) ->
524                     Some (n,
525                      C.Def ((eta_fix conjectures canonical_context' t),None))
526                  | Some (_,C.Def (_,Some _)) -> assert false
527                in
528                 d::canonical_context'
529              ) canonical_context []
530            in
531            let term' = eta_fix conjectures canonical_context' term in
532             (i,canonical_context',term')
533          ) conjectures
534        in
535        let aconjectures = 
536         List.map
537          (function (i,canonical_context,term) as conjecture ->
538            let cid = "c" ^ string_of_int !conjectures_seed in
539             xxx_add ids_to_conjectures cid conjecture ;
540             incr conjectures_seed ;
541            let (i,acanonical_context,aterm) 
542              = aconjecture_of_conjecture' conjectures conjecture in
543            (cid,i,acanonical_context,aterm))
544           conjectures' in 
545 (*        let time1 = Sys.time () in *)
546        let bo' = eta_fix conjectures' [] bo in
547        let ty' = eta_fix conjectures' [] ty in
548 (*
549        let time2 = Sys.time () in
550        prerr_endline
551         ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
552        hashtbl_add_time := 0.0 ;
553        type_of_aux'_add_time := 0.0 ;
554        DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
555 *)
556        let abo =
557         acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in
558        let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in
559 (*
560        let time3 = Sys.time () in
561        prerr_endline
562         ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
563        prerr_endline
564         ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
565        prerr_endline
566         ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ;
567        prerr_endline
568         ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
569        prerr_endline
570         ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
571        prerr_endline
572         ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
573 *)
574         C.ACurrentProof
575          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
576     | C.InductiveDefinition (tys,params,paramsno,attrs) ->
577        let tys =
578         List.map
579          (fun (name,i,arity,cl) ->
580            (name,i,Unshare.unshare arity,
581              List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
582        let context =
583         List.map
584          (fun (name,_,arity,_) ->
585            Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
586        let idrefs = List.map (function _ -> gen_id seed) tys in
587        let atys =
588         List.map2
589          (fun id (name,inductive,ty,cons) ->
590            let acons =
591             List.map
592              (function (name,ty) ->
593                (name,
594                  acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None)
595              ) cons
596            in
597             (id,name,inductive,
598              acic_term_of_cic_term' ~computeinnertypes:false ty None,acons)
599          ) (List.rev idrefs) tys
600        in
601         C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
602    in
603     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
604      ids_to_conjectures,ids_to_hypotheses
605 ;;
606
607 let plain_acic_term_of_cic_term =
608  let module C = Cic in
609  let mk_fresh_id =
610   let id = ref 0 in
611    function () -> incr id; "i" ^ string_of_int !id in
612  let rec aux context t =
613   let fresh_id = mk_fresh_id () in
614   match t with
615      C.Rel n ->
616       let idref,id =
617        match get_nth context n with
618           idref,(Some (C.Name s,_)) -> idref,s
619         | idref,_ -> idref,"__" ^ string_of_int n
620       in
621        C.ARel (fresh_id, idref, n, id)
622    | C.Var (uri,exp_named_subst) ->
623       let exp_named_subst' =
624        List.map
625         (function i,t -> i, (aux context t)) exp_named_subst
626       in
627        C.AVar (fresh_id,uri,exp_named_subst')
628    | C.Implicit _
629    | C.Meta _ -> assert false
630    | C.Sort s -> C.ASort (fresh_id, s)
631    | C.Cast (v,t) ->
632       C.ACast (fresh_id, aux context v, aux context t)
633    | C.Prod (n,s,t) ->
634         C.AProd
635          (fresh_id, n, aux context s,
636           aux ((fresh_id, Some (n, C.Decl s))::context) t)
637    | C.Lambda (n,s,t) ->
638        C.ALambda
639         (fresh_id,n, aux context s,
640          aux ((fresh_id, Some (n, C.Decl s))::context) t)
641    | C.LetIn (n,s,t) ->
642       C.ALetIn
643        (fresh_id, n, aux context s,
644         aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
645    | C.Appl l ->
646       C.AAppl (fresh_id, List.map (aux context) l)
647    | C.Const (uri,exp_named_subst) ->
648       let exp_named_subst' =
649        List.map
650         (function i,t -> i, (aux context t)) exp_named_subst
651       in
652        C.AConst (fresh_id, uri, exp_named_subst')
653    | C.MutInd (uri,tyno,exp_named_subst) ->
654       let exp_named_subst' =
655        List.map
656         (function i,t -> i, (aux context t)) exp_named_subst
657       in
658        C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
659    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
660       let exp_named_subst' =
661        List.map
662         (function i,t -> i, (aux context t)) exp_named_subst
663       in
664        C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
665    | C.MutCase (uri, tyno, outty, term, patterns) ->
666       C.AMutCase (fresh_id, uri, tyno, aux context outty,
667        aux context term, List.map (aux context) patterns)
668    | C.Fix (funno, funs) ->
669       let tys =
670        List.map
671         (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
672       in
673        C.AFix (fresh_id, funno,
674         List.map2
675          (fun (id,_) (name, indidx, ty, bo) ->
676            (id, name, indidx, aux context ty, aux (tys@context) bo)
677          ) tys funs
678       )
679    | C.CoFix (funno, funs) ->
680       let tys =
681        List.map (fun (name,ty,_) ->
682         mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
683       in
684        C.ACoFix (fresh_id, funno,
685         List.map2
686          (fun (id,_) (name, ty, bo) ->
687            (id, name, aux context ty, aux (tys@context) bo)
688          ) tys funs
689        )
690  in
691   aux
692 ;;
693
694 let plain_acic_object_of_cic_object obj =
695  let module C = Cic in
696  let mk_fresh_id =
697   let id = ref 0 in
698    function () -> incr id; "it" ^ string_of_int !id
699  in
700   match obj with
701     C.Constant (id,Some bo,ty,params,attrs) ->
702      let abo = plain_acic_term_of_cic_term [] bo in
703      let aty = plain_acic_term_of_cic_term [] ty in
704       C.AConstant
705        ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
706   | C.Constant (id,None,ty,params,attrs) ->
707      let aty = plain_acic_term_of_cic_term [] ty in
708       C.AConstant
709        ("mettereaposto",None,id,None,aty,params,attrs)
710   | C.Variable (id,bo,ty,params,attrs) ->
711      let abo =
712       match bo with
713          None -> None
714        | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
715      in
716      let aty = plain_acic_term_of_cic_term [] ty in
717       C.AVariable
718        ("mettereaposto",id,abo,aty,params,attrs)
719   | C.CurrentProof _ -> assert false
720   | C.InductiveDefinition (tys,params,paramsno,attrs) ->
721      let context =
722       List.map
723        (fun (name,_,arity,_) ->
724          mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
725      let atys =
726       List.map2
727        (fun (id,_) (name,inductive,ty,cons) ->
728          let acons =
729           List.map
730            (function (name,ty) ->
731              (name,
732                plain_acic_term_of_cic_term context ty)
733            ) cons
734          in
735           (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
736        ) context tys
737      in
738       C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
739 ;;