helm/software/components/cic_acic/cic2acic.ml

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