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