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