helm/ocaml/cic_omdoc/cic2content.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 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             16/62003                                   *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35 (* e se mettessi la conversione di BY nell'apply_context ? *)
  36 (* sarebbe carino avere l'invariante che la proof2pres
  37 generasse sempre prove con contesto vuoto *)
  38
  39 let gen_id seed =
  40  let res = "p" ^ string_of_int !seed in
  41   incr seed ;
  42   res
  43 ;;
  44
  45 let name_of = function
  46     Cic.Anonymous -> None
  47   | Cic.Name b -> Some b;;
  48
  49 exception Not_a_proof;;
  50 exception NotImplemented;;
  51 exception NotApplicable;;
  52
  53 (* we do not care for positivity, here, that in any case is enforced by
  54    well typing. Just a brutal search *)
  55
  56 let rec occur uri =
  57   let module C = Cic in
  58   function
  59       C.Rel _ -> false
  60     | C.Var _ -> false
  61     | C.Meta _ -> false
  62     | C.Sort _ -> false
  63     | C.Implicit -> raise NotImplemented
  64     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
  65     | C.Cast (te,ty) -> (occur uri te)
  66     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
  67     | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
  68     | C.Appl l ->
  69         List.fold_left
  70           (fun b a ->
  71              if b then b
  72              else (occur uri a)) false l
  73     | C.Const (_,_) -> false
  74     | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
  75     | C.MutConstruct (_,_,_,_) -> false
  76     | C.MutCase _ -> false (* presuming too much?? *)
  77     | C.Fix _ -> false (* presuming too much?? *)
  78     | C.CoFix (_,_) -> false (* presuming too much?? *)
  79 ;;
  80
  81 let get_id =
  82   let module C = Cic in
  83   function
  84       C.ARel (id,_,_,_) -> id
  85     | C.AVar (id,_,_) -> id
  86     | C.AMeta (id,_,_) -> id
  87     | C.ASort (id,_) -> id
  88     | C.AImplicit _ -> raise NotImplemented
  89     | C.AProd (id,_,_,_) -> id
  90     | C.ACast (id,_,_) -> id
  91     | C.ALambda (id,_,_,_) -> id
  92     | C.ALetIn (id,_,_,_) -> id
  93     | C.AAppl (id,_) -> id
  94     | C.AConst (id,_,_) -> id
  95     | C.AMutInd (id,_,_,_) -> id
  96     | C.AMutConstruct (id,_,_,_,_) -> id
  97     | C.AMutCase (id,_,_,_,_,_) -> id
  98     | C.AFix (id,_,_) -> id
  99     | C.ACoFix (id,_,_) -> id
 100 ;;
 101
 102 let test_for_lifting ~ids_to_inner_types =
 103   let module C = Cic in
 104   let module C2A = Cic2acic in
 105   (* atomic terms are never lifted, according to my policy *)
 106   function
 107       C.ARel (id,_,_,_) -> false
 108     | C.AVar (id,_,_) -> false
 109     | C.AMeta (id,_,_) -> false
 110     | C.ASort (id,_) -> false
 111     | C.AImplicit _ -> raise NotImplemented
 112     | C.AProd (id,_,_,_) -> false
 113     | C.ACast (id,_,_) ->
 114          (try
 115             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 116             true;
 117           with notfound -> false)
 118     | C.ALambda (id,_,_,_) ->
 119          (try
 120             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 121             true;
 122           with notfound -> false)
 123     | C.ALetIn (id,_,_,_) ->
 124          (try
 125             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 126             true;
 127           with notfound -> false)
 128     | C.AAppl (id,_) ->
 129          (try
 130             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 131             true;
 132           with notfound -> false)
 133     | C.AConst (id,_,_) ->
 134          (try
 135             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 136             true;
 137           with notfound -> false)
 138     | C.AMutInd (id,_,_,_) -> false
 139     | C.AMutConstruct (id,_,_,_,_) ->
 140        (try
 141             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 142             true;
 143           with notfound -> false)
 144         (* oppure: false *)
 145     | C.AMutCase (id,_,_,_,_,_) ->
 146          (try
 147             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 148             true;
 149           with notfound -> false)
 150     | C.AFix (id,_,_) ->
 151           (try
 152             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 153             true;
 154           with notfound -> false)
 155     | C.ACoFix (id,_,_) ->
 156          (try
 157             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
 158             true;
 159           with notfound -> false)
 160 ;;
 161
 162 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
 163   let module C = Cic in
 164   let module K = Content in
 165   let rec aux l subrpoofs =
 166     match l with
 167       [] -> []
 168     | t::l1 ->
 169         if (test_for_lifting t ~ids_to_inner_types) then
 170           (match subproofs with
 171              [] -> assert false
 172            | p::tl ->
 173               let new_arg =
 174                 K.Premise
 175                   { K.premise_id = gen_id seed;
 176                     K.premise_xref = p.K.proof_id;
 177                     K.premise_binder = p.K.proof_name;
 178                     K.premise_n = None
 179                   }
 180                 in new_arg::(aux l1 tl))
 181         else
 182           let hd =
 183             (match t with
 184                C.ARel (idr,idref,n,b) ->
 185                  let sort =
 186                    (try Hashtbl.find ids_to_inner_sorts idr
 187                     with notfound -> "Type") in
 188                  if sort ="Prop" then
 189                     K.Premise
 190                       { K.premise_id = gen_id seed;
 191                         K.premise_xref = idr;
 192                         K.premise_binder = Some b;
 193                         K.premise_n = Some n
 194                       }
 195                  else (K.Term t)
 196              | _ -> (K.Term t)) in
 197           hd::(aux l1 subproofs)
 198   in aux l subproofs
 199 ;;
 200
 201 (* transform a proof p into a proof list, concatenating the last
 202 conclude element to the apply_context list, in case context is
 203 empty. Otherwise, it just returns [p] *)
 204
 205 let flat seed p =
 206  let module K = Content in
 207   if (p.K.proof_context = []) then
 208     if p.K.proof_apply_context = [] then [p]
 209     else
 210       let p1 =
 211         { p with
 212           K.proof_id = gen_id seed;
 213           K.proof_context = [];
 214           K.proof_apply_context = []
 215         } in
 216       p.K.proof_apply_context@[p1]
 217   else
 218     [p]
 219 ;;
 220
 221 let rec serialize seed =
 222   function
 223       [] -> []
 224     | p::tl -> (flat seed p)@(serialize seed tl);;
 225
 226 (* top_down = true if the term is a LAMBDA or a decl *)
 227 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
 228  let module C2A = Cic2acic in
 229  let module K = Content in
 230  let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
 231             with Not_found -> None)
 232  in
 233  match exp with
 234      None -> inner_proof
 235    | Some expty ->
 236        if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
 237          { K.proof_name = None ;
 238             K.proof_id   = gen_id seed;
 239             K.proof_context = [] ;
 240             K.proof_apply_context = [];
 241             K.proof_conclude =
 242               { K.conclude_id = gen_id seed;
 243                 K.conclude_aref = id;
 244                 K.conclude_method = "TD_Conversion";
 245                 K.conclude_args = [K.ArgProof inner_proof];
 246                 K.conclude_conclusion = Some expty
 247               };
 248           }
 249         else
 250           { K.proof_name = None ;
 251             K.proof_id   = gen_id seed;
 252             K.proof_context = [] ;
 253             K.proof_apply_context = [inner_proof];
 254             K.proof_conclude =
 255               { K.conclude_id = gen_id seed;
 256                 K.conclude_aref = id;
 257                 K.conclude_method = "BU_Conversion";
 258                 K.conclude_args =
 259                  [K.Premise
 260                   { K.premise_id = gen_id seed;
 261                     K.premise_xref = inner_proof.K.proof_id;
 262                     K.premise_binder = None;
 263                     K.premise_n = None
 264                   }
 265                  ];
 266                 K.conclude_conclusion = Some expty
 267               };
 268           }
 269 ;;
 270
 271 let generate_exact seed t id name ~ids_to_inner_types =
 272   let module C2A = Cic2acic in
 273   let module K = Content in
 274     { K.proof_name = name;
 275       K.proof_id   = id ;
 276       K.proof_context = [] ;
 277       K.proof_apply_context = [];
 278       K.proof_conclude =
 279         { K.conclude_id = gen_id seed;
 280           K.conclude_aref = id;
 281           K.conclude_method = "Exact";
 282           K.conclude_args = [K.Term t];
 283           K.conclude_conclusion =
 284               try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 285               with notfound -> None
 286         };
 287     }
 288 ;;
 289
 290 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
 291   let module C2A = Cic2acic in
 292   let module C = Cic in
 293   let module K = Content in
 294     { K.proof_name = name;
 295       K.proof_id   = id ;
 296       K.proof_context = [] ;
 297       K.proof_apply_context = [];
 298       K.proof_conclude =
 299         { K.conclude_id = gen_id seed;
 300           K.conclude_aref = id;
 301           K.conclude_method = "Intros+LetTac";
 302           K.conclude_args = [K.ArgProof inner_proof];
 303           K.conclude_conclusion =
 304             try Some
 305              (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 306             with notfound ->
 307               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
 308                  None -> None
 309               | Some t ->
 310                   if is_intro then Some (C.AProd ("gen"^id,n,s,t))
 311                   else Some (C.ALetIn ("gen"^id,n,s,t)))
 312         };
 313     }
 314 ;;
 315
 316 let build_decl_item seed id n s ~ids_to_inner_sorts =
 317  let module K = Content in
 318   let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
 319   if sort = "Prop" then
 320      `Hypothesis
 321        { K.dec_name = name_of n;
 322          K.dec_id = gen_id seed;
 323          K.dec_inductive = false;
 324          K.dec_aref = id;
 325          K.dec_type = s
 326        }
 327   else
 328      `Declaration
 329        { K.dec_name = name_of n;
 330          K.dec_id = gen_id seed;
 331          K.dec_inductive = false;
 332          K.dec_aref = id;
 333          K.dec_type = s
 334        }
 335 ;;
 336
 337 let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
 338  let module K = Content in
 339   let sort = Hashtbl.find ids_to_inner_sorts id in
 340   if sort = "Prop" then
 341      `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
 342   else
 343      `Definition
 344        { K.def_name = name_of n;
 345          K.def_id = gen_id seed;
 346          K.def_aref = id;
 347          K.def_term = t
 348        }
 349
 350 (* the following function must be called with an object of sort
 351 Prop. For debugging purposes this is tested again, possibly raising an
 352 Not_a_proof exception *)
 353
 354 and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
 355   let rec aux ?(name = None) t =
 356   let module C = Cic in
 357   let module K = Content in
 358   let module C2A = Cic2acic in
 359   let t1 =
 360     match t with
 361       C.ARel (id,idref,n,b) as t ->
 362         let sort = Hashtbl.find ids_to_inner_sorts id in
 363         if sort = "Prop" then
 364           generate_exact seed t id name ~ids_to_inner_types
 365         else raise Not_a_proof
 366     | C.AVar (id,uri,exp_named_subst) as t ->
 367         let sort = Hashtbl.find ids_to_inner_sorts id in
 368         if sort = "Prop" then
 369           generate_exact seed t id name ~ids_to_inner_types
 370         else raise Not_a_proof
 371     | C.AMeta (id,n,l) as t ->
 372         let sort = Hashtbl.find ids_to_inner_sorts id in
 373         if sort = "Prop" then
 374           generate_exact seed t id name ~ids_to_inner_types
 375         else raise Not_a_proof
 376     | C.ASort (id,s) -> raise Not_a_proof
 377     | C.AImplicit _ -> raise NotImplemented
 378     | C.AProd (_,_,_,_) -> raise Not_a_proof
 379     | C.ACast (id,v,t) -> aux v
 380     | C.ALambda (id,n,s,t) ->
 381         let sort = Hashtbl.find ids_to_inner_sorts id in
 382         if sort = "Prop" then
 383           let proof = aux t ~name:None in
 384           let proof' =
 385             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
 386                match proof.K.proof_conclude.K.conclude_args with
 387                  [K.ArgProof p] -> p
 388                | _ -> assert false
 389             else proof in
 390           let proof'' =
 391             { proof' with
 392               K.proof_name = None;
 393               K.proof_context =
 394                 (build_decl_item seed id n s ids_to_inner_sorts)::
 395                   proof'.K.proof_context
 396             }
 397           in
 398           generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
 399         else raise Not_a_proof
 400     | C.ALetIn (id,n,s,t) ->
 401         let sort = Hashtbl.find ids_to_inner_sorts id in
 402         if sort = "Prop" then
 403           let proof = aux t in
 404           let proof' =
 405             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
 406                match proof.K.proof_conclude.K.conclude_args with
 407                  [K.ArgProof p] -> p
 408                | _ -> assert false
 409             else proof in
 410           let proof'' =
 411             { proof' with
 412                K.proof_name = name;
 413                K.proof_context =
 414                  ((build_def_item seed id n s ids_to_inner_sorts
 415                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
 416                  ::proof'.K.proof_context;
 417             }
 418           in
 419           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
 420         else raise Not_a_proof
 421     | C.AAppl (id,li) ->
 422         (try rewrite
 423            seed name id li ids_to_inner_types ids_to_inner_sorts
 424          with NotApplicable ->
 425          try inductive
 426           seed name id li ids_to_inner_types ids_to_inner_sorts
 427          with NotApplicable ->
 428           let args_to_lift =
 429             List.filter (test_for_lifting ~ids_to_inner_types) li in
 430           let subproofs =
 431             match args_to_lift with
 432                 [_] -> List.map aux args_to_lift
 433             | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
 434           let args = build_args seed li subproofs
 435                  ~ids_to_inner_types ~ids_to_inner_sorts in
 436             { K.proof_name = name;
 437               K.proof_id   = gen_id seed;
 438               K.proof_context = [];
 439               K.proof_apply_context = serialize seed subproofs;
 440               K.proof_conclude =
 441                 { K.conclude_id = gen_id seed;
 442                   K.conclude_aref = id;
 443                   K.conclude_method = "Apply";
 444                   K.conclude_args = args;
 445                   K.conclude_conclusion =
 446                      try Some
 447                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 448                      with notfound -> None
 449                  };
 450             })
 451     | C.AConst (id,uri,exp_named_subst) as t ->
 452         let sort = Hashtbl.find ids_to_inner_sorts id in
 453         if sort = "Prop" then
 454           generate_exact seed t id name ~ids_to_inner_types
 455         else raise Not_a_proof
 456     | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
 457     | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
 458         let sort = Hashtbl.find ids_to_inner_sorts id in
 459         if sort = "Prop" then
 460           generate_exact seed t id name ~ids_to_inner_types
 461         else raise Not_a_proof
 462     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 463         let teid = get_id te in
 464         let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
 465         (match
 466           (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
 467            with notfound -> None)
 468          with
 469              Some tety -> (* we must lift up the argument *)
 470                let p = (aux te) in
 471                { K.proof_name = Some "name";
 472                  K.proof_id   = gen_id seed;
 473                  K.proof_context = [];
 474                  K.proof_apply_context = flat seed p;
 475                  K.proof_conclude =
 476                    { K.conclude_id = gen_id seed;
 477                      K.conclude_aref = id;
 478                      K.conclude_method = "Case";
 479                      K.conclude_args = (K.Term ty)::(K.Term te)::pp;
 480                      K.conclude_conclusion =
 481                        try Some
 482                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 483                        with notfound -> None
 484                    }
 485                }
 486            | None ->
 487                { K.proof_name = name;
 488                  K.proof_id   = gen_id seed;
 489                  K.proof_context = [];
 490                  K.proof_apply_context = [];
 491                  K.proof_conclude =
 492                    { K.conclude_id = gen_id seed;
 493                      K.conclude_aref = id;
 494                      K.conclude_method = "Case";
 495                      K.conclude_args = (K.Term ty)::(K.Term te)::pp;
 496                      K.conclude_conclusion =
 497                        try Some
 498                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 499                        with notfound -> None
 500                    }
 501                }
 502          )
 503     | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
 504         let proof = (aux bo) in (* must be recursive !! *)
 505           { K.proof_name = name;
 506             K.proof_id   = gen_id seed;
 507             K.proof_context = [`Proof proof];
 508             K.proof_apply_context = [];
 509             K.proof_conclude =
 510               { K.conclude_id = gen_id seed;
 511                 K.conclude_aref = id;
 512                 K.conclude_method = "Exact";
 513                 K.conclude_args =
 514                 [ K.Premise
 515                   { K.premise_id = gen_id seed;
 516                     K.premise_xref = proof.K.proof_id;
 517                     K.premise_binder = proof.K.proof_name;
 518                     K.premise_n = Some 1;
 519                   }
 520                 ];
 521                 K.conclude_conclusion =
 522                    try Some
 523                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 524                    with notfound -> None
 525               }
 526         }
 527     | C.AFix (id, no, funs) ->
 528         let proofs =
 529           List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
 530         let jo =
 531           { K.joint_id = gen_id seed;
 532             K.joint_kind = `Recursive;
 533             K.joint_defs = proofs
 534           }
 535         in
 536           { K.proof_name = name;
 537             K.proof_id   = gen_id seed;
 538             K.proof_context = [`Joint jo];
 539             K.proof_apply_context = [];
 540             K.proof_conclude =
 541               { K.conclude_id = gen_id seed;
 542                 K.conclude_aref = id;
 543                 K.conclude_method = "Exact";
 544                 K.conclude_args =
 545                 [ K.Premise
 546                   { K.premise_id = gen_id seed;
 547                     K.premise_xref = jo.K.joint_id;
 548                     K.premise_binder = Some "tiralo fuori";
 549                     K.premise_n = Some no;
 550                   }
 551                 ];
 552                 K.conclude_conclusion =
 553                    try Some
 554                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 555                    with notfound -> None
 556               }
 557         }
 558     | C.ACoFix (id,no,[(id1,n,ty,bo)]) ->
 559         let proof = (aux bo) in (* must be recursive !! *)
 560           { K.proof_name = name;
 561             K.proof_id   = gen_id seed;
 562             K.proof_context = [`Proof proof];
 563             K.proof_apply_context = [];
 564             K.proof_conclude =
 565               { K.conclude_id = gen_id seed;
 566                 K.conclude_aref = id;
 567                 K.conclude_method = "Exact";
 568                 K.conclude_args =
 569                 [ K.Premise
 570                   { K.premise_id = gen_id seed;
 571                     K.premise_xref = proof.K.proof_id;
 572                     K.premise_binder = proof.K.proof_name;
 573                     K.premise_n = Some 1;
 574                   }
 575                 ];
 576                 K.conclude_conclusion =
 577                    try Some
 578                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 579                    with notfound -> None
 580               }
 581         }
 582     | C.ACoFix (id,no,funs) ->
 583         let proofs =
 584           List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
 585         let jo =
 586           { K.joint_id = gen_id seed;
 587             K.joint_kind = `Recursive;
 588             K.joint_defs = proofs
 589           }
 590         in
 591           { K.proof_name = name;
 592             K.proof_id   = gen_id seed;
 593             K.proof_context = [`Joint jo];
 594             K.proof_apply_context = [];
 595             K.proof_conclude =
 596               { K.conclude_id = gen_id seed;
 597                 K.conclude_aref = id;
 598                 K.conclude_method = "Exact";
 599                 K.conclude_args =
 600                 [ K.Premise
 601                   { K.premise_id = gen_id seed;
 602                     K.premise_xref = jo.K.joint_id;
 603                     K.premise_binder = Some "tiralo fuori";
 604                     K.premise_n = Some no;
 605                   }
 606                 ];
 607                 K.conclude_conclusion =
 608                   try Some
 609                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 610                   with notfound -> None
 611               };
 612         }
 613      in
 614      let id = get_id t in
 615      generate_conversion seed false id t1 ~ids_to_inner_types
 616 in aux ~name:name t
 617
 618 and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
 619   let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
 620   let module C2A = Cic2acic in
 621   let module K = Content in
 622   let module C = Cic in
 623   match li with
 624     C.AConst (idc,uri,exp_named_subst)::args ->
 625       let uri_str = UriManager.string_of_uri uri in
 626       let suffix = Str.regexp_string "_ind.con" in
 627       let len = String.length uri_str in
 628       let n = (try (Str.search_backward suffix uri_str len)
 629                with Not_found -> -1) in
 630       if n<0 then raise NotApplicable
 631       else
 632         let prefix = String.sub uri_str 0 n in
 633         let ind_str = (prefix ^ ".ind") in
 634         let ind_uri = UriManager.uri_of_string ind_str in
 635         let inductive_types,noparams =
 636            (match CicEnvironment.get_obj ind_uri with
 637                Cic.Constant _ -> assert false
 638              | Cic.Variable _ -> assert false
 639              | Cic.CurrentProof _ -> assert false
 640              | Cic.InductiveDefinition (l,_,n) -> (l,n)
 641            ) in
 642         let rec split n l =
 643           if n = 0 then ([],l) else
 644           let p,a = split (n-1) (List.tl l) in
 645           ((List.hd l::p),a) in
 646         let params_and_IP,tail_args = split (noparams+1) args in
 647         let constructors =
 648             (match inductive_types with
 649               [(_,_,_,l)] -> l
 650             | _ -> raise NotApplicable) (* don't care for mutual ind *) in
 651         let constructors1 =
 652           let rec clean_up n t =
 653              if n = 0 then t else
 654              (match t with
 655                 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
 656               | _ -> assert false) in
 657           List.map (clean_up noparams) constructors in
 658         let no_constructors= List.length constructors in
 659         let args_for_cases, other_args =
 660           split no_constructors tail_args in
 661         let args_to_lift =
 662           List.filter (test_for_lifting ~ids_to_inner_types) other_args in
 663         let subproofs =
 664           match args_to_lift with
 665             [_] -> List.map aux args_to_lift
 666           | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
 667         prerr_endline "****** end subproofs *******"; flush stderr;
 668         let other_method_args =
 669           build_args seed other_args subproofs
 670              ~ids_to_inner_types ~ids_to_inner_sorts in
 671 (*
 672         let rparams,inductive_arg =
 673           let rec aux =
 674             function
 675               [] -> assert false
 676             | [ia] -> [],ia
 677             | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
 678           aux other_method_args in
 679 *)
 680         prerr_endline "****** end other *******"; flush stderr;
 681         let method_args=
 682           let rec build_method_args =
 683             function
 684                 [],_-> [] (* extra args are ignored ???? *)
 685               | (name,ty)::tlc,arg::tla ->
 686                   let idarg = get_id arg in
 687                   let sortarg =
 688                     (try (Hashtbl.find ids_to_inner_sorts idarg)
 689                      with Not_found -> "Type") in
 690                   let hdarg =
 691                     if sortarg = "Prop" then
 692                       let (co,bo) =
 693                         let rec bc =
 694                           function
 695                             Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
 696                               let ce =
 697                                 build_decl_item
 698                                   seed idl n s1 ~ids_to_inner_sorts in
 699                               if (occur ind_uri s) then
 700                                 (  prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
 701                                    match t1 with
 702                                    Cic.ALambda(id2,n2,s2,t2) ->
 703                                      let inductive_hyp =
 704                                        `Hypothesis
 705                                          { K.dec_name = name_of n2;
 706                                            K.dec_id = gen_id seed;
 707                                            K.dec_inductive = true;
 708                                            K.dec_aref = id2;
 709                                            K.dec_type = s2
 710                                          } in
 711                                      let (context,body) = bc (t,t2) in
 712                                      (ce::inductive_hyp::context,body)
 713                                  | _ -> assert false)
 714                               else
 715                                 (  prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
 716                                 let (context,body) = bc (t,t1) in
 717                                 (ce::context,body))
 718                             | _ , t -> ([],aux t ~name:None) in
 719                         bc (ty,arg) in
 720                       K.ArgProof
 721                        { bo with
 722                          K.proof_name = Some name;
 723                          K.proof_context = co;
 724                        };
 725                     else (K.Term arg) in
 726                   hdarg::(build_method_args (tlc,tla))
 727               | _ -> assert false in
 728           build_method_args (constructors1,args_for_cases) in
 729           { K.proof_name = None;
 730             K.proof_id   = gen_id seed;
 731             K.proof_context = [];
 732             K.proof_apply_context = subproofs;
 733             K.proof_conclude =
 734               { K.conclude_id = gen_id seed;
 735                 K.conclude_aref = id;
 736                 K.conclude_method = "ByInduction";
 737                 K.conclude_args =
 738                   K.Aux no_constructors
 739                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
 740                   ::method_args@other_method_args;
 741                 K.conclude_conclusion =
 742                    try Some
 743                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 744                    with notfound -> None
 745               }
 746           }
 747   | _ -> raise NotApplicable
 748
 749 and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
 750   let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
 751   let module C2A = Cic2acic in
 752   let module K = Content in
 753   let module C = Cic in
 754   match li with
 755     C.AConst (sid,uri,exp_named_subst)::args ->
 756       let uri_str = UriManager.string_of_uri uri in
 757       if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
 758          uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
 759         let subproof = aux (List.nth args 3) in
 760         let method_args =
 761           let rec ma_aux n = function
 762               [] -> []
 763             | a::tl ->
 764                 let hd =
 765                   if n = 0 then
 766                     K.Premise
 767                      { K.premise_id = gen_id seed;
 768                        K.premise_xref = subproof.K.proof_id;
 769                        K.premise_binder = None;
 770                        K.premise_n = None
 771                      }
 772                   else
 773                     let aid = get_id a in
 774                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
 775                       with Not_found -> "Type") in
 776                     if asort = "Prop" then
 777                       K.ArgProof (aux a)
 778                     else K.Term a in
 779                 hd::(ma_aux (n-1) tl) in
 780           (ma_aux 3 args) in
 781           { K.proof_name = None;
 782             K.proof_id   = gen_id seed;
 783             K.proof_context = [];
 784             K.proof_apply_context = [subproof];
 785             K.proof_conclude =
 786               { K.conclude_id = gen_id seed;
 787                 K.conclude_aref = id;
 788                 K.conclude_method = "Rewrite";
 789                 K.conclude_args =
 790                   K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
 791                 K.conclude_conclusion =
 792                    try Some
 793                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 794                    with notfound -> None
 795               }
 796           }
 797       else raise NotApplicable
 798   | _ -> raise NotApplicable
 799 ;;
 800
 801 let map_conjectures
 802  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
 803 =
 804  let context' =
 805   List.map
 806    (function
 807        (id,None) as item -> item
 808      | (id,Some (name,Cic.ADecl t)) ->
 809          id,
 810           Some
 811            (build_decl_item seed (get_id t) name t
 812             ~ids_to_inner_sorts)
 813      | (id,Some (name,Cic.ADef t)) ->
 814          id,
 815           Some
 816            (build_def_item seed (get_id t) name t
 817             ~ids_to_inner_sorts ~ids_to_inner_types)
 818    ) context
 819  in
 820   (id,n,context',ty)
 821 ;;
 822
 823 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
 824   let module C = Cic in
 825   let module K = Content in
 826   let module C2A = Cic2acic in
 827   let seed = ref 0 in
 828   function
 829       C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
 830         (gen_id seed, params,
 831           Some
 832            (List.map
 833              (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
 834              conjectures),
 835           `Def (K.Const,ty,
 836             build_def_item seed (get_id bo) (C.Name n) bo
 837              ~ids_to_inner_sorts ~ids_to_inner_types))
 838     | C.AConstant (_,_,n,Some bo,ty,params) ->
 839          (gen_id seed, params, None,
 840            `Def (K.Const,ty,
 841              build_def_item seed (get_id bo) (C.Name n) bo
 842                ~ids_to_inner_sorts ~ids_to_inner_types))
 843     | C.AConstant (id,_,n,None,ty,params) ->
 844          (gen_id seed, params, None,
 845            `Decl (K.Const,
 846              build_decl_item seed id (C.Name n) ty
 847                ~ids_to_inner_sorts))
 848     | C.AVariable (_,n,Some bo,ty,params) ->
 849          (gen_id seed, params, None,
 850            `Def (K.Var,ty,
 851              build_def_item seed (get_id bo) (C.Name n) bo
 852                ~ids_to_inner_sorts ~ids_to_inner_types))
 853     | C.AVariable (id,n,None,ty,params) ->
 854          (gen_id seed, params, None,
 855            `Decl (K.Var,
 856              build_decl_item seed id (C.Name n) ty
 857               ~ids_to_inner_sorts))
 858     | C.AInductiveDefinition (id,l,params,nparams) ->
 859          (gen_id seed, params, None,
 860             `Joint
 861               { K.joint_id = gen_id seed;
 862                 K.joint_kind = `Inductive nparams;
 863                 K.joint_defs = List.map (build_inductive seed) l
 864               })
 865
 866 and
 867     build_inductive seed =
 868      let module K = Content in
 869       fun (_,n,b,ty,l) ->
 870         `Inductive
 871           { K.inductive_id = gen_id seed;
 872             K.inductive_kind = b;
 873             K.inductive_type = ty;
 874             K.inductive_constructors = build_constructors seed l
 875            }
 876
 877 and
 878     build_constructors seed l =
 879      let module K = Content in
 880       List.map
 881        (fun (n,t) ->
 882            { K.dec_name = Some n;
 883              K.dec_id = gen_id seed;
 884              K.dec_inductive = false;
 885              K.dec_aref = "";
 886              K.dec_type = t
 887            }) l
 888 ;;
 889
 890 (*
 891 and 'term cinductiveType =
 892  id * string * bool * 'term *                (* typename, inductive, arity *)
 893    'term cconstructor list                   (*  constructors        *)
 894
 895 and 'term cconstructor =
 896  string * 'term
 897 *)
 898
 899