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