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 *)
56 CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
58 | CicTypeChecker.AssertFailure _
59 | CicTypeChecker.TypeCheckerFailure _ ->
60 Cic.Sort Cic.Prop, CicUniv.empty_ugraph
62 (* let t2 = Sys.time () in
63 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
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;;
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 *)
95 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
96 | (_,_) -> raise NotEnoughElements
99 let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
100 seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
101 metasenv context idrefs t expectedty
103 let module D = DoubleTypeInference in
104 let module C = Cic in
105 let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
106 (* let time1 = Sys.time () in *)
109 let time0 = Sys.time () in
110 let prova = CicTypeChecker.type_of_aux' metasenv context t in
111 let time1 = Sys.time () in
112 prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
113 let res = D.double_type_of metasenv context t expectedty in
114 let time2 = Sys.time () in
115 prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
118 if global_computeinnertypes then
119 D.double_type_of metasenv context t expectedty
121 Cic.CicHash.create 1 (* empty table *)
124 let time2 = Sys.time () in
126 ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
128 let rec aux computeinnertypes father context idrefs tt =
129 let fresh_id'' = fresh_id' father tt in
130 (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
131 let aux' = aux computeinnertypes (Some fresh_id'') in
132 (* First of all we compute the inner type and the inner sort *)
133 (* of the term. They may be useful in what follows. *)
134 (*CSC: This is a very inefficient way of computing inner types *)
135 (*CSC: and inner sorts: very deep terms have their types/sorts *)
136 (*CSC: computed again and again. *)
138 match CicReduction.whd context t with
139 C.Sort C.Prop -> `Prop
140 | C.Sort C.Set -> `Set
141 | C.Sort (C.Type u) -> `Type u
142 | C.Meta _ -> `Type (CicUniv.fresh())
143 | C.Sort C.CProp -> `CProp
145 prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
148 let ainnertypes,innertype,innersort,expected_available =
149 (*CSC: Here we need the algorithm for Coscoy's double type-inference *)
150 (*CSC: (expected type + inferred type). Just for now we use the usual *)
151 (*CSC: type-inference, but the result is very poor. As a very weak *)
152 (*CSC: patch, I apply whd to the computed type. Full beta *)
153 (*CSC: reduction would be a much better option. *)
154 (*CSC: solo per testare i tempi *)
158 let {D.synthesized = synthesized; D.expected = expected} =
159 if computeinnertypes then
160 Cic.CicHash.find terms_to_types tt
162 (* We are already in an inner-type and Coscoy's double *)
163 (* type inference algorithm has not been applied. *)
165 (***CSC: patch per provare i tempi
166 CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
167 if global_computeinnertypes then
168 Cic.Sort (Cic.Type (CicUniv.fresh()))
170 CicReduction.whd context (xxx_type_of_aux' metasenv context tt);
173 (* incr number_new_type_of_aux' ; *)
174 let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
175 let ainnertypes,expected_available =
176 if computeinnertypes then
177 let annexpected,expected_available =
180 | Some expectedty' ->
182 (aux false (Some fresh_id'') context idrefs expectedty'),
187 aux false (Some fresh_id'') context idrefs synthesized ;
188 annexpected = annexpected
189 }, expected_available
193 ainnertypes,synthesized, sort_of innersort, expected_available
196 Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *)
197 (* CSC: Type or Set? I can not tell *)
198 let u = CicUniv.fresh() in
199 None,Cic.Sort (Cic.Type u),`Type u,false
200 (* TASSI non dovrebbe fare danni *)
203 let add_inner_type id =
204 match ainnertypes with
206 | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
211 match get_nth context n with
212 (Some (C.Name s,_)) -> s
213 | _ -> "__" ^ string_of_int n
215 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
216 if innersort = `Prop && expected_available then
217 add_inner_type fresh_id'' ;
218 C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
219 | C.Var (uri,exp_named_subst) ->
220 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
221 if innersort = `Prop && expected_available then
222 add_inner_type fresh_id'' ;
223 let exp_named_subst' =
225 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
227 C.AVar (fresh_id'', uri,exp_named_subst')
229 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
230 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
231 if innersort = `Prop && expected_available then
232 add_inner_type fresh_id'' ;
233 C.AMeta (fresh_id'', n,
238 | _, Some t -> Some (aux' context idrefs t)
239 | Some _, None -> assert false (* due to typing rules *))
240 canonical_context l))
241 | C.Sort s -> C.ASort (fresh_id'', s)
242 | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
244 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
245 if innersort = `Prop then
246 add_inner_type fresh_id'' ;
247 C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
249 xxx_add ids_to_inner_sorts fresh_id''
250 (sort_of innertype) ;
251 let sourcetype = xxx_type_of_aux' metasenv context s in
252 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
253 (sort_of sourcetype) ;
258 if DoubleTypeInference.does_not_occur 1 t then
264 (fresh_id'', n', aux' context idrefs s,
265 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
266 | C.Lambda (n,s,t) ->
267 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
268 let sourcetype = xxx_type_of_aux' metasenv context s in
269 xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
270 (sort_of sourcetype) ;
271 if innersort = `Prop then
273 let father_is_lambda =
277 match Hashtbl.find ids_to_terms father' with
281 if (not father_is_lambda) || expected_available then
282 add_inner_type fresh_id''
285 (fresh_id'',n, aux' context idrefs s,
286 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
288 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
289 if innersort = `Prop then
290 add_inner_type fresh_id'' ;
292 (fresh_id'', n, aux' context idrefs s,
293 aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
295 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
296 if innersort = `Prop then
297 add_inner_type fresh_id'' ;
298 C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
299 | C.Const (uri,exp_named_subst) ->
300 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
301 if innersort = `Prop && expected_available then
302 add_inner_type fresh_id'' ;
303 let exp_named_subst' =
305 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
307 C.AConst (fresh_id'', uri, exp_named_subst')
308 | C.MutInd (uri,tyno,exp_named_subst) ->
309 let exp_named_subst' =
311 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
313 C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
314 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
315 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
316 if innersort = `Prop && expected_available then
317 add_inner_type fresh_id'' ;
318 let exp_named_subst' =
320 (function i,t -> i, (aux' context idrefs t)) exp_named_subst
322 C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
323 | C.MutCase (uri, tyno, outty, term, patterns) ->
324 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
325 if innersort = `Prop then
326 add_inner_type fresh_id'' ;
327 C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
328 aux' context idrefs term, List.map (aux' context idrefs) patterns)
329 | C.Fix (funno, funs) ->
331 List.map (function _ -> gen_id seed) funs in
332 let new_idrefs = List.rev fresh_idrefs @ idrefs in
334 List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
336 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
337 if innersort = `Prop then
338 add_inner_type fresh_id'' ;
339 C.AFix (fresh_id'', funno,
341 (fun id (name, indidx, ty, bo) ->
342 (id, name, indidx, aux' context idrefs ty,
343 aux' (tys@context) new_idrefs bo)
346 | C.CoFix (funno, funs) ->
348 List.map (function _ -> gen_id seed) funs in
349 let new_idrefs = List.rev fresh_idrefs @ idrefs in
351 List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
353 xxx_add ids_to_inner_sorts fresh_id'' innersort ;
354 if innersort = `Prop then
355 add_inner_type fresh_id'' ;
356 C.ACoFix (fresh_id'', funno,
358 (fun id (name, ty, bo) ->
359 (id, name, aux' context idrefs ty,
360 aux' (tys@context) new_idrefs bo)
365 let timea = Sys.time () in
366 let res = aux true None context idrefs t in
367 let timeb = Sys.time () in
369 ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
372 aux global_computeinnertypes None context idrefs t
375 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
376 let ids_to_terms = Hashtbl.create 503 in
377 let ids_to_father_ids = Hashtbl.create 503 in
378 let ids_to_inner_sorts = Hashtbl.create 503 in
379 let ids_to_inner_types = Hashtbl.create 503 in
381 acic_of_cic_context' ~computeinnertypes seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
382 ids_to_inner_types metasenv context idrefs t,
383 ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
386 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
387 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
388 metasenv (metano,context,goal)
390 let computeinnertypes = false in
391 let acic_of_cic_context =
392 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
393 ids_to_inner_types metasenv in
394 let _, acontext,final_idrefs =
396 (fun binding (context, acontext,idrefs) ->
397 let hid = "h" ^ string_of_int !hypotheses_seed in
398 Hashtbl.add ids_to_hypotheses hid binding ;
399 incr hypotheses_seed ;
401 Some (n,Cic.Def (t,_)) ->
402 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
403 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
406 ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
407 | Some (n,Cic.Decl t) ->
408 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
409 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
412 ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
414 (* Invariant: "" is never looked up *)
415 (None::context),((hid,None)::acontext),""::idrefs
419 let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in
420 (metano,acontext,agoal)
423 let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
424 let ids_to_terms = Hashtbl.create 503 in
425 let ids_to_father_ids = Hashtbl.create 503 in
426 let ids_to_inner_sorts = Hashtbl.create 503 in
427 let ids_to_inner_types = Hashtbl.create 503 in
428 let ids_to_hypotheses = Hashtbl.create 23 in
429 let hypotheses_seed = ref 0 in
430 let seed = ref 1 in (* 'i0' is used for the whole sequent *)
432 let i,canonical_context,term = sequent in
433 let canonical_context' =
435 (fun d canonical_context' ->
439 | Some (n, Cic.Decl t)->
440 Some (n, Cic.Decl (Unshare.unshare t))
441 | Some (n, Cic.Def (t,None)) ->
442 Some (n, Cic.Def ((Unshare.unshare t),None))
443 | Some (n,Cic.Def (bo,Some ty)) ->
444 Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
446 d::canonical_context'
447 ) canonical_context []
449 let term' = Unshare.unshare term in
450 (i,canonical_context',term')
452 let (metano,acontext,agoal) =
453 aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
454 ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
455 metasenv unsh_sequent in
457 (("i0",metano,acontext,agoal),
458 ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
461 let acic_object_of_cic_object ?(eta_fix=true) obj =
462 let module C = Cic in
463 let module E = Eta_fixing in
464 let ids_to_terms = Hashtbl.create 503 in
465 let ids_to_father_ids = Hashtbl.create 503 in
466 let ids_to_inner_sorts = Hashtbl.create 503 in
467 let ids_to_inner_types = Hashtbl.create 503 in
468 let ids_to_conjectures = Hashtbl.create 11 in
469 let ids_to_hypotheses = Hashtbl.create 127 in
470 let hypotheses_seed = ref 0 in
471 let conjectures_seed = ref 0 in
473 let acic_term_of_cic_term_context' =
474 acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
475 ids_to_inner_types in
476 let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
477 let aconjecture_of_conjecture' = aconjecture_of_conjecture seed
478 ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
479 ids_to_hypotheses hypotheses_seed in
480 let eta_fix metasenv context t =
481 let t = if eta_fix then E.eta_fix metasenv context t else t in
485 C.Constant (id,Some bo,ty,params,attrs) ->
486 let bo' = eta_fix [] [] bo in
487 let ty' = eta_fix [] [] ty in
488 let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
489 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
491 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
492 | C.Constant (id,None,ty,params,attrs) ->
493 let ty' = eta_fix [] [] ty in
494 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
496 ("mettereaposto",None,id,None,aty,params,attrs)
497 | C.Variable (id,bo,ty,params,attrs) ->
498 let ty' = eta_fix [] [] ty in
503 let bo' = eta_fix [] [] bo in
504 Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
506 let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
508 ("mettereaposto",id,abo,aty,params,attrs)
509 | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
512 (function (i,canonical_context,term) ->
513 let canonical_context' =
515 (fun d canonical_context' ->
519 | Some (n, C.Decl t)->
520 Some (n, C.Decl (eta_fix conjectures canonical_context' t))
521 | Some (n, C.Def (t,None)) ->
523 C.Def ((eta_fix conjectures canonical_context' t),None))
524 | Some (_,C.Def (_,Some _)) -> assert false
526 d::canonical_context'
527 ) canonical_context []
529 let term' = eta_fix conjectures canonical_context' term in
530 (i,canonical_context',term')
535 (function (i,canonical_context,term) as conjecture ->
536 let cid = "c" ^ string_of_int !conjectures_seed in
537 xxx_add ids_to_conjectures cid conjecture ;
538 incr conjectures_seed ;
539 let (i,acanonical_context,aterm)
540 = aconjecture_of_conjecture' conjectures conjecture in
541 (cid,i,acanonical_context,aterm))
543 (* let time1 = Sys.time () in *)
544 let bo' = eta_fix conjectures' [] bo in
545 let ty' = eta_fix conjectures' [] ty in
547 let time2 = Sys.time () in
549 ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
550 hashtbl_add_time := 0.0 ;
551 type_of_aux'_add_time := 0.0 ;
552 DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
555 acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in
556 let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in
558 let time3 = Sys.time () in
560 ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
562 ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
564 ("++++++++++++ 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) ;
566 ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
568 ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
570 ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
573 ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
574 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
577 (fun (name,i,arity,cl) ->
578 (name,i,Unshare.unshare arity,
579 List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
582 (fun (name,_,arity,_) ->
583 Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
584 let idrefs = List.map (function _ -> gen_id seed) tys in
587 (fun id (name,inductive,ty,cons) ->
590 (function (name,ty) ->
592 acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None)
596 acic_term_of_cic_term' ~computeinnertypes:false ty None,acons)
597 ) (List.rev idrefs) tys
599 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
601 aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
602 ids_to_conjectures,ids_to_hypotheses
605 let plain_acic_term_of_cic_term =
606 let module C = Cic in
609 function () -> incr id; "i" ^ string_of_int !id in
610 let rec aux context t =
611 let fresh_id = mk_fresh_id () in
615 match get_nth context n with
616 idref,(Some (C.Name s,_)) -> idref,s
617 | idref,_ -> idref,"__" ^ string_of_int n
619 C.ARel (fresh_id, idref, n, id)
620 | C.Var (uri,exp_named_subst) ->
621 let exp_named_subst' =
623 (function i,t -> i, (aux context t)) exp_named_subst
625 C.AVar (fresh_id,uri,exp_named_subst')
627 | C.Meta _ -> assert false
628 | C.Sort s -> C.ASort (fresh_id, s)
630 C.ACast (fresh_id, aux context v, aux context t)
633 (fresh_id, n, aux context s,
634 aux ((fresh_id, Some (n, C.Decl s))::context) t)
635 | C.Lambda (n,s,t) ->
637 (fresh_id,n, aux context s,
638 aux ((fresh_id, Some (n, C.Decl s))::context) t)
641 (fresh_id, n, aux context s,
642 aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
644 C.AAppl (fresh_id, List.map (aux context) l)
645 | C.Const (uri,exp_named_subst) ->
646 let exp_named_subst' =
648 (function i,t -> i, (aux context t)) exp_named_subst
650 C.AConst (fresh_id, uri, exp_named_subst')
651 | C.MutInd (uri,tyno,exp_named_subst) ->
652 let exp_named_subst' =
654 (function i,t -> i, (aux context t)) exp_named_subst
656 C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
657 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
658 let exp_named_subst' =
660 (function i,t -> i, (aux context t)) exp_named_subst
662 C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
663 | C.MutCase (uri, tyno, outty, term, patterns) ->
664 C.AMutCase (fresh_id, uri, tyno, aux context outty,
665 aux context term, List.map (aux context) patterns)
666 | C.Fix (funno, funs) ->
669 (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
671 C.AFix (fresh_id, funno,
673 (fun (id,_) (name, indidx, ty, bo) ->
674 (id, name, indidx, aux context ty, aux (tys@context) bo)
677 | C.CoFix (funno, funs) ->
679 List.map (fun (name,ty,_) ->
680 mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
682 C.ACoFix (fresh_id, funno,
684 (fun (id,_) (name, ty, bo) ->
685 (id, name, aux context ty, aux (tys@context) bo)
692 let plain_acic_object_of_cic_object obj =
693 let module C = Cic in
696 function () -> incr id; "it" ^ string_of_int !id
699 C.Constant (id,Some bo,ty,params,attrs) ->
700 let abo = plain_acic_term_of_cic_term [] bo in
701 let aty = plain_acic_term_of_cic_term [] ty in
703 ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
704 | C.Constant (id,None,ty,params,attrs) ->
705 let aty = plain_acic_term_of_cic_term [] ty in
707 ("mettereaposto",None,id,None,aty,params,attrs)
708 | C.Variable (id,bo,ty,params,attrs) ->
712 | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
714 let aty = plain_acic_term_of_cic_term [] ty in
716 ("mettereaposto",id,abo,aty,params,attrs)
717 | C.CurrentProof _ -> assert false
718 | C.InductiveDefinition (tys,params,paramsno,attrs) ->
721 (fun (name,_,arity,_) ->
722 mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
725 (fun (id,_) (name,inductive,ty,cons) ->
728 (function (name,ty) ->
730 plain_acic_term_of_cic_term context ty)
733 (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
736 C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)