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