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