1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (**************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (**************************************************************************)
35 (* e se mettessi la conversione di BY nell'apply_context ? *)
36 (* sarebbe carino avere l'invariante che la proof2pres
37 generasse sempre prove con contesto vuoto *)
40 let res = "p" ^ string_of_int !seed in
45 let name_of = function
47 | Cic.Name b -> Some b;;
49 exception Not_a_proof;;
50 exception NotImplemented;;
51 exception NotApplicable;;
53 (* we do not care for positivity, here, that in any case is enforced by
54 well typing. Just a brutal search *)
63 | C.Implicit -> raise NotImplemented
64 | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
65 | C.Cast (te,ty) -> (occur uri te)
66 | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
67 | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
72 else (occur uri a)) false l
73 | C.Const (_,_) -> false
74 | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
75 | C.MutConstruct (_,_,_,_) -> false
76 | C.MutCase _ -> false (* presuming too much?? *)
77 | C.Fix _ -> false (* presuming too much?? *)
78 | C.CoFix (_,_) -> false (* presuming too much?? *)
84 C.ARel (id,_,_,_) -> id
85 | C.AVar (id,_,_) -> id
86 | C.AMeta (id,_,_) -> id
87 | C.ASort (id,_) -> id
88 | C.AImplicit _ -> raise NotImplemented
89 | C.AProd (id,_,_,_) -> id
90 | C.ACast (id,_,_) -> id
91 | C.ALambda (id,_,_,_) -> id
92 | C.ALetIn (id,_,_,_) -> id
93 | C.AAppl (id,_) -> id
94 | C.AConst (id,_,_) -> id
95 | C.AMutInd (id,_,_,_) -> id
96 | C.AMutConstruct (id,_,_,_,_) -> id
97 | C.AMutCase (id,_,_,_,_,_) -> id
98 | C.AFix (id,_,_) -> id
99 | C.ACoFix (id,_,_) -> id
102 let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
103 let module C = Cic in
104 let module C2A = Cic2acic in
105 (* atomic terms are never lifted, according to my policy *)
107 C.ARel (id,_,_,_) -> false
110 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
112 with Not_found -> false)
113 | C.AMeta (id,_,_) ->
115 Hashtbl.find ids_to_inner_sorts id = "Prop"
116 with Not_found -> assert false)
117 | C.ASort (id,_) -> false
118 | C.AImplicit _ -> raise NotImplemented
119 | C.AProd (id,_,_,_) -> false
120 | C.ACast (id,_,_) ->
122 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
124 with Not_found -> false)
125 | C.ALambda (id,_,_,_) ->
127 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
129 with Not_found -> false)
130 | C.ALetIn (id,_,_,_) ->
132 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
134 with Not_found -> false)
137 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
139 with Not_found -> false)
140 | C.AConst (id,_,_) ->
142 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
144 with Not_found -> false)
145 | C.AMutInd (id,_,_,_) -> false
146 | C.AMutConstruct (id,_,_,_,_) ->
148 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
150 with Not_found -> false)
152 | C.AMutCase (id,_,_,_,_,_) ->
154 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
156 with Not_found -> false)
159 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
161 with Not_found -> false)
162 | C.ACoFix (id,_,_) ->
164 ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
166 with Not_found -> false)
170 let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
171 let module C = Cic in
172 let module K = Content in
173 let rec aux l subproofs =
177 if (test_for_lifting t ~ids_to_inner_types) then
178 (match subproofs with
183 { K.premise_id = gen_id seed;
184 K.premise_xref = p.K.proof_id;
185 K.premise_binder = p.K.proof_name;
188 in new_arg::(aux l1 tl))
192 C.ARel (idr,idref,n,b) ->
194 (try Hashtbl.find ids_to_inner_sorts idr
195 with Not_found -> "Type") in
198 { K.premise_id = gen_id seed;
199 K.premise_xref = idr;
200 K.premise_binder = Some b;
204 | _ -> (K.Term t)) in
205 hd::(aux l1 subproofs)
210 (* transform a proof p into a proof list, concatenating the last
211 conclude element to the apply_context list, in case context is
212 empty. Otherwise, it just returns [p] *)
215 let module K = Content in
216 if (p.K.proof_context = []) then
217 if p.K.proof_apply_context = [] then [p]
221 K.proof_context = [];
222 K.proof_apply_context = []
224 p.K.proof_apply_context@[p1]
229 let rec serialize seed =
232 | a::l -> (flat seed a)@(serialize seed l)
235 (* top_down = true if the term is a LAMBDA or a decl *)
236 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
237 let module C2A = Cic2acic in
238 let module K = Content in
239 let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
240 with Not_found -> None)
245 if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
246 { K.proof_name = inner_proof.K.proof_name;
247 K.proof_id = gen_id seed;
248 K.proof_context = [] ;
249 K.proof_apply_context = [];
251 { K.conclude_id = gen_id seed;
252 K.conclude_aref = id;
253 K.conclude_method = "TD_Conversion";
255 [K.ArgProof {inner_proof with K.proof_name = None}];
256 K.conclude_conclusion = Some expty
260 { K.proof_name = None ;
261 K.proof_id = gen_id seed;
262 K.proof_context = [] ;
263 K.proof_apply_context = [inner_proof];
265 { K.conclude_id = gen_id seed;
266 K.conclude_aref = id;
267 K.conclude_method = "BU_Conversion";
270 { K.premise_id = gen_id seed;
271 K.premise_xref = inner_proof.K.proof_id;
272 K.premise_binder = None;
276 K.conclude_conclusion = Some expty
281 let generate_exact seed t id name ~ids_to_inner_types =
282 let module C2A = Cic2acic in
283 let module K = Content in
284 { K.proof_name = name;
286 K.proof_context = [] ;
287 K.proof_apply_context = [];
289 { K.conclude_id = gen_id seed;
290 K.conclude_aref = id;
291 K.conclude_method = "Exact";
292 K.conclude_args = [K.Term t];
293 K.conclude_conclusion =
294 try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
295 with Not_found -> None
300 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
301 let module C2A = Cic2acic in
302 let module C = Cic in
303 let module K = Content in
304 { K.proof_name = name;
306 K.proof_context = [] ;
307 K.proof_apply_context = [];
309 { K.conclude_id = gen_id seed;
310 K.conclude_aref = id;
311 K.conclude_method = "Intros+LetTac";
312 K.conclude_args = [K.ArgProof inner_proof];
313 K.conclude_conclusion =
315 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
317 (match inner_proof.K.proof_conclude.K.conclude_conclusion with
320 if is_intro then Some (C.AProd ("gen"^id,n,s,t))
321 else Some (C.ALetIn ("gen"^id,n,s,t)))
326 let build_decl_item seed id n s ~ids_to_inner_sorts =
327 let module K = Content in
329 let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
330 if sort = "Prop" then
332 { K.dec_name = name_of n;
333 K.dec_id = gen_id seed;
334 K.dec_inductive = false;
340 { K.dec_name = name_of n;
341 K.dec_id = gen_id seed;
342 K.dec_inductive = false;
347 Not_found -> assert false
350 let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
351 let module C = Cic in
352 let module K = Content in
357 let subproofs,args = aux l1 in
358 if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
361 seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
364 { K.premise_id = gen_id seed;
365 K.premise_xref = new_subproof.K.proof_id;
366 K.premise_binder = new_subproof.K.proof_name;
369 new_subproof::subproofs,new_arg::args
373 C.ARel (idr,idref,n,b) ->
375 (try Hashtbl.find ids_to_inner_sorts idr
376 with Not_found -> "Type") in
379 { K.premise_id = gen_id seed;
380 K.premise_xref = idr;
381 K.premise_binder = Some b;
385 | C.AConst(id,uri,[]) ->
387 (try Hashtbl.find ids_to_inner_sorts id
388 with Not_found -> "Type") in
391 { K.lemma_id = gen_id seed;
392 K.lemma_name = UriManager.name_of_uri uri;
393 K.lemma_uri = UriManager.string_of_uri uri
396 | C.AMutConstruct(id,uri,tyno,consno,[]) ->
398 (try Hashtbl.find ids_to_inner_sorts id
399 with Not_found -> "Type") in
401 let inductive_types =
402 (match CicEnvironment.get_obj uri with
403 Cic.Constant _ -> assert false
404 | Cic.Variable _ -> assert false
405 | Cic.CurrentProof _ -> assert false
406 | Cic.InductiveDefinition (l,_,_) -> l
408 let (_,_,_,constructors) =
409 List.nth inductive_types tyno in
410 let name,_ = List.nth constructors (consno - 1) in
412 { K.lemma_id = gen_id seed;
415 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
416 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
420 | _ -> (K.Term t)) in
425 [{p with K.proof_name = None}],
428 K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
429 K.Premise {prem with K.premise_binder = None}
435 build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
436 let module K = Content in
438 let sort = Hashtbl.find ids_to_inner_sorts id in
439 if sort = "Prop" then
440 `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
443 { K.def_name = name_of n;
444 K.def_id = gen_id seed;
449 Not_found -> assert false
451 (* the following function must be called with an object of sort
452 Prop. For debugging purposes this is tested again, possibly raising an
453 Not_a_proof exception *)
455 and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
456 let rec aux ?name t =
457 let module C = Cic in
458 let module K = Content in
459 let module C2A = Cic2acic in
462 C.ARel (id,idref,n,b) 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.AVar (id,uri,exp_named_subst) as t ->
468 let sort = Hashtbl.find ids_to_inner_sorts id in
469 if sort = "Prop" then
470 generate_exact seed t id name ~ids_to_inner_types
471 else raise Not_a_proof
472 | C.AMeta (id,n,l) as t ->
473 let sort = Hashtbl.find ids_to_inner_sorts id in
474 if sort = "Prop" then
475 generate_exact seed t id name ~ids_to_inner_types
476 else raise Not_a_proof
477 | C.ASort (id,s) -> raise Not_a_proof
478 | C.AImplicit _ -> raise NotImplemented
479 | C.AProd (_,_,_,_) -> raise Not_a_proof
480 | C.ACast (id,v,t) -> aux v
481 | C.ALambda (id,n,s,t) ->
482 let sort = Hashtbl.find ids_to_inner_sorts id in
483 if sort = "Prop" then
486 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
487 match proof.K.proof_conclude.K.conclude_args with
495 (build_decl_item seed id n s ids_to_inner_sorts)::
496 proof'.K.proof_context
499 generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
500 else raise Not_a_proof
501 | C.ALetIn (id,n,s,t) ->
502 let sort = Hashtbl.find ids_to_inner_sorts id in
503 if sort = "Prop" then
506 if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
507 match proof.K.proof_conclude.K.conclude_args with
515 ((build_def_item seed id n s ids_to_inner_sorts
516 ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
517 ::proof'.K.proof_context;
520 generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
521 else raise Not_a_proof
524 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
525 with NotApplicable ->
527 seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
528 with NotApplicable ->
529 let subproofs, args =
530 build_subproofs_and_args
531 seed li ~ids_to_inner_types ~ids_to_inner_sorts in
534 List.filter (test_for_lifting ~ids_to_inner_types) li in
536 match args_to_lift with
537 [_] -> List.map aux args_to_lift
538 | _ -> List.map (aux ~name:"H") args_to_lift in
539 let args = build_args seed li subproofs
540 ~ids_to_inner_types ~ids_to_inner_sorts in *)
541 { K.proof_name = name;
542 K.proof_id = gen_id seed;
543 K.proof_context = [];
544 K.proof_apply_context = serialize seed subproofs;
546 { K.conclude_id = gen_id seed;
547 K.conclude_aref = id;
548 K.conclude_method = "Apply";
549 K.conclude_args = args;
550 K.conclude_conclusion =
552 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
553 with Not_found -> None
556 | C.AConst (id,uri,exp_named_subst) as t ->
557 let sort = Hashtbl.find ids_to_inner_sorts id in
558 if sort = "Prop" then
559 generate_exact seed t id name ~ids_to_inner_types
560 else raise Not_a_proof
561 | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
562 | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
563 let sort = Hashtbl.find ids_to_inner_sorts id in
564 if sort = "Prop" then
565 generate_exact seed t id name ~ids_to_inner_types
566 else raise Not_a_proof
567 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
568 let inductive_types =
569 (match CicEnvironment.get_obj uri with
570 Cic.Constant _ -> assert false
571 | Cic.Variable _ -> assert false
572 | Cic.CurrentProof _ -> assert false
573 | Cic.InductiveDefinition (l,_,_) -> l
575 let (_,_,_,constructors) = List.nth inductive_types typeno in
576 let teid = get_id te in
578 (fun p (name,_) -> (K.ArgProof (aux ~name p)))
579 patterns constructors in
582 build_subproofs_and_args
583 seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
586 | _ -> assert false) in
587 { K.proof_name = name;
588 K.proof_id = gen_id seed;
589 K.proof_context = [];
590 K.proof_apply_context = serialize seed context;
592 { K.conclude_id = gen_id seed;
593 K.conclude_aref = id;
594 K.conclude_method = "Case";
596 (K.Aux (UriManager.string_of_uri uri))::
597 (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
598 K.conclude_conclusion =
600 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
601 with Not_found -> None
604 | C.AFix (id, no, funs) ->
607 (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
608 let decreasing_args =
609 List.map (function (_,_,n,_,_) -> n) funs in
611 { K.joint_id = gen_id seed;
612 K.joint_kind = `Recursive decreasing_args;
613 K.joint_defs = proofs
616 { K.proof_name = name;
617 K.proof_id = gen_id seed;
618 K.proof_context = [`Joint jo];
619 K.proof_apply_context = [];
621 { K.conclude_id = gen_id seed;
622 K.conclude_aref = id;
623 K.conclude_method = "Exact";
626 { K.premise_id = gen_id seed;
627 K.premise_xref = jo.K.joint_id;
628 K.premise_binder = Some "tiralo fuori";
629 K.premise_n = Some no;
632 K.conclude_conclusion =
634 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
635 with Not_found -> None
638 | C.ACoFix (id,no,funs) ->
641 (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
643 { K.joint_id = gen_id seed;
644 K.joint_kind = `CoRecursive;
645 K.joint_defs = proofs
648 { K.proof_name = name;
649 K.proof_id = gen_id seed;
650 K.proof_context = [`Joint jo];
651 K.proof_apply_context = [];
653 { K.conclude_id = gen_id seed;
654 K.conclude_aref = id;
655 K.conclude_method = "Exact";
658 { K.premise_id = gen_id seed;
659 K.premise_xref = jo.K.joint_id;
660 K.premise_binder = Some "tiralo fuori";
661 K.premise_n = Some no;
664 K.conclude_conclusion =
666 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
667 with Not_found -> None
672 generate_conversion seed false id t1 ~ids_to_inner_types
675 and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
676 let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
677 let module C2A = Cic2acic in
678 let module K = Content in
679 let module C = Cic in
681 C.AConst (idc,uri,exp_named_subst)::args ->
682 let uri_str = UriManager.string_of_uri uri in
683 let suffix = Str.regexp_string "_ind.con" in
684 let len = String.length uri_str in
685 let n = (try (Str.search_backward suffix uri_str len)
686 with Not_found -> -1) in
687 if n<0 then raise NotApplicable
689 let prefix = String.sub uri_str 0 n in
690 let ind_str = (prefix ^ ".ind") in
691 let ind_uri = UriManager.uri_of_string ind_str in
692 let inductive_types,noparams =
693 (match CicEnvironment.get_obj ind_uri with
694 Cic.Constant _ -> assert false
695 | Cic.Variable _ -> assert false
696 | Cic.CurrentProof _ -> assert false
697 | Cic.InductiveDefinition (l,_,n) -> (l,n)
700 if n = 0 then ([],l) else
701 let p,a = split (n-1) (List.tl l) in
702 ((List.hd l::p),a) in
703 let params_and_IP,tail_args = split (noparams+1) args in
705 (match inductive_types with
707 | _ -> raise NotApplicable) (* don't care for mutual ind *) in
709 let rec clean_up n t =
712 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
713 | _ -> assert false) in
714 List.map (clean_up noparams) constructors in
715 let no_constructors= List.length constructors in
716 let args_for_cases, other_args =
717 split no_constructors tail_args in
718 let subproofs,other_method_args =
719 build_subproofs_and_args seed other_args
720 ~ids_to_inner_types ~ids_to_inner_sorts in
721 prerr_endline "****** end other *******"; flush stderr;
723 let rec build_method_args =
725 [],_-> [] (* extra args are ignored ???? *)
726 | (name,ty)::tlc,arg::tla ->
727 let idarg = get_id arg in
729 (try (Hashtbl.find ids_to_inner_sorts idarg)
730 with Not_found -> "Type") in
732 if sortarg = "Prop" then
736 Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
739 seed idl n s1 ~ids_to_inner_sorts in
740 if (occur ind_uri s) then
741 ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
743 Cic.ALambda(id2,n2,s2,t2) ->
746 { K.dec_name = name_of n2;
747 K.dec_id = gen_id seed;
748 K.dec_inductive = true;
752 let (context,body) = bc (t,t2) in
753 (ce::inductive_hyp::context,body)
756 ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
757 let (context,body) = bc (t,t1) in
759 | _ , t -> ([],aux t) in
763 K.proof_name = Some name;
764 K.proof_context = co;
767 hdarg::(build_method_args (tlc,tla))
768 | _ -> assert false in
769 build_method_args (constructors1,args_for_cases) in
770 { K.proof_name = None;
771 K.proof_id = gen_id seed;
772 K.proof_context = [];
773 K.proof_apply_context = serialize seed subproofs;
775 { K.conclude_id = gen_id seed;
776 K.conclude_aref = id;
777 K.conclude_method = "ByInduction";
779 K.Aux (string_of_int no_constructors)
780 ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
781 ::method_args@other_method_args;
782 K.conclude_conclusion =
784 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
785 with Not_found -> None
788 | _ -> raise NotApplicable
790 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
791 let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
792 let module C2A = Cic2acic in
793 let module K = Content in
794 let module C = Cic in
796 C.AConst (sid,uri,exp_named_subst)::args ->
797 let uri_str = UriManager.string_of_uri uri in
798 if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
799 uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
802 build_subproofs_and_args
803 seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
806 | _,_ -> assert false) in
808 let rec ma_aux n = function
814 let aid = get_id a in
815 let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
816 with Not_found -> "Type") in
817 if asort = "Prop" then
820 hd::(ma_aux (n-1) tl) in
822 { K.proof_name = None;
823 K.proof_id = gen_id seed;
824 K.proof_context = [];
825 K.proof_apply_context = serialize seed subproofs;
827 { K.conclude_id = gen_id seed;
828 K.conclude_aref = id;
829 K.conclude_method = "Rewrite";
831 K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
832 K.conclude_conclusion =
834 (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
835 with Not_found -> None
838 else raise NotApplicable
839 | _ -> raise NotApplicable
843 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
845 let module K = Content in
849 (id,None) as item -> item
850 | (id,Some (name,Cic.ADecl t)) ->
853 (* We should call build_decl_item, but we have not computed *)
854 (* the inner-types ==> we always produce a declaration *)
856 { K.dec_name = name_of name;
857 K.dec_id = gen_id seed;
858 K.dec_inductive = false;
859 K.dec_aref = get_id t;
862 | (id,Some (name,Cic.ADef t)) ->
865 (* We should call build_def_item, but we have not computed *)
866 (* the inner-types ==> we always produce a declaration *)
868 { K.def_name = name_of name;
869 K.def_id = gen_id seed;
870 K.def_aref = get_id t;
878 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
879 let module C = Cic in
880 let module K = Content in
881 let module C2A = Cic2acic in
884 C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
885 (gen_id seed, params,
888 (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
891 build_def_item seed (get_id bo) (C.Name n) bo
892 ~ids_to_inner_sorts ~ids_to_inner_types))
893 | C.AConstant (_,_,n,Some bo,ty,params) ->
894 (gen_id seed, params, None,
896 build_def_item seed (get_id bo) (C.Name n) bo
897 ~ids_to_inner_sorts ~ids_to_inner_types))
898 | C.AConstant (id,_,n,None,ty,params) ->
899 (gen_id seed, params, None,
901 build_decl_item seed id (C.Name n) ty
902 ~ids_to_inner_sorts))
903 | C.AVariable (_,n,Some bo,ty,params) ->
904 (gen_id seed, params, None,
906 build_def_item seed (get_id bo) (C.Name n) bo
907 ~ids_to_inner_sorts ~ids_to_inner_types))
908 | C.AVariable (id,n,None,ty,params) ->
909 (gen_id seed, params, None,
911 build_decl_item seed id (C.Name n) ty
912 ~ids_to_inner_sorts))
913 | C.AInductiveDefinition (id,l,params,nparams) ->
914 (gen_id seed, params, None,
916 { K.joint_id = gen_id seed;
917 K.joint_kind = `Inductive nparams;
918 K.joint_defs = List.map (build_inductive seed) l
922 build_inductive seed =
923 let module K = Content in
926 { K.inductive_id = gen_id seed;
927 K.inductive_kind = b;
928 K.inductive_type = ty;
929 K.inductive_constructors = build_constructors seed l
933 build_constructors seed l =
934 let module K = Content in
937 { K.dec_name = Some n;
938 K.dec_id = gen_id seed;
939 K.dec_inductive = false;
946 and 'term cinductiveType =
947 id * string * bool * 'term * (* typename, inductive, arity *)
948 'term cconstructor list (* constructors *)
950 and 'term cconstructor =