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/.
26 type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
28 let string_of_sort = function
31 | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
34 let sort_of_sort = function
37 | Cic.Type u -> `Type u
40 (* let hashtbl_add_time = ref 0.0;; *)
43 (* let t1 = Sys.time () in *)
45 (* let t2 = Sys.time () in
46 hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 *)
49 (* let number_new_type_of_aux' = ref 0;;
50 let type_of_aux'_add_time = ref 0.0;; *)
52 let xxx_type_of_aux' m c t =
53 (* let t1 = Sys.time () in *)
54 let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
55 (* let t2 = Sys.time () in
56 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
61 {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
65 let res = "i" ^ string_of_int !seed in
70 let fresh_id seed ids_to_terms ids_to_father_ids =
72 let res = gen_id seed in
73 xxx_add ids_to_father_ids res father ;
74 xxx_add ids_to_terms res t ;
78 let source_id_of_id id = "#source#" ^ id;;
80 exception NotEnoughElements;;
82 (*CSC: cut&paste da cicPp.ml *)
83 (* get_nth l n returns the nth element of the list l if it exists or *)
84 (* raises NotEnoughElements if l has less than n elements *)
88 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
89 | (_,_) -> raise NotEnoughElements
92 let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
93 ids_to_inner_types metasenv context idrefs t expectedty
95 let module D = DoubleTypeInference in
97 let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
98 (* let time1 = Sys.time () in *)
101 let time0 = Sys.time () in
102 let prova = CicTypeChecker.type_of_aux' metasenv context t in
103 let time1 = Sys.time () in
104 prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
105 let res = D.double_type_of metasenv context t expectedty in
106 let time2 = Sys.time () in
107 prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
110 D.double_type_of metasenv context t expectedty
113 let time2 = Sys.time () in
115 ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
117 let rec aux computeinnertypes father context idrefs tt =
118 let fresh_id'' = fresh_id' father tt in
119 (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
120 let aux' = aux computeinnertypes (Some fresh_id'') in
121 (* First of all we compute the inner type and the inner sort *)
122 (* of the term. They may be useful in what follows. *)
123 (*CSC: This is a very inefficient way of computing inner types *)
124 (*CSC: and inner sorts: very deep terms have their types/sorts *)
125 (*CSC: computed again and again. *)
127 match CicReduction.whd context t with
128 C.Sort C.Prop -> `Prop
129 | C.Sort C.Set -> `Set
130 | C.Sort (C.Type u) -> `Type u
131 | C.Meta _ -> `Type (CicUniv.fresh())
132 | C.Sort C.CProp -> `CProp
134 prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
137 let ainnertypes,innertype,innersort,expected_available =
138 (*CSC: Here we need the algorithm for Coscoy's double type-inference *)
139 (*CSC: (expected type + inferred type). Just for now we use the usual *)
140 (*CSC: type-inference, but the result is very poor. As a very weak *)
141 (*CSC: patch, I apply whd to the computed type. Full beta *)
142 (*CSC: reduction would be a much better option. *)
143 (*CSC: solo per testare i tempi *)
147 let {D.synthesized = synthesized; D.expected = expected} =
148 if computeinnertypes then
149 D.CicHash.find terms_to_types tt
151 (* We are already in an inner-type and Coscoy's double *)
152 (* type inference algorithm has not been applied. *)
154 (***CSC: patch per provare i tempi
155 CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
156 Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
159 (* incr number_new_type_of_aux' ; *)
160 let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
161 let ainnertypes,expected_available =
162 if computeinnertypes then
163 let annexpected,expected_available =
166 | Some expectedty' ->
168 (aux false (Some fresh_id'') context idrefs expectedty'),
173 aux false (Some fresh_id'') context idrefs synthesized ;
174 annexpected = annexpected
175 }, expected_available
179 ainnertypes,synthesized, sort_of innersort, expected_available
182 Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *)
183 (* CSC: Type or Set? I can not tell *)
184 let u = CicUniv.fresh() in
185 None,Cic.Sort (Cic.Type u),`Type u,false
186 (* TASSI non dovrebbe fare danni *)
189 let add_inner_type id =
190 match ainnertypes with
192 | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
197 match get_nth context n with
198 (Some (C.Name s,_)) -> s
199 | _ -> "__" ^ string_of_int n
201 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
202 if innersort = `Prop && expected_available then
203 add_inner_type fresh_id'' ;
204 C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
205 | C.Var (uri,exp_named_subst) ->
206 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
207 if innersort = `Prop && expected_available then
208 add_inner_type fresh_id'' ;
209 let exp_named_subst' =
211 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
213 C.AVar (fresh_id'', uri,exp_named_subst')
215 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
216 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
217 if innersort = `Prop && expected_available then
218 add_inner_type fresh_id'' ;
219 C.AMeta (fresh_id'', n,
224 | _, Some t -> Some (aux' context idrefs t)
225 | Some _, None -> assert false (* due to typing rules *))
226 canonical_context l))
227 | C.Sort s -> C.ASort (fresh_id'', s)
228 | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
230 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
231 if innersort = `Prop then
232 add_inner_type fresh_id'' ;
233 C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
235 xxx_add ids_to_inner_sorts fresh_id''
236 (sort_of innertype) ;
237 let sourcetype = xxx_type_of_aux' metasenv context s in
238 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
239 (sort_of sourcetype) ;
244 if DoubleTypeInference.does_not_occur 1 t then
250 (fresh_id'', n', aux' context idrefs s,
251 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
252 | C.Lambda (n,s,t) ->
253 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
254 let sourcetype = xxx_type_of_aux' metasenv context s in
255 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
256 (sort_of sourcetype) ;
257 if innersort = `Prop then
259 let father_is_lambda =
263 match Hashtbl.find ids_to_terms father' with
267 if (not father_is_lambda) || expected_available then
268 add_inner_type fresh_id''
271 (fresh_id'',n, aux' context idrefs s,
272 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
274 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
275 if innersort = `Prop then
276 add_inner_type fresh_id'' ;
278 (fresh_id'', n, aux' context idrefs s,
279 aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
281 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
282 if innersort = `Prop then
283 add_inner_type fresh_id'' ;
284 C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
285 | C.Const (uri,exp_named_subst) ->
286 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
287 if innersort = `Prop && expected_available then
288 add_inner_type fresh_id'' ;
289 let exp_named_subst' =
291 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
293 C.AConst (fresh_id'', uri, exp_named_subst')
294 | C.MutInd (uri,tyno,exp_named_subst) ->
295 let exp_named_subst' =
297 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
299 C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
300 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
301 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
302 if innersort = `Prop && expected_available then
303 add_inner_type fresh_id'' ;
304 let exp_named_subst' =
306 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
308 C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
309 | C.MutCase (uri, tyno, outty, term, patterns) ->
310 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
311 if innersort = `Prop then
312 add_inner_type fresh_id'' ;
313 C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
314 aux' context idrefs term, List.map (aux' context idrefs) patterns)
315 | C.Fix (funno, funs) ->
317 List.map (function _ -> gen_id seed) funs in
318 let new_idrefs = List.rev fresh_idrefs @ idrefs in
320 List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
322 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
323 if innersort = `Prop then
324 add_inner_type fresh_id'' ;
325 C.AFix (fresh_id'', funno,
327 (fun id (name, indidx, ty, bo) ->
328 (id, name, indidx, aux' context idrefs ty,
329 aux' (tys@context) new_idrefs bo)
332 | C.CoFix (funno, funs) ->
334 List.map (function _ -> gen_id seed) funs in
335 let new_idrefs = List.rev fresh_idrefs @ idrefs in
337 List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
339 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
340 if innersort = `Prop then
341 add_inner_type fresh_id'' ;
342 C.ACoFix (fresh_id'', funno,
344 (fun id (name, ty, bo) ->
345 (id, name, aux' context idrefs ty,
346 aux' (tys@context) new_idrefs bo)
351 let timea = Sys.time () in
352 let res = aux true None context idrefs t in
353 let timeb = Sys.time () in
355 ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
358 aux true None context idrefs t
361 let acic_of_cic_context metasenv context idrefs t =
362 let ids_to_terms = Hashtbl.create 503 in
363 let ids_to_father_ids = Hashtbl.create 503 in
364 let ids_to_inner_sorts = Hashtbl.create 503 in
365 let ids_to_inner_types = Hashtbl.create 503 in
367 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
368 ids_to_inner_types metasenv context idrefs t,
369 ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
372 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
373 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
374 metasenv (metano,context,goal) =
375 let acic_of_cic_context =
376 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
377 ids_to_inner_types metasenv in
378 let _, acontext,final_idrefs =
380 (fun binding (context, acontext,idrefs) ->
381 let hid = "h" ^ string_of_int !hypotheses_seed in
382 Hashtbl.add ids_to_hypotheses hid binding ;
383 incr hypotheses_seed ;
385 Some (n,Cic.Def (t,None)) ->
386 let acic = acic_of_cic_context context idrefs t None in
388 ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
389 | Some (n,Cic.Decl t) ->
390 let acic = acic_of_cic_context context idrefs t None in
392 ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
394 (* Invariant: "" is never looked up *)
395 (None::context),((hid,None)::acontext),""::idrefs
396 | Some (_,Cic.Def (_,Some _)) -> assert false
400 let agoal = acic_of_cic_context context final_idrefs goal None in
401 (metano,acontext,agoal)
404 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
405 let ids_to_terms = Hashtbl.create 503 in
406 let ids_to_father_ids = Hashtbl.create 503 in
407 let ids_to_inner_sorts = Hashtbl.create 503 in
408 let ids_to_inner_types = Hashtbl.create 503 in
409 let ids_to_hypotheses = Hashtbl.create 23 in
410 let hypotheses_seed = ref 0 in
411 let seed = ref 1 in (* 'i0' is used for the whole sequent *)
413 let i,canonical_context,term = sequent in
414 let canonical_context' =
416 (fun d canonical_context' ->
420 | Some (n, Cic.Decl t)->
421 Some (n, Cic.Decl (Unshare.unshare t))
422 | Some (n, Cic.Def (t,None)) ->
423 Some (n, Cic.Def ((Unshare.unshare t),None))
424 | Some (_,Cic.Def (_,Some _)) -> assert false
426 d::canonical_context'
427 ) canonical_context []
429 let term' = Unshare.unshare term in
430 (i,canonical_context',term')
432 let (metano,acontext,agoal) =
433 aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
434 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
436 ("i0",metano,acontext,agoal),
437 ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
440 let acic_object_of_cic_object ?(eta_fix=true) obj =
441 let module C = Cic in
442 let module E = Eta_fixing in
443 let ids_to_terms = Hashtbl.create 503 in
444 let ids_to_father_ids = Hashtbl.create 503 in
445 let ids_to_inner_sorts = Hashtbl.create 503 in
446 let ids_to_inner_types = Hashtbl.create 503 in
447 let ids_to_conjectures = Hashtbl.create 11 in
448 let ids_to_hypotheses = Hashtbl.create 127 in
449 let hypotheses_seed = ref 0 in
450 let conjectures_seed = ref 0 in
452 let acic_term_of_cic_term_context' =
453 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
454 ids_to_inner_types in
455 let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
456 let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
457 ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
458 ids_to_hypotheses hypotheses_seed in
459 let eta_fix metasenv context t =
460 let t = if eta_fix then E.eta_fix metasenv context t else t in
464 C.Constant (id,Some bo,ty,params,attrs) ->
465 let bo' = eta_fix [] [] bo in
466 let ty' = eta_fix [] [] ty in
467 let abo = acic_term_of_cic_term' bo' (Some ty') in
468 let aty = acic_term_of_cic_term' ty' None in
470 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
471 | C.Constant (id,None,ty,params,attrs) ->
472 let ty' = eta_fix [] [] ty in
473 let aty = acic_term_of_cic_term' ty' None in
475 ("mettereaposto",None,id,None,aty,params,attrs)
476 | C.Variable (id,bo,ty,params,attrs) ->
477 let ty' = eta_fix [] [] ty in
482 let bo' = eta_fix [] [] bo in
483 Some (acic_term_of_cic_term' bo' (Some ty'))
485 let aty = acic_term_of_cic_term' ty' None in
487 ("mettereaposto",id,abo,aty,params,attrs)
488 | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
491 (function (i,canonical_context,term) ->
492 let canonical_context' =
494 (fun d canonical_context' ->
498 | Some (n, C.Decl t)->
499 Some (n, C.Decl (eta_fix conjectures canonical_context' t))
500 | Some (n, C.Def (t,None)) ->
502 C.Def ((eta_fix conjectures canonical_context' t),None))
503 | Some (_,C.Def (_,Some _)) -> assert false
505 d::canonical_context'
506 ) canonical_context []
508 let term' = eta_fix conjectures canonical_context' term in
509 (i,canonical_context',term')
514 (function (i,canonical_context,term) as conjecture ->
515 let cid = "c" ^ string_of_int !conjectures_seed in
516 xxx_add ids_to_conjectures cid conjecture ;
517 incr conjectures_seed ;
518 let (i,acanonical_context,aterm)
519 = aconjecture_of_conjecture' conjectures conjecture in
520 (cid,i,acanonical_context,aterm))
522 (* let time1 = Sys.time () in *)
523 let bo' = eta_fix conjectures' [] bo in
524 let ty' = eta_fix conjectures' [] ty in
526 let time2 = Sys.time () in
528 ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
529 hashtbl_add_time := 0.0 ;
530 type_of_aux'_add_time := 0.0 ;
531 DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
534 acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
535 let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
537 let time3 = Sys.time () in
539 ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
541 ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
543 ("++++++++++++ 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) ;
545 ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
547 ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
549 ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
552 ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
553 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
556 (fun (name,i,arity,cl) ->
557 (name,i,Unshare.unshare arity,
558 List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
561 (fun (name,_,arity,_) ->
562 Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
563 let idrefs = List.map (function _ -> gen_id seed) tys in
566 (fun id (name,inductive,ty,cons) ->
569 (function (name,ty) ->
571 acic_term_of_cic_term_context' [] context idrefs ty None)
574 (id,name,inductive,acic_term_of_cic_term' ty None,acons)
575 ) (List.rev idrefs) tys
577 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
579 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
580 ids_to_conjectures,ids_to_hypotheses
583 let plain_acic_term_of_cic_term =
584 let module C = Cic in
587 function () -> incr id; "i" ^ string_of_int !id in
588 let rec aux context t =
589 let fresh_id = mk_fresh_id () in
593 match get_nth context n with
594 idref,(Some (C.Name s,_)) -> idref,s
595 | idref,_ -> idref,"__" ^ string_of_int n
597 C.ARel (fresh_id, idref, n, id)
598 | C.Var (uri,exp_named_subst) ->
599 let exp_named_subst' =
601 (function i,t -> i, (aux context t)) exp_named_subst
603 C.AVar (fresh_id,uri,exp_named_subst')
605 | C.Meta _ -> assert false
606 | C.Sort s -> C.ASort (fresh_id, s)
608 C.ACast (fresh_id, aux context v, aux context t)
611 (fresh_id, n, aux context s,
612 aux ((fresh_id, Some (n, C.Decl s))::context) t)
613 | C.Lambda (n,s,t) ->
615 (fresh_id,n, aux context s,
616 aux ((fresh_id, Some (n, C.Decl s))::context) t)
619 (fresh_id, n, aux context s,
620 aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
622 C.AAppl (fresh_id, List.map (aux context) l)
623 | C.Const (uri,exp_named_subst) ->
624 let exp_named_subst' =
626 (function i,t -> i, (aux context t)) exp_named_subst
628 C.AConst (fresh_id, uri, exp_named_subst')
629 | C.MutInd (uri,tyno,exp_named_subst) ->
630 let exp_named_subst' =
632 (function i,t -> i, (aux context t)) exp_named_subst
634 C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
635 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
636 let exp_named_subst' =
638 (function i,t -> i, (aux context t)) exp_named_subst
640 C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
641 | C.MutCase (uri, tyno, outty, term, patterns) ->
642 C.AMutCase (fresh_id, uri, tyno, aux context outty,
643 aux context term, List.map (aux context) patterns)
644 | C.Fix (funno, funs) ->
647 (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
649 C.AFix (fresh_id, funno,
651 (fun (id,_) (name, indidx, ty, bo) ->
652 (id, name, indidx, aux context ty, aux (tys@context) bo)
655 | C.CoFix (funno, funs) ->
657 List.map (fun (name,ty,_) ->
658 mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
660 C.ACoFix (fresh_id, funno,
662 (fun (id,_) (name, ty, bo) ->
663 (id, name, aux context ty, aux (tys@context) bo)
670 let plain_acic_object_of_cic_object obj =
671 let module C = Cic in
674 function () -> incr id; "it" ^ string_of_int !id
677 C.Constant (id,Some bo,ty,params,attrs) ->
678 let abo = plain_acic_term_of_cic_term [] bo in
679 let aty = plain_acic_term_of_cic_term [] ty in
681 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
682 | C.Constant (id,None,ty,params,attrs) ->
683 let aty = plain_acic_term_of_cic_term [] ty in
685 ("mettereaposto",None,id,None,aty,params,attrs)
686 | C.Variable (id,bo,ty,params,attrs) ->
690 | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
692 let aty = plain_acic_term_of_cic_term [] ty in
694 ("mettereaposto",id,abo,aty,params,attrs)
695 | C.CurrentProof _ -> assert false
696 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
699 (fun (name,_,arity,_) ->
700 mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
703 (fun (id,_) (name,inductive,ty,cons) ->
706 (function (name,ty) ->
708 plain_acic_term_of_cic_term context ty)
711 (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
714 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)