helm/ocaml/cic_omdoc/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 let hashtbl_add_time = ref 0.0;;
  27
  28 let xxx_add h k v =
  29  let t1 = Sys.time () in
  30   Hashtbl.add h k v ;
  31   let t2 = Sys.time () in
  32    hashtbl_add_time := !hashtbl_add_time +. t2 -. t1
  33 ;;
  34
  35 let number_new_type_of_aux' = ref 0;;
  36 let type_of_aux'_add_time = ref 0.0;;
  37
  38 let xxx_type_of_aux' m c t =
  39  let t1 = Sys.time () in
  40  let res = CicTypeChecker.type_of_aux' m c t in
  41  let t2 = Sys.time () in
  42  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
  43  res
  44 ;;
  45
  46 type anntypes =
  47  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
  48 ;;
  49
  50 let gen_id seed =
  51  let res = "i" ^ string_of_int !seed in
  52   incr seed ;
  53   res
  54 ;;
  55
  56 let fresh_id seed ids_to_terms ids_to_father_ids =
  57  fun father t ->
  58   let res = gen_id seed in
  59    xxx_add ids_to_father_ids res father ;
  60    xxx_add ids_to_terms res t ;
  61    res
  62 ;;
  63
  64 let source_id_of_id id = "#source#" ^ id;;
  65
  66 exception NotEnoughElements;;
  67 exception NameExpected;;
  68
  69 (*CSC: cut&paste da cicPp.ml *)
  70 (* get_nth l n   returns the nth element of the list l if it exists or *)
  71 (* raises NotEnoughElements if l has less than n elements             *)
  72 let rec get_nth l n =
  73  match (n,l) with
  74     (1, he::_) -> he
  75   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
  76   | (_,_) -> raise NotEnoughElements
  77 ;;
  78
  79 let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
  80      ids_to_inner_types metasenv context idrefs t expectedty
  81 =
  82  let module D = DoubleTypeInference in
  83  let module C = Cic in
  84   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
  85    let time1 = Sys.time () in
  86    let terms_to_types =
  87      let time0 = Sys.time () in
  88      let prova = CicTypeChecker.type_of_aux' metasenv context t in
  89      let time1 = Sys.time () in
  90      prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
  91      let res = D.double_type_of metasenv context t expectedty in
  92      let time2 = Sys.time () in
  93    prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
  94      res
  95    in
  96    let time2 = Sys.time () in
  97    prerr_endline
  98     ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
  99     let rec aux computeinnertypes father context idrefs tt =
 100      let fresh_id'' = fresh_id' father tt in
 101      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
 102      let aux' = aux computeinnertypes (Some fresh_id'') in
 103       (* First of all we compute the inner type and the inner sort *)
 104       (* of the term. They may be useful in what follows.          *)
 105       (*CSC: This is a very inefficient way of computing inner types *)
 106       (*CSC: and inner sorts: very deep terms have their types/sorts *)
 107       (*CSC: computed again and again.                               *)
 108       let string_of_sort t =
 109        match CicReduction.whd context t with
 110           C.Sort C.Prop  -> "Prop"
 111         | C.Sort C.Set   -> "Set"
 112         | C.Sort C.Type  -> "Type"
 113         | C.Sort C.CProp -> "CProp"
 114         | _              -> assert false
 115       in
 116        let ainnertypes,innertype,innersort,expected_available =
 117 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
 118 (*CSC: (expected type + inferred type). Just for now we use the usual *)
 119 (*CSC: type-inference, but the result is very poor. As a very weak    *)
 120 (*CSC: patch, I apply whd to the computed type. Full beta             *)
 121 (*CSC: reduction would be a much better option.                       *)
 122 (*CSC: solo per testare i tempi *)
 123 (*XXXXXXX *)
 124         try
 125 (* *)
 126         let {D.synthesized = synthesized; D.expected = expected} =
 127          if computeinnertypes then
 128           D.CicHash.find terms_to_types tt
 129          else
 130           (* We are already in an inner-type and Coscoy's double *)
 131           (* type inference algorithm has not been applied.      *)
 132           {D.synthesized =
 133 (***CSC: patch per provare i tempi
 134             CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
 135 Cic.Sort Cic.Type ;
 136           D.expected = None}
 137         in
 138          incr number_new_type_of_aux' ;
 139          let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
 140           let ainnertypes,expected_available =
 141            if computeinnertypes then
 142             let annexpected,expected_available =
 143                match expected with
 144                   None -> None,false
 145                 | Some expectedty' ->
 146                    Some
 147                     (aux false (Some fresh_id'') context idrefs expectedty'),
 148                     true
 149             in
 150              Some
 151               {annsynthesized =
 152                 aux false (Some fresh_id'') context idrefs synthesized ;
 153                annexpected = annexpected
 154               }, expected_available
 155            else
 156             None,false
 157           in
 158            ainnertypes,synthesized, string_of_sort innersort, expected_available
 159 (*XXXXXXXX *)
 160         with
 161          Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
 162           (* CSC: Type or Set? I can not tell *)
 163           None,Cic.Sort Cic.Type,"Type",false
 164 (* *)
 165        in
 166         let add_inner_type id =
 167          match ainnertypes with
 168             None -> ()
 169           | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
 170         in
 171          match tt with
 172             C.Rel n ->
 173              let id =
 174               match get_nth context n with
 175                  (Some (C.Name s,_)) -> s
 176                | _ -> raise NameExpected
 177              in
 178               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 179               if innersort = "Prop"  && expected_available then
 180                add_inner_type fresh_id'' ;
 181               C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
 182           | C.Var (uri,exp_named_subst) ->
 183              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 184              if innersort = "Prop"  && expected_available then
 185               add_inner_type fresh_id'' ;
 186              let exp_named_subst' =
 187               List.map
 188                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
 189              in
 190               C.AVar (fresh_id'', uri,exp_named_subst')
 191           | C.Meta (n,l) ->
 192              let (_,canonical_context,_) =
 193               List.find (function (m,_,_) -> n = m) metasenv
 194              in
 195              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 196              if innersort = "Prop"  && expected_available then
 197               add_inner_type fresh_id'' ;
 198              C.AMeta (fresh_id'', n,
 199               (List.map2
 200                 (fun ct t ->
 201                   match (ct, t) with
 202                   | None, _ -> None
 203                   | _, Some t -> Some (aux' context idrefs t)
 204                   | Some _, None -> assert false (* due to typing rules *))
 205                 canonical_context l))
 206           | C.Sort s -> C.ASort (fresh_id'', s)
 207           | C.Implicit -> C.AImplicit (fresh_id'')
 208           | C.Cast (v,t) ->
 209              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 210              if innersort = "Prop" then
 211               add_inner_type fresh_id'' ;
 212              C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
 213           | C.Prod (n,s,t) ->
 214               xxx_add ids_to_inner_sorts fresh_id''
 215                (string_of_sort innertype) ;
 216                     let sourcetype = xxx_type_of_aux' metasenv context s in
 217                      xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
 218                       (string_of_sort sourcetype) ;
 219               let n' =
 220                match n with
 221                   C.Anonymous -> n
 222                 | C.Name n' ->
 223                    if DoubleTypeInference.does_not_occur 1 t then
 224                     C.Anonymous
 225                    else
 226                     C.Name n'
 227               in
 228                C.AProd
 229                 (fresh_id'', n', aux' context idrefs s,
 230                  aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
 231           | C.Lambda (n,s,t) ->
 232              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 233                    let sourcetype = xxx_type_of_aux' metasenv context s in
 234                     xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
 235                      (string_of_sort sourcetype) ;
 236               if innersort = "Prop" then
 237                begin
 238                 let father_is_lambda =
 239                  match father with
 240                     None -> false
 241                   | Some father' ->
 242                      match Hashtbl.find ids_to_terms father' with
 243                         C.Lambda _ -> true
 244                       | _ -> false
 245                 in
 246                  if (not father_is_lambda) || expected_available then
 247                   add_inner_type fresh_id''
 248                end ;
 249               C.ALambda
 250                (fresh_id'',n, aux' context idrefs s,
 251                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
 252           | C.LetIn (n,s,t) ->
 253              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 254              if innersort = "Prop" then
 255               add_inner_type fresh_id'' ;
 256              C.ALetIn
 257               (fresh_id'', n, aux' context idrefs s,
 258                aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
 259           | C.Appl l ->
 260              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 261              if innersort = "Prop" then
 262               add_inner_type fresh_id'' ;
 263              C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
 264           | C.Const (uri,exp_named_subst) ->
 265              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 266              if innersort = "Prop"  && expected_available then
 267               add_inner_type fresh_id'' ;
 268              let exp_named_subst' =
 269               List.map
 270                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
 271              in
 272               C.AConst (fresh_id'', uri, exp_named_subst')
 273           | C.MutInd (uri,tyno,exp_named_subst) ->
 274              let exp_named_subst' =
 275               List.map
 276                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
 277              in
 278               C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
 279           | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 280              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 281              if innersort = "Prop"  && expected_available then
 282               add_inner_type fresh_id'' ;
 283              let exp_named_subst' =
 284               List.map
 285                (function i,t -> i, (aux' context idrefs t)) exp_named_subst
 286              in
 287               C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
 288           | C.MutCase (uri, tyno, outty, term, patterns) ->
 289              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 290              if innersort = "Prop" then
 291               add_inner_type fresh_id'' ;
 292              C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
 293               aux' context idrefs term, List.map (aux' context idrefs) patterns)
 294           | C.Fix (funno, funs) ->
 295              let fresh_idrefs =
 296               List.map (function _ -> gen_id seed) funs in
 297              let new_idrefs = List.rev fresh_idrefs @ idrefs in
 298              let tys =
 299               List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
 300              in
 301               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 302               if innersort = "Prop" then
 303                add_inner_type fresh_id'' ;
 304               C.AFix (fresh_id'', funno,
 305                List.map2
 306                 (fun id (name, indidx, ty, bo) ->
 307                   (id, name, indidx, aux' context idrefs ty,
 308                     aux' (tys@context) new_idrefs bo)
 309                 ) fresh_idrefs funs
 310              )
 311           | C.CoFix (funno, funs) ->
 312              let fresh_idrefs =
 313               List.map (function _ -> gen_id seed) funs in
 314              let new_idrefs = List.rev fresh_idrefs @ idrefs in
 315              let tys =
 316               List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
 317              in
 318               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 319               if innersort = "Prop" then
 320                add_inner_type fresh_id'' ;
 321               C.ACoFix (fresh_id'', funno,
 322                List.map2
 323                 (fun id (name, ty, bo) ->
 324                   (id, name, aux' context idrefs ty,
 325                     aux' (tys@context) new_idrefs bo)
 326                 ) fresh_idrefs funs
 327               )
 328         in
 329          let timea = Sys.time () in
 330          let res = aux true None context idrefs t in
 331          let timeb = Sys.time () in
 332           prerr_endline
 333            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
 334           res
 335 ;;
 336
 337 let acic_of_cic_context metasenv context idrefs t =
 338  let ids_to_terms = Hashtbl.create 503 in
 339  let ids_to_father_ids = Hashtbl.create 503 in
 340  let ids_to_inner_sorts = Hashtbl.create 503 in
 341  let ids_to_inner_types = Hashtbl.create 503 in
 342  let seed = ref 0 in
 343    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 344     ids_to_inner_types metasenv context idrefs t,
 345    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 346 ;;
 347
 348 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
 349   ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
 350   metasenv (metano,context,goal) =
 351   let acic_of_cic_context =
 352     acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 353       ids_to_inner_types  metasenv in
 354   let _, acontext,final_idrefs =
 355     (List.fold_right
 356       (fun binding (context, acontext,idrefs) ->
 357          let hid = "h" ^ string_of_int !hypotheses_seed in
 358            Hashtbl.add ids_to_hypotheses hid binding ;
 359            incr hypotheses_seed ;
 360            match binding with
 361                Some (n,Cic.Def (t,None)) ->
 362                  let acic = acic_of_cic_context context idrefs t None in
 363                  (binding::context),
 364                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
 365              | Some (n,Cic.Decl t) ->
 366                  let acic = acic_of_cic_context context idrefs t None in
 367                  (binding::context),
 368                    ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
 369              | None ->
 370                  (* Invariant: "" is never looked up *)
 371                   (None::context),((hid,None)::acontext),""::idrefs
 372              | Some (_,Cic.Def (_,Some _)) -> assert false
 373          ) context ([],[],[])
 374        )
 375   in
 376   let agoal = acic_of_cic_context context final_idrefs goal None in
 377   (metano,acontext,agoal)
 378 ;;
 379
 380 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
 381     let ids_to_terms = Hashtbl.create 503 in
 382     let ids_to_father_ids = Hashtbl.create 503 in
 383     let ids_to_inner_sorts = Hashtbl.create 503 in
 384     let ids_to_inner_types = Hashtbl.create 503 in
 385     let ids_to_hypotheses = Hashtbl.create 23 in
 386     let hypotheses_seed = ref 0 in
 387     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
 388     let (metano,acontext,agoal) =
 389       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
 390       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
 391       metasenv sequent in
 392     ("i0",metano,acontext,agoal),
 393      ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
 394 ;;
 395
 396 let acic_object_of_cic_object obj =
 397  let module C = Cic in
 398  let module E = Eta_fixing in
 399   let ids_to_terms = Hashtbl.create 503 in
 400   let ids_to_father_ids = Hashtbl.create 503 in
 401   let ids_to_inner_sorts = Hashtbl.create 503 in
 402   let ids_to_inner_types = Hashtbl.create 503 in
 403   let ids_to_conjectures = Hashtbl.create 11 in
 404   let ids_to_hypotheses = Hashtbl.create 127 in
 405   let hypotheses_seed = ref 0 in
 406   let conjectures_seed = ref 0 in
 407   let seed = ref 0 in
 408   let acic_term_of_cic_term_context' =
 409    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 410     ids_to_inner_types in
 411   let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
 412   let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
 413     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
 414     ids_to_hypotheses hypotheses_seed in
 415    let aobj =
 416     match obj with
 417       C.Constant (id,Some bo,ty,params) ->
 418        let bo' = E.eta_fix [] bo in
 419        let ty' = E.eta_fix [] ty in
 420        let abo = acic_term_of_cic_term' bo' (Some ty') in
 421        let aty = acic_term_of_cic_term' ty' None in
 422         C.AConstant
 423          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
 424     | C.Constant (id,None,ty,params) ->
 425        let ty' = E.eta_fix [] ty in
 426        let aty = acic_term_of_cic_term' ty' None in
 427         C.AConstant
 428          ("mettereaposto",None,id,None,aty,params)
 429     | C.Variable (id,bo,ty,params) ->
 430        let ty' = E.eta_fix [] ty in
 431        let abo =
 432         match bo with
 433            None -> None
 434          | Some bo ->
 435             let bo' = E.eta_fix [] bo in
 436              Some (acic_term_of_cic_term' bo' (Some ty'))
 437        in
 438        let aty = acic_term_of_cic_term' ty' None in
 439         C.AVariable
 440          ("mettereaposto",id,abo,aty, params)
 441     | C.CurrentProof (id,conjectures,bo,ty,params) ->
 442        let conjectures' =
 443         List.map
 444          (function (i,canonical_context,term) ->
 445            let canonical_context' =
 446             List.map
 447              (function
 448                  None -> None
 449                | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
 450                | Some (n, C.Def (t,None)) ->
 451                   Some (n, C.Def ((E.eta_fix conjectures t),None))
 452                | Some (_,C.Def (_,Some _)) -> assert false
 453              ) canonical_context
 454            in
 455            let term' = E.eta_fix conjectures term in
 456             (i,canonical_context',term')
 457          ) conjectures
 458        in
 459        let aconjectures =
 460         List.map
 461          (function (i,canonical_context,term) as conjecture ->
 462            let cid = "c" ^ string_of_int !conjectures_seed in
 463             xxx_add ids_to_conjectures cid conjecture ;
 464             incr conjectures_seed ;
 465            let (i,acanonical_context,aterm)
 466              = aconjecture_of_conjecture' conjectures conjecture in
 467            (cid,i,acanonical_context,aterm))
 468           conjectures' in
 469 (*           let idrefs',revacanonical_context =
 470              let rec aux context idrefs =
 471               function
 472                  [] -> idrefs,[]
 473                | hyp::tl ->
 474                   let hid = "h" ^ string_of_int !hypotheses_seed in
 475                   let new_idrefs = hid::idrefs in
 476                    xxx_add ids_to_hypotheses hid hyp ;
 477                    incr hypotheses_seed ;
 478                    match hyp with
 479                       (Some (n,C.Decl t)) ->
 480                         let final_idrefs,atl =
 481                          aux (hyp::context) new_idrefs tl in
 482                         let at =
 483                          acic_term_of_cic_term_context'
 484                           conjectures context idrefs t None
 485                         in
 486                          final_idrefs,(hid,Some (n,C.ADecl at))::atl
 487                     | (Some (n,C.Def (t,_))) ->
 488                         let final_idrefs,atl =
 489                          aux (hyp::context) new_idrefs tl in
 490                         let at =
 491                          acic_term_of_cic_term_context'
 492                           conjectures context idrefs t None
 493                         in
 494                          final_idrefs,(hid,Some (n,C.ADef at))::atl
 495                     | None ->
 496                        let final_idrefs,atl =
 497                         aux (hyp::context) new_idrefs tl
 498                        in
 499                         final_idrefs,(hid,None)::atl
 500              in
 501               aux [] [] (List.rev canonical_context)
 502             in
 503              let aterm =
 504               acic_term_of_cic_term_context' conjectures
 505                canonical_context idrefs' term None
 506              in
 507               (cid,i,(List.rev revacanonical_context),aterm)
 508          ) conjectures' in *)
 509        let time1 = Sys.time () in
 510        let bo' = E.eta_fix conjectures' bo in
 511        let ty' = E.eta_fix conjectures' ty in
 512        let time2 = Sys.time () in
 513        prerr_endline
 514         ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
 515        hashtbl_add_time := 0.0 ;
 516        type_of_aux'_add_time := 0.0 ;
 517        DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
 518        let abo =
 519         acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
 520        let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
 521        let time3 = Sys.time () in
 522        prerr_endline
 523         ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
 524        prerr_endline
 525         ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
 526        prerr_endline
 527         ("++++++++++++ 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) ;
 528        prerr_endline
 529         ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
 530        prerr_endline
 531         ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
 532        prerr_endline
 533         ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
 534         C.ACurrentProof
 535          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
 536     | C.InductiveDefinition (tys,params,paramsno) ->
 537        let context =
 538         List.map
 539          (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
 540        let idrefs = List.map (function _ -> gen_id seed) tys in
 541        let atys =
 542         List.map2
 543          (fun id (name,inductive,ty,cons) ->
 544            let acons =
 545             List.map
 546              (function (name,ty) ->
 547                (name,
 548                  acic_term_of_cic_term_context' [] context idrefs ty None)
 549              ) cons
 550            in
 551             (id,name,inductive,acic_term_of_cic_term' ty None,acons)
 552          ) (List.rev idrefs) tys
 553        in
 554         C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
 555    in
 556     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
 557      ids_to_conjectures,ids_to_hypotheses
 558 ;;
 559
 560