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