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 (**************************************************************************)
36 type joint_recursion_kind =
39 | `Inductive of int (* paramsno *)
40 | `CoInductive of int (* paramsno *)
44 type var_or_const = Var | Const;;
46 type 'term declaration =
47 { dec_name : string option;
55 type 'term definition =
56 { def_name : string option;
63 type 'term inductive =
64 { inductive_id : string ;
65 inductive_kind : bool;
66 inductive_type : 'term;
67 inductive_constructors : 'term declaration list
71 type 'term decl_context_element =
72 [ `Declaration of 'term declaration
73 | `Hypothesis of 'term declaration
77 type ('term,'proof) def_context_element =
79 | `Definition of 'term definition
83 type ('term,'proof) in_joint_context_element =
84 [ `Inductive of 'term inductive
85 | 'term decl_context_element
86 | ('term,'proof) def_context_element
90 type ('term,'proof) joint =
92 joint_kind : joint_recursion_kind ;
93 joint_defs : ('term,'proof) in_joint_context_element list
97 type ('term,'proof) joint_context_element =
98 [ `Joint of ('term,'proof) joint ]
102 { proof_name : string option;
104 proof_context : 'term in_proof_context_element list ;
105 proof_apply_context: 'term proof list;
106 proof_conclude : 'term conclude_item
109 and 'term in_proof_context_element =
110 [ 'term decl_context_element
111 | ('term,'term proof) def_context_element
112 | ('term,'term proof) joint_context_element
115 and 'term conclude_item =
116 { conclude_id :string;
117 conclude_aref : string;
118 conclude_method : string;
119 conclude_args : ('term arg) list ;
120 conclude_conclusion : 'term option
127 | ArgProof of 'term proof
128 | ArgMethod of string (* ???? *)
131 { premise_id: string;
132 premise_xref : string ;
133 premise_binder : string option;
134 premise_n : int option;
138 type 'term conjecture = id * int * 'term context * 'term
140 and 'term context = 'term hypothesis list
142 and 'term hypothesis =
144 ['term decl_context_element | ('term,'term proof) def_context_element ] option
147 type 'term in_object_context_element =
148 [ `Decl of var_or_const * 'term decl_context_element
149 | `Def of var_or_const * 'term * ('term,'term proof) def_context_element
150 | ('term,'term proof) joint_context_element
156 UriManager.uri list * (* params *)
157 'term conjecture list option * (* optional metasenv *)
158 'term in_object_context_element (* actual object *)
163 (* e se mettessi la conversione di BY nell'apply_context ? *)
164 (* sarebbe carino avere l'invariante che la proof2pres
165 generasse sempre prove con contesto vuoto *)
168 let res = "p" ^ string_of_int !seed in
173 let name_of = function
174 Cic.Anonymous -> None
175 | Cic.Name b -> Some b;;
177 exception Not_a_proof;;
178 exception NotImplemented;;
179 exception NotApplicable;;
181 (* we do not care for positivity, here, that in any case is enforced by
182 well typing. Just a brutal search *)
185 let module C = Cic in
191 | C.Implicit -> raise NotImplemented
192 | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
193 | C.Cast (te,ty) -> (occur uri te)
194 | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
195 | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
200 else (occur uri a)) false l
201 | C.Const (_,_) -> false
202 | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
203 | C.MutConstruct (_,_,_,_) -> false
204 | C.MutCase _ -> false (* presuming too much?? *)
205 | C.Fix _ -> false (* presuming too much?? *)
206 | C.CoFix (_,_) -> false (* presuming too much?? *)
210 let module C = Cic in
212 C.ARel (id,_,_,_) -> id
213 | C.AVar (id,_,_) -> id
214 | C.AMeta (id,_,_) -> id
215 | C.ASort (id,_) -> id
216 | C.AImplicit _ -> raise NotImplemented
217 | C.AProd (id,_,_,_) -> id
218 | C.ACast (id,_,_) -> id
219 | C.ALambda (id,_,_,_) -> id
220 | C.ALetIn (id,_,_,_) -> id
221 | C.AAppl (id,_) -> id
222 | C.AConst (id,_,_) -> id
223 | C.AMutInd (id,_,_,_) -> id
224 | C.AMutConstruct (id,_,_,_,_) -> id
225 | C.AMutCase (id,_,_,_,_,_) -> id
226 | C.AFix (id,_,_) -> id
227 | C.ACoFix (id,_,_) -> id
230 let test_for_lifting ~ids_to_inner_types =
231 let module C = Cic in
232 let module C2A = Cic2acic in
233 (* atomic terms are never lifted, according to my policy *)
235 C.ARel (id,_,_,_) -> false
236 | C.AVar (id,_,_) -> false
237 | C.AMeta (id,_,_) -> false
238 | C.ASort (id,_) -> false
239 | C.AImplicit _ -> raise NotImplemented
240 | C.AProd (id,_,_,_) -> false
241 | C.ACast (id,_,_) ->
243 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
245 with notfound -> false)
246 | C.ALambda (id,_,_,_) ->
248 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
250 with notfound -> false)
251 | C.ALetIn (id,_,_,_) ->
253 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
255 with notfound -> false)
258 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
260 with notfound -> false)
261 | C.AConst (id,_,_) ->
263 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
265 with notfound -> false)
266 | C.AMutInd (id,_,_,_) -> false
267 | C.AMutConstruct (id,_,_,_,_) ->
269 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
271 with notfound -> false)
273 | C.AMutCase (id,_,_,_,_,_) ->
275 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
277 with notfound -> false)
280 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
282 with notfound -> false)
283 | C.ACoFix (id,_,_) ->
285 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
287 with notfound -> false)
290 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
291 let module C = Cic in
292 let rec aux l subrpoofs =
296 if (test_for_lifting t ~ids_to_inner_types) then
297 (match subproofs with
302 { premise_id = gen_id seed;
303 premise_xref = p.proof_id;
304 premise_binder = p.proof_name;
307 in new_arg::(aux l1 tl))
311 C.ARel (idr,idref,n,b) ->
313 (try Hashtbl.find ids_to_inner_sorts idr
314 with notfound -> "Type") in
317 { premise_id = gen_id seed;
319 premise_binder = Some b;
324 hd::(aux l1 subproofs)
328 (* transform a proof p into a proof list, concatenating the last
329 conclude element to the apply_context list, in case context is
330 empty. Otherwise, it just returns [p] *)
333 if (p.proof_context = []) then
334 if p.proof_apply_context = [] then [p]
337 { proof_name = p.proof_name;
338 proof_id = gen_id seed;
340 proof_apply_context = [];
341 proof_conclude = p.proof_conclude;
343 p.proof_apply_context@[p1]
348 let rec serialize seed =
351 | p::tl -> (flat seed p)@(serialize seed tl);;
353 (* top_down = true if the term is a LAMBDA or a decl *)
354 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
355 let module C2A = Cic2acic in
356 let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
357 with Not_found -> None)
362 if inner_proof.proof_conclude.conclude_method = "Intros+LetTac" then
363 { proof_name = None ;
364 proof_id = gen_id seed;
366 proof_apply_context = [];
368 { conclude_id = gen_id seed;
370 conclude_method = "TD_Conversion";
371 conclude_args = [ArgProof inner_proof];
372 conclude_conclusion = Some expty
376 { proof_name = None ;
377 proof_id = gen_id seed;
379 proof_apply_context = [inner_proof];
381 { conclude_id = gen_id seed;
383 conclude_method = "BU_Conversion";
386 { premise_id = gen_id seed;
387 premise_xref = inner_proof.proof_id;
388 premise_binder = None;
392 conclude_conclusion = Some expty
397 let generate_exact seed t id name ~ids_to_inner_types =
398 let module C2A = Cic2acic in
402 proof_apply_context = [];
404 { conclude_id = gen_id seed;
406 conclude_method = "Exact";
407 conclude_args = [Term t];
408 conclude_conclusion =
409 try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
410 with notfound -> None
415 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
416 let module C2A = Cic2acic in
417 let module C = Cic in
421 proof_apply_context = [];
423 { conclude_id = gen_id seed;
425 conclude_method = "Intros+LetTac";
426 conclude_args = [ArgProof inner_proof];
427 conclude_conclusion =
429 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
431 (match inner_proof.proof_conclude.conclude_conclusion with
434 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
435 else Some (C.ALetIn ("gen"^id,n,s,t)))
440 let build_decl_item seed id n s ~ids_to_inner_sorts =
441 let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
442 if sort = "Prop" then
444 { dec_name = name_of n;
445 dec_id = gen_id seed;
446 dec_inductive = false;
452 { dec_name = name_of n;
453 dec_id = gen_id seed;
454 dec_inductive = false;
460 let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
461 let sort = Hashtbl.find ids_to_inner_sorts id in
462 if sort = "Prop" then
463 `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
466 { def_name = name_of n;
467 def_id = gen_id seed;
472 (* the following function must be called with an object of sort
473 Prop. For debugging purposes this is tested again, possibly raising an
474 Not_a_proof exception *)
476 and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
477 let rec aux ?(name = None) t =
478 let module C = Cic in
479 let module X = Xml in
480 let module U = UriManager in
481 let module C2A = Cic2acic in
484 C.ARel (id,idref,n,b) 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.AVar (id,uri,exp_named_subst) as t ->
490 let sort = Hashtbl.find ids_to_inner_sorts id in
491 if sort = "Prop" then
492 generate_exact seed t id name ~ids_to_inner_types
493 else raise Not_a_proof
494 | C.AMeta (id,n,l) as t ->
495 let sort = Hashtbl.find ids_to_inner_sorts id in
496 if sort = "Prop" then
497 generate_exact seed t id name ~ids_to_inner_types
498 else raise Not_a_proof
499 | C.ASort (id,s) -> raise Not_a_proof
500 | C.AImplicit _ -> raise NotImplemented
501 | C.AProd (_,_,_,_) -> raise Not_a_proof
502 | C.ACast (id,v,t) -> aux v
503 | C.ALambda (id,n,s,t) ->
504 let sort = Hashtbl.find ids_to_inner_sorts id in
505 if sort = "Prop" then
506 let proof = aux t ~name:None in
508 if proof.proof_conclude.conclude_method = "Intros+LetTac" then
509 match proof.proof_conclude.conclude_args with
515 proof_id = proof'.proof_id;
517 (build_decl_item seed id n s ids_to_inner_sorts)::
518 proof'.proof_context;
519 proof_apply_context = proof'.proof_apply_context;
520 proof_conclude = proof'.proof_conclude;
523 generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
524 else raise Not_a_proof
525 | C.ALetIn (id,n,s,t) ->
526 let sort = Hashtbl.find ids_to_inner_sorts id in
527 if sort = "Prop" then
530 if proof.proof_conclude.conclude_method = "Intros+LetTac" then
531 match proof.proof_conclude.conclude_args with
539 ((build_def_item seed id n s ids_to_inner_sorts
540 ids_to_inner_types) :> Cic.annterm in_proof_context_element)
541 ::proof'.proof_context;
544 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
545 else raise Not_a_proof
548 seed name id li ids_to_inner_types ids_to_inner_sorts
549 with NotApplicable ->
551 seed name id li ids_to_inner_types ids_to_inner_sorts
552 with NotApplicable ->
554 List.filter (test_for_lifting ~ids_to_inner_types) li in
556 match args_to_lift with
557 [_] -> List.map aux args_to_lift
558 | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
559 let args = build_args seed li subproofs
560 ~ids_to_inner_types ~ids_to_inner_sorts in
562 proof_id = gen_id seed;
564 proof_apply_context = serialize seed subproofs;
566 { conclude_id = gen_id seed;
568 conclude_method = "Apply";
569 conclude_args = args;
570 conclude_conclusion =
572 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
573 with notfound -> None
576 | C.AConst (id,uri,exp_named_subst) as t ->
577 let sort = Hashtbl.find ids_to_inner_sorts id in
578 if sort = "Prop" then
579 generate_exact seed t id name ~ids_to_inner_types
580 else raise Not_a_proof
581 | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
582 | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
583 let sort = Hashtbl.find ids_to_inner_sorts id in
584 if sort = "Prop" then
585 generate_exact seed t id name ~ids_to_inner_types
586 else raise Not_a_proof
587 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
588 let teid = get_id te in
589 let pp = List.map (function p -> (ArgProof (aux p))) patterns in
591 (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
592 with notfound -> None)
594 Some tety -> (* we must lift up the argument *)
596 { proof_name = Some "name";
597 proof_id = gen_id seed;
599 proof_apply_context = flat seed p;
601 { conclude_id = gen_id seed;
603 conclude_method = "Case";
604 conclude_args = (Term ty)::(Term te)::pp;
605 conclude_conclusion =
607 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
608 with notfound -> None
613 proof_id = gen_id seed;
615 proof_apply_context = [];
617 { conclude_id = gen_id seed;
619 conclude_method = "Case";
620 conclude_args = (Term ty)::(Term te)::pp;
621 conclude_conclusion =
623 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
624 with notfound -> None
628 | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
629 let proof = (aux bo) in (* must be recursive !! *)
631 proof_id = gen_id seed;
632 proof_context = [`Proof proof];
633 proof_apply_context = [];
635 { conclude_id = gen_id seed;
637 conclude_method = "Exact";
640 { premise_id = gen_id seed;
641 premise_xref = proof.proof_id;
642 premise_binder = proof.proof_name;
646 conclude_conclusion =
648 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
649 with notfound -> None
652 | C.AFix (id, no, funs) ->
654 List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
656 { joint_id = gen_id seed;
657 joint_kind = `Recursive;
662 proof_id = gen_id seed;
663 proof_context = [`Joint jo];
664 proof_apply_context = [];
666 { conclude_id = gen_id seed;
668 conclude_method = "Exact";
671 { premise_id = gen_id seed;
672 premise_xref = jo.joint_id;
673 premise_binder = Some "tiralo fuori";
677 conclude_conclusion =
679 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
680 with notfound -> None
683 | C.ACoFix (id,no,[(id1,n,ty,bo)]) ->
684 let proof = (aux bo) in (* must be recursive !! *)
686 proof_id = gen_id seed;
687 proof_context = [`Proof proof];
688 proof_apply_context = [];
690 { conclude_id = gen_id seed;
692 conclude_method = "Exact";
695 { premise_id = gen_id seed;
696 premise_xref = proof.proof_id;
697 premise_binder = proof.proof_name;
701 conclude_conclusion =
703 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
704 with notfound -> None
707 | C.ACoFix (id,no,funs) ->
709 List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
711 { joint_id = gen_id seed;
712 joint_kind = `Recursive;
717 proof_id = gen_id seed;
718 proof_context = [`Joint jo];
719 proof_apply_context = [];
721 { conclude_id = gen_id seed;
723 conclude_method = "Exact";
726 { premise_id = gen_id seed;
727 premise_xref = jo.joint_id;
728 premise_binder = Some "tiralo fuori";
732 conclude_conclusion =
734 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
735 with notfound -> None
740 generate_conversion seed false id t1 ~ids_to_inner_types
743 and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
744 let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
745 let module C2A = Cic2acic in
746 let module C = Cic in
748 C.AConst (idc,uri,exp_named_subst)::args ->
749 let uri_str = UriManager.string_of_uri uri in
750 let suffix = Str.regexp_string "_ind.con" in
751 let len = String.length uri_str in
752 let n = (try (Str.search_backward suffix uri_str len)
753 with Not_found -> -1) in
754 if n<0 then raise NotApplicable
756 let prefix = String.sub uri_str 0 n in
757 let ind_str = (prefix ^ ".ind") in
758 let ind_uri = UriManager.uri_of_string ind_str in
759 let inductive_types,noparams =
760 (match CicEnvironment.get_obj ind_uri with
761 Cic.Constant _ -> assert false
762 | Cic.Variable _ -> assert false
763 | Cic.CurrentProof _ -> assert false
764 | Cic.InductiveDefinition (l,_,n) -> (l,n)
767 if n = 0 then ([],l) else
768 let p,a = split (n-1) (List.tl l) in
769 ((List.hd l::p),a) in
770 let params_and_IP,tail_args = split (noparams+1) args in
772 (match inductive_types with
774 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
776 let rec clean_up n t =
779 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
780 | _ -> assert false) in
781 List.map (clean_up noparams) constructors in
782 let no_constructors= List.length constructors in
783 let args_for_cases, other_args =
784 split no_constructors tail_args in
786 List.filter (test_for_lifting ~ids_to_inner_types) other_args in
788 match args_to_lift with
789 [_] -> List.map aux args_to_lift
790 | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
791 prerr_endline "****** end subproofs *******"; flush stderr;
792 let other_method_args =
793 build_args seed other_args subproofs
794 ~ids_to_inner_types ~ids_to_inner_sorts in
796 let rparams,inductive_arg =
801 | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
802 aux other_method_args in
804 prerr_endline "****** end other *******"; flush stderr;
806 let rec build_method_args =
808 [],_-> [] (* extra args are ignored ???? *)
809 | (name,ty)::tlc,arg::tla ->
810 let idarg = get_id arg in
812 (try (Hashtbl.find ids_to_inner_sorts idarg)
813 with Not_found -> "Type") in
815 if sortarg = "Prop" then
819 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
822 seed idl n s1 ~ids_to_inner_sorts in
823 if (occur ind_uri s) then
824 ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
826 Cic.ALambda(id2,n2,s2,t2) ->
829 { dec_name = name_of n2;
830 dec_id = gen_id seed;
831 dec_inductive = true;
835 let (context,body) = bc (t,t2) in
836 (ce::inductive_hyp::context,body)
839 ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
840 let (context,body) = bc (t,t1) in
842 | _ , t -> ([],aux t ~name:None) in
845 { proof_name = Some name;
846 proof_id = bo.proof_id;
848 proof_apply_context = bo.proof_apply_context;
849 proof_conclude = bo.proof_conclude;
852 hdarg::(build_method_args (tlc,tla))
853 | _ -> assert false in
854 build_method_args (constructors1,args_for_cases) in
856 proof_id = gen_id seed;
858 proof_apply_context = subproofs;
860 { conclude_id = gen_id seed;
862 conclude_method = "ByInduction";
865 ::Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
866 ::method_args@other_method_args;
867 conclude_conclusion =
869 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
870 with notfound -> None
873 | _ -> raise NotApplicable
875 and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
876 let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
877 let module C2A = Cic2acic in
878 let module C = Cic in
880 C.AConst (sid,uri,exp_named_subst)::args ->
881 let uri_str = UriManager.string_of_uri uri in
882 if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
883 uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
884 let subproof = aux (List.nth args 3) in
886 let rec ma_aux n = function
892 { premise_id = gen_id seed;
893 premise_xref = subproof.proof_id;
894 premise_binder = None;
898 let aid = get_id a in
899 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
900 with Not_found -> "Type") in
901 if asort = "Prop" then
904 hd::(ma_aux (n-1) tl) in
907 proof_id = gen_id seed;
909 proof_apply_context = [subproof];
911 { conclude_id = gen_id seed;
913 conclude_method = "Rewrite";
915 Term (C.AConst (sid,uri,exp_named_subst))::method_args;
916 conclude_conclusion =
918 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
919 with notfound -> None
922 else raise NotApplicable
923 | _ -> raise NotApplicable
927 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
932 (id,None) as item -> item
933 | (id,Some (name,Cic.ADecl t)) ->
936 (build_decl_item seed (get_id t) name t
938 | (id,Some (name,Cic.ADef t)) ->
941 (build_def_item seed (get_id t) name t
942 ~ids_to_inner_sorts ~ids_to_inner_types)
948 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
949 let module C = Cic in
950 let module C2A = Cic2acic in
953 C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
954 (gen_id seed, params,
957 (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
960 build_def_item seed (get_id bo) (C.Name n) bo
961 ~ids_to_inner_sorts ~ids_to_inner_types))
962 | C.AConstant (_,_,n,Some bo,ty,params) ->
963 (gen_id seed, params, None,
965 build_def_item seed (get_id bo) (C.Name n) bo
966 ~ids_to_inner_sorts ~ids_to_inner_types))
967 | C.AConstant (id,_,n,None,ty,params) ->
968 (gen_id seed, params, None,
970 build_decl_item seed id (C.Name n) ty
971 ~ids_to_inner_sorts))
972 | C.AVariable (_,n,Some bo,ty,params) ->
973 (gen_id seed, params, None,
975 build_def_item seed (get_id bo) (C.Name n) bo
976 ~ids_to_inner_sorts ~ids_to_inner_types))
977 | C.AVariable (id,n,None,ty,params) ->
978 (gen_id seed, params, None,
980 build_decl_item seed id (C.Name n) ty
981 ~ids_to_inner_sorts))
982 | C.AInductiveDefinition (id,l,params,nparams) ->
983 (gen_id seed, params, None,
985 { joint_id = gen_id seed;
986 joint_kind = `Inductive nparams;
987 joint_defs = List.map (build_inductive seed) l
991 build_inductive seed =
994 { inductive_id = gen_id seed;
997 inductive_constructors = build_constructors seed l
1001 build_constructors seed l =
1004 { dec_name = Some n;
1005 dec_id = gen_id seed;
1006 dec_inductive = false;
1013 and 'term cinductiveType =
1014 id * string * bool * 'term * (* typename, inductive, arity *)
1015 'term cconstructor list (* constructors *)
1017 and 'term cconstructor =