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