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 ())