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