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 *)
123 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
125 with Not_found -> false)
128 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
130 with Not_found -> false)
131 | C.AMeta (id,_,_) ->
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,_,_) ->
140 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
142 with Not_found -> false)
143 | C.ALambda (id,_,_,_) ->
145 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
147 with Not_found -> false)
148 | C.ALetIn (id,_,_,_) ->
150 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
152 with Not_found -> false)
155 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
157 with Not_found -> false)
158 | C.AConst (id,_,_) ->
160 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
162 with Not_found -> false)
163 | C.AMutInd (id,_,_,_) -> false
164 | C.AMutConstruct (id,_,_,_,_) ->
166 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
168 with Not_found -> false)
170 | C.AMutCase (id,_,_,_,_,_) ->
172 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
174 with Not_found -> false)
177 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
179 with Not_found -> false)
180 | C.ACoFix (id,_,_) ->
182 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
184 with Not_found -> false)
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] *)
192 let module K = Content in
193 if (p.K.proof_context = []) then
194 if p.K.proof_apply_context = [] then [p]
198 K.proof_context = [];
199 K.proof_apply_context = []
201 p.K.proof_apply_context@[p1]
206 let rec serialize seed =
209 | a::l -> (flat seed a)@(serialize seed l)
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)
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 = [];
228 { K.conclude_id = gen_id conclude_prefix seed;
229 K.conclude_aref = id;
230 K.conclude_method = "TD_Conversion";
232 [K.ArgProof {inner_proof with K.proof_name = None}];
233 K.conclude_conclusion = Some expty
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}];
242 { K.conclude_id = gen_id conclude_prefix seed;
243 K.conclude_aref = id;
244 K.conclude_method = "BU_Conversion";
247 { K.premise_id = gen_id premise_prefix seed;
248 K.premise_xref = inner_proof.K.proof_id;
249 K.premise_binder = None;
253 K.conclude_conclusion = Some expty
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 = [];
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
277 let generate_intros_let_tac seed id n s is_intro 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 = [];
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 =
292 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
294 (match inner_proof.K.proof_conclude.K.conclude_conclusion with
297 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
298 else Some (C.ALetIn ("gen"^id,n,s,t)))
303 let build_decl_item seed id n s ~ids_to_inner_sorts =
304 let module K = Content in
307 Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
308 with Not_found -> None
313 { K.dec_name = name_of n;
314 K.dec_id = gen_id declaration_prefix seed;
315 K.dec_inductive = false;
321 { K.dec_name = name_of n;
322 K.dec_id = gen_id declaration_prefix seed;
323 K.dec_inductive = false;
329 let infer_dependent ~headless context metasenv = function
334 List.map (function s -> false,s) l
338 CicTypeChecker.type_of_aux'
339 metasenv context (Deannotate.deannotate_term he)
340 CicUniv.oblivion_ugraph
343 match CicReduction.whd context t with
344 | Cic.Prod _ -> false
347 let rec dummify_last_tgt t =
348 match CicReduction.whd context t with
349 | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt)
350 | _ -> Cic.Implicit None
352 let rec aux ty = function
356 FreshNamesGenerator.clean_dummy_dependent_types
357 (dummify_last_tgt ty)
359 | Cic.Prod (n,src,tgt) ->
360 (n <> Cic.Anonymous && fstorder src, t) ::
361 aux (CicSubstitution.subst
362 (Deannotate.deannotate_term t) tgt) tl
365 (false, he) :: aux hety tl
366 with CicTypeChecker.TypeCheckerFailure _ -> assert false
369 let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
370 let module C = Cic in
371 let module K = Content in
376 let subproofs,args = aux l1 in
377 if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
380 seed context metasenv
381 ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
384 { K.premise_id = gen_id premise_prefix seed;
385 K.premise_xref = new_subproof.K.proof_id;
386 K.premise_binder = new_subproof.K.proof_name;
389 new_subproof::subproofs,new_arg::args
393 C.ARel (idr,idref,n,b) ->
396 Hashtbl.find ids_to_inner_sorts idr
397 with Not_found -> `Type (CicUniv.fresh())) in
400 { K.premise_id = gen_id premise_prefix seed;
401 K.premise_xref = idr;
402 K.premise_binder = Some b;
405 else (K.Term (dep,t))
406 | C.AConst(id,uri,[]) ->
409 Hashtbl.find ids_to_inner_sorts id
410 with Not_found -> `Type (CicUniv.fresh())) in
413 { K.lemma_id = gen_id lemma_prefix seed;
414 K.lemma_name = UriManager.name_of_uri uri;
415 K.lemma_uri = UriManager.string_of_uri uri
417 else (K.Term (dep,t))
418 | C.AMutConstruct(id,uri,tyno,consno,[]) ->
421 Hashtbl.find ids_to_inner_sorts id
422 with Not_found -> `Type (CicUniv.fresh())) in
424 let inductive_types =
426 CicEnvironment.get_obj CicUniv.empty_ugraph uri
429 | Cic.InductiveDefinition (l,_,_,_) -> l
432 let (_,_,_,constructors) =
433 List.nth inductive_types tyno in
434 let name,_ = List.nth constructors (consno - 1) in
436 { K.lemma_id = gen_id lemma_prefix seed;
439 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
440 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
443 else (K.Term (dep,t))
444 | _ -> (K.Term (dep,t))) in
447 match (aux (infer_dependent ~headless context metasenv l)) with
449 [{p with K.proof_name = None}],
452 K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
453 K.Premise {prem with K.premise_binder = None}
459 build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
460 let module K = Content in
462 let sort = Hashtbl.find ids_to_inner_sorts id in
465 (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
470 { K.def_name = name_of n;
471 K.def_id = gen_id definition_prefix seed;
476 Not_found -> assert false
478 (* the following function must be called with an object of sort
479 Prop. For debugging purposes this is tested again, possibly raising an
480 Not_a_proof exception *)
482 and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
483 let rec aux ?name context t =
484 let module C = Cic in
485 let module K = Content in
486 let module C2A = Cic2acic in
489 C.ARel (id,idref,n,b) as t ->
490 let sort = Hashtbl.find ids_to_inner_sorts id in
492 generate_exact seed t id name ~ids_to_inner_types
493 else raise Not_a_proof
494 | C.AVar (id,uri,exp_named_subst) as t ->
495 let sort = Hashtbl.find ids_to_inner_sorts id in
497 generate_exact seed t id name ~ids_to_inner_types
498 else raise Not_a_proof
499 | C.AMeta (id,n,l) as t ->
500 let sort = Hashtbl.find ids_to_inner_sorts id in
502 generate_exact seed t id name ~ids_to_inner_types
503 else raise Not_a_proof
504 | C.ASort (id,s) -> raise Not_a_proof
505 | C.AImplicit _ -> raise NotImplemented
506 | C.AProd (_,_,_,_) -> raise Not_a_proof
507 | C.ACast (id,v,t) -> aux context v
508 | C.ALambda (id,n,s,t) ->
509 let sort = Hashtbl.find ids_to_inner_sorts id in
512 aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t
515 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
516 match proof.K.proof_conclude.K.conclude_args with
524 (build_decl_item seed id n s ids_to_inner_sorts)::
525 proof'.K.proof_context
528 generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
531 | C.ALetIn (id,n,s,t) ->
532 let sort = Hashtbl.find ids_to_inner_sorts id in
534 let proof = (* XXX TIPAMI!!! *)
535 aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t
538 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
539 match proof.K.proof_conclude.K.conclude_args with
547 ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
548 ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
549 ::proof'.K.proof_context;
552 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
557 seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
558 with NotApplicable ->
560 seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
561 with NotApplicable ->
563 seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
564 with NotApplicable ->
566 seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
567 with NotApplicable ->
568 let subproofs, args =
569 build_subproofs_and_args
570 seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in
573 List.filter (test_for_lifting ~ids_to_inner_types) li in
575 match args_to_lift with
576 [_] -> List.map aux args_to_lift
577 | _ -> List.map (aux ~name:"H") args_to_lift in
578 let args = build_args seed li subproofs
579 ~ids_to_inner_types ~ids_to_inner_sorts in *)
580 { K.proof_name = name;
581 K.proof_id = gen_id proof_prefix seed;
582 K.proof_context = [];
583 K.proof_apply_context = serialize seed subproofs;
585 { K.conclude_id = gen_id conclude_prefix seed;
586 K.conclude_aref = id;
587 K.conclude_method = "Apply";
588 K.conclude_args = args;
589 K.conclude_conclusion =
591 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
592 with Not_found -> None
595 | C.AConst (id,uri,exp_named_subst) as t ->
596 let sort = Hashtbl.find ids_to_inner_sorts id in
598 generate_exact seed t id name ~ids_to_inner_types
599 else raise Not_a_proof
600 | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
601 | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
602 let sort = Hashtbl.find ids_to_inner_sorts id in
604 generate_exact seed t id name ~ids_to_inner_types
605 else raise Not_a_proof
606 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
607 let inductive_types,noparams =
608 (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
610 Cic.Constant _ -> assert false
611 | Cic.Variable _ -> assert false
612 | Cic.CurrentProof _ -> assert false
613 | Cic.InductiveDefinition (l,_,n,_) -> l,n
615 let (_,_,_,constructors) = List.nth inductive_types typeno in
616 let name_and_arities =
617 let rec count_prods =
619 C.Prod (_,_,t) -> 1 + count_prods t
622 (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in
624 let build_proof p (name,arity) =
625 let rec make_context_and_body c p n =
626 if n = 0 then c,(aux context p)
629 Cic.ALambda(idl,vname,s1,t1) ->
632 seed idl vname s1 ~ids_to_inner_sorts in
633 make_context_and_body (ce::c) t1 (n-1)
634 | _ -> assert false) in
635 let context,body = make_context_and_body [] p arity in
637 {body with K.proof_name = name; K.proof_context=context} in
638 List.map2 build_proof patterns name_and_arities in
641 build_subproofs_and_args ~headless:true
642 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te]
645 | _ -> assert false) in
646 { K.proof_name = name;
647 K.proof_id = gen_id proof_prefix seed;
648 K.proof_context = [];
649 K.proof_apply_context = serialize seed context;
651 { K.conclude_id = gen_id conclude_prefix seed;
652 K.conclude_aref = id;
653 K.conclude_method = "Case";
655 (K.Aux (UriManager.string_of_uri uri))::
656 (K.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp;
657 K.conclude_conclusion =
659 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
660 with Not_found -> None
663 | C.AFix (id, no, funs) ->
666 (fun ctx (_,n,_,ty,_) ->
667 let ty = Deannotate.deannotate_term ty in
668 Some (Cic.Name n,Cic.Decl ty) :: ctx)
673 (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in
675 List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no
677 let decreasing_args =
678 List.map (function (_,_,n,_,_) -> n) funs in
680 { K.joint_id = gen_id joint_prefix seed;
681 K.joint_kind = `Recursive decreasing_args;
682 K.joint_defs = proofs
685 { K.proof_name = name;
686 K.proof_id = gen_id proof_prefix seed;
687 K.proof_context = [`Joint jo];
688 K.proof_apply_context = [];
690 { K.conclude_id = gen_id conclude_prefix seed;
691 K.conclude_aref = id;
692 K.conclude_method = "Exact";
695 { K.premise_id = gen_id premise_prefix seed;
696 K.premise_xref = jo.K.joint_id;
697 K.premise_binder = Some fun_name;
698 K.premise_n = Some no;
701 K.conclude_conclusion =
703 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
704 with Not_found -> None
707 | C.ACoFix (id,no,funs) ->
710 (fun ctx (_,n,ty,_) ->
711 let ty = Deannotate.deannotate_term ty in
712 Some (Cic.Name n,Cic.Decl ty) :: ctx)
717 (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in
719 { K.joint_id = gen_id joint_prefix seed;
720 K.joint_kind = `CoRecursive;
721 K.joint_defs = proofs
724 { K.proof_name = name;
725 K.proof_id = gen_id proof_prefix seed;
726 K.proof_context = [`Joint jo];
727 K.proof_apply_context = [];
729 { K.conclude_id = gen_id conclude_prefix seed;
730 K.conclude_aref = id;
731 K.conclude_method = "Exact";
734 { K.premise_id = gen_id premise_prefix seed;
735 K.premise_xref = jo.K.joint_id;
736 K.premise_binder = Some "tiralo fuori";
737 K.premise_n = Some no;
740 K.conclude_conclusion =
742 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
743 with Not_found -> None
748 generate_conversion seed false id t1 ~ids_to_inner_types
749 in aux ?name context t
751 and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
752 let aux context ?name =
753 acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
755 let module C2A = Cic2acic in
756 let module K = Content in
757 let module C = Cic in
759 C.AConst (idc,uri,exp_named_subst)::args ->
760 let uri_str = UriManager.string_of_uri uri in
761 let suffix = Str.regexp_string "_ind.con" in
762 let len = String.length uri_str in
763 let n = (try (Str.search_backward suffix uri_str len)
764 with Not_found -> -1) in
765 if n<0 then raise NotApplicable
768 if UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists"
769 else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd"
770 else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd"
771 else "ByInduction" in
772 let prefix = String.sub uri_str 0 n in
773 let ind_str = (prefix ^ ".ind") in
774 let ind_uri = UriManager.uri_of_string ind_str in
775 let inductive_types,noparams =
776 (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
778 | Cic.InductiveDefinition (l,_,n,_) -> (l,n)
782 if n = 0 then ([],l) else
783 let p,a = split (n-1) (List.tl l) in
784 ((List.hd l::p),a) in
785 let params_and_IP,tail_args = split (noparams+1) args in
787 (match inductive_types with
789 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
791 let rec clean_up n t =
794 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
795 | _ -> assert false) in
796 List.map (clean_up noparams) constructors in
797 let no_constructors= List.length constructors in
798 let args_for_cases, other_args =
799 split no_constructors tail_args in
800 let subproofs,other_method_args =
801 build_subproofs_and_args ~headless:true seed context metasenv
802 other_args ~ids_to_inner_types ~ids_to_inner_sorts in
804 let rec build_method_args =
806 [],_-> [] (* extra args are ignored ???? *)
807 | (name,ty)::tlc,arg::tla ->
808 let idarg = get_id arg in
810 (try (Hashtbl.find ids_to_inner_sorts idarg)
811 with Not_found -> `Type (CicUniv.fresh())) in
813 if sortarg = `Prop then
817 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
819 Some (n,Cic.Decl(Deannotate.deannotate_term s1))
824 seed idl n s1 ~ids_to_inner_sorts in
825 if (occur ind_uri s) then
827 Cic.ALambda(id2,n2,s2,t2) ->
831 (Deannotate.deannotate_term s2))
836 { K.dec_name = name_of n2;
838 gen_id declaration_prefix seed;
839 K.dec_inductive = true;
843 let (context,body) = bc context'' (t,t2) in
844 (ce::inductive_hyp::context,body)
848 let (context,body) = bc context' (t,t1) in
850 | _ , t -> ([],aux context t) in
851 bc context (ty,arg) in
854 K.proof_name = Some name;
855 K.proof_context = co;
857 else (K.Term (false,arg)) in
858 hdarg::(build_method_args (tlc,tla))
859 | _ -> assert false in
860 build_method_args (constructors1,args_for_cases) in
861 { K.proof_name = name;
862 K.proof_id = gen_id proof_prefix seed;
863 K.proof_context = [];
864 K.proof_apply_context = serialize seed subproofs;
866 { K.conclude_id = gen_id conclude_prefix seed;
867 K.conclude_aref = id;
868 K.conclude_method = method_name;
870 K.Aux (string_of_int no_constructors)
871 ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))))
872 ::method_args@other_method_args;
873 K.conclude_conclusion =
875 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
876 with Not_found -> None
879 | _ -> raise NotApplicable
881 and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
883 | ((Cic.AConst _) as he)::tl
884 | ((Cic.AMutInd _) as he)::tl
885 | ((Cic.AMutConstruct _) as he)::tl when
886 CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
895 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
896 | _ -> raise NotApplicable
898 and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
899 let aux context ?name =
900 acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
902 let module C2A = Cic2acic in
903 let module K = Content in
904 let module C = Cic in
906 C.AConst (sid,uri,exp_named_subst)::args ->
907 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
908 UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or
909 LibraryObjects.is_eq_ind_URI uri or
910 LibraryObjects.is_eq_ind_r_URI uri then
913 build_subproofs_and_args
914 seed context metasenv
915 ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
918 | _,_ -> assert false) in
920 let rec ma_aux n = function
926 let aid = get_id a in
927 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
928 with Not_found -> `Type (CicUniv.fresh())) in
929 if asort = `Prop then
930 K.ArgProof (aux context a)
931 else K.Term (false,a) in
932 hd::(ma_aux (n-1) tl) in
934 { K.proof_name = name;
935 K.proof_id = gen_id proof_prefix seed;
936 K.proof_context = [];
937 K.proof_apply_context = serialize seed subproofs;
939 { K.conclude_id = gen_id conclude_prefix seed;
940 K.conclude_aref = id;
942 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI then
947 K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
948 K.conclude_conclusion =
950 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
951 with Not_found -> None
954 else raise NotApplicable
955 | _ -> raise NotApplicable
958 seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
960 let module C2A = Cic2acic in
961 let module K = Content in
962 let module C = Cic in
964 | C.AConst (sid,uri,exp_named_subst)::args
965 when LibraryObjects.is_trans_eq_URI uri ->
966 let exp_args = List.map snd exp_named_subst in
968 match exp_args@args with
969 | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
970 | _ -> raise NotApplicable
972 { K.proof_name = name;
973 K.proof_id = gen_id proof_prefix seed;
974 K.proof_context = [];
975 K.proof_apply_context = [];
977 { K.conclude_id = gen_id conclude_prefix seed;
978 K.conclude_aref = id;
979 K.conclude_method = "Eq_chain";
983 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
984 @ [K.Term (false,t2)]@
986 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
987 @ [K.Term (false,t3)];
988 K.conclude_conclusion =
990 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
991 with Not_found -> None
994 | _ -> raise NotApplicable
996 and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t =
997 let module C2A = Cic2acic in
998 let module K = Content in
999 let module C = Cic in
1001 | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args)
1002 when LibraryObjects.is_trans_eq_URI uri ->
1003 let exp_args = List.map snd exp_named_subst in
1004 let t1,t2,t3,p1,p2 =
1005 match exp_args@args with
1006 | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
1007 | _ -> raise NotApplicable
1010 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
1011 @[K.Term (false,t2)]
1013 seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
1015 (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)]
1021 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
1023 let module K = Content in
1028 | (id,Some (name,Cic.ADecl t)) ->
1030 (* We should call build_decl_item, but we have not computed *)
1031 (* the inner-types ==> we always produce a declaration *)
1033 { K.dec_name = name_of name;
1034 K.dec_id = gen_id declaration_prefix seed;
1035 K.dec_inductive = false;
1036 K.dec_aref = get_id t;
1039 | (id,Some (name,Cic.ADef t)) ->
1041 (* We should call build_def_item, but we have not computed *)
1042 (* the inner-types ==> we always produce a declaration *)
1044 { K.def_name = name_of name;
1045 K.def_id = gen_id definition_prefix seed;
1046 K.def_aref = get_id t;
1054 (* map_sequent is similar to map_conjectures, but the for the hid
1055 of the hypothesis, which are preserved instead of generating
1056 fresh ones. We shall have to adopt a uniform policy, soon or later *)
1058 let map_sequent ((id,n,context,ty):Cic.annconjecture) =
1059 let module K = Content in
1064 | (id,Some (name,Cic.ADecl t)) ->
1066 (* We should call build_decl_item, but we have not computed *)
1067 (* the inner-types ==> we always produce a declaration *)
1069 { K.dec_name = name_of name;
1071 K.dec_inductive = false;
1072 K.dec_aref = get_id t;
1075 | (id,Some (name,Cic.ADef t)) ->
1077 (* We should call build_def_item, but we have not computed *)
1078 (* the inner-types ==> we always produce a declaration *)
1080 { K.def_name = name_of name;
1082 K.def_aref = get_id t;
1090 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
1091 let module C = Cic in
1092 let module K = Content in
1093 let module C2A = Cic2acic in
1096 C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
1097 (gen_id object_prefix seed, params,
1100 (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
1104 seed [] (Deannotate.deannotate_conjectures conjectures)
1105 (get_id bo) (C.Name n) bo
1106 ~ids_to_inner_sorts ~ids_to_inner_types))
1107 | C.AConstant (_,_,n,Some bo,ty,params,_) ->
1108 (gen_id object_prefix seed, params, None,
1110 build_def_item seed [] [] (get_id bo) (C.Name n) bo
1111 ~ids_to_inner_sorts ~ids_to_inner_types))
1112 | C.AConstant (id,_,n,None,ty,params,_) ->
1113 (gen_id object_prefix seed, params, None,
1115 build_decl_item seed id (C.Name n) ty
1116 ~ids_to_inner_sorts))
1117 | C.AVariable (_,n,Some bo,ty,params,_) ->
1118 (gen_id object_prefix seed, params, None,
1120 build_def_item seed [] [] (get_id bo) (C.Name n) bo
1121 ~ids_to_inner_sorts ~ids_to_inner_types))
1122 | C.AVariable (id,n,None,ty,params,_) ->
1123 (gen_id object_prefix seed, params, None,
1125 build_decl_item seed id (C.Name n) ty
1126 ~ids_to_inner_sorts))
1127 | C.AInductiveDefinition (id,l,params,nparams,_) ->
1128 (gen_id object_prefix seed, params, None,
1130 { K.joint_id = gen_id joint_prefix seed;
1131 K.joint_kind = `Inductive nparams;
1132 K.joint_defs = List.map (build_inductive seed) l
1136 build_inductive seed =
1137 let module K = Content in
1140 { K.inductive_id = gen_id inductive_prefix seed;
1141 K.inductive_name = n;
1142 K.inductive_kind = b;
1143 K.inductive_type = ty;
1144 K.inductive_constructors = build_constructors seed l
1148 build_constructors seed l =
1149 let module K = Content in
1152 { K.dec_name = Some n;
1153 K.dec_id = gen_id declaration_prefix seed;
1154 K.dec_inductive = false;
1161 and 'term cinductiveType =
1162 id * string * bool * 'term * (* typename, inductive, arity *)
1163 'term cconstructor list (* constructors *)
1165 and 'term cconstructor =