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 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      D.CicHash.empty ()
 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           D.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                  (binding::context),
 404                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
 405              | Some (n,Cic.Decl t) ->
 406                  let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
 407                  (binding::context),
 408                    ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
 409              | None ->
 410                  (* Invariant: "" is never looked up *)
 411                   (None::context),((hid,None)::acontext),""::idrefs
 412          ) context ([],[],[])
 413        )
 414   in
 415   let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in
 416   (metano,acontext,agoal)
 417 ;;
 418
 419 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
 420     let ids_to_terms = Hashtbl.create 503 in
 421     let ids_to_father_ids = Hashtbl.create 503 in
 422     let ids_to_inner_sorts = Hashtbl.create 503 in
 423     let ids_to_inner_types = Hashtbl.create 503 in
 424     let ids_to_hypotheses = Hashtbl.create 23 in
 425     let hypotheses_seed = ref 0 in
 426     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
 427     let unsh_sequent =
 428      let i,canonical_context,term = sequent in
 429       let canonical_context' =
 430        List.fold_right
 431         (fun d canonical_context' ->
 432           let d =
 433            match d with
 434               None -> None
 435             | Some (n, Cic.Decl t)->
 436                Some (n, Cic.Decl (Unshare.unshare t))
 437             | Some (n, Cic.Def (t,None)) ->
 438                Some (n, Cic.Def ((Unshare.unshare t),None))
 439             | Some (n,Cic.Def (bo,Some ty)) ->
 440                Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
 441           in
 442            d::canonical_context'
 443         ) canonical_context []
 444       in
 445       let term' = Unshare.unshare term in
 446        (i,canonical_context',term')
 447     in
 448     let (metano,acontext,agoal) =
 449       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
 450       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
 451       metasenv unsh_sequent in
 452     (unsh_sequent,
 453      (("i0",metano,acontext,agoal),
 454       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 455 ;;
 456
 457 let acic_object_of_cic_object ?(eta_fix=true) obj =
 458  let module C = Cic in
 459  let module E = Eta_fixing in
 460   let ids_to_terms = Hashtbl.create 503 in
 461   let ids_to_father_ids = Hashtbl.create 503 in
 462   let ids_to_inner_sorts = Hashtbl.create 503 in
 463   let ids_to_inner_types = Hashtbl.create 503 in
 464   let ids_to_conjectures = Hashtbl.create 11 in
 465   let ids_to_hypotheses = Hashtbl.create 127 in
 466   let hypotheses_seed = ref 0 in
 467   let conjectures_seed = ref 0 in
 468   let seed = ref 0 in
 469   let acic_term_of_cic_term_context' =
 470    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 471     ids_to_inner_types in
 472   let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
 473   let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
 474     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
 475     ids_to_hypotheses hypotheses_seed in
 476    let eta_fix metasenv context t =
 477     let t = if eta_fix then E.eta_fix metasenv context t else t in
 478      Unshare.unshare t in
 479    let aobj =
 480     match obj with
 481       C.Constant (id,Some bo,ty,params,attrs) ->
 482        let bo' = eta_fix [] [] bo in
 483        let ty' = eta_fix [] [] ty in
 484        let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
 485        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
 486         C.AConstant
 487          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
 488     | C.Constant (id,None,ty,params,attrs) ->
 489        let ty' = eta_fix [] [] ty in
 490        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
 491         C.AConstant
 492          ("mettereaposto",None,id,None,aty,params,attrs)
 493     | C.Variable (id,bo,ty,params,attrs) ->
 494        let ty' = eta_fix [] [] ty in
 495        let abo =
 496         match bo with
 497            None -> None
 498          | Some bo ->
 499             let bo' = eta_fix [] [] bo in
 500              Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
 501        in
 502        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
 503         C.AVariable
 504          ("mettereaposto",id,abo,aty,params,attrs)
 505     | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
 506        let conjectures' =
 507         List.map
 508          (function (i,canonical_context,term) ->
 509            let canonical_context' =
 510             List.fold_right
 511              (fun d canonical_context' ->
 512                let d =
 513                 match d with
 514                    None -> None
 515                  | Some (n, C.Decl t)->
 516                     Some (n, C.Decl (eta_fix conjectures canonical_context' t))
 517                  | Some (n, C.Def (t,None)) ->
 518                     Some (n,
 519                      C.Def ((eta_fix conjectures canonical_context' t),None))
 520                  | Some (_,C.Def (_,Some _)) -> assert false
 521                in
 522                 d::canonical_context'
 523              ) canonical_context []
 524            in
 525            let term' = eta_fix conjectures canonical_context' term in
 526             (i,canonical_context',term')
 527          ) conjectures
 528        in
 529        let aconjectures =
 530         List.map
 531          (function (i,canonical_context,term) as conjecture ->
 532            let cid = "c" ^ string_of_int !conjectures_seed in
 533             xxx_add ids_to_conjectures cid conjecture ;
 534             incr conjectures_seed ;
 535            let (i,acanonical_context,aterm)
 536              = aconjecture_of_conjecture' conjectures conjecture in
 537            (cid,i,acanonical_context,aterm))
 538           conjectures' in
 539 (*        let time1 = Sys.time () in *)
 540        let bo' = eta_fix conjectures' [] bo in
 541        let ty' = eta_fix conjectures' [] ty in
 542 (*
 543        let time2 = Sys.time () in
 544        prerr_endline
 545         ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
 546        hashtbl_add_time := 0.0 ;
 547        type_of_aux'_add_time := 0.0 ;
 548        DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
 549 *)
 550        let abo =
 551         acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in
 552        let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in
 553 (*
 554        let time3 = Sys.time () in
 555        prerr_endline
 556         ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
 557        prerr_endline
 558         ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
 559        prerr_endline
 560         ("++++++++++++ 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) ;
 561        prerr_endline
 562         ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
 563        prerr_endline
 564         ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
 565        prerr_endline
 566         ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
 567 *)
 568         C.ACurrentProof
 569          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
 570     | C.InductiveDefinition (tys,params,paramsno,attrs) ->
 571        let tys =
 572         List.map
 573          (fun (name,i,arity,cl) ->
 574            (name,i,Unshare.unshare arity,
 575              List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
 576        let context =
 577         List.map
 578          (fun (name,_,arity,_) ->
 579            Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
 580        let idrefs = List.map (function _ -> gen_id seed) tys in
 581        let atys =
 582         List.map2
 583          (fun id (name,inductive,ty,cons) ->
 584            let acons =
 585             List.map
 586              (function (name,ty) ->
 587                (name,
 588                  acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None)
 589              ) cons
 590            in
 591             (id,name,inductive,
 592              acic_term_of_cic_term' ~computeinnertypes:false ty None,acons)
 593          ) (List.rev idrefs) tys
 594        in
 595         C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
 596    in
 597     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
 598      ids_to_conjectures,ids_to_hypotheses
 599 ;;
 600
 601 let plain_acic_term_of_cic_term =
 602  let module C = Cic in
 603  let mk_fresh_id =
 604   let id = ref 0 in
 605    function () -> incr id; "i" ^ string_of_int !id in
 606  let rec aux context t =
 607   let fresh_id = mk_fresh_id () in
 608   match t with
 609      C.Rel n ->
 610       let idref,id =
 611        match get_nth context n with
 612           idref,(Some (C.Name s,_)) -> idref,s
 613         | idref,_ -> idref,"__" ^ string_of_int n
 614       in
 615        C.ARel (fresh_id, idref, n, id)
 616    | C.Var (uri,exp_named_subst) ->
 617       let exp_named_subst' =
 618        List.map
 619         (function i,t -> i, (aux context t)) exp_named_subst
 620       in
 621        C.AVar (fresh_id,uri,exp_named_subst')
 622    | C.Implicit _
 623    | C.Meta _ -> assert false
 624    | C.Sort s -> C.ASort (fresh_id, s)
 625    | C.Cast (v,t) ->
 626       C.ACast (fresh_id, aux context v, aux context t)
 627    | C.Prod (n,s,t) ->
 628         C.AProd
 629          (fresh_id, n, aux context s,
 630           aux ((fresh_id, Some (n, C.Decl s))::context) t)
 631    | C.Lambda (n,s,t) ->
 632        C.ALambda
 633         (fresh_id,n, aux context s,
 634          aux ((fresh_id, Some (n, C.Decl s))::context) t)
 635    | C.LetIn (n,s,t) ->
 636       C.ALetIn
 637        (fresh_id, n, aux context s,
 638         aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
 639    | C.Appl l ->
 640       C.AAppl (fresh_id, List.map (aux context) l)
 641    | C.Const (uri,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.AConst (fresh_id, uri, exp_named_subst')
 647    | C.MutInd (uri,tyno,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.AMutInd (fresh_id, uri, tyno, exp_named_subst')
 653    | C.MutConstruct (uri,tyno,consno,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.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
 659    | C.MutCase (uri, tyno, outty, term, patterns) ->
 660       C.AMutCase (fresh_id, uri, tyno, aux context outty,
 661        aux context term, List.map (aux context) patterns)
 662    | C.Fix (funno, funs) ->
 663       let tys =
 664        List.map
 665         (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
 666       in
 667        C.AFix (fresh_id, funno,
 668         List.map2
 669          (fun (id,_) (name, indidx, ty, bo) ->
 670            (id, name, indidx, aux context ty, aux (tys@context) bo)
 671          ) tys funs
 672       )
 673    | C.CoFix (funno, funs) ->
 674       let tys =
 675        List.map (fun (name,ty,_) ->
 676         mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
 677       in
 678        C.ACoFix (fresh_id, funno,
 679         List.map2
 680          (fun (id,_) (name, ty, bo) ->
 681            (id, name, aux context ty, aux (tys@context) bo)
 682          ) tys funs
 683        )
 684  in
 685   aux
 686 ;;
 687
 688 let plain_acic_object_of_cic_object obj =
 689  let module C = Cic in
 690  let mk_fresh_id =
 691   let id = ref 0 in
 692    function () -> incr id; "it" ^ string_of_int !id
 693  in
 694   match obj with
 695     C.Constant (id,Some bo,ty,params,attrs) ->
 696      let abo = plain_acic_term_of_cic_term [] bo in
 697      let aty = plain_acic_term_of_cic_term [] ty in
 698       C.AConstant
 699        ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
 700   | C.Constant (id,None,ty,params,attrs) ->
 701      let aty = plain_acic_term_of_cic_term [] ty in
 702       C.AConstant
 703        ("mettereaposto",None,id,None,aty,params,attrs)
 704   | C.Variable (id,bo,ty,params,attrs) ->
 705      let abo =
 706       match bo with
 707          None -> None
 708        | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
 709      in
 710      let aty = plain_acic_term_of_cic_term [] ty in
 711       C.AVariable
 712        ("mettereaposto",id,abo,aty,params,attrs)
 713   | C.CurrentProof _ -> assert false
 714   | C.InductiveDefinition (tys,params,paramsno,attrs) ->
 715      let context =
 716       List.map
 717        (fun (name,_,arity,_) ->
 718          mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
 719      let atys =
 720       List.map2
 721        (fun (id,_) (name,inductive,ty,cons) ->
 722          let acons =
 723           List.map
 724            (function (name,ty) ->
 725              (name,
 726                plain_acic_term_of_cic_term context ty)
 727            ) cons
 728          in
 729           (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
 730        ) context tys
 731      in
 732       C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
 733 ;;