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