helm/ocaml/cic_transformations/cic2content.ml

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