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