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