components/cic_acic/cic2acic.ml

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