1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (**************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (**************************************************************************)
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 *)
40 let res = "p" ^ string_of_int !seed in
45 let name_of = function
47 | Cic.Name b -> Some b;;
49 exception Not_a_proof;;
50 exception NotImplemented;;
51 exception NotApplicable;;
53 (* we do not care for positivity, here, that in any case is enforced by
54 well typing. Just a brutal search *)
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)
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?? *)
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
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 *)
107 C.ARel (id,_,_,_) -> false
110 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
112 with Not_found -> false)
113 | C.AMeta (id,_,_) ->
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,_,_) ->
122 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
124 with Not_found -> false)
125 | C.ALambda (id,_,_,_) ->
127 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
129 with Not_found -> false)
130 | C.ALetIn (id,_,_,_) ->
132 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
134 with Not_found -> false)
137 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
139 with Not_found -> false)
140 | C.AConst (id,_,_) ->
142 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
144 with Not_found -> false)
145 | C.AMutInd (id,_,_,_) -> false
146 | C.AMutConstruct (id,_,_,_,_) ->
148 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
150 with Not_found -> false)
152 | C.AMutCase (id,_,_,_,_,_) ->
154 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
156 with Not_found -> false)
159 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
161 with Not_found -> false)
162 | C.ACoFix (id,_,_) ->
164 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
166 with Not_found -> false)
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 =
177 if (test_for_lifting t ~ids_to_inner_types) then
178 (match subproofs with
183 { K.premise_id = gen_id seed;
184 K.premise_xref = p.K.proof_id;
185 K.premise_binder = p.K.proof_name;
188 in new_arg::(aux l1 tl))
192 C.ARel (idr,idref,n,b) ->
194 (try Hashtbl.find ids_to_inner_sorts idr
195 with Not_found -> "Type") in
198 { K.premise_id = gen_id seed;
199 K.premise_xref = idr;
200 K.premise_binder = Some b;
204 | _ -> (K.Term t)) in
205 hd::(aux l1 subproofs)
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] *)
215 let module K = Content in
216 if (p.K.proof_context = []) then
217 if p.K.proof_apply_context = [] then [p]
221 K.proof_context = [];
222 K.proof_apply_context = []
224 p.K.proof_apply_context@[p1]
229 let rec serialize seed =
232 | a::l -> (flat seed a)@(serialize seed l)
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)
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 = [];
251 { K.conclude_id = gen_id seed;
252 K.conclude_aref = id;
253 K.conclude_method = "TD_Conversion";
255 [K.ArgProof {inner_proof with K.proof_name = None}];
256 K.conclude_conclusion = Some expty
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}];
265 { K.conclude_id = gen_id seed;
266 K.conclude_aref = id;
267 K.conclude_method = "BU_Conversion";
270 { K.premise_id = gen_id seed;
271 K.premise_xref = inner_proof.K.proof_id;
272 K.premise_binder = None;
276 K.conclude_conclusion = Some expty
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;
286 K.proof_context = [] ;
287 K.proof_apply_context = [];
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
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;
306 K.proof_context = [] ;
307 K.proof_apply_context = [];
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 =
315 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
317 (match inner_proof.K.proof_conclude.K.conclude_conclusion with
320 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
321 else Some (C.ALetIn ("gen"^id,n,s,t)))
326 let build_decl_item seed id n s ~ids_to_inner_sorts =
327 let module K = Content in
329 let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
330 if sort = "Prop" then
332 { K.dec_name = name_of n;
333 K.dec_id = gen_id seed;
334 K.dec_inductive = false;
340 { K.dec_name = name_of n;
341 K.dec_id = gen_id seed;
342 K.dec_inductive = false;
347 Not_found -> assert false
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
357 let subproofs,args = aux l1 in
358 if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
361 seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
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;
369 new_subproof::subproofs,new_arg::args
373 C.ARel (idr,idref,n,b) ->
375 (try Hashtbl.find ids_to_inner_sorts idr
376 with Not_found -> "Type") in
379 { K.premise_id = gen_id seed;
380 K.premise_xref = idr;
381 K.premise_binder = Some b;
385 | C.AConst(id,uri,[]) ->
387 (try Hashtbl.find ids_to_inner_sorts id
388 with Not_found -> "Type") in
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
396 | C.AMutConstruct(id,uri,tyno,consno,[]) ->
398 (try Hashtbl.find ids_to_inner_sorts id
399 with Not_found -> "Type") in
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
408 let (_,_,_,constructors) =
409 List.nth inductive_types tyno in
410 let name,_ = List.nth constructors (consno - 1) in
412 { K.lemma_id = gen_id seed;
415 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
416 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
420 | _ -> (K.Term t)) in
425 [{p with K.proof_name = None}],
428 K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
429 K.Premise {prem with K.premise_binder = None}
435 build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
436 let module K = Content in
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 );
442 if sort = "Prop" then
443 (prerr_endline ("entro");
445 (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
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;)
453 (prerr_endline ("siamo qui???");
455 { K.def_name = name_of n;
456 K.def_id = gen_id seed;
461 Not_found -> assert false
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 *)
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
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
498 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
499 match proof.K.proof_conclude.K.conclude_args with
507 (build_decl_item seed id n s ids_to_inner_sorts)::
508 proof'.K.proof_context
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
518 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
519 match proof.K.proof_conclude.K.conclude_args with
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;
532 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
533 else raise Not_a_proof
536 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
537 with NotApplicable ->
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
546 List.filter (test_for_lifting ~ids_to_inner_types) li in
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;
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 =
564 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
565 with Not_found -> None
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
587 let (_,_,_,constructors) = List.nth inductive_types typeno in
588 let teid = get_id te in
590 (fun p (name,_) -> (K.ArgProof (aux ~name p)))
591 patterns constructors in
594 build_subproofs_and_args
595 seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
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;
604 { K.conclude_id = gen_id seed;
605 K.conclude_aref = id;
606 K.conclude_method = "Case";
608 (K.Aux (UriManager.string_of_uri uri))::
609 (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
610 K.conclude_conclusion =
612 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
613 with Not_found -> None
616 | C.AFix (id, no, funs) ->
619 (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
620 let decreasing_args =
621 List.map (function (_,_,n,_,_) -> n) funs in
623 { K.joint_id = gen_id seed;
624 K.joint_kind = `Recursive decreasing_args;
625 K.joint_defs = proofs
628 { K.proof_name = name;
629 K.proof_id = gen_id seed;
630 K.proof_context = [`Joint jo];
631 K.proof_apply_context = [];
633 { K.conclude_id = gen_id seed;
634 K.conclude_aref = id;
635 K.conclude_method = "Exact";
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;
644 K.conclude_conclusion =
646 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
647 with Not_found -> None
650 | C.ACoFix (id,no,funs) ->
653 (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
655 { K.joint_id = gen_id seed;
656 K.joint_kind = `CoRecursive;
657 K.joint_defs = proofs
660 { K.proof_name = name;
661 K.proof_id = gen_id seed;
662 K.proof_context = [`Joint jo];
663 K.proof_apply_context = [];
665 { K.conclude_id = gen_id seed;
666 K.conclude_aref = id;
667 K.conclude_method = "Exact";
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;
676 K.conclude_conclusion =
678 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
679 with Not_found -> None
684 generate_conversion seed false id t1 ~ids_to_inner_types
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
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
702 if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then
704 else "ByInduction" in
705 let prefix = String.sub uri_str 0 n in
706 let ind_str = (prefix ^ ".ind") in
707 let ind_uri = UriManager.uri_of_string ind_str in
708 let inductive_types,noparams =
709 (match CicEnvironment.get_obj ind_uri with
710 Cic.Constant _ -> assert false
711 | Cic.Variable _ -> assert false
712 | Cic.CurrentProof _ -> assert false
713 | Cic.InductiveDefinition (l,_,n) -> (l,n)
716 if n = 0 then ([],l) else
717 let p,a = split (n-1) (List.tl l) in
718 ((List.hd l::p),a) in
719 let params_and_IP,tail_args = split (noparams+1) args in
720 if method_name = "Exists" then
721 (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
722 prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
724 (match inductive_types with
726 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
728 let rec clean_up n t =
731 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
732 | _ -> assert false) in
733 List.map (clean_up noparams) constructors in
734 let no_constructors= List.length constructors in
735 let args_for_cases, other_args =
736 split no_constructors tail_args in
737 let subproofs,other_method_args =
738 build_subproofs_and_args seed other_args
739 ~ids_to_inner_types ~ids_to_inner_sorts in
740 prerr_endline "****** end other *******"; flush stderr;
742 let rec build_method_args =
744 [],_-> [] (* extra args are ignored ???? *)
745 | (name,ty)::tlc,arg::tla ->
746 let idarg = get_id arg in
748 (try (Hashtbl.find ids_to_inner_sorts idarg)
749 with Not_found -> "Type") in
751 if sortarg = "Prop" then
755 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
758 seed idl n s1 ~ids_to_inner_sorts in
759 if (occur ind_uri s) then
760 ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
762 Cic.ALambda(id2,n2,s2,t2) ->
765 { K.dec_name = name_of n2;
766 K.dec_id = gen_id seed;
767 K.dec_inductive = true;
771 let (context,body) = bc (t,t2) in
772 (ce::inductive_hyp::context,body)
775 ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
776 let (context,body) = bc (t,t1) in
778 | _ , t -> ([],aux t) in
782 K.proof_name = Some name;
783 K.proof_context = co;
786 hdarg::(build_method_args (tlc,tla))
787 | _ -> assert false in
788 build_method_args (constructors1,args_for_cases) in
789 { K.proof_name = name;
790 K.proof_id = gen_id seed;
791 K.proof_context = [];
792 K.proof_apply_context = serialize seed subproofs;
794 { K.conclude_id = gen_id seed;
795 K.conclude_aref = id;
796 K.conclude_method = method_name;
798 K.Aux (string_of_int no_constructors)
799 ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
800 ::method_args@other_method_args;
801 K.conclude_conclusion =
803 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
804 with Not_found -> None
807 | _ -> raise NotApplicable
809 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
810 let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
811 let module C2A = Cic2acic in
812 let module K = Content in
813 let module C = Cic in
815 C.AConst (sid,uri,exp_named_subst)::args ->
816 let uri_str = UriManager.string_of_uri uri in
817 if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
818 uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
821 build_subproofs_and_args
822 seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
825 | _,_ -> assert false) in
827 let rec ma_aux n = function
833 let aid = get_id a in
834 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
835 with Not_found -> "Type") in
836 if asort = "Prop" then
839 hd::(ma_aux (n-1) tl) in
841 { K.proof_name = name;
842 K.proof_id = gen_id seed;
843 K.proof_context = [];
844 K.proof_apply_context = serialize seed subproofs;
846 { K.conclude_id = gen_id seed;
847 K.conclude_aref = id;
848 K.conclude_method = "Rewrite";
850 K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
851 K.conclude_conclusion =
853 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
854 with Not_found -> None
857 else raise NotApplicable
858 | _ -> raise NotApplicable
862 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
864 let module K = Content in
868 (id,None) as item -> item
869 | (id,Some (name,Cic.ADecl t)) ->
872 (* We should call build_decl_item, but we have not computed *)
873 (* the inner-types ==> we always produce a declaration *)
875 { K.dec_name = name_of name;
876 K.dec_id = gen_id seed;
877 K.dec_inductive = false;
878 K.dec_aref = get_id t;
881 | (id,Some (name,Cic.ADef t)) ->
884 (* We should call build_def_item, but we have not computed *)
885 (* the inner-types ==> we always produce a declaration *)
887 { K.def_name = name_of name;
888 K.def_id = gen_id seed;
889 K.def_aref = get_id t;
897 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
898 let module C = Cic in
899 let module K = Content in
900 let module C2A = Cic2acic in
903 C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
904 (gen_id seed, params,
907 (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
910 build_def_item seed (get_id bo) (C.Name n) bo
911 ~ids_to_inner_sorts ~ids_to_inner_types))
912 | C.AConstant (_,_,n,Some bo,ty,params) ->
913 (gen_id seed, params, None,
915 build_def_item seed (get_id bo) (C.Name n) bo
916 ~ids_to_inner_sorts ~ids_to_inner_types))
917 | C.AConstant (id,_,n,None,ty,params) ->
918 (gen_id seed, params, None,
920 build_decl_item seed id (C.Name n) ty
921 ~ids_to_inner_sorts))
922 | C.AVariable (_,n,Some bo,ty,params) ->
923 (gen_id seed, params, None,
925 build_def_item seed (get_id bo) (C.Name n) bo
926 ~ids_to_inner_sorts ~ids_to_inner_types))
927 | C.AVariable (id,n,None,ty,params) ->
928 (gen_id seed, params, None,
930 build_decl_item seed id (C.Name n) ty
931 ~ids_to_inner_sorts))
932 | C.AInductiveDefinition (id,l,params,nparams) ->
933 (gen_id seed, params, None,
935 { K.joint_id = gen_id seed;
936 K.joint_kind = `Inductive nparams;
937 K.joint_defs = List.map (build_inductive seed) l
941 build_inductive seed =
942 let module K = Content in
945 { K.inductive_id = gen_id seed;
946 K.inductive_kind = b;
947 K.inductive_type = ty;
948 K.inductive_constructors = build_constructors seed l
952 build_constructors seed l =
953 let module K = Content in
956 { K.dec_name = Some n;
957 K.dec_id = gen_id seed;
958 K.dec_inductive = false;
965 and 'term cinductiveType =
966 id * string * bool * 'term * (* typename, inductive, arity *)
967 'term cconstructor list (* constructors *)
969 and 'term cconstructor =