helm/ocaml/cic_transformations/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 X = Xml in
 358   let module K = Content in
 359   let module U = UriManager in
 360   let module C2A = Cic2acic in
 361   let t1 =
 362     match t with
 363       C.ARel (id,idref,n,b) as t ->
 364         let sort = Hashtbl.find ids_to_inner_sorts id in
 365         if sort = "Prop" then
 366           generate_exact seed t id name ~ids_to_inner_types
 367         else raise Not_a_proof
 368     | C.AVar (id,uri,exp_named_subst) as t ->
 369         let sort = Hashtbl.find ids_to_inner_sorts id in
 370         if sort = "Prop" then
 371           generate_exact seed t id name ~ids_to_inner_types
 372         else raise Not_a_proof
 373     | C.AMeta (id,n,l) as t ->
 374         let sort = Hashtbl.find ids_to_inner_sorts id in
 375         if sort = "Prop" then
 376           generate_exact seed t id name ~ids_to_inner_types
 377         else raise Not_a_proof
 378     | C.ASort (id,s) -> raise Not_a_proof
 379     | C.AImplicit _ -> raise NotImplemented
 380     | C.AProd (_,_,_,_) -> raise Not_a_proof
 381     | C.ACast (id,v,t) -> aux v
 382     | C.ALambda (id,n,s,t) ->
 383         let sort = Hashtbl.find ids_to_inner_sorts id in
 384         if sort = "Prop" then
 385           let proof = aux t ~name:None in
 386           let proof' =
 387             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
 388                match proof.K.proof_conclude.K.conclude_args with
 389                  [K.ArgProof p] -> p
 390                | _ -> assert false
 391             else proof in
 392           let proof'' =
 393             { proof' with
 394               K.proof_name = None;
 395               K.proof_context =
 396                 (build_decl_item seed id n s ids_to_inner_sorts)::
 397                   proof'.K.proof_context
 398             }
 399           in
 400           generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
 401         else raise Not_a_proof
 402     | C.ALetIn (id,n,s,t) ->
 403         let sort = Hashtbl.find ids_to_inner_sorts id in
 404         if sort = "Prop" then
 405           let proof = aux t in
 406           let proof' =
 407             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
 408                match proof.K.proof_conclude.K.conclude_args with
 409                  [K.ArgProof p] -> p
 410                | _ -> assert false
 411             else proof in
 412           let proof'' =
 413             { proof' with
 414                K.proof_name = name;
 415                K.proof_context =
 416                  ((build_def_item seed id n s ids_to_inner_sorts
 417                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
 418                  ::proof'.K.proof_context;
 419             }
 420           in
 421           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
 422         else raise Not_a_proof
 423     | C.AAppl (id,li) ->
 424         (try rewrite
 425            seed name id li ids_to_inner_types ids_to_inner_sorts
 426          with NotApplicable ->
 427          try inductive
 428           seed name id li ids_to_inner_types ids_to_inner_sorts
 429          with NotApplicable ->
 430           let args_to_lift =
 431             List.filter (test_for_lifting ~ids_to_inner_types) li in
 432           let subproofs =
 433             match args_to_lift with
 434                 [_] -> List.map aux args_to_lift
 435             | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
 436           let args = build_args seed li subproofs
 437                  ~ids_to_inner_types ~ids_to_inner_sorts in
 438             { K.proof_name = name;
 439               K.proof_id   = gen_id seed;
 440               K.proof_context = [];
 441               K.proof_apply_context = serialize seed subproofs;
 442               K.proof_conclude =
 443                 { K.conclude_id = gen_id seed;
 444                   K.conclude_aref = id;
 445                   K.conclude_method = "Apply";
 446                   K.conclude_args = args;
 447                   K.conclude_conclusion =
 448                      try Some
 449                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 450                      with notfound -> None
 451                  };
 452             })
 453     | C.AConst (id,uri,exp_named_subst) as t ->
 454         let sort = Hashtbl.find ids_to_inner_sorts id in
 455         if sort = "Prop" then
 456           generate_exact seed t id name ~ids_to_inner_types
 457         else raise Not_a_proof
 458     | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
 459     | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
 460         let sort = Hashtbl.find ids_to_inner_sorts id in
 461         if sort = "Prop" then
 462           generate_exact seed t id name ~ids_to_inner_types
 463         else raise Not_a_proof
 464     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 465         let teid = get_id te in
 466         let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
 467         (match
 468           (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
 469            with notfound -> None)
 470          with
 471              Some tety -> (* we must lift up the argument *)
 472                let p = (aux te) in
 473                { K.proof_name = Some "name";
 474                  K.proof_id   = gen_id seed;
 475                  K.proof_context = [];
 476                  K.proof_apply_context = flat seed p;
 477                  K.proof_conclude =
 478                    { K.conclude_id = gen_id seed;
 479                      K.conclude_aref = id;
 480                      K.conclude_method = "Case";
 481                      K.conclude_args = (K.Term ty)::(K.Term te)::pp;
 482                      K.conclude_conclusion =
 483                        try Some
 484                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 485                        with notfound -> None
 486                    }
 487                }
 488            | None ->
 489                { K.proof_name = name;
 490                  K.proof_id   = gen_id seed;
 491                  K.proof_context = [];
 492                  K.proof_apply_context = [];
 493                  K.proof_conclude =
 494                    { K.conclude_id = gen_id seed;
 495                      K.conclude_aref = id;
 496                      K.conclude_method = "Case";
 497                      K.conclude_args = (K.Term ty)::(K.Term te)::pp;
 498                      K.conclude_conclusion =
 499                        try Some
 500                         (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 501                        with notfound -> None
 502                    }
 503                }
 504          )
 505     | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
 506         let proof = (aux bo) in (* must be recursive !! *)
 507           { K.proof_name = name;
 508             K.proof_id   = gen_id seed;
 509             K.proof_context = [`Proof proof];
 510             K.proof_apply_context = [];
 511             K.proof_conclude =
 512               { K.conclude_id = gen_id seed;
 513                 K.conclude_aref = id;
 514                 K.conclude_method = "Exact";
 515                 K.conclude_args =
 516                 [ K.Premise
 517                   { K.premise_id = gen_id seed;
 518                     K.premise_xref = proof.K.proof_id;
 519                     K.premise_binder = proof.K.proof_name;
 520                     K.premise_n = Some 1;
 521                   }
 522                 ];
 523                 K.conclude_conclusion =
 524                    try Some
 525                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 526                    with notfound -> None
 527               }
 528         }
 529     | C.AFix (id, no, funs) ->
 530         let proofs =
 531           List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
 532         let jo =
 533           { K.joint_id = gen_id seed;
 534             K.joint_kind = `Recursive;
 535             K.joint_defs = proofs
 536           }
 537         in
 538           { K.proof_name = name;
 539             K.proof_id   = gen_id seed;
 540             K.proof_context = [`Joint jo];
 541             K.proof_apply_context = [];
 542             K.proof_conclude =
 543               { K.conclude_id = gen_id seed;
 544                 K.conclude_aref = id;
 545                 K.conclude_method = "Exact";
 546                 K.conclude_args =
 547                 [ K.Premise
 548                   { K.premise_id = gen_id seed;
 549                     K.premise_xref = jo.K.joint_id;
 550                     K.premise_binder = Some "tiralo fuori";
 551                     K.premise_n = Some no;
 552                   }
 553                 ];
 554                 K.conclude_conclusion =
 555                    try Some
 556                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 557                    with notfound -> None
 558               }
 559         }
 560     | C.ACoFix (id,no,[(id1,n,ty,bo)]) ->
 561         let proof = (aux bo) in (* must be recursive !! *)
 562           { K.proof_name = name;
 563             K.proof_id   = gen_id seed;
 564             K.proof_context = [`Proof proof];
 565             K.proof_apply_context = [];
 566             K.proof_conclude =
 567               { K.conclude_id = gen_id seed;
 568                 K.conclude_aref = id;
 569                 K.conclude_method = "Exact";
 570                 K.conclude_args =
 571                 [ K.Premise
 572                   { K.premise_id = gen_id seed;
 573                     K.premise_xref = proof.K.proof_id;
 574                     K.premise_binder = proof.K.proof_name;
 575                     K.premise_n = Some 1;
 576                   }
 577                 ];
 578                 K.conclude_conclusion =
 579                    try Some
 580                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 581                    with notfound -> None
 582               }
 583         }
 584     | C.ACoFix (id,no,funs) ->
 585         let proofs =
 586           List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
 587         let jo =
 588           { K.joint_id = gen_id seed;
 589             K.joint_kind = `Recursive;
 590             K.joint_defs = proofs
 591           }
 592         in
 593           { K.proof_name = name;
 594             K.proof_id   = gen_id seed;
 595             K.proof_context = [`Joint jo];
 596             K.proof_apply_context = [];
 597             K.proof_conclude =
 598               { K.conclude_id = gen_id seed;
 599                 K.conclude_aref = id;
 600                 K.conclude_method = "Exact";
 601                 K.conclude_args =
 602                 [ K.Premise
 603                   { K.premise_id = gen_id seed;
 604                     K.premise_xref = jo.K.joint_id;
 605                     K.premise_binder = Some "tiralo fuori";
 606                     K.premise_n = Some no;
 607                   }
 608                 ];
 609                 K.conclude_conclusion =
 610                   try Some
 611                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 612                   with notfound -> None
 613               };
 614         }
 615      in
 616      let id = get_id t in
 617      generate_conversion seed false id t1 ~ids_to_inner_types
 618 in aux ~name:name t
 619
 620 and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
 621   let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
 622   let module C2A = Cic2acic in
 623   let module K = Content in
 624   let module C = Cic in
 625   match li with
 626     C.AConst (idc,uri,exp_named_subst)::args ->
 627       let uri_str = UriManager.string_of_uri uri in
 628       let suffix = Str.regexp_string "_ind.con" in
 629       let len = String.length uri_str in
 630       let n = (try (Str.search_backward suffix uri_str len)
 631                with Not_found -> -1) in
 632       if n<0 then raise NotApplicable
 633       else
 634         let prefix = String.sub uri_str 0 n in
 635         let ind_str = (prefix ^ ".ind") in
 636         let ind_uri = UriManager.uri_of_string ind_str in
 637         let inductive_types,noparams =
 638            (match CicEnvironment.get_obj ind_uri with
 639                Cic.Constant _ -> assert false
 640              | Cic.Variable _ -> assert false
 641              | Cic.CurrentProof _ -> assert false
 642              | Cic.InductiveDefinition (l,_,n) -> (l,n)
 643            ) in
 644         let rec split n l =
 645           if n = 0 then ([],l) else
 646           let p,a = split (n-1) (List.tl l) in
 647           ((List.hd l::p),a) in
 648         let params_and_IP,tail_args = split (noparams+1) args in
 649         let constructors =
 650             (match inductive_types with
 651               [(_,_,_,l)] -> l
 652             | _ -> raise NotApplicable) (* don't care for mutual ind *) in
 653         let constructors1 =
 654           let rec clean_up n t =
 655              if n = 0 then t else
 656              (match t with
 657                 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
 658               | _ -> assert false) in
 659           List.map (clean_up noparams) constructors in
 660         let no_constructors= List.length constructors in
 661         let args_for_cases, other_args =
 662           split no_constructors tail_args in
 663         let args_to_lift =
 664           List.filter (test_for_lifting ~ids_to_inner_types) other_args in
 665         let subproofs =
 666           match args_to_lift with
 667             [_] -> List.map aux args_to_lift
 668           | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
 669         prerr_endline "****** end subproofs *******"; flush stderr;
 670         let other_method_args =
 671           build_args seed other_args subproofs
 672              ~ids_to_inner_types ~ids_to_inner_sorts in
 673 (*
 674         let rparams,inductive_arg =
 675           let rec aux =
 676             function
 677               [] -> assert false
 678             | [ia] -> [],ia
 679             | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
 680           aux other_method_args in
 681 *)
 682         prerr_endline "****** end other *******"; flush stderr;
 683         let method_args=
 684           let rec build_method_args =
 685             function
 686                 [],_-> [] (* extra args are ignored ???? *)
 687               | (name,ty)::tlc,arg::tla ->
 688                   let idarg = get_id arg in
 689                   let sortarg =
 690                     (try (Hashtbl.find ids_to_inner_sorts idarg)
 691                      with Not_found -> "Type") in
 692                   let hdarg =
 693                     if sortarg = "Prop" then
 694                       let (co,bo) =
 695                         let rec bc =
 696                           function
 697                             Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
 698                               let ce =
 699                                 build_decl_item
 700                                   seed idl n s1 ~ids_to_inner_sorts in
 701                               if (occur ind_uri s) then
 702                                 (  prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
 703                                    match t1 with
 704                                    Cic.ALambda(id2,n2,s2,t2) ->
 705                                      let inductive_hyp =
 706                                        `Hypothesis
 707                                          { K.dec_name = name_of n2;
 708                                            K.dec_id = gen_id seed;
 709                                            K.dec_inductive = true;
 710                                            K.dec_aref = id2;
 711                                            K.dec_type = s2
 712                                          } in
 713                                      let (context,body) = bc (t,t2) in
 714                                      (ce::inductive_hyp::context,body)
 715                                  | _ -> assert false)
 716                               else
 717                                 (  prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
 718                                 let (context,body) = bc (t,t1) in
 719                                 (ce::context,body))
 720                             | _ , t -> ([],aux t ~name:None) in
 721                         bc (ty,arg) in
 722                       K.ArgProof
 723                        { bo with
 724                          K.proof_name = Some name;
 725                          K.proof_context = co;
 726                        };
 727                     else (K.Term arg) in
 728                   hdarg::(build_method_args (tlc,tla))
 729               | _ -> assert false in
 730           build_method_args (constructors1,args_for_cases) in
 731           { K.proof_name = None;
 732             K.proof_id   = gen_id seed;
 733             K.proof_context = [];
 734             K.proof_apply_context = subproofs;
 735             K.proof_conclude =
 736               { K.conclude_id = gen_id seed;
 737                 K.conclude_aref = id;
 738                 K.conclude_method = "ByInduction";
 739                 K.conclude_args =
 740                   K.Aux no_constructors
 741                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
 742                   ::method_args@other_method_args;
 743                 K.conclude_conclusion =
 744                    try Some
 745                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 746                    with notfound -> None
 747               }
 748           }
 749   | _ -> raise NotApplicable
 750
 751 and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
 752   let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
 753   let module C2A = Cic2acic in
 754   let module K = Content in
 755   let module C = Cic in
 756   match li with
 757     C.AConst (sid,uri,exp_named_subst)::args ->
 758       let uri_str = UriManager.string_of_uri uri in
 759       if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
 760          uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
 761         let subproof = aux (List.nth args 3) in
 762         let method_args =
 763           let rec ma_aux n = function
 764               [] -> []
 765             | a::tl ->
 766                 let hd =
 767                   if n = 0 then
 768                     K.Premise
 769                      { K.premise_id = gen_id seed;
 770                        K.premise_xref = subproof.K.proof_id;
 771                        K.premise_binder = None;
 772                        K.premise_n = None
 773                      }
 774                   else
 775                     let aid = get_id a in
 776                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
 777                       with Not_found -> "Type") in
 778                     if asort = "Prop" then
 779                       K.ArgProof (aux a)
 780                     else K.Term a in
 781                 hd::(ma_aux (n-1) tl) in
 782           (ma_aux 3 args) in
 783           { K.proof_name = None;
 784             K.proof_id   = gen_id seed;
 785             K.proof_context = [];
 786             K.proof_apply_context = [subproof];
 787             K.proof_conclude =
 788               { K.conclude_id = gen_id seed;
 789                 K.conclude_aref = id;
 790                 K.conclude_method = "Rewrite";
 791                 K.conclude_args =
 792                   K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
 793                 K.conclude_conclusion =
 794                    try Some
 795                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
 796                    with notfound -> None
 797               }
 798           }
 799       else raise NotApplicable
 800   | _ -> raise NotApplicable
 801 ;;
 802
 803 let map_conjectures
 804  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
 805 =
 806  let context' =
 807   List.map
 808    (function
 809        (id,None) as item -> item
 810      | (id,Some (name,Cic.ADecl t)) ->
 811          id,
 812           Some
 813            (build_decl_item seed (get_id t) name t
 814             ~ids_to_inner_sorts)
 815      | (id,Some (name,Cic.ADef t)) ->
 816          id,
 817           Some
 818            (build_def_item seed (get_id t) name t
 819             ~ids_to_inner_sorts ~ids_to_inner_types)
 820    ) context
 821  in
 822   (id,n,context',ty)
 823 ;;
 824
 825 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
 826   let module C = Cic in
 827   let module K = Content in
 828   let module C2A = Cic2acic in
 829   let seed = ref 0 in
 830   function
 831       C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
 832         (gen_id seed, params,
 833           Some
 834            (List.map
 835              (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
 836              conjectures),
 837           `Def (K.Const,ty,
 838             build_def_item seed (get_id bo) (C.Name n) bo
 839              ~ids_to_inner_sorts ~ids_to_inner_types))
 840     | C.AConstant (_,_,n,Some bo,ty,params) ->
 841          (gen_id seed, params, None,
 842            `Def (K.Const,ty,
 843              build_def_item seed (get_id bo) (C.Name n) bo
 844                ~ids_to_inner_sorts ~ids_to_inner_types))
 845     | C.AConstant (id,_,n,None,ty,params) ->
 846          (gen_id seed, params, None,
 847            `Decl (K.Const,
 848              build_decl_item seed id (C.Name n) ty
 849                ~ids_to_inner_sorts))
 850     | C.AVariable (_,n,Some bo,ty,params) ->
 851          (gen_id seed, params, None,
 852            `Def (K.Var,ty,
 853              build_def_item seed (get_id bo) (C.Name n) bo
 854                ~ids_to_inner_sorts ~ids_to_inner_types))
 855     | C.AVariable (id,n,None,ty,params) ->
 856          (gen_id seed, params, None,
 857            `Decl (K.Var,
 858              build_decl_item seed id (C.Name n) ty
 859               ~ids_to_inner_sorts))
 860     | C.AInductiveDefinition (id,l,params,nparams) ->
 861          (gen_id seed, params, None,
 862             `Joint
 863               { K.joint_id = gen_id seed;
 864                 K.joint_kind = `Inductive nparams;
 865                 K.joint_defs = List.map (build_inductive seed) l
 866               })
 867
 868 and
 869     build_inductive seed =
 870      let module K = Content in
 871       fun (_,n,b,ty,l) ->
 872         `Inductive
 873           { K.inductive_id = gen_id seed;
 874             K.inductive_kind = b;
 875             K.inductive_type = ty;
 876             K.inductive_constructors = build_constructors seed l
 877            }
 878
 879 and
 880     build_constructors seed l =
 881      let module K = Content in
 882       List.map
 883        (fun (n,t) ->
 884            { K.dec_name = Some n;
 885              K.dec_id = gen_id seed;
 886              K.dec_inductive = false;
 887              K.dec_aref = "";
 888              K.dec_type = t
 889            }) l
 890 ;;
 891
 892 (*
 893 and 'term cinductiveType =
 894  id * string * bool * 'term *                (* typename, inductive, arity *)
 895    'term cconstructor list                   (*  constructors        *)
 896
 897 and 'term cconstructor =
 898  string * 'term
 899 *)
 900
 901