]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/acic_content/acic2content.ml
"21" -> "Implicit found"
[helm.git] / helm / software / components / acic_content / acic2content.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (**************************************************************************)
27 (*                                                                        *)
28 (*                           PROJECT HELM                                 *)
29 (*                                                                        *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
31 (*                             16/6/2003                                   *)
32 (*                                                                        *)
33 (**************************************************************************)
34
35 (* $Id$ *)
36
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:";;
46
47 let hide_coercions = ref true;;
48
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 *)
52  
53 let gen_id prefix seed =
54  let res = prefix ^ string_of_int !seed in
55   incr seed ;
56   res
57 ;;
58
59 let name_of = function
60     Cic.Anonymous -> None
61   | Cic.Name b -> Some b;;
62  
63 exception Not_a_proof;;
64 exception NotImplemented;;
65 exception NotApplicable;;
66    
67 (* we do not care for positivity, here, that in any case is enforced by
68    well typing. Just a brutal search *)
69
70 let rec occur uri = 
71   let module C = Cic in
72   function
73       C.Rel _ -> false
74     | C.Var _ -> false
75     | C.Meta _ -> false
76     | C.Sort _ -> false
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)
82     | C.Appl l -> 
83         List.fold_left 
84           (fun b a -> 
85              if b then b  
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?? *)
93 ;;
94
95 let get_id = 
96   let module C = Cic in
97   function
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
114 ;;
115
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 *)
120   function
121       C.ARel (id,_,_,_) -> false
122     | C.AVar (id,_,_) -> 
123          (try 
124             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
125             true;
126           with Not_found -> false) 
127     | C.AMeta (id,_,_) -> 
128          (try 
129             Hashtbl.find ids_to_inner_sorts id = `Prop
130           with Not_found -> assert false)
131     | C.ASort (id,_) -> false
132     | C.AImplicit _ -> raise NotImplemented
133     | C.AProd (id,_,_,_) -> false
134     | C.ACast (id,_,_) -> 
135          (try 
136             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
137             true;
138           with Not_found -> false)
139     | C.ALambda (id,_,_,_) -> 
140          (try 
141             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
142             true;
143           with Not_found -> false)
144     | C.ALetIn (id,_,_,_) -> 
145          (try 
146             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
147             true;
148           with Not_found -> false)
149     | C.AAppl (id,_) ->
150          (try 
151             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
152             true;
153           with Not_found -> false) 
154     | C.AConst (id,_,_) -> 
155          (try 
156             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
157             true;
158           with Not_found -> false) 
159     | C.AMutInd (id,_,_,_) -> false
160     | C.AMutConstruct (id,_,_,_,_) -> 
161        (try 
162             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
163             true;
164           with Not_found -> false)
165         (* oppure: false *)
166     | C.AMutCase (id,_,_,_,_,_) ->
167          (try 
168             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
169             true;
170           with Not_found -> false)
171     | C.AFix (id,_,_) ->
172           (try 
173             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
174             true;
175           with Not_found -> false)
176     | C.ACoFix (id,_,_) ->
177          (try 
178             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
179             true;
180           with Not_found -> false)
181 ;;
182
183 (* transform a proof p into a proof list, concatenating the last 
184 conclude element to the apply_context list, in case context is
185 empty. Otherwise, it just returns [p] *)
186
187 let flat seed p = 
188  let module K = Content in
189   if (p.K.proof_context = []) then
190     if p.K.proof_apply_context = [] then [p]
191     else 
192       let p1 =
193         { p with
194           K.proof_context = []; 
195           K.proof_apply_context = []
196         } in
197       p.K.proof_apply_context@[p1]
198   else 
199     [p]
200 ;;
201
202 let rec serialize seed = 
203   function 
204     [] -> []
205   | a::l -> (flat seed a)@(serialize seed l) 
206 ;;
207
208 (* top_down = true if the term is a LAMBDA or a decl *)
209 let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
210  let module C2A = Cic2acic in
211  let module K = Content in
212  let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
213             with Not_found -> None)
214  in
215  match exp with
216      None -> inner_proof
217    | Some expty ->
218        if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
219          { K.proof_name = inner_proof.K.proof_name;
220             K.proof_id   = gen_id proof_prefix seed;
221             K.proof_context = [] ;
222             K.proof_apply_context = [];
223             K.proof_conclude = 
224               { K.conclude_id = gen_id conclude_prefix seed; 
225                 K.conclude_aref = id;
226                 K.conclude_method = "TD_Conversion";
227                 K.conclude_args = 
228                   [K.ArgProof {inner_proof with K.proof_name = None}];
229                 K.conclude_conclusion = Some expty
230               };
231           }
232         else
233           { K.proof_name =  inner_proof.K.proof_name;
234             K.proof_id   = gen_id proof_prefix seed;
235             K.proof_context = [] ;
236             K.proof_apply_context = [{inner_proof with K.proof_name = None}];
237             K.proof_conclude = 
238               { K.conclude_id = gen_id conclude_prefix seed; 
239                 K.conclude_aref = id;
240                 K.conclude_method = "BU_Conversion";
241                 K.conclude_args =  
242                  [K.Premise 
243                   { K.premise_id = gen_id premise_prefix seed;
244                     K.premise_xref = inner_proof.K.proof_id; 
245                     K.premise_binder = None;
246                     K.premise_n = None
247                   } 
248                  ]; 
249                 K.conclude_conclusion = Some expty
250               };
251           }
252 ;;
253
254 let generate_exact seed t id name ~ids_to_inner_types =
255   let module C2A = Cic2acic in
256   let module K = Content in
257     { K.proof_name = name;
258       K.proof_id   = gen_id proof_prefix seed ;
259       K.proof_context = [] ;
260       K.proof_apply_context = [];
261       K.proof_conclude = 
262         { K.conclude_id = gen_id conclude_prefix seed; 
263           K.conclude_aref = id;
264           K.conclude_method = "Exact";
265           K.conclude_args = [K.Term t];
266           K.conclude_conclusion = 
267               try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
268               with Not_found -> None
269         };
270     }
271 ;;
272
273 let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
274   let module C2A = Cic2acic in
275   let module C = Cic in
276   let module K = Content in
277     { K.proof_name = name;
278       K.proof_id  = gen_id proof_prefix seed ;
279       K.proof_context = [] ;
280       K.proof_apply_context = [];
281       K.proof_conclude = 
282         { K.conclude_id = gen_id conclude_prefix seed; 
283           K.conclude_aref = id;
284           K.conclude_method = "Intros+LetTac";
285           K.conclude_args = [K.ArgProof inner_proof];
286           K.conclude_conclusion = 
287             try Some 
288              (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
289             with Not_found -> 
290               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
291                  None -> None
292               | Some t -> 
293                   if is_intro then Some (C.AProd ("gen"^id,n,s,t))
294                   else Some (C.ALetIn ("gen"^id,n,s,t)))
295         };
296     }
297 ;;
298
299 let build_decl_item seed id n s ~ids_to_inner_sorts =
300  let module K = Content in
301  let sort =
302    try
303     Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
304    with Not_found -> None
305  in
306  match sort with
307  | Some `Prop ->
308     `Hypothesis
309       { K.dec_name = name_of n;
310         K.dec_id = gen_id declaration_prefix seed; 
311         K.dec_inductive = false;
312         K.dec_aref = id;
313         K.dec_type = s
314       }
315  | _ ->
316     `Declaration
317       { K.dec_name = name_of n;
318         K.dec_id = gen_id declaration_prefix seed; 
319         K.dec_inductive = false;
320         K.dec_aref = id;
321         K.dec_type = s
322       }
323 ;;
324
325 let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
326   let module C = Cic in
327   let module K = Content in
328   let rec aux =
329     function
330       [] -> [],[]
331     | t::l1 -> 
332        let subproofs,args = aux l1 in
333         if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
334           let new_subproof = 
335             acic2content 
336               seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
337           let new_arg = 
338             K.Premise
339               { K.premise_id = gen_id premise_prefix seed;
340                 K.premise_xref = new_subproof.K.proof_id;
341                 K.premise_binder = new_subproof.K.proof_name;
342                 K.premise_n = None
343               } in
344           new_subproof::subproofs,new_arg::args
345         else 
346           let hd = 
347             (match t with 
348                C.ARel (idr,idref,n,b) ->
349                  let sort = 
350                    (try
351                      Hashtbl.find ids_to_inner_sorts idr 
352                     with Not_found -> `Type (CicUniv.fresh())) in 
353                  if sort = `Prop then 
354                     K.Premise 
355                       { K.premise_id = gen_id premise_prefix seed;
356                         K.premise_xref = idr;
357                         K.premise_binder = Some b;
358                         K.premise_n = Some n
359                       }
360                  else (K.Term t)
361              | C.AConst(id,uri,[]) ->
362                  let sort = 
363                    (try
364                      Hashtbl.find ids_to_inner_sorts id 
365                     with Not_found -> `Type (CicUniv.fresh())) in 
366                  if sort = `Prop then 
367                     K.Lemma 
368                       { K.lemma_id = gen_id lemma_prefix seed;
369                         K.lemma_name = UriManager.name_of_uri uri;
370                         K.lemma_uri = UriManager.string_of_uri uri
371                       }
372                  else (K.Term t)
373              | C.AMutConstruct(id,uri,tyno,consno,[]) ->
374                  let sort = 
375                    (try
376                      Hashtbl.find ids_to_inner_sorts id 
377                     with Not_found -> `Type (CicUniv.fresh())) in 
378                  if sort = `Prop then 
379                     let inductive_types =
380                       (let o,_ = 
381                          CicEnvironment.get_obj CicUniv.empty_ugraph uri
382                        in
383                          match o with 
384                            | Cic.InductiveDefinition (l,_,_,_) -> l 
385                            | _ -> assert false
386                       ) in
387                     let (_,_,_,constructors) = 
388                       List.nth inductive_types tyno in 
389                     let name,_ = List.nth constructors (consno - 1) in
390                     K.Lemma 
391                       { K.lemma_id = gen_id lemma_prefix seed;
392                         K.lemma_name = name;
393                         K.lemma_uri = 
394                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
395                           string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
396                           ")"
397                       }
398                  else (K.Term t) 
399              | _ -> (K.Term t)) in
400           subproofs,hd::args
401   in 
402   match (aux l) with
403     [p],args -> 
404       [{p with K.proof_name = None}], 
405         List.map 
406           (function 
407               K.Premise prem when prem.K.premise_xref = p.K.proof_id ->
408                K.Premise {prem with K.premise_binder = None}
409             | i -> i) args
410   | p,a as c -> c
411
412 and
413
414 build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
415  let module K = Content in
416   try
417    let sort = Hashtbl.find ids_to_inner_sorts id in
418    if sort = `Prop then
419        (let p = 
420         (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
421        in 
422         `Proof p;)
423    else 
424       `Definition
425         { K.def_name = name_of n;
426           K.def_id = gen_id definition_prefix seed; 
427           K.def_aref = id;
428           K.def_term = t
429         }
430   with
431    Not_found -> assert false
432
433 (* the following function must be called with an object of sort
434 Prop. For debugging purposes this is tested again, possibly raising an 
435 Not_a_proof exception *)
436
437 and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
438   let rec aux ?name t =
439   let module C = Cic in
440   let module K = Content in
441   let module C2A = Cic2acic in
442   let t1 =
443     match t with 
444       C.ARel (id,idref,n,b) as t ->
445         let sort = Hashtbl.find ids_to_inner_sorts id in
446         if sort = `Prop then
447           generate_exact seed t id name ~ids_to_inner_types 
448         else raise Not_a_proof
449     | C.AVar (id,uri,exp_named_subst) as t ->
450         let sort = Hashtbl.find ids_to_inner_sorts id in
451         if sort = `Prop then
452           generate_exact seed t id name ~ids_to_inner_types 
453         else raise Not_a_proof
454     | C.AMeta (id,n,l) as t ->
455         let sort = Hashtbl.find ids_to_inner_sorts id in
456         if sort = `Prop then
457           generate_exact seed t id name ~ids_to_inner_types 
458         else raise Not_a_proof
459     | C.ASort (id,s) -> raise Not_a_proof
460     | C.AImplicit _ -> raise NotImplemented
461     | C.AProd (_,_,_,_) -> raise Not_a_proof
462     | C.ACast (id,v,t) -> aux v
463     | C.ALambda (id,n,s,t) -> 
464         let sort = Hashtbl.find ids_to_inner_sorts id in
465         if sort = `Prop then 
466           let proof = aux t in
467           let proof' = 
468             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
469                match proof.K.proof_conclude.K.conclude_args with
470                  [K.ArgProof p] -> p
471                | _ -> assert false                  
472             else proof in
473           let proof'' =
474             { proof' with
475               K.proof_name = None;
476               K.proof_context = 
477                 (build_decl_item seed id n s ids_to_inner_sorts)::
478                   proof'.K.proof_context
479             }
480           in
481           generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
482         else raise Not_a_proof 
483     | C.ALetIn (id,n,s,t) ->
484         let sort = Hashtbl.find ids_to_inner_sorts id in
485         if sort = `Prop then
486           let proof = aux t in
487           let proof' = 
488             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
489                match proof.K.proof_conclude.K.conclude_args with
490                  [K.ArgProof p] -> p
491                | _ -> assert false                  
492             else proof in
493           let proof'' =
494             { proof' with
495                K.proof_name = None;
496                K.proof_context = 
497                  ((build_def_item seed id n s ids_to_inner_sorts 
498                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
499                  ::proof'.K.proof_context;
500             }
501           in
502           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
503         else raise Not_a_proof 
504     | C.AAppl (id,li) ->
505         (try coercion 
506            seed li ~ids_to_inner_types ~ids_to_inner_sorts
507          with NotApplicable ->
508          try rewrite 
509            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
510          with NotApplicable ->
511          try inductive 
512           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
513          with NotApplicable ->
514          try transitivity 
515            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
516          with NotApplicable ->
517           let subproofs, args =
518             build_subproofs_and_args 
519               seed li ~ids_to_inner_types ~ids_to_inner_sorts in
520 (*            
521           let args_to_lift = 
522             List.filter (test_for_lifting ~ids_to_inner_types) li in
523           let subproofs = 
524             match args_to_lift with
525                 [_] -> List.map aux args_to_lift 
526             | _ -> List.map (aux ~name:"H") args_to_lift in
527           let args = build_args seed li subproofs 
528                  ~ids_to_inner_types ~ids_to_inner_sorts in *)
529             { K.proof_name = name;
530               K.proof_id   = gen_id proof_prefix seed;
531               K.proof_context = [];
532               K.proof_apply_context = serialize seed subproofs;
533               K.proof_conclude = 
534                 { K.conclude_id = gen_id conclude_prefix seed;
535                   K.conclude_aref = id;
536                   K.conclude_method = "Apply";
537                   K.conclude_args = args;
538                   K.conclude_conclusion = 
539                      try Some 
540                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
541                      with Not_found -> None
542                  };
543             })
544     | C.AConst (id,uri,exp_named_subst) as t ->
545         let sort = Hashtbl.find ids_to_inner_sorts id in
546         if sort = `Prop then
547           generate_exact seed t id name ~ids_to_inner_types
548         else raise Not_a_proof
549     | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
550     | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
551         let sort = Hashtbl.find ids_to_inner_sorts id in
552         if sort = `Prop then 
553           generate_exact seed t id name ~ids_to_inner_types
554         else raise Not_a_proof
555     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
556         let inductive_types,noparams =
557           (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
558              match o with
559                  Cic.Constant _ -> assert false
560                | Cic.Variable _ -> assert false
561                | Cic.CurrentProof _ -> assert false
562                | Cic.InductiveDefinition (l,_,n,_) -> l,n 
563           ) in
564         let (_,_,_,constructors) = List.nth inductive_types typeno in
565         let name_and_arities = 
566           let rec count_prods =
567             function 
568                C.Prod (_,_,t) -> 1 + count_prods t
569              | _ -> 0 in
570           List.map 
571             (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in
572         let pp = 
573           let build_proof p (name,arity) =
574             let rec make_context_and_body c p n =
575               if n = 0 then c,(aux p)
576               else 
577                 (match p with
578                    Cic.ALambda(idl,vname,s1,t1) ->
579                      let ce = 
580                        build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
581                      make_context_and_body (ce::c) t1 (n-1)
582                    | _ -> assert false) in
583              let context,body = make_context_and_body [] p arity in
584                K.ArgProof
585                 {body with K.proof_name = name; K.proof_context=context} in
586           List.map2 build_proof patterns name_and_arities in
587         let context,term =
588           (match 
589              build_subproofs_and_args 
590                seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
591            with
592              l,[t] -> l,t
593            | _ -> assert false) in
594         { K.proof_name = name;
595           K.proof_id   = gen_id proof_prefix seed;
596           K.proof_context = []; 
597           K.proof_apply_context = serialize seed context;
598           K.proof_conclude = 
599             { K.conclude_id = gen_id conclude_prefix seed; 
600               K.conclude_aref = id;
601               K.conclude_method = "Case";
602               K.conclude_args = 
603                 (K.Aux (UriManager.string_of_uri uri))::
604                 (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
605               K.conclude_conclusion = 
606                 try Some 
607                   (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
608                 with Not_found -> None  
609              }
610         }
611     | C.AFix (id, no, funs) -> 
612         let proofs = 
613           List.map 
614             (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
615         let fun_name = 
616           List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no 
617         in
618         let decreasing_args = 
619           List.map (function (_,_,n,_,_) -> n) funs in
620         let jo = 
621           { K.joint_id = gen_id joint_prefix seed;
622             K.joint_kind = `Recursive decreasing_args;
623             K.joint_defs = proofs
624           } 
625         in
626           { K.proof_name = name;
627             K.proof_id  = gen_id proof_prefix seed;
628             K.proof_context = [`Joint jo]; 
629             K.proof_apply_context = [];
630             K.proof_conclude = 
631               { K.conclude_id = gen_id conclude_prefix seed; 
632                 K.conclude_aref = id;
633                 K.conclude_method = "Exact";
634                 K.conclude_args =
635                 [ K.Premise
636                   { K.premise_id = gen_id premise_prefix seed; 
637                     K.premise_xref = jo.K.joint_id;
638                     K.premise_binder = Some fun_name;
639                     K.premise_n = Some no;
640                   }
641                 ];
642                 K.conclude_conclusion =
643                    try Some 
644                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
645                    with Not_found -> None
646               }
647         } 
648     | C.ACoFix (id,no,funs) -> 
649         let proofs = 
650           List.map 
651             (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
652         let jo = 
653           { K.joint_id = gen_id joint_prefix seed;
654             K.joint_kind = `CoRecursive;
655             K.joint_defs = proofs
656           } 
657         in
658           { K.proof_name = name;
659             K.proof_id   = gen_id proof_prefix seed;
660             K.proof_context = [`Joint jo]; 
661             K.proof_apply_context = [];
662             K.proof_conclude = 
663               { K.conclude_id = gen_id conclude_prefix seed; 
664                 K.conclude_aref = id;
665                 K.conclude_method = "Exact";
666                 K.conclude_args =
667                 [ K.Premise
668                   { K.premise_id = gen_id premise_prefix seed; 
669                     K.premise_xref = jo.K.joint_id;
670                     K.premise_binder = Some "tiralo fuori";
671                     K.premise_n = Some no;
672                   }
673                 ];
674                 K.conclude_conclusion =
675                   try Some 
676                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
677                   with Not_found -> None
678               };
679         } 
680      in 
681      let id = get_id t in
682      generate_conversion seed false id t1 ~ids_to_inner_types
683 in aux ?name t
684
685 and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
686   let aux ?name = acic2content seed  ~ids_to_inner_types ~ids_to_inner_sorts in
687   let module C2A = Cic2acic in
688   let module K = Content in
689   let module C = Cic in
690   match li with 
691     C.AConst (idc,uri,exp_named_subst)::args ->
692       let uri_str = UriManager.string_of_uri uri in
693       let suffix = Str.regexp_string "_ind.con" in
694       let len = String.length uri_str in 
695       let n = (try (Str.search_backward suffix uri_str len)
696                with Not_found -> -1) in
697       if n<0 then raise NotApplicable
698       else 
699         let method_name =
700           if UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists"
701           else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd"
702           else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd"
703           else "ByInduction" in
704         let prefix = String.sub uri_str 0 n in
705         let ind_str = (prefix ^ ".ind") in 
706         let ind_uri = UriManager.uri_of_string ind_str in
707         let inductive_types,noparams =
708           (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
709              match o with
710                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
711                | _ -> assert false
712           ) in
713         let rec split n l =
714           if n = 0 then ([],l) else
715           let p,a = split (n-1) (List.tl l) in
716           ((List.hd l::p),a) in
717         let params_and_IP,tail_args = split (noparams+1) args in
718         let constructors = 
719             (match inductive_types with
720               [(_,_,_,l)] -> l
721             | _ -> raise NotApplicable) (* don't care for mutual ind *) in
722         let constructors1 = 
723           let rec clean_up n t =
724              if n = 0 then t else
725              (match t with
726                 (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
727               | _ -> assert false) in
728           List.map (clean_up noparams) constructors in
729         let no_constructors= List.length constructors in
730         let args_for_cases, other_args = 
731           split no_constructors tail_args in
732         let subproofs,other_method_args =
733           build_subproofs_and_args seed other_args
734              ~ids_to_inner_types ~ids_to_inner_sorts in
735         let method_args=
736           let rec build_method_args =
737             function
738                 [],_-> [] (* extra args are ignored ???? *)
739               | (name,ty)::tlc,arg::tla ->
740                   let idarg = get_id arg in
741                   let sortarg = 
742                     (try (Hashtbl.find ids_to_inner_sorts idarg)
743                      with Not_found -> `Type (CicUniv.fresh())) in
744                   let hdarg = 
745                     if sortarg = `Prop then
746                       let (co,bo) = 
747                         let rec bc = 
748                           function 
749                             Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
750                               let ce = 
751                                 build_decl_item 
752                                   seed idl n s1 ~ids_to_inner_sorts in
753                               if (occur ind_uri s) then
754                                 ( match t1 with
755                                    Cic.ALambda(id2,n2,s2,t2) ->
756                                      let inductive_hyp =
757                                        `Hypothesis
758                                          { K.dec_name = name_of n2;
759                                            K.dec_id =
760                                             gen_id declaration_prefix seed; 
761                                            K.dec_inductive = true;
762                                            K.dec_aref = id2;
763                                            K.dec_type = s2
764                                          } in
765                                      let (context,body) = bc (t,t2) in
766                                      (ce::inductive_hyp::context,body)
767                                  | _ -> assert false)
768                               else 
769                                 ( 
770                                 let (context,body) = bc (t,t1) in
771                                 (ce::context,body))
772                             | _ , t -> ([],aux t) in
773                         bc (ty,arg) in
774                       K.ArgProof
775                        { bo with
776                          K.proof_name = Some name;
777                          K.proof_context = co; 
778                        };
779                     else (K.Term arg) in
780                   hdarg::(build_method_args (tlc,tla))
781               | _ -> assert false in
782           build_method_args (constructors1,args_for_cases) in
783           { K.proof_name = name;
784             K.proof_id   = gen_id proof_prefix seed;
785             K.proof_context = []; 
786             K.proof_apply_context = serialize seed subproofs;
787             K.proof_conclude = 
788               { K.conclude_id = gen_id conclude_prefix seed; 
789                 K.conclude_aref = id;
790                 K.conclude_method = method_name;
791                 K.conclude_args =
792                   K.Aux (string_of_int no_constructors) 
793                   ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
794                   ::method_args@other_method_args;
795                 K.conclude_conclusion = 
796                    try Some 
797                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
798                    with Not_found -> None  
799               }
800           } 
801   | _ -> raise NotApplicable
802
803 and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
804   match li with
805     | ((Cic.AConst _) as he)::tl
806     | ((Cic.AMutInd _) as he)::tl
807     | ((Cic.AMutConstruct _) as he)::tl when 
808        CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
809        !hide_coercions ->
810         let rec last =
811          function
812             [] -> assert false
813           | [t] -> t
814           | _::tl -> last tl
815         in
816           acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
817     | _ -> raise NotApplicable
818
819 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
820   let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
821   let module C2A = Cic2acic in
822   let module K = Content in
823   let module C = Cic in
824   match li with 
825     C.AConst (sid,uri,exp_named_subst)::args ->
826       if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or
827          UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI or
828          LibraryObjects.is_eq_ind_URI uri or
829          LibraryObjects.is_eq_ind_r_URI uri then 
830         let subproofs,arg = 
831           (match 
832              build_subproofs_and_args 
833                seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
834            with 
835              l,[p] -> l,p
836            | _,_ -> assert false) in 
837         let method_args =
838           let rec ma_aux n = function
839               [] -> []
840             | a::tl -> 
841                 let hd = 
842                   if n = 0 then arg
843                   else 
844                     let aid = get_id a in
845                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
846                       with Not_found -> `Type (CicUniv.fresh())) in
847                     if asort = `Prop then
848                       K.ArgProof (aux a)
849                     else K.Term a in
850                 hd::(ma_aux (n-1) tl) in
851           (ma_aux 3 args) in 
852           { K.proof_name = name;
853             K.proof_id  = gen_id proof_prefix seed;
854             K.proof_context = []; 
855             K.proof_apply_context = serialize seed subproofs;
856             K.proof_conclude = 
857               { K.conclude_id = gen_id conclude_prefix seed; 
858                 K.conclude_aref = id;
859                 K.conclude_method = "Rewrite";
860                 K.conclude_args = 
861                   K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
862                 K.conclude_conclusion = 
863                    try Some 
864                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
865                    with Not_found -> None
866               }
867           } 
868       else raise NotApplicable
869   | _ -> raise NotApplicable
870
871 and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
872   let module C2A = Cic2acic in
873   let module K = Content in
874   let module C = Cic in
875   match li with 
876     | C.AConst (sid,uri,exp_named_subst)::args 
877         when LibraryObjects.is_trans_eq_URI uri ->
878         let exp_args = List.map snd exp_named_subst in
879         let t1,t2,t3,p1,p2 =
880           match exp_args@args with
881             | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
882             | _ -> raise NotApplicable
883         in
884           { K.proof_name = name;
885             K.proof_id  = gen_id proof_prefix seed;
886             K.proof_context = []; 
887             K.proof_apply_context = [];
888             K.proof_conclude = 
889               { K.conclude_id = gen_id conclude_prefix seed; 
890                 K.conclude_aref = id;
891                 K.conclude_method = "Eq_chain";
892                 K.conclude_args = 
893                    K.Term t1::
894                      (transitivity_aux 
895                         seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
896                      [K.Term t2]@
897                      (transitivity_aux 
898                         seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
899                      [K.Term t3];
900                 K.conclude_conclusion = 
901                    try Some 
902                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
903                    with Not_found -> None
904               }
905           } 
906     | _ -> raise NotApplicable
907
908 and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
909   let module C2A = Cic2acic in
910   let module K = Content in
911   let module C = Cic in
912   match t with 
913     | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args) 
914         when LibraryObjects.is_trans_eq_URI uri ->
915         let exp_args = List.map snd exp_named_subst in
916         let t1,t2,t3,p1,p2 =
917           match exp_args@args with
918             | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
919             | _ -> raise NotApplicable
920         in
921           (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
922           @[K.Term t2]
923           @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
924     | _ -> [K.ArgProof 
925         (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
926
927 ;; 
928
929
930 let map_conjectures
931  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
932 =
933  let module K = Content in
934  let context' =
935   List.map
936    (function
937        (id,None) -> None
938      | (id,Some (name,Cic.ADecl t)) ->
939          Some
940           (* We should call build_decl_item, but we have not computed *)
941           (* the inner-types ==> we always produce a declaration      *)
942           (`Declaration
943             { K.dec_name = name_of name;
944               K.dec_id = gen_id declaration_prefix seed; 
945               K.dec_inductive = false;
946               K.dec_aref = get_id t;
947               K.dec_type = t
948             })
949      | (id,Some (name,Cic.ADef t)) ->
950          Some
951           (* We should call build_def_item, but we have not computed *)
952           (* the inner-types ==> we always produce a declaration     *)
953           (`Definition
954              { K.def_name = name_of name;
955                K.def_id = gen_id definition_prefix seed; 
956                K.def_aref = get_id t;
957                K.def_term = t
958              })
959    ) context
960  in
961   (id,n,context',ty)
962 ;;
963
964 (* map_sequent is similar to map_conjectures, but the for the hid
965 of the hypothesis, which are preserved instead of generating
966 fresh ones. We shall have to adopt a uniform policy, soon or later *)
967
968 let map_sequent ((id,n,context,ty):Cic.annconjecture) =
969  let module K = Content in
970  let context' =
971   List.map
972    (function
973        (id,None) -> None
974      | (id,Some (name,Cic.ADecl t)) ->
975          Some
976           (* We should call build_decl_item, but we have not computed *)
977           (* the inner-types ==> we always produce a declaration      *)
978           (`Declaration
979             { K.dec_name = name_of name;
980               K.dec_id = id; 
981               K.dec_inductive = false;
982               K.dec_aref = get_id t;
983               K.dec_type = t
984             })
985      | (id,Some (name,Cic.ADef t)) ->
986          Some
987           (* We should call build_def_item, but we have not computed *)
988           (* the inner-types ==> we always produce a declaration     *)
989           (`Definition
990              { K.def_name = name_of name;
991                K.def_id = id; 
992                K.def_aref = get_id t;
993                K.def_term = t
994              })
995    ) context
996  in
997   (id,n,context',ty)
998 ;;
999
1000 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = 
1001   let module C = Cic in
1002   let module K = Content in
1003   let module C2A = Cic2acic in
1004   let seed = ref 0 in
1005   function
1006       C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
1007         (gen_id object_prefix seed, params,
1008           Some
1009            (List.map
1010              (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
1011              conjectures),
1012           `Def (K.Const,ty,
1013             build_def_item seed (get_id bo) (C.Name n) bo 
1014              ~ids_to_inner_sorts ~ids_to_inner_types))
1015     | C.AConstant (_,_,n,Some bo,ty,params,_) ->
1016          (gen_id object_prefix seed, params, None,
1017            `Def (K.Const,ty,
1018              build_def_item seed (get_id bo) (C.Name n) bo 
1019                ~ids_to_inner_sorts ~ids_to_inner_types))
1020     | C.AConstant (id,_,n,None,ty,params,_) ->
1021          (gen_id object_prefix seed, params, None,
1022            `Decl (K.Const,
1023              build_decl_item seed id (C.Name n) ty 
1024                ~ids_to_inner_sorts))
1025     | C.AVariable (_,n,Some bo,ty,params,_) ->
1026          (gen_id object_prefix seed, params, None,
1027            `Def (K.Var,ty,
1028              build_def_item seed (get_id bo) (C.Name n) bo
1029                ~ids_to_inner_sorts ~ids_to_inner_types))
1030     | C.AVariable (id,n,None,ty,params,_) ->
1031          (gen_id object_prefix seed, params, None,
1032            `Decl (K.Var,
1033              build_decl_item seed id (C.Name n) ty
1034               ~ids_to_inner_sorts))
1035     | C.AInductiveDefinition (id,l,params,nparams,_) ->
1036          (gen_id object_prefix seed, params, None,
1037             `Joint
1038               { K.joint_id = gen_id joint_prefix seed;
1039                 K.joint_kind = `Inductive nparams;
1040                 K.joint_defs = List.map (build_inductive seed) l
1041               }) 
1042
1043 and
1044     build_inductive seed = 
1045      let module K = Content in
1046       fun (_,n,b,ty,l) ->
1047         `Inductive
1048           { K.inductive_id = gen_id inductive_prefix seed;
1049             K.inductive_name = n;
1050             K.inductive_kind = b;
1051             K.inductive_type = ty;
1052             K.inductive_constructors = build_constructors seed l
1053            }
1054
1055 and 
1056     build_constructors seed l =
1057      let module K = Content in
1058       List.map 
1059        (fun (n,t) ->
1060            { K.dec_name = Some n;
1061              K.dec_id = gen_id declaration_prefix seed;
1062              K.dec_inductive = false;
1063              K.dec_aref = "";
1064              K.dec_type = t
1065            }) l
1066 ;;
1067    
1068 (* 
1069 and 'term cinductiveType = 
1070  id * string * bool * 'term *                (* typename, inductive, arity *)
1071    'term cconstructor list                   (*  constructors        *)
1072
1073 and 'term cconstructor =
1074  string * 'term    
1075 *)
1076
1077