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,_)) ->
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
399 let agoal = acic_of_cic_context context final_idrefs goal None in
400 (metano,acontext,agoal)
403 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
404 let ids_to_terms = Hashtbl.create 503 in
405 let ids_to_father_ids = Hashtbl.create 503 in
406 let ids_to_inner_sorts = Hashtbl.create 503 in
407 let ids_to_inner_types = Hashtbl.create 503 in
408 let ids_to_hypotheses = Hashtbl.create 23 in
409 let hypotheses_seed = ref 0 in
410 let seed = ref 1 in (* 'i0' is used for the whole sequent *)
412 let i,canonical_context,term = sequent in
413 let canonical_context' =
415 (fun d canonical_context' ->
419 | Some (n, Cic.Decl t)->
420 Some (n, Cic.Decl (Unshare.unshare t))
421 | Some (n, Cic.Def (t,None)) ->
422 Some (n, Cic.Def ((Unshare.unshare t),None))
423 | Some (n,Cic.Def (bo,Some ty)) ->
424 Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
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
435 metasenv unsh_sequent in
437 (("i0",metano,acontext,agoal),
438 ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
441 let acic_object_of_cic_object ?(eta_fix=true) obj =
442 let module C = Cic in
443 let module E = Eta_fixing in
444 let ids_to_terms = Hashtbl.create 503 in
445 let ids_to_father_ids = Hashtbl.create 503 in
446 let ids_to_inner_sorts = Hashtbl.create 503 in
447 let ids_to_inner_types = Hashtbl.create 503 in
448 let ids_to_conjectures = Hashtbl.create 11 in
449 let ids_to_hypotheses = Hashtbl.create 127 in
450 let hypotheses_seed = ref 0 in
451 let conjectures_seed = ref 0 in
453 let acic_term_of_cic_term_context' =
454 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
455 ids_to_inner_types in
456 let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
457 let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
458 ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
459 ids_to_hypotheses hypotheses_seed in
460 let eta_fix metasenv context t =
461 let t = if eta_fix then E.eta_fix metasenv context t else t in
465 C.Constant (id,Some bo,ty,params,attrs) ->
466 let bo' = eta_fix [] [] bo in
467 let ty' = eta_fix [] [] ty in
468 let abo = acic_term_of_cic_term' bo' (Some ty') in
469 let aty = acic_term_of_cic_term' ty' None in
471 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
472 | C.Constant (id,None,ty,params,attrs) ->
473 let ty' = eta_fix [] [] ty in
474 let aty = acic_term_of_cic_term' ty' None in
476 ("mettereaposto",None,id,None,aty,params,attrs)
477 | C.Variable (id,bo,ty,params,attrs) ->
478 let ty' = eta_fix [] [] ty in
483 let bo' = eta_fix [] [] bo in
484 Some (acic_term_of_cic_term' bo' (Some ty'))
486 let aty = acic_term_of_cic_term' ty' None in
488 ("mettereaposto",id,abo,aty,params,attrs)
489 | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
492 (function (i,canonical_context,term) ->
493 let canonical_context' =
495 (fun d canonical_context' ->
499 | Some (n, C.Decl t)->
500 Some (n, C.Decl (eta_fix conjectures canonical_context' t))
501 | Some (n, C.Def (t,None)) ->
503 C.Def ((eta_fix conjectures canonical_context' t),None))
504 | Some (_,C.Def (_,Some _)) -> assert false
506 d::canonical_context'
507 ) canonical_context []
509 let term' = eta_fix conjectures canonical_context' term in
510 (i,canonical_context',term')
515 (function (i,canonical_context,term) as conjecture ->
516 let cid = "c" ^ string_of_int !conjectures_seed in
517 xxx_add ids_to_conjectures cid conjecture ;
518 incr conjectures_seed ;
519 let (i,acanonical_context,aterm)
520 = aconjecture_of_conjecture' conjectures conjecture in
521 (cid,i,acanonical_context,aterm))
523 (* let time1 = Sys.time () in *)
524 let bo' = eta_fix conjectures' [] bo in
525 let ty' = eta_fix conjectures' [] ty in
527 let time2 = Sys.time () in
529 ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
530 hashtbl_add_time := 0.0 ;
531 type_of_aux'_add_time := 0.0 ;
532 DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
535 acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
536 let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
538 let time3 = Sys.time () in
540 ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
542 ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
544 ("++++++++++++ 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) ;
546 ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
548 ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
550 ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
553 ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
554 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
557 (fun (name,i,arity,cl) ->
558 (name,i,Unshare.unshare arity,
559 List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
562 (fun (name,_,arity,_) ->
563 Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
564 let idrefs = List.map (function _ -> gen_id seed) tys in
567 (fun id (name,inductive,ty,cons) ->
570 (function (name,ty) ->
572 acic_term_of_cic_term_context' [] context idrefs ty None)
575 (id,name,inductive,acic_term_of_cic_term' ty None,acons)
576 ) (List.rev idrefs) tys
578 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
580 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
581 ids_to_conjectures,ids_to_hypotheses
584 let plain_acic_term_of_cic_term =
585 let module C = Cic in
588 function () -> incr id; "i" ^ string_of_int !id in
589 let rec aux context t =
590 let fresh_id = mk_fresh_id () in
594 match get_nth context n with
595 idref,(Some (C.Name s,_)) -> idref,s
596 | idref,_ -> idref,"__" ^ string_of_int n
598 C.ARel (fresh_id, idref, n, id)
599 | C.Var (uri,exp_named_subst) ->
600 let exp_named_subst' =
602 (function i,t -> i, (aux context t)) exp_named_subst
604 C.AVar (fresh_id,uri,exp_named_subst')
606 | C.Meta _ -> assert false
607 | C.Sort s -> C.ASort (fresh_id, s)
609 C.ACast (fresh_id, aux context v, aux context t)
612 (fresh_id, n, aux context s,
613 aux ((fresh_id, Some (n, C.Decl s))::context) t)
614 | C.Lambda (n,s,t) ->
616 (fresh_id,n, aux context s,
617 aux ((fresh_id, Some (n, C.Decl s))::context) t)
620 (fresh_id, n, aux context s,
621 aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
623 C.AAppl (fresh_id, List.map (aux context) l)
624 | C.Const (uri,exp_named_subst) ->
625 let exp_named_subst' =
627 (function i,t -> i, (aux context t)) exp_named_subst
629 C.AConst (fresh_id, uri, exp_named_subst')
630 | C.MutInd (uri,tyno,exp_named_subst) ->
631 let exp_named_subst' =
633 (function i,t -> i, (aux context t)) exp_named_subst
635 C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
636 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
637 let exp_named_subst' =
639 (function i,t -> i, (aux context t)) exp_named_subst
641 C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
642 | C.MutCase (uri, tyno, outty, term, patterns) ->
643 C.AMutCase (fresh_id, uri, tyno, aux context outty,
644 aux context term, List.map (aux context) patterns)
645 | C.Fix (funno, funs) ->
648 (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
650 C.AFix (fresh_id, funno,
652 (fun (id,_) (name, indidx, ty, bo) ->
653 (id, name, indidx, aux context ty, aux (tys@context) bo)
656 | C.CoFix (funno, funs) ->
658 List.map (fun (name,ty,_) ->
659 mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
661 C.ACoFix (fresh_id, funno,
663 (fun (id,_) (name, ty, bo) ->
664 (id, name, aux context ty, aux (tys@context) bo)
671 let plain_acic_object_of_cic_object obj =
672 let module C = Cic in
675 function () -> incr id; "it" ^ string_of_int !id
678 C.Constant (id,Some bo,ty,params,attrs) ->
679 let abo = plain_acic_term_of_cic_term [] bo in
680 let aty = plain_acic_term_of_cic_term [] ty in
682 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
683 | C.Constant (id,None,ty,params,attrs) ->
684 let aty = plain_acic_term_of_cic_term [] ty in
686 ("mettereaposto",None,id,None,aty,params,attrs)
687 | C.Variable (id,bo,ty,params,attrs) ->
691 | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
693 let aty = plain_acic_term_of_cic_term [] ty in
695 ("mettereaposto",id,abo,aty,params,attrs)
696 | C.CurrentProof _ -> assert false
697 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
700 (fun (name,_,arity,_) ->
701 mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
704 (fun (id,_) (name,inductive,ty,cons) ->
707 (function (name,ty) ->
709 plain_acic_term_of_cic_term context ty)
712 (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
715 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)