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 type recursion_kind = NoRecursive | Recursive | CoRecursive;;
38 Def of id * id option * string * (* name, *)
39 'term option * 'term * (* body, type, *)
40 UriManager.uri list (* parameters *)
41 | Theorem of id * id option * string * (* name, *)
42 ('term proof) option * 'term * (* body, type, *)
43 UriManager.uri list (* parameters *)
45 string * 'term option * 'term * (* name, body, type *)
48 | CurrentProof of id * id *
49 string * annmetasenv * (* name, conjectures, *)
50 'term proof * 'term * UriManager.uri list (* value,type,parameters *)
52 | InductiveDefinition of id *
53 'term cinductiveType list * (* inductive types , *)
54 UriManager.uri list * int (* parameters,n ind. pars *)
56 and 'term cinductiveType =
57 id * string * bool * 'term * (* typename, inductive, arity *)
58 'term cconstructor list (* constructors *)
60 and 'term cconstructor =
61 string * 'term (* id, type *)
65 { proof_name : string option;
67 proof_kind : recursion_kind ;
68 proof_context : ('term context_element) list ;
69 proof_apply_context: ('term proof) list;
70 proof_conclude : 'term conclude_item;
73 'term context_element =
74 Declaration of 'term declaration
75 | Hypothesis of 'term declaration
76 | Proof of 'term proof
77 | Definition of 'term definition
78 | Joint of 'term joint
81 { dec_name : string option;
89 { def_name : string option;
97 joint_kind : recursion_kind ;
98 joint_defs : 'term context_element list
101 'term conclude_item =
102 { conclude_id :string;
103 conclude_aref : string;
104 conclude_method : string;
105 conclude_args : ('term arg) list ;
106 conclude_conclusion : 'term option
113 | ArgProof of 'term proof
114 | ArgMethod of string (* ???? *)
117 { premise_id: string;
118 premise_xref : string ;
119 premise_binder : string option;
120 premise_n : int option;
125 (* e se mettessi la conversione di BY nell'apply_context ? *)
126 (* sarebbe carino avere l'invariante che la proof2pres
127 generasse sempre prove con contesto vuoto *)
130 let res = "p" ^ string_of_int !seed in
135 let name_of = function
136 Cic.Anonymous -> None
137 | Cic.Name b -> Some b;;
139 exception Not_a_proof;;
140 exception NotImplemented;;
141 exception NotApplicable;;
144 (* we do not care for positivity, here, that in any case is enforced by
145 well typing. Just a brutal search *)
148 let module C = Cic in
154 | C.Implicit -> raise NotImplemented
155 | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
156 | C.Cast (te,ty) -> (occur uri te)
157 | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
158 | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
163 else (occur uri a)) false l
164 | C.Const (_,_) -> false
165 | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
166 | C.MutConstruct (_,_,_,_) -> false
167 | C.MutCase _ -> false (* presuming too much?? *)
168 | C.Fix _ -> false (* presuming too much?? *)
169 | C.CoFix (_,_) -> false (* presuming too much?? *)
173 let module C = Cic in
175 C.ARel (id,_,_,_) -> id
176 | C.AVar (id,_,_) -> id
177 | C.AMeta (id,_,_) -> id
178 | C.ASort (id,_) -> id
179 | C.AImplicit _ -> raise NotImplemented
180 | C.AProd (id,_,_,_) -> id
181 | C.ACast (id,_,_) -> id
182 | C.ALambda (id,_,_,_) -> id
183 | C.ALetIn (id,_,_,_) -> id
184 | C.AAppl (id,_) -> id
185 | C.AConst (id,_,_) -> id
186 | C.AMutInd (id,_,_,_) -> id
187 | C.AMutConstruct (id,_,_,_,_) -> id
188 | C.AMutCase (id,_,_,_,_,_) -> id
189 | C.AFix (id,_,_) -> id
190 | C.ACoFix (id,_,_) -> id
193 let test_for_lifting ~ids_to_inner_types =
194 let module C = Cic in
195 let module C2A = Cic2acic in
196 (* atomic terms are never lifted, according to my policy *)
198 C.ARel (id,_,_,_) -> false
199 | C.AVar (id,_,_) -> false
200 | C.AMeta (id,_,_) -> false
201 | C.ASort (id,_) -> false
202 | C.AImplicit _ -> raise NotImplemented
203 | C.AProd (id,_,_,_) -> false
204 | C.ACast (id,_,_) ->
206 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
208 with notfound -> false)
209 | C.ALambda (id,_,_,_) ->
211 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
213 with notfound -> false)
214 | C.ALetIn (id,_,_,_) ->
216 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
218 with notfound -> false)
221 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
223 with notfound -> false)
224 | C.AConst (id,_,_) ->
226 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
228 with notfound -> false)
229 | C.AMutInd (id,_,_,_) -> false
230 | C.AMutConstruct (id,_,_,_,_) ->
232 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
234 with notfound -> false)
236 | C.AMutCase (id,_,_,_,_,_) ->
238 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
240 with notfound -> false)
243 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
245 with notfound -> false)
246 | C.ACoFix (id,_,_) ->
248 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
250 with notfound -> false)
253 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
254 let module C = Cic in
255 let rec aux l subrpoofs =
259 if (test_for_lifting t ~ids_to_inner_types) then
260 (match subproofs with
265 { premise_id = gen_id seed;
266 premise_xref = p.proof_id;
267 premise_binder = p.proof_name;
270 in new_arg::(aux l1 tl))
274 C.ARel (idr,idref,n,b) ->
276 (try Hashtbl.find ids_to_inner_sorts idr
277 with notfound -> "Type") in
280 { premise_id = gen_id seed;
282 premise_binder = Some b;
287 hd::(aux l1 subproofs)
291 (* transform a proof p into a proof list, concatenating the last
292 conclude element to the apply_context list, in case context is
293 empty. Otherwise, it just returns [p] *)
296 if (p.proof_context = []) then
297 if p.proof_apply_context = [] then [p]
300 { proof_name = p.proof_name;
301 proof_id = gen_id seed;
302 proof_kind = NoRecursive;
304 proof_apply_context = [];
305 proof_conclude = p.proof_conclude;
307 p.proof_apply_context@[p1]
312 let rec serialize seed =
315 | p::tl -> (flat seed p)@(serialize seed tl);;
317 (* top_down = true if the term is a LAMBDA or a decl *)
318 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
319 let module C2A = Cic2acic in
320 let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
321 with Not_found -> None)
326 if inner_proof.proof_conclude.conclude_method = "Intros+LetTac" then
327 { proof_name = None ;
328 proof_id = gen_id seed;
329 proof_kind = NoRecursive;
331 proof_apply_context = [];
333 { conclude_id = gen_id seed;
335 conclude_method = "TD_Conversion";
336 conclude_args = [ArgProof inner_proof];
337 conclude_conclusion = Some expty
341 { proof_name = None ;
342 proof_id = gen_id seed;
343 proof_kind = NoRecursive;
345 proof_apply_context = [inner_proof];
347 { conclude_id = gen_id seed;
349 conclude_method = "BU_Conversion";
352 { premise_id = gen_id seed;
353 premise_xref = inner_proof.proof_id;
354 premise_binder = None;
358 conclude_conclusion = Some expty
363 let generate_exact seed t id name ~ids_to_inner_types =
364 let module C2A = Cic2acic in
367 proof_kind = NoRecursive;
369 proof_apply_context = [];
371 { conclude_id = gen_id seed;
373 conclude_method = "Exact";
374 conclude_args = [Term t];
375 conclude_conclusion =
376 try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
377 with notfound -> None
382 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
383 let module C2A = Cic2acic in
384 let module C = Cic in
387 proof_kind = NoRecursive;
389 proof_apply_context = [];
391 { conclude_id = gen_id seed;
393 conclude_method = "Intros+LetTac";
394 conclude_args = [ArgProof inner_proof];
395 conclude_conclusion =
397 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
399 (match inner_proof.proof_conclude.conclude_conclusion with
402 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
403 else Some (C.ALetIn ("gen"^id,n,s,t)))
408 let build_decl_item seed id n s ~ids_to_inner_sorts =
409 let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
410 if sort = "Prop" then
412 { dec_name = name_of n;
413 dec_id = gen_id seed;
414 dec_inductive = false;
420 { dec_name = name_of n;
421 dec_id = gen_id seed;
422 dec_inductive = false;
428 let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
429 let sort = Hashtbl.find ids_to_inner_sorts id in
430 if sort = "Prop" then
431 Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
434 { def_name = name_of n;
435 def_id = gen_id seed;
440 (* the following function must be called with an object of sort
441 Prop. For debugging purposes this is tested again, possibly raising an
442 Not_a_proof exception *)
444 and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
445 let rec aux ?(name = None) t =
446 let module C = Cic in
447 let module X = Xml in
448 let module U = UriManager in
449 let module C2A = Cic2acic in
452 C.ARel (id,idref,n,b) as t ->
453 let sort = Hashtbl.find ids_to_inner_sorts id in
454 if sort = "Prop" then
455 generate_exact seed t id name ~ids_to_inner_types
456 else raise Not_a_proof
457 | C.AVar (id,uri,exp_named_subst) as t ->
458 let sort = Hashtbl.find ids_to_inner_sorts id in
459 if sort = "Prop" then
460 generate_exact seed t id name ~ids_to_inner_types
461 else raise Not_a_proof
462 | C.AMeta (id,n,l) as t ->
463 let sort = Hashtbl.find ids_to_inner_sorts id in
464 if sort = "Prop" then
465 generate_exact seed t id name ~ids_to_inner_types
466 else raise Not_a_proof
467 | C.ASort (id,s) -> raise Not_a_proof
468 | C.AImplicit _ -> raise NotImplemented
469 | C.AProd (_,_,_,_) -> raise Not_a_proof
470 | C.ACast (id,v,t) -> aux v
471 | C.ALambda (id,n,s,t) ->
472 let sort = Hashtbl.find ids_to_inner_sorts id in
473 if sort = "Prop" then
474 let proof = aux t ~name:None in
476 if proof.proof_conclude.conclude_method = "Intros+LetTac" then
477 match proof.proof_conclude.conclude_args with
483 proof_id = proof'.proof_id;
484 proof_kind = proof'.proof_kind ;
486 (build_decl_item seed id n s ids_to_inner_sorts)::
487 proof'.proof_context;
488 proof_apply_context = proof'.proof_apply_context;
489 proof_conclude = proof'.proof_conclude;
492 generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
493 else raise Not_a_proof
494 | C.ALetIn (id,n,s,t) ->
495 let sort = Hashtbl.find ids_to_inner_sorts id in
496 if sort = "Prop" then
499 if proof.proof_conclude.conclude_method = "Intros+LetTac" then
500 match proof.proof_conclude.conclude_args with
506 proof_id = proof'.proof_id;
507 proof_kind = proof'.proof_kind ;
509 (build_def_item seed id n s ids_to_inner_sorts
510 ids_to_inner_types)::proof'.proof_context;
511 proof_apply_context = proof'.proof_apply_context;
512 proof_conclude = proof'.proof_conclude;
515 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
516 else raise Not_a_proof
519 seed name id li ids_to_inner_types ids_to_inner_sorts
520 with NotApplicable ->
522 seed name id li ids_to_inner_types ids_to_inner_sorts
523 with NotApplicable ->
525 List.filter (test_for_lifting ~ids_to_inner_types) li in
527 match args_to_lift with
528 [_] -> List.map aux args_to_lift
529 | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
530 let args = build_args seed li subproofs
531 ~ids_to_inner_types ~ids_to_inner_sorts in
533 proof_id = gen_id seed;
534 proof_kind = NoRecursive;
536 proof_apply_context = serialize seed subproofs;
538 { conclude_id = gen_id seed;
540 conclude_method = "Apply";
541 conclude_args = args;
542 conclude_conclusion =
544 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
545 with notfound -> None
548 | C.AConst (id,uri,exp_named_subst) as t ->
549 let sort = Hashtbl.find ids_to_inner_sorts id in
550 if sort = "Prop" then
551 generate_exact seed t id name ~ids_to_inner_types
552 else raise Not_a_proof
553 | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
554 | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
555 let sort = Hashtbl.find ids_to_inner_sorts id in
556 if sort = "Prop" then
557 generate_exact seed t id name ~ids_to_inner_types
558 else raise Not_a_proof
559 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
560 let teid = get_id te in
561 let pp = List.map (function p -> (ArgProof (aux p))) patterns in
563 (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
564 with notfound -> None)
566 Some tety -> (* we must lift up the argument *)
568 { proof_name = Some "name";
569 proof_id = gen_id seed;
570 proof_kind = NoRecursive;
572 proof_apply_context = flat seed p;
574 { conclude_id = gen_id seed;
576 conclude_method = "Case";
577 conclude_args = (Term ty)::(Term te)::pp;
578 conclude_conclusion =
580 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
581 with notfound -> None
586 proof_id = gen_id seed;
587 proof_kind = NoRecursive;
589 proof_apply_context = [];
591 { conclude_id = gen_id seed;
593 conclude_method = "Case";
594 conclude_args = (Term ty)::(Term te)::pp;
595 conclude_conclusion =
597 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
598 with notfound -> None
602 | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
603 let proof = (aux bo) in (* must be recursive !! *)
605 proof_id = gen_id seed;
606 proof_kind = NoRecursive;
607 proof_context = [Proof proof];
608 proof_apply_context = [];
610 { conclude_id = gen_id seed;
612 conclude_method = "Exact";
615 { premise_id = gen_id seed;
616 premise_xref = proof.proof_id;
617 premise_binder = proof.proof_name;
621 conclude_conclusion =
623 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
624 with notfound -> None
627 | C.AFix (id, no, funs) ->
629 List.map (function (id1,n,_,ty,bo) -> (Proof (aux bo))) funs in
631 { joint_id = gen_id seed;
632 joint_kind = Recursive;
637 proof_id = gen_id seed;
638 proof_kind = NoRecursive;
639 proof_context = [Joint jo];
640 proof_apply_context = [];
642 { conclude_id = gen_id seed;
644 conclude_method = "Exact";
647 { premise_id = gen_id seed;
648 premise_xref = jo.joint_id;
649 premise_binder = Some "tiralo fuori";
653 conclude_conclusion =
655 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
656 with notfound -> None
659 | C.ACoFix (id,no,[(id1,n,ty,bo)]) ->
660 let proof = (aux bo) in (* must be recursive !! *)
662 proof_id = gen_id seed;
663 proof_kind = NoRecursive;
664 proof_context = [Proof proof];
665 proof_apply_context = [];
667 { conclude_id = gen_id seed;
669 conclude_method = "Exact";
672 { premise_id = gen_id seed;
673 premise_xref = proof.proof_id;
674 premise_binder = proof.proof_name;
678 conclude_conclusion =
680 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
681 with notfound -> None
684 | C.ACoFix (id,no,funs) ->
686 List.map (function (id1,n,ty,bo) -> (Proof (aux bo))) funs in
688 { joint_id = gen_id seed;
689 joint_kind = Recursive;
694 proof_id = gen_id seed;
695 proof_kind = NoRecursive;
696 proof_context = [Joint jo];
697 proof_apply_context = [];
699 { conclude_id = gen_id seed;
701 conclude_method = "Exact";
704 { premise_id = gen_id seed;
705 premise_xref = jo.joint_id;
706 premise_binder = Some "tiralo fuori";
710 conclude_conclusion =
712 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
713 with notfound -> None
718 generate_conversion seed false id t1 ~ids_to_inner_types
721 and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
722 let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
723 let module C2A = Cic2acic in
724 let module C = Cic in
726 C.AConst (idc,uri,exp_named_subst)::args ->
727 let uri_str = UriManager.string_of_uri uri in
728 let suffix = Str.regexp_string "_ind.con" in
729 let len = String.length uri_str in
730 let n = (try (Str.search_backward suffix uri_str len)
731 with Not_found -> -1) in
732 if n<0 then raise NotApplicable
734 let prefix = String.sub uri_str 0 n in
735 let ind_str = (prefix ^ ".ind") in
736 let ind_uri = UriManager.uri_of_string ind_str in
737 let inductive_types,noparams =
738 (match CicEnvironment.get_obj ind_uri with
739 Cic.Constant _ -> assert false
740 | Cic.Variable _ -> assert false
741 | Cic.CurrentProof _ -> assert false
742 | Cic.InductiveDefinition (l,_,n) -> (l,n)
745 if n = 0 then ([],l) else
746 let p,a = split (n-1) (List.tl l) in
747 ((List.hd l::p),a) in
748 let params_and_IP,tail_args = split (noparams+1) args in
750 (match inductive_types with
752 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
754 let rec clean_up n t =
757 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
758 | _ -> assert false) in
759 List.map (clean_up noparams) constructors in
760 let no_constructors= List.length constructors in
761 let args_for_cases, other_args =
762 split no_constructors tail_args in
764 List.filter (test_for_lifting ~ids_to_inner_types) other_args in
766 match args_to_lift with
767 [_] -> List.map aux args_to_lift
768 | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
769 prerr_endline "****** end subproofs *******"; flush stderr;
770 let other_method_args =
771 build_args seed other_args subproofs
772 ~ids_to_inner_types ~ids_to_inner_sorts in
774 let rparams,inductive_arg =
779 | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
780 aux other_method_args in
782 prerr_endline "****** end other *******"; flush stderr;
784 let rec build_method_args =
786 [],_-> [] (* extra args are ignored ???? *)
787 | (name,ty)::tlc,arg::tla ->
788 let idarg = get_id arg in
790 (try (Hashtbl.find ids_to_inner_sorts idarg)
791 with Not_found -> "Type") in
793 if sortarg = "Prop" then
797 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
800 seed idl n s1 ~ids_to_inner_sorts in
801 if (occur ind_uri s) then
802 ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
804 Cic.ALambda(id2,n2,s2,t2) ->
807 { dec_name = name_of n2;
808 dec_id = gen_id seed;
809 dec_inductive = true;
813 let (context,body) = bc (t,t2) in
814 (ce::inductive_hyp::context,body)
817 ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
818 let (context,body) = bc (t,t1) in
820 | _ , t -> ([],aux t ~name:None) in
823 { proof_name = Some name;
824 proof_id = bo.proof_id;
825 proof_kind = NoRecursive;
827 proof_apply_context = bo.proof_apply_context;
828 proof_conclude = bo.proof_conclude;
831 hdarg::(build_method_args (tlc,tla))
832 | _ -> assert false in
833 build_method_args (constructors1,args_for_cases) in
835 proof_id = gen_id seed;
836 proof_kind = NoRecursive;
838 proof_apply_context = subproofs;
840 { conclude_id = gen_id seed;
842 conclude_method = "ByInduction";
845 ::Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
846 ::method_args@other_method_args;
847 conclude_conclusion =
849 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
850 with notfound -> None
853 | _ -> raise NotApplicable
855 and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
856 let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
857 let module C2A = Cic2acic in
858 let module C = Cic in
860 C.AConst (sid,uri,exp_named_subst)::args ->
861 let uri_str = UriManager.string_of_uri uri in
862 if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
863 uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
864 let subproof = aux (List.nth args 3) in
866 let rec ma_aux n = function
872 { premise_id = gen_id seed;
873 premise_xref = subproof.proof_id;
874 premise_binder = None;
878 let aid = get_id a in
879 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
880 with Not_found -> "Type") in
881 if asort = "Prop" then
884 hd::(ma_aux (n-1) tl) in
887 proof_id = gen_id seed;
888 proof_kind = NoRecursive;
890 proof_apply_context = [subproof];
892 { conclude_id = gen_id seed;
894 conclude_method = "Rewrite";
896 Term (C.AConst (sid,uri,exp_named_subst))::method_args;
897 conclude_conclusion =
899 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
900 with notfound -> None
903 else raise NotApplicable
904 | _ -> raise NotApplicable
907 let annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
908 let module C = Cic in
909 let module C2A = Cic2acic in
912 C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
913 assert false (* TO DO *)
914 | C.AConstant (id,idbody,n,bo,ty,params) ->
918 (try Hashtbl.find ids_to_inner_sorts idb
919 with notfound -> "Type") in
920 if sort = "Prop" then
924 acic2content seed ~name:None ~ids_to_inner_sorts
925 ~ids_to_inner_types body
926 | None -> assert false) in
927 Theorem(id,idbody,n,Some proof,ty,params)
929 Def(id,idbody,n,bo,ty,params)
930 | None -> Def(id,idbody,n,bo,ty,params))
931 | C.AVariable (id,n,bo,ty,params) ->
932 Variable(id,n,bo,ty,params)
933 | C.AInductiveDefinition (id,tys,params,nparams) ->
934 InductiveDefinition(id,tys,params,nparams)
937 and 'term cinductiveType =
938 id * string * bool * 'term * (* typename, inductive, arity *)
939 'term cconstructor list (* constructors *)
941 and 'term cconstructor =