1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ]
30 let string_of_sort = function
33 | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
34 | `NType s -> "Type[" ^ s ^ "]"
35 | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
38 let sort_of_sort = function
41 | Cic.Type u -> `Type u
42 | Cic.CProp u -> `CProp u
44 (* let hashtbl_add_time = ref 0.0;; *)
46 let xxx_add_profiler = HExtlib.profile "xxx_add";;
48 xxx_add_profiler.HExtlib.profile (Hashtbl.add h k) v
51 let xxx_type_of_aux' m c t =
54 CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph
56 | CicTypeChecker.AssertFailure _
57 | CicTypeChecker.TypeCheckerFailure _ ->
58 Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph
63 let xxx_type_of_aux'_profiler = HExtlib.profile "xxx_type_of_aux'";;
64 let xxx_type_of_aux' m c t =
65 xxx_type_of_aux'_profiler.HExtlib.profile (xxx_type_of_aux' m c) t
68 {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
72 let res = "i" ^ string_of_int !seed in
77 let fresh_id seed ids_to_terms ids_to_father_ids =
79 let res = gen_id seed in
80 xxx_add ids_to_father_ids res father ;
81 xxx_add ids_to_terms res t ;
85 let source_id_of_id id = "#source#" ^ id;;
87 exception NotEnoughElements of string;;
89 (*CSC: cut&paste da cicPp.ml *)
90 (* get_nth l n returns the nth element of the list l if it exists or *)
91 (* raises NotEnoughElements if l has less than n elements *)
92 let rec get_nth msg l n =
95 | (n, he::tail) when n > 1 -> get_nth msg tail (n-1)
96 | (_,_) -> raise (NotEnoughElements msg)
100 let profiler_for_find = HExtlib.profile "CicHash" ;;
101 let profiler_for_whd = HExtlib.profile "whd" ;;
103 let cic_CicHash_find a b =
104 profiler_for_find.HExtlib.profile (Cic.CicHash.find a) b
107 let cicReduction_whd c t =
108 profiler_for_whd.HExtlib.profile (CicReduction.whd c) t
111 let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
112 seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
113 metasenv context idrefs t expectedty
115 let module D = DoubleTypeInference in
116 let module C = Cic in
117 let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
118 (* let time1 = Sys.time () in *)
121 let time0 = Sys.time () in
122 let prova = CicTypeChecker.type_of_aux' metasenv context t in
123 let time1 = Sys.time () in
124 prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
125 let res = D.double_type_of metasenv context t expectedty in
126 let time2 = Sys.time () in
127 prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
130 if global_computeinnertypes then
131 D.double_type_of metasenv context t expectedty
133 Cic.CicHash.create 1 (* empty table *)
136 let time2 = Sys.time () in
138 ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
140 let rec aux computeinnertypes father context idrefs tt =
141 let fresh_id'' = fresh_id' father tt in
142 (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
143 (* First of all we compute the inner type and the inner sort *)
144 (* of the term. They may be useful in what follows. *)
145 (*CSC: This is a very inefficient way of computing inner types *)
146 (*CSC: and inner sorts: very deep terms have their types/sorts *)
147 (*CSC: computed again and again. *)
149 match cicReduction_whd context t with
150 C.Sort C.Prop -> `Prop
151 | C.Sort C.Set -> `Set
152 | C.Sort (C.Type u) -> `Type u
153 | C.Meta _ -> `Type (CicUniv.fresh())
154 | C.Sort (C.CProp u) -> `CProp u
156 prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
159 let ainnertypes,innertype,innersort,expected_available =
161 (*CSC: Here we need the algorithm for Coscoy's double type-inference *)
162 (*CSC: (expected type + inferred type). Just for now we use the usual *)
163 (*CSC: type-inference, but the result is very poor. As a very weak *)
164 (*CSC: patch, I apply whd to the computed type. Full beta *)
165 (*CSC: reduction would be a much better option. *)
166 (*CSC: solo per testare i tempi *)
170 let {D.synthesized = synthesized; D.expected = expected} =
171 if computeinnertypes then
172 cic_CicHash_find terms_to_types tt
174 (* We are already in an inner-type and Coscoy's double *)
175 (* type inference algorithm has not been applied. *)
177 (***CSC: patch per provare i tempi
178 CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
179 (*if global_computeinnertypes then
180 Cic.Sort (Cic.Type (CicUniv.fresh()))
182 cicReduction_whd context (xxx_type_of_aux' metasenv context tt);
185 (* incr number_new_type_of_aux' ; *)
186 let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
187 let ainnertypes,expected_available =
188 if computeinnertypes then
189 let annexpected,expected_available =
192 | Some expectedty' ->
194 (aux false (Some fresh_id'') context idrefs expectedty'),
199 aux false (Some fresh_id'') context idrefs synthesized ;
200 annexpected = annexpected
201 }, expected_available
205 ainnertypes,synthesized, sort_of innersort, expected_available
208 Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *)
209 (* CSC: Type or Set? I can not tell *)
210 let u = CicUniv.fresh() in
211 None,Cic.Sort (Cic.Type u),`Type u,false
212 (* TASSI non dovrebbe fare danni *)
216 if innersort = `Prop then
217 aux computeinnertypes (Some fresh_id'')
219 aux false (Some fresh_id'')
221 let add_inner_type id =
222 match ainnertypes with
224 | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
229 match get_nth "1" context n with
230 (Some (C.Name s,_)) -> s
231 | _ -> "__" ^ string_of_int n
233 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
234 if innersort = `Prop && expected_available then
235 add_inner_type fresh_id'' ;
236 C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
237 | C.Var (uri,exp_named_subst) ->
238 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
239 if innersort = `Prop && expected_available then
240 add_inner_type fresh_id'' ;
241 let exp_named_subst' =
243 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
245 C.AVar (fresh_id'', uri,exp_named_subst')
247 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
248 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
249 if innersort = `Prop && expected_available then
250 add_inner_type fresh_id'' ;
251 C.AMeta (fresh_id'', n,
256 | _, Some t -> Some (aux' context idrefs t)
257 | Some _, None -> assert false (* due to typing rules *))
258 canonical_context l))
259 | C.Sort s -> C.ASort (fresh_id'', s)
260 | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
262 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
263 if innersort = `Prop then
264 add_inner_type fresh_id'' ;
265 C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
267 xxx_add ids_to_inner_sorts fresh_id''
268 (sort_of innertype) ;
269 let sourcetype = xxx_type_of_aux' metasenv context s in
270 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
271 (sort_of sourcetype) ;
276 if DoubleTypeInference.does_not_occur 1 t then
282 (fresh_id'', n', aux' context idrefs s,
283 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
284 | C.Lambda (n,s,t) ->
285 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
286 let sourcetype = xxx_type_of_aux' metasenv context s in
287 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
288 (sort_of sourcetype) ;
289 if innersort = `Prop then
291 let father_is_lambda =
295 match Hashtbl.find ids_to_terms father' with
299 if (not father_is_lambda) || expected_available then
300 add_inner_type fresh_id''
303 (fresh_id'',n, aux' context idrefs s,
304 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
305 | C.LetIn (n,s,ty,t) ->
306 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
307 if innersort = `Prop then
308 add_inner_type fresh_id'' ;
310 (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty,
311 aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t)
313 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
314 if innersort = `Prop then
315 add_inner_type fresh_id'' ;
316 C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
317 | C.Const (uri,exp_named_subst) ->
318 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
319 if innersort = `Prop && expected_available then
320 add_inner_type fresh_id'' ;
321 let exp_named_subst' =
323 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
325 C.AConst (fresh_id'', uri, exp_named_subst')
326 | C.MutInd (uri,tyno,exp_named_subst) ->
327 let exp_named_subst' =
329 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
331 C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
332 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
333 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
334 if innersort = `Prop && expected_available then
335 add_inner_type fresh_id'' ;
336 let exp_named_subst' =
338 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
340 C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
341 | C.MutCase (uri, tyno, outty, term, patterns) ->
342 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
343 if innersort = `Prop then
344 add_inner_type fresh_id'' ;
345 C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
346 aux' context idrefs term, List.map (aux' context idrefs) patterns)
347 | C.Fix (funno, funs) ->
349 List.map (function _ -> gen_id seed) funs in
350 let new_idrefs = List.rev fresh_idrefs @ idrefs in
353 (fun (types,len) (n,_,ty,_) ->
354 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
358 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
359 if innersort = `Prop then
360 add_inner_type fresh_id'' ;
361 C.AFix (fresh_id'', funno,
363 (fun id (name, indidx, ty, bo) ->
364 (id, name, indidx, aux' context idrefs ty,
365 aux' (tys@context) new_idrefs bo)
368 | C.CoFix (funno, funs) ->
370 List.map (function _ -> gen_id seed) funs in
371 let new_idrefs = List.rev fresh_idrefs @ idrefs in
374 (fun (types,len) (n,ty,_) ->
375 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
379 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
380 if innersort = `Prop then
381 add_inner_type fresh_id'' ;
382 C.ACoFix (fresh_id'', funno,
384 (fun id (name, ty, bo) ->
385 (id, name, aux' context idrefs ty,
386 aux' (tys@context) new_idrefs bo)
391 let timea = Sys.time () in
392 let res = aux true None context idrefs t in
393 let timeb = Sys.time () in
395 ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
398 aux global_computeinnertypes None context idrefs t
401 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
402 let ids_to_terms = Hashtbl.create 503 in
403 let ids_to_father_ids = Hashtbl.create 503 in
404 let ids_to_inner_sorts = Hashtbl.create 503 in
405 let ids_to_inner_types = Hashtbl.create 503 in
407 acic_of_cic_context' ~computeinnertypes seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
408 ids_to_inner_types metasenv context idrefs t,
409 ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
412 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
413 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
414 metasenv (metano,context,goal)
416 let computeinnertypes = false in
417 let acic_of_cic_context =
418 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
419 ids_to_inner_types metasenv in
420 let _, acontext,final_idrefs =
422 (fun binding (context, acontext,idrefs) ->
423 let hid = "h" ^ string_of_int !hypotheses_seed in
424 Hashtbl.add ids_to_hypotheses hid binding ;
425 incr hypotheses_seed ;
427 Some (n,Cic.Def (t,ty)) ->
429 acic_of_cic_context ~computeinnertypes context idrefs t
432 acic_of_cic_context ~computeinnertypes context idrefs ty
435 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
437 Hashtbl.replace ids_to_father_ids
438 (CicUtil.id_of_annterm acic2) (Some hid);
440 ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext),
442 | Some (n,Cic.Decl t) ->
443 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
444 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
447 ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
449 (* Invariant: "" is never looked up *)
450 (None::context),((hid,None)::acontext),""::idrefs
454 let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in
455 (metano,acontext,agoal)
458 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
459 let ids_to_terms = Hashtbl.create 503 in
460 let ids_to_father_ids = Hashtbl.create 503 in
461 let ids_to_inner_sorts = Hashtbl.create 503 in
462 let ids_to_inner_types = Hashtbl.create 503 in
463 let ids_to_hypotheses = Hashtbl.create 23 in
464 let hypotheses_seed = ref 0 in
465 let seed = ref 1 in (* 'i0' is used for the whole sequent *)
467 let i,canonical_context,term = sequent in
468 let canonical_context' =
470 (fun d canonical_context' ->
474 | Some (n, Cic.Decl t)->
475 Some (n, Cic.Decl (Unshare.unshare t))
476 | Some (n,Cic.Def (bo,ty)) ->
477 Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty))
479 d::canonical_context'
480 ) canonical_context []
482 let term' = Unshare.unshare term in
483 (i,canonical_context',term')
485 let (metano,acontext,agoal) =
486 aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
487 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
488 metasenv unsh_sequent in
490 (("i0",metano,acontext,agoal),
491 ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
494 let acic_term_or_object_of_cic_term_or_object ?(eta_fix=false) () =
495 let module C = Cic in
496 let module E = Eta_fixing in
497 let ids_to_terms = Hashtbl.create 503 in
498 let ids_to_father_ids = Hashtbl.create 503 in
499 let ids_to_inner_sorts = Hashtbl.create 503 in
500 let ids_to_inner_types = Hashtbl.create 503 in
501 let ids_to_conjectures = Hashtbl.create 11 in
502 let ids_to_hypotheses = Hashtbl.create 127 in
503 let hypotheses_seed = ref 0 in
504 let conjectures_seed = ref 0 in
506 let acic_term_of_cic_term_context' =
507 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
508 ids_to_inner_types in
509 let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
510 let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
511 ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
512 ids_to_hypotheses hypotheses_seed in
513 let eta_fix_and_unshare metasenv context t =
514 let t = if eta_fix then E.eta_fix metasenv context t else t in
519 | Some (n, C.Decl ty) -> Some (n, C.Decl (Unshare.unshare ty))
520 | Some (n, C.Def (bo, ty)) ->
521 Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty))
523 let t = Unshare.unshare t in
524 let context = List.map map context in
525 let idrefs = List.map (function _ -> gen_id seed) context in
526 let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in
527 t, ids_to_inner_sorts, ids_to_inner_types
531 C.Constant (id,Some bo,ty,params,attrs) ->
532 let bo' = (*eta_fix_and_unshare[] [] bo*) Unshare.unshare bo in
533 let ty' = eta_fix_and_unshare [] [] ty in
534 let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
535 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
537 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
538 | C.Constant (id,None,ty,params,attrs) ->
539 let ty' = eta_fix_and_unshare [] [] ty in
540 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
542 ("mettereaposto",None,id,None,aty,params,attrs)
543 | C.Variable (id,bo,ty,params,attrs) ->
544 let ty' = eta_fix_and_unshare [] [] ty in
549 let bo' = eta_fix_and_unshare [] [] bo in
550 Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
552 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
554 ("mettereaposto",id,abo,aty,params,attrs)
555 | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
558 (function (i,canonical_context,term) ->
559 let canonical_context' =
561 (fun d canonical_context' ->
565 | Some (n, C.Decl t)->
566 Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
567 | Some (n, C.Def (t,ty)) ->
570 (eta_fix_and_unshare conjectures canonical_context' t,
571 eta_fix_and_unshare conjectures canonical_context' ty))
573 d::canonical_context'
574 ) canonical_context []
576 let term' = eta_fix_and_unshare conjectures canonical_context' term in
577 (i,canonical_context',term')
582 (function (i,canonical_context,term) as conjecture ->
583 let cid = "c" ^ string_of_int !conjectures_seed in
584 xxx_add ids_to_conjectures cid conjecture ;
585 incr conjectures_seed ;
586 let (i,acanonical_context,aterm)
587 = aconjecture_of_conjecture' conjectures conjecture in
588 (cid,i,acanonical_context,aterm))
590 (* let bo' = eta_fix conjectures' [] bo in *)
592 let ty' = eta_fix_and_unshare conjectures' [] ty in
594 let time2 = Sys.time () in
596 ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
597 hashtbl_add_time := 0.0 ;
598 type_of_aux'_add_time := 0.0 ;
599 DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
602 acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in
603 let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in
605 let time3 = Sys.time () in
607 ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
609 ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
611 ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ;
613 ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
615 ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
617 ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
620 ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
621 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
624 (fun (name,i,arity,cl) ->
625 (name,i,Unshare.unshare arity,
626 List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
629 (fun (name,_,arity,_) ->
630 Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
631 let idrefs = List.map (function _ -> gen_id seed) tys in
634 (fun id (name,inductive,ty,cons) ->
637 (function (name,ty) ->
639 acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None)
643 acic_term_of_cic_term' ~computeinnertypes:false ty None,acons)
644 ) (List.rev idrefs) tys
646 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
648 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
649 ids_to_conjectures,ids_to_hypotheses
652 let acic_object_of_cic_object ?eta_fix =
653 snd (acic_term_or_object_of_cic_term_or_object ?eta_fix ())
655 let plain_acic_term_of_cic_term =
656 let module C = Cic in
659 function () -> incr id; "i" ^ string_of_int !id in
660 let rec aux context t =
661 let fresh_id = mk_fresh_id () in
665 match get_nth "2" context n with
666 idref,(Some (C.Name s,_)) -> idref,s
667 | idref,_ -> idref,"__" ^ string_of_int n
669 C.ARel (fresh_id, idref, n, id)
670 | C.Var (uri,exp_named_subst) ->
671 let exp_named_subst' =
673 (function i,t -> i, (aux context t)) exp_named_subst
675 C.AVar (fresh_id,uri,exp_named_subst')
677 | C.Meta _ -> assert false
678 | C.Sort s -> C.ASort (fresh_id, s)
680 C.ACast (fresh_id, aux context v, aux context t)
683 (fresh_id, n, aux context s,
684 aux ((fresh_id, Some (n, C.Decl s))::context) t)
685 | C.Lambda (n,s,t) ->
687 (fresh_id,n, aux context s,
688 aux ((fresh_id, Some (n, C.Decl s))::context) t)
689 | C.LetIn (n,s,ty,t) ->
691 (fresh_id, n, aux context s, aux context ty,
692 aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t)
694 C.AAppl (fresh_id, List.map (aux context) l)
695 | C.Const (uri,exp_named_subst) ->
696 let exp_named_subst' =
698 (function i,t -> i, (aux context t)) exp_named_subst
700 C.AConst (fresh_id, uri, exp_named_subst')
701 | C.MutInd (uri,tyno,exp_named_subst) ->
702 let exp_named_subst' =
704 (function i,t -> i, (aux context t)) exp_named_subst
706 C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
707 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
708 let exp_named_subst' =
710 (function i,t -> i, (aux context t)) exp_named_subst
712 C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
713 | C.MutCase (uri, tyno, outty, term, patterns) ->
714 C.AMutCase (fresh_id, uri, tyno, aux context outty,
715 aux context term, List.map (aux context) patterns)
716 | C.Fix (funno, funs) ->
719 (fun (types,len) (n,_,ty,_) ->
720 (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
724 C.AFix (fresh_id, funno,
726 (fun (id,_) (name, indidx, ty, bo) ->
727 (id, name, indidx, aux context ty, aux (tys@context) bo)
730 | C.CoFix (funno, funs) ->
733 (fun (types,len) (n,ty,_) ->
734 (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
738 C.ACoFix (fresh_id, funno,
740 (fun (id,_) (name, ty, bo) ->
741 (id, name, aux context ty, aux (tys@context) bo)
748 let plain_acic_object_of_cic_object obj =
749 let module C = Cic in
752 function () -> incr id; "it" ^ string_of_int !id
755 C.Constant (id,Some bo,ty,params,attrs) ->
756 let abo = plain_acic_term_of_cic_term [] bo in
757 let aty = plain_acic_term_of_cic_term [] ty in
759 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
760 | C.Constant (id,None,ty,params,attrs) ->
761 let aty = plain_acic_term_of_cic_term [] ty in
763 ("mettereaposto",None,id,None,aty,params,attrs)
764 | C.Variable (id,bo,ty,params,attrs) ->
768 | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
770 let aty = plain_acic_term_of_cic_term [] ty in
772 ("mettereaposto",id,abo,aty,params,attrs)
773 | C.CurrentProof _ -> assert false
774 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
777 (fun (name,_,arity,_) ->
778 mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
781 (fun (id,_) (name,inductive,ty,cons) ->
784 (function (name,ty) ->
786 plain_acic_term_of_cic_term context ty)
789 (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
792 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
795 let acic_term_of_cic_term ?eta_fix =
796 fst (acic_term_or_object_of_cic_term_or_object ?eta_fix ())