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 (**************************************************************************)
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:";;
47 let hide_coercions = ref true;;
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 *)
53 let gen_id prefix seed =
54 let res = prefix ^ string_of_int !seed in
59 let name_of = function
61 | Cic.Name b -> Some b;;
63 exception Not_a_proof;;
64 exception NotImplemented;;
65 exception NotApplicable;;
67 (* we do not care for positivity, here, that in any case is enforced by
68 well typing. Just a brutal search *)
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,t) -> (occur uri s) or (occur uri t)
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?? *)
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
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 *)
121 C.ARel (id,_,_,_) -> false
124 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
126 with Not_found -> false)
127 | C.AMeta (id,_,_) ->
129 Hashtbl.find ids_to_inner_sorts id = `Prop
130 with Not_found -> assert false)
131 | C.ASort (id,_) -> false
132 | C.AImplicit _ -> raise NotImplemented
133 | C.AProd (id,_,_,_) -> false
134 | C.ACast (id,_,_) ->
136 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
138 with Not_found -> false)
139 | C.ALambda (id,_,_,_) ->
141 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
143 with Not_found -> false)
144 | C.ALetIn (id,_,_,_) ->
146 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
148 with Not_found -> false)
151 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
153 with Not_found -> false)
154 | C.AConst (id,_,_) ->
156 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
158 with Not_found -> false)
159 | C.AMutInd (id,_,_,_) -> false
160 | C.AMutConstruct (id,_,_,_,_) ->
162 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
164 with Not_found -> false)
166 | C.AMutCase (id,_,_,_,_,_) ->
168 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
170 with Not_found -> false)
173 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
175 with Not_found -> false)
176 | C.ACoFix (id,_,_) ->
178 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
180 with Not_found -> false)
183 (* transform a proof p into a proof list, concatenating the last
184 conclude element to the apply_context list, in case context is
185 empty. Otherwise, it just returns [p] *)
188 let module K = Content in
189 if (p.K.proof_context = []) then
190 if p.K.proof_apply_context = [] then [p]
194 K.proof_context = [];
195 K.proof_apply_context = []
197 p.K.proof_apply_context@[p1]
202 let rec serialize seed =
205 | a::l -> (flat seed a)@(serialize seed l)
208 (* top_down = true if the term is a LAMBDA or a decl *)
209 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
210 let module C2A = Cic2acic in
211 let module K = Content in
212 let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
213 with Not_found -> None)
218 if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
219 { K.proof_name = inner_proof.K.proof_name;
220 K.proof_id = gen_id proof_prefix seed;
221 K.proof_context = [] ;
222 K.proof_apply_context = [];
224 { K.conclude_id = gen_id conclude_prefix seed;
225 K.conclude_aref = id;
226 K.conclude_method = "TD_Conversion";
228 [K.ArgProof {inner_proof with K.proof_name = None}];
229 K.conclude_conclusion = Some expty
233 { K.proof_name = inner_proof.K.proof_name;
234 K.proof_id = gen_id proof_prefix seed;
235 K.proof_context = [] ;
236 K.proof_apply_context = [{inner_proof with K.proof_name = None}];
238 { K.conclude_id = gen_id conclude_prefix seed;
239 K.conclude_aref = id;
240 K.conclude_method = "BU_Conversion";
243 { K.premise_id = gen_id premise_prefix seed;
244 K.premise_xref = inner_proof.K.proof_id;
245 K.premise_binder = None;
249 K.conclude_conclusion = Some expty
254 let generate_exact seed t id name ~ids_to_inner_types =
255 let module C2A = Cic2acic in
256 let module K = Content in
257 { K.proof_name = name;
258 K.proof_id = gen_id proof_prefix seed ;
259 K.proof_context = [] ;
260 K.proof_apply_context = [];
262 { K.conclude_id = gen_id conclude_prefix seed;
263 K.conclude_aref = id;
264 K.conclude_method = "Exact";
265 K.conclude_args = [K.Term t];
266 K.conclude_conclusion =
267 try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
268 with Not_found -> None
273 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
274 let module C2A = Cic2acic in
275 let module C = Cic in
276 let module K = Content in
277 { K.proof_name = name;
278 K.proof_id = gen_id proof_prefix seed ;
279 K.proof_context = [] ;
280 K.proof_apply_context = [];
282 { K.conclude_id = gen_id conclude_prefix seed;
283 K.conclude_aref = id;
284 K.conclude_method = "Intros+LetTac";
285 K.conclude_args = [K.ArgProof inner_proof];
286 K.conclude_conclusion =
288 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
290 (match inner_proof.K.proof_conclude.K.conclude_conclusion with
293 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
294 else Some (C.ALetIn ("gen"^id,n,s,t)))
299 let build_decl_item seed id n s ~ids_to_inner_sorts =
300 let module K = Content in
303 Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
304 with Not_found -> None
309 { K.dec_name = name_of n;
310 K.dec_id = gen_id declaration_prefix seed;
311 K.dec_inductive = false;
317 { K.dec_name = name_of n;
318 K.dec_id = gen_id declaration_prefix seed;
319 K.dec_inductive = false;
325 let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
326 let module C = Cic in
327 let module K = Content in
332 let subproofs,args = aux l1 in
333 if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
336 seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
339 { K.premise_id = gen_id premise_prefix seed;
340 K.premise_xref = new_subproof.K.proof_id;
341 K.premise_binder = new_subproof.K.proof_name;
344 new_subproof::subproofs,new_arg::args
348 C.ARel (idr,idref,n,b) ->
351 Hashtbl.find ids_to_inner_sorts idr
352 with Not_found -> `Type (CicUniv.fresh())) in
355 { K.premise_id = gen_id premise_prefix seed;
356 K.premise_xref = idr;
357 K.premise_binder = Some b;
361 | C.AConst(id,uri,[]) ->
364 Hashtbl.find ids_to_inner_sorts id
365 with Not_found -> `Type (CicUniv.fresh())) in
368 { K.lemma_id = gen_id lemma_prefix seed;
369 K.lemma_name = UriManager.name_of_uri uri;
370 K.lemma_uri = UriManager.string_of_uri uri
373 | C.AMutConstruct(id,uri,tyno,consno,[]) ->
376 Hashtbl.find ids_to_inner_sorts id
377 with Not_found -> `Type (CicUniv.fresh())) in
379 let inductive_types =
381 CicEnvironment.get_obj CicUniv.empty_ugraph uri
384 | Cic.InductiveDefinition (l,_,_,_) -> l
387 let (_,_,_,constructors) =
388 List.nth inductive_types tyno in
389 let name,_ = List.nth constructors (consno - 1) in
391 { K.lemma_id = gen_id lemma_prefix seed;
394 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
395 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
399 | _ -> (K.Term t)) in
404 [{p with K.proof_name = None}],
407 K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
408 K.Premise {prem with K.premise_binder = None}
414 build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
415 let module K = Content in
417 let sort = Hashtbl.find ids_to_inner_sorts id in
420 (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
425 { K.def_name = name_of n;
426 K.def_id = gen_id definition_prefix seed;
431 Not_found -> assert false
433 (* the following function must be called with an object of sort
434 Prop. For debugging purposes this is tested again, possibly raising an
435 Not_a_proof exception *)
437 and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
438 let rec aux ?name t =
439 let module C = Cic in
440 let module K = Content in
441 let module C2A = Cic2acic in
444 C.ARel (id,idref,n,b) as t ->
445 let sort = Hashtbl.find ids_to_inner_sorts id in
447 generate_exact seed t id name ~ids_to_inner_types
448 else raise Not_a_proof
449 | C.AVar (id,uri,exp_named_subst) as t ->
450 let sort = Hashtbl.find ids_to_inner_sorts id in
452 generate_exact seed t id name ~ids_to_inner_types
453 else raise Not_a_proof
454 | C.AMeta (id,n,l) as t ->
455 let sort = Hashtbl.find ids_to_inner_sorts id in
457 generate_exact seed t id name ~ids_to_inner_types
458 else raise Not_a_proof
459 | C.ASort (id,s) -> raise Not_a_proof
460 | C.AImplicit _ -> raise NotImplemented
461 | C.AProd (_,_,_,_) -> raise Not_a_proof
462 | C.ACast (id,v,t) -> aux v
463 | C.ALambda (id,n,s,t) ->
464 let sort = Hashtbl.find ids_to_inner_sorts id in
468 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
469 match proof.K.proof_conclude.K.conclude_args with
477 (build_decl_item seed id n s ids_to_inner_sorts)::
478 proof'.K.proof_context
481 generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
484 | C.ALetIn (id,n,s,t) ->
485 let sort = Hashtbl.find ids_to_inner_sorts id in
489 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
490 match proof.K.proof_conclude.K.conclude_args with
498 ((build_def_item seed (get_id s) n s ids_to_inner_sorts
499 ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
500 ::proof'.K.proof_context;
503 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
508 seed li ~ids_to_inner_types ~ids_to_inner_sorts
509 with NotApplicable ->
511 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
512 with NotApplicable ->
514 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
515 with NotApplicable ->
517 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
518 with NotApplicable ->
519 let subproofs, args =
520 build_subproofs_and_args
521 seed li ~ids_to_inner_types ~ids_to_inner_sorts in
524 List.filter (test_for_lifting ~ids_to_inner_types) li in
526 match args_to_lift with
527 [_] -> List.map aux args_to_lift
528 | _ -> List.map (aux ~name:"H") args_to_lift in
529 let args = build_args seed li subproofs
530 ~ids_to_inner_types ~ids_to_inner_sorts in *)
531 { K.proof_name = name;
532 K.proof_id = gen_id proof_prefix seed;
533 K.proof_context = [];
534 K.proof_apply_context = serialize seed subproofs;
536 { K.conclude_id = gen_id conclude_prefix seed;
537 K.conclude_aref = id;
538 K.conclude_method = "Apply";
539 K.conclude_args = args;
540 K.conclude_conclusion =
542 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
543 with Not_found -> None
546 | C.AConst (id,uri,exp_named_subst) as t ->
547 let sort = Hashtbl.find ids_to_inner_sorts id in
549 generate_exact seed t id name ~ids_to_inner_types
550 else raise Not_a_proof
551 | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
552 | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
553 let sort = Hashtbl.find ids_to_inner_sorts id in
555 generate_exact seed t id name ~ids_to_inner_types
556 else raise Not_a_proof
557 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
558 let inductive_types,noparams =
559 (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
561 Cic.Constant _ -> assert false
562 | Cic.Variable _ -> assert false
563 | Cic.CurrentProof _ -> assert false
564 | Cic.InductiveDefinition (l,_,n,_) -> l,n
566 let (_,_,_,constructors) = List.nth inductive_types typeno in
567 let name_and_arities =
568 let rec count_prods =
570 C.Prod (_,_,t) -> 1 + count_prods t
573 (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in
575 let build_proof p (name,arity) =
576 let rec make_context_and_body c p n =
577 if n = 0 then c,(aux p)
580 Cic.ALambda(idl,vname,s1,t1) ->
582 build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
583 make_context_and_body (ce::c) t1 (n-1)
584 | _ -> assert false) in
585 let context,body = make_context_and_body [] p arity in
587 {body with K.proof_name = name; K.proof_context=context} in
588 List.map2 build_proof patterns name_and_arities in
591 build_subproofs_and_args
592 seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
595 | _ -> assert false) in
596 { K.proof_name = name;
597 K.proof_id = gen_id proof_prefix seed;
598 K.proof_context = [];
599 K.proof_apply_context = serialize seed context;
601 { K.conclude_id = gen_id conclude_prefix seed;
602 K.conclude_aref = id;
603 K.conclude_method = "Case";
605 (K.Aux (UriManager.string_of_uri uri))::
606 (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
607 K.conclude_conclusion =
609 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
610 with Not_found -> None
613 | C.AFix (id, no, funs) ->
616 (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
618 List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no
620 let decreasing_args =
621 List.map (function (_,_,n,_,_) -> n) funs in
623 { K.joint_id = gen_id joint_prefix seed;
624 K.joint_kind = `Recursive decreasing_args;
625 K.joint_defs = proofs
628 { K.proof_name = name;
629 K.proof_id = gen_id proof_prefix seed;
630 K.proof_context = [`Joint jo];
631 K.proof_apply_context = [];
633 { K.conclude_id = gen_id conclude_prefix seed;
634 K.conclude_aref = id;
635 K.conclude_method = "Exact";
638 { K.premise_id = gen_id premise_prefix seed;
639 K.premise_xref = jo.K.joint_id;
640 K.premise_binder = Some fun_name;
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 joint_prefix seed;
656 K.joint_kind = `CoRecursive;
657 K.joint_defs = proofs
660 { K.proof_name = name;
661 K.proof_id = gen_id proof_prefix seed;
662 K.proof_context = [`Joint jo];
663 K.proof_apply_context = [];
665 { K.conclude_id = gen_id conclude_prefix seed;
666 K.conclude_aref = id;
667 K.conclude_method = "Exact";
670 { K.premise_id = gen_id premise_prefix 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 UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists"
703 else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd"
704 else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd"
705 else "ByInduction" in
706 let prefix = String.sub uri_str 0 n in
707 let ind_str = (prefix ^ ".ind") in
708 let ind_uri = UriManager.uri_of_string ind_str in
709 let inductive_types,noparams =
710 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
712 | 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
721 (match inductive_types with
723 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
725 let rec clean_up n t =
728 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
729 | _ -> assert false) in
730 List.map (clean_up noparams) constructors in
731 let no_constructors= List.length constructors in
732 let args_for_cases, other_args =
733 split no_constructors tail_args in
734 let subproofs,other_method_args =
735 build_subproofs_and_args seed other_args
736 ~ids_to_inner_types ~ids_to_inner_sorts in
738 let rec build_method_args =
740 [],_-> [] (* extra args are ignored ???? *)
741 | (name,ty)::tlc,arg::tla ->
742 let idarg = get_id arg in
744 (try (Hashtbl.find ids_to_inner_sorts idarg)
745 with Not_found -> `Type (CicUniv.fresh())) in
747 if sortarg = `Prop then
751 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
754 seed idl n s1 ~ids_to_inner_sorts in
755 if (occur ind_uri s) then
757 Cic.ALambda(id2,n2,s2,t2) ->
760 { K.dec_name = name_of n2;
762 gen_id declaration_prefix seed;
763 K.dec_inductive = true;
767 let (context,body) = bc (t,t2) in
768 (ce::inductive_hyp::context,body)
772 let (context,body) = bc (t,t1) in
774 | _ , t -> ([],aux t) in
778 K.proof_name = Some name;
779 K.proof_context = co;
782 hdarg::(build_method_args (tlc,tla))
783 | _ -> assert false in
784 build_method_args (constructors1,args_for_cases) in
785 { K.proof_name = name;
786 K.proof_id = gen_id proof_prefix seed;
787 K.proof_context = [];
788 K.proof_apply_context = serialize seed subproofs;
790 { K.conclude_id = gen_id conclude_prefix seed;
791 K.conclude_aref = id;
792 K.conclude_method = method_name;
794 K.Aux (string_of_int no_constructors)
795 ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
796 ::method_args@other_method_args;
797 K.conclude_conclusion =
799 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
800 with Not_found -> None
803 | _ -> raise NotApplicable
805 and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
807 | ((Cic.AConst _) as he)::tl
808 | ((Cic.AMutInd _) as he)::tl
809 | ((Cic.AMutConstruct _) as he)::tl when
810 CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
818 acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
819 | _ -> raise NotApplicable
821 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
822 let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
823 let module C2A = Cic2acic in
824 let module K = Content in
825 let module C = Cic in
827 C.AConst (sid,uri,exp_named_subst)::args ->
828 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
829 UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or
830 LibraryObjects.is_eq_ind_URI uri or
831 LibraryObjects.is_eq_ind_r_URI uri then
834 build_subproofs_and_args
835 seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
838 | _,_ -> assert false) in
840 let rec ma_aux n = function
846 let aid = get_id a in
847 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
848 with Not_found -> `Type (CicUniv.fresh())) in
849 if asort = `Prop then
852 hd::(ma_aux (n-1) tl) in
854 { K.proof_name = name;
855 K.proof_id = gen_id proof_prefix seed;
856 K.proof_context = [];
857 K.proof_apply_context = serialize seed subproofs;
859 { K.conclude_id = gen_id conclude_prefix seed;
860 K.conclude_aref = id;
861 K.conclude_method = "Rewrite";
863 K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
864 K.conclude_conclusion =
866 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
867 with Not_found -> None
870 else raise NotApplicable
871 | _ -> raise NotApplicable
873 and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
874 let module C2A = Cic2acic in
875 let module K = Content in
876 let module C = Cic in
878 | C.AConst (sid,uri,exp_named_subst)::args
879 when LibraryObjects.is_trans_eq_URI uri ->
880 let exp_args = List.map snd exp_named_subst in
882 match exp_args@args with
883 | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
884 | _ -> raise NotApplicable
886 { K.proof_name = name;
887 K.proof_id = gen_id proof_prefix seed;
888 K.proof_context = [];
889 K.proof_apply_context = [];
891 { K.conclude_id = gen_id conclude_prefix seed;
892 K.conclude_aref = id;
893 K.conclude_method = "Eq_chain";
897 seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
900 seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
902 K.conclude_conclusion =
904 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
905 with Not_found -> None
908 | _ -> raise NotApplicable
910 and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
911 let module C2A = Cic2acic in
912 let module K = Content in
913 let module C = Cic in
915 | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args)
916 when LibraryObjects.is_trans_eq_URI uri ->
917 let exp_args = List.map snd exp_named_subst in
919 match exp_args@args with
920 | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
921 | _ -> raise NotApplicable
923 (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
925 @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
927 (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
933 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
935 let module K = Content in
940 | (id,Some (name,Cic.ADecl t)) ->
942 (* We should call build_decl_item, but we have not computed *)
943 (* the inner-types ==> we always produce a declaration *)
945 { K.dec_name = name_of name;
946 K.dec_id = gen_id declaration_prefix seed;
947 K.dec_inductive = false;
948 K.dec_aref = get_id t;
951 | (id,Some (name,Cic.ADef t)) ->
953 (* We should call build_def_item, but we have not computed *)
954 (* the inner-types ==> we always produce a declaration *)
956 { K.def_name = name_of name;
957 K.def_id = gen_id definition_prefix seed;
958 K.def_aref = get_id t;
966 (* map_sequent is similar to map_conjectures, but the for the hid
967 of the hypothesis, which are preserved instead of generating
968 fresh ones. We shall have to adopt a uniform policy, soon or later *)
970 let map_sequent ((id,n,context,ty):Cic.annconjecture) =
971 let module K = Content in
976 | (id,Some (name,Cic.ADecl t)) ->
978 (* We should call build_decl_item, but we have not computed *)
979 (* the inner-types ==> we always produce a declaration *)
981 { K.dec_name = name_of name;
983 K.dec_inductive = false;
984 K.dec_aref = get_id t;
987 | (id,Some (name,Cic.ADef t)) ->
989 (* We should call build_def_item, but we have not computed *)
990 (* the inner-types ==> we always produce a declaration *)
992 { K.def_name = name_of name;
994 K.def_aref = get_id t;
1002 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
1003 let module C = Cic in
1004 let module K = Content in
1005 let module C2A = Cic2acic in
1008 C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
1009 (gen_id object_prefix seed, params,
1012 (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
1015 build_def_item seed (get_id bo) (C.Name n) bo
1016 ~ids_to_inner_sorts ~ids_to_inner_types))
1017 | C.AConstant (_,_,n,Some bo,ty,params,_) ->
1018 (gen_id object_prefix seed, params, None,
1020 build_def_item seed (get_id bo) (C.Name n) bo
1021 ~ids_to_inner_sorts ~ids_to_inner_types))
1022 | C.AConstant (id,_,n,None,ty,params,_) ->
1023 (gen_id object_prefix seed, params, None,
1025 build_decl_item seed id (C.Name n) ty
1026 ~ids_to_inner_sorts))
1027 | C.AVariable (_,n,Some bo,ty,params,_) ->
1028 (gen_id object_prefix seed, params, None,
1030 build_def_item seed (get_id bo) (C.Name n) bo
1031 ~ids_to_inner_sorts ~ids_to_inner_types))
1032 | C.AVariable (id,n,None,ty,params,_) ->
1033 (gen_id object_prefix seed, params, None,
1035 build_decl_item seed id (C.Name n) ty
1036 ~ids_to_inner_sorts))
1037 | C.AInductiveDefinition (id,l,params,nparams,_) ->
1038 (gen_id object_prefix seed, params, None,
1040 { K.joint_id = gen_id joint_prefix seed;
1041 K.joint_kind = `Inductive nparams;
1042 K.joint_defs = List.map (build_inductive seed) l
1046 build_inductive seed =
1047 let module K = Content in
1050 { K.inductive_id = gen_id inductive_prefix seed;
1051 K.inductive_name = n;
1052 K.inductive_kind = b;
1053 K.inductive_type = ty;
1054 K.inductive_constructors = build_constructors seed l
1058 build_constructors seed l =
1059 let module K = Content in
1062 { K.dec_name = Some n;
1063 K.dec_id = gen_id declaration_prefix seed;
1064 K.dec_inductive = false;
1071 and 'term cinductiveType =
1072 id * string * bool * 'term * (* typename, inductive, arity *)
1073 'term cconstructor list (* constructors *)
1075 and 'term cconstructor =