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