]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_unification/cicRefine.ml
replace assert false with AssertFailure
[helm.git] / helm / software / components / cic_unification / cicRefine.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 (* $Id$ *)
27
28 open Printf
29
30 exception RefineFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
33
34 (* for internal use only; the integer is the number of surplus arguments *)
35 exception MoreArgsThanExpected of int * exn;;
36
37 let insert_coercions = ref true
38 let pack_coercions = ref true
39
40 let debug = false;;
41
42 let debug_print = 
43   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
44
45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
46
47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
48   try
49 let foo () =
50     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
51 in profiler_eat_prods2.HExtlib.profile foo ()
52   with
53       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
54     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
55 ;;
56
57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
58
59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
60   try
61 let foo () =
62     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
63 in profiler_eat_prods.HExtlib.profile foo ()
64   with
65       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
66     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
67 ;;
68
69 let profiler = HExtlib.profile "CicRefine.fo_unif"
70
71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
72   try
73 let foo () =
74     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
75 in profiler.HExtlib.profile foo ()
76   with
77       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
78     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
79 ;;
80
81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
82  let exn' =
83   match exn with
84      RefineFailure msg -> RefineFailure (f msg)
85    | Uncertain msg -> Uncertain (f msg)
86    | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
87    | Sys.Break -> raise exn
88    | _ -> prerr_endline (Printexc.to_string exn); assert false 
89  in
90  let loc =
91   try
92    Cic.CicHash.find localization_tbl t
93   with Not_found ->
94    HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
95    raise exn'
96  in
97   raise (HExtlib.Localized (loc,exn'))
98
99 let relocalize localization_tbl oldt newt =
100  try
101   let infos = Cic.CicHash.find localization_tbl oldt in
102    Cic.CicHash.remove localization_tbl oldt;
103    Cic.CicHash.add localization_tbl newt infos;
104  with
105   Not_found -> ()
106 ;;
107                        
108 let rec split l n =
109  match (l,n) with
110     (l,0) -> ([], l)
111   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
112   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
113 ;;
114
115 let exp_impl metasenv subst context =
116  function
117   | Some `Type ->
118       let (metasenv', idx) = 
119         CicMkImplicit.mk_implicit_type metasenv subst context in
120       let irl = 
121         CicMkImplicit.identity_relocation_list_for_metavariable context in
122       metasenv', Cic.Meta (idx, irl)
123   | Some `Closed ->
124       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
125       metasenv', Cic.Meta (idx, [])
126   | None ->
127       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
128       let irl = 
129         CicMkImplicit.identity_relocation_list_for_metavariable context in
130       metasenv', Cic.Meta (idx, irl)
131   | _ -> assert false
132 ;;
133
134 let is_a_double_coercion t =
135   let last_of l = 
136     let rec aux acc = function
137       | x::[] -> acc,x
138       | x::tl -> aux (acc@[x]) tl
139       | [] -> assert false
140     in
141     aux [] l
142   in
143   let imp = Cic.Implicit None in
144   let dummyres = false,imp, imp,imp,imp in
145   match t with
146   | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
147       (match last_of tl with
148       | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
149           let sib2,head = last_of tl2 in
150           true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
151             (c2::sib2@[imp])]) 
152       | _ -> dummyres)
153   | _ -> dummyres
154
155 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
156 =
157   let len = List.length tlbody_and_type in
158   let msg = 
159     lazy ("The term " ^
160       CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ 
161       " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
162       ") is here applied to " ^ string_of_int len ^
163       " arguments but here it can handle only up to " ^
164       string_of_int (len - residuals) ^ " arguments")
165   in
166   enrich localization_tbl he ~f:(fun _-> msg) exn
167 ;; 
168
169 let mk_prod_of_metas metasenv context subst args = 
170   let rec mk_prod metasenv context' = function
171     | [] ->
172         let (metasenv, idx) = 
173           CicMkImplicit.mk_implicit_type metasenv subst context'
174         in
175         let irl =
176           CicMkImplicit.identity_relocation_list_for_metavariable context'
177         in
178           metasenv,Cic.Meta (idx, irl)
179     | (_,argty)::tl ->
180         let (metasenv, idx) = 
181           CicMkImplicit.mk_implicit_type metasenv subst context' 
182         in
183         let irl =
184           CicMkImplicit.identity_relocation_list_for_metavariable context'
185         in
186         let meta = Cic.Meta (idx,irl) in
187         let name =
188           (* The name must be fresh for context.                 *)
189           (* Nevertheless, argty is well-typed only in context.  *)
190           (* Thus I generate a name (name_hint) in context and   *)
191           (* then I generate a name --- using the hint name_hint *)
192           (* --- that is fresh in context'.                      *)
193           let name_hint = 
194             FreshNamesGenerator.mk_fresh_name ~subst metasenv 
195               (CicMetaSubst.apply_subst_context subst context)
196               Cic.Anonymous
197               ~typ:(CicMetaSubst.apply_subst subst argty) 
198           in
199             FreshNamesGenerator.mk_fresh_name ~subst
200               [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
201         in
202         let metasenv,target =
203           mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
204         in
205           metasenv,Cic.Prod (name,meta,target)
206   in
207   mk_prod metasenv context args
208 ;;
209   
210 let rec type_of_constant uri ugraph =
211  let module C = Cic in
212  let module R = CicReduction in
213  let module U = UriManager in
214   let _ = CicTypeChecker.typecheck uri in
215   let obj,u =
216    try
217     CicEnvironment.get_cooked_obj ugraph uri
218    with Not_found -> assert false
219   in
220    match obj with
221       C.Constant (_,_,ty,_,_) -> ty,u
222     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
223     | _ ->
224        raise
225         (RefineFailure 
226           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
227
228 and type_of_variable uri ugraph =
229   let module C = Cic in
230   let module R = CicReduction in
231   let module U = UriManager in
232   let _ = CicTypeChecker.typecheck uri in
233   let obj,u =
234    try
235     CicEnvironment.get_cooked_obj ugraph uri
236     with Not_found -> assert false
237   in
238    match obj with
239       C.Variable (_,_,ty,_,_) -> ty,u
240     | _ ->
241         raise
242          (RefineFailure
243           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
244
245 and type_of_mutual_inductive_defs uri i ugraph =
246   let module C = Cic in
247   let module R = CicReduction in
248   let module U = UriManager in
249   let _ = CicTypeChecker.typecheck uri in
250   let obj,u =
251    try
252     CicEnvironment.get_cooked_obj ugraph uri
253    with Not_found -> assert false
254   in
255    match obj with
256       C.InductiveDefinition (dl,_,_,_) ->
257         let (_,_,arity,_) = List.nth dl i in
258          arity,u
259     | _ ->
260        raise
261         (RefineFailure
262          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
263
264 and type_of_mutual_inductive_constr uri i j ugraph =
265   let module C = Cic in
266   let module R = CicReduction in
267   let module U = UriManager in
268   let _ = CicTypeChecker.typecheck uri in
269    let obj,u =
270     try
271      CicEnvironment.get_cooked_obj ugraph uri
272     with Not_found -> assert false
273    in
274     match obj with
275         C.InductiveDefinition (dl,_,_,_) ->
276           let (_,_,_,cl) = List.nth dl i in
277           let (_,ty) = List.nth cl (j-1) in
278             ty,u
279       | _ -> 
280           raise
281                   (RefineFailure
282               (lazy 
283                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
284
285
286 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
287
288 (* the check_branch function checks if a branch of a case is refinable. 
289    It returns a pair (outype_instance,args), a subst and a metasenv.
290    outype_instance is the expected result of applying the case outtype 
291    to args. 
292    The problem is that outype is in general unknown, and we should
293    try to synthesize it from the above information, that is in general
294    a second order unification problem. *)
295  
296 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
297   let module C = Cic in
298   let module R = CicReduction in
299     match R.whd ~subst context expectedtype with
300         C.MutInd (_,_,_) ->
301           (n,context,actualtype, [term]), subst, metasenv, ugraph
302       | C.Appl (C.MutInd (_,_,_)::tl) ->
303           let (_,arguments) = split tl left_args_no in
304             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
305       | C.Prod (_,so,de) ->
306           (* we expect that the actual type of the branch has the due 
307              number of Prod *)
308           (match R.whd ~subst context actualtype with
309                C.Prod (name',so',de') ->
310                  let subst, metasenv, ugraph1 = 
311                    fo_unif_subst subst context metasenv so so' ugraph in
312                  let term' =
313                    (match CicSubstitution.lift 1 term with
314                         C.Appl l -> C.Appl (l@[C.Rel 1])
315                       | t -> C.Appl [t ; C.Rel 1]) in
316                    (* we should also check that the name variable is anonymous in
317                       the actual type de' ?? *)
318                    check_branch (n+1) 
319                      ((Some (name',(C.Decl so)))::context) 
320                        metasenv subst left_args_no de' term' de ugraph1
321              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
322       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
323
324 and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
325      ugraph
326 =
327   let rec type_of_aux subst metasenv context t ugraph =
328     let module C = Cic in
329     let module S = CicSubstitution in
330     let module U = UriManager in
331      let (t',_,_,_,_) as res =
332       match t with
333           (*    function *)
334           C.Rel n ->
335             (try
336                match List.nth context (n - 1) with
337                    Some (_,C.Decl ty) -> 
338                      t,S.lift n ty,subst,metasenv, ugraph
339                  | Some (_,C.Def (_,ty)) -> 
340                      t,S.lift n ty,subst,metasenv, ugraph
341                  | None ->
342                     enrich localization_tbl t
343                      (RefineFailure (lazy "Rel to hidden hypothesis"))
344              with
345               Failure _ ->
346                enrich localization_tbl t
347                 (RefineFailure (lazy "Not a closed term")))
348         | C.Var (uri,exp_named_subst) ->
349             let exp_named_subst',subst',metasenv',ugraph1 =
350               check_exp_named_subst 
351                 subst metasenv context exp_named_subst ugraph 
352             in
353             let ty_uri,ugraph1 = type_of_variable uri ugraph in
354             let ty =
355               CicSubstitution.subst_vars exp_named_subst' ty_uri
356             in
357               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
358         | C.Meta (n,l) -> 
359             (try
360                let (canonical_context, term,ty) = 
361                  CicUtil.lookup_subst n subst 
362                in
363                let l',subst',metasenv',ugraph1 =
364                  check_metasenv_consistency n subst metasenv context
365                    canonical_context l ugraph 
366                in
367                  (* trust or check ??? *)
368                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
369                    subst', metasenv', ugraph1
370                    (* type_of_aux subst metasenv 
371                       context (CicSubstitution.subst_meta l term) *)
372              with CicUtil.Subst_not_found _ ->
373                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
374                let l',subst',metasenv', ugraph1 =
375                  check_metasenv_consistency n subst metasenv context
376                    canonical_context l ugraph
377                in
378                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
379                    subst', metasenv',ugraph1)
380         | C.Sort (C.Type tno) -> 
381             let tno' = CicUniv.fresh() in 
382              (try
383                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
384                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
385               with
386                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
387         | C.Sort _ -> 
388             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
389         | C.Implicit infos ->
390            let metasenv',t' = exp_impl metasenv subst context infos in
391             type_of_aux subst metasenv' context t' ugraph
392         | C.Cast (te,ty) ->
393             let ty',_,subst',metasenv',ugraph1 =
394               type_of_aux subst metasenv context ty ugraph 
395             in
396             let te',inferredty,subst'',metasenv'',ugraph2 =
397               type_of_aux subst' metasenv' context te ugraph1
398             in
399             let (te', ty'), subst''',metasenv''',ugraph3 =
400               coerce_to_something true localization_tbl te' inferredty ty'
401                 subst'' metasenv'' context ugraph2
402             in
403              C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
404         | C.Prod (name,s,t) ->
405             let s',sort1,subst',metasenv',ugraph1 = 
406               type_of_aux subst metasenv context s ugraph 
407             in
408             let s',sort1,subst', metasenv',ugraph1 = 
409               coerce_to_sort localization_tbl 
410               s' sort1 subst' context metasenv' ugraph1
411             in
412             let context_for_t = ((Some (name,(C.Decl s')))::context) in
413             let t',sort2,subst'',metasenv'',ugraph2 =
414               type_of_aux subst' metasenv' 
415                 context_for_t t ugraph1
416             in
417             let t',sort2,subst'',metasenv'',ugraph2 = 
418               coerce_to_sort localization_tbl 
419               t' sort2 subst'' context_for_t metasenv'' ugraph2
420             in
421               let sop,subst''',metasenv''',ugraph3 =
422                 sort_of_prod localization_tbl subst'' metasenv'' 
423                   context (name,s') t' (sort1,sort2) ugraph2
424               in
425                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
426         | C.Lambda (n,s,t) ->
427             let s',sort1,subst',metasenv',ugraph1 = 
428               type_of_aux subst metasenv context s ugraph 
429             in
430             let s',sort1,subst',metasenv',ugraph1 =
431               coerce_to_sort localization_tbl 
432               s' sort1 subst' context metasenv' ugraph1
433             in
434             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
435             let t',type2,subst'',metasenv'',ugraph2 =
436               type_of_aux subst' metasenv' context_for_t t ugraph1
437             in
438               C.Lambda (n,s',t'),C.Prod (n,s',type2),
439                 subst'',metasenv'',ugraph2
440         | C.LetIn (n,s,ty,t) ->
441            (* only to check if s is well-typed *)
442            let s',ty',subst',metasenv',ugraph1 = 
443              type_of_aux subst metasenv context s ugraph in
444            let ty,_,subst',metasenv',ugraph1 =
445              type_of_aux subst' metasenv' context ty ugraph1 in
446            let subst',metasenv',ugraph1 =
447             try
448              fo_unif_subst subst' context metasenv'
449                ty ty' ugraph1
450             with
451              exn ->
452               enrich localization_tbl s' exn
453                ~f:(function _ ->
454                  lazy ("The term " ^
455                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
456                    context ^ " has type " ^
457                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
458                    context ^ " but is here used with type " ^
459                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
460                    context))
461            in
462            let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
463            
464             let t',inferredty,subst'',metasenv'',ugraph2 =
465               type_of_aux subst' metasenv' 
466                 context_for_t t ugraph1
467             in
468               (* One-step LetIn reduction. 
469                * Even faster than the previous solution.
470                * Moreover the inferred type is closer to the expected one. 
471                *)
472               C.LetIn (n,s',ty,t'),
473                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
474                subst'',metasenv'',ugraph2
475         | C.Appl (he::((_::_) as tl)) ->
476             let he',hetype,subst',metasenv',ugraph1 = 
477               type_of_aux subst metasenv context he ugraph 
478             in
479             let tlbody_and_type,subst'',metasenv'',ugraph2 =
480                typeof_list subst' metasenv' context ugraph1 tl
481             in
482             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
483               eat_prods true subst'' metasenv'' context 
484                 he' hetype tlbody_and_type ugraph2
485             in
486             let newappl = (C.Appl (coerced_he::coerced_args)) in
487             avoid_double_coercion 
488               context subst''' metasenv''' ugraph3 newappl applty
489         | C.Appl _ -> assert false
490         | C.Const (uri,exp_named_subst) ->
491             let exp_named_subst',subst',metasenv',ugraph1 =
492               check_exp_named_subst subst metasenv context 
493                 exp_named_subst ugraph in
494             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
495             let cty =
496               CicSubstitution.subst_vars exp_named_subst' ty_uri
497             in
498               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
499         | C.MutInd (uri,i,exp_named_subst) ->
500             let exp_named_subst',subst',metasenv',ugraph1 =
501               check_exp_named_subst subst metasenv context 
502                 exp_named_subst ugraph 
503             in
504             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
505             let cty =
506               CicSubstitution.subst_vars exp_named_subst' ty_uri in
507               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
508         | C.MutConstruct (uri,i,j,exp_named_subst) ->
509             let exp_named_subst',subst',metasenv',ugraph1 =
510               check_exp_named_subst subst metasenv context 
511                 exp_named_subst ugraph 
512             in
513             let ty_uri,ugraph2 = 
514               type_of_mutual_inductive_constr uri i j ugraph1 
515             in
516             let cty =
517               CicSubstitution.subst_vars exp_named_subst' ty_uri 
518             in
519               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
520                 metasenv',ugraph2
521         | C.MutCase (uri, i, outtype, term, pl) ->
522             (* first, get the inductive type (and noparams) 
523              * in the environment  *)
524             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
525               let _ = CicTypeChecker.typecheck uri in
526               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
527               match obj with
528                   C.InductiveDefinition (l,expl_params,parsno,_) -> 
529                     List.nth l i , expl_params, parsno, u
530                 | _ ->
531                     enrich localization_tbl t
532                      (RefineFailure
533                        (lazy ("Unkown mutual inductive definition " ^ 
534                          U.string_of_uri uri)))
535            in
536            if List.length constructors <> List.length pl then
537             enrich localization_tbl t
538              (RefineFailure
539                (lazy "Wrong number of cases")) ;
540            let rec count_prod t =
541              match CicReduction.whd ~subst context t with
542                  C.Prod (_, _, t) -> 1 + (count_prod t)
543                | _ -> 0 
544            in 
545            let no_args = count_prod arity in
546              (* now, create a "generic" MutInd *)
547            let metasenv,left_args = 
548              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
549            in
550            let metasenv,right_args = 
551              let no_right_params = no_args - no_left_params in
552                if no_right_params < 0 then assert false
553                else CicMkImplicit.n_fresh_metas 
554                       metasenv subst context no_right_params 
555            in
556            let metasenv,exp_named_subst = 
557              CicMkImplicit.fresh_subst metasenv subst context expl_params in
558            let expected_type = 
559              if no_args = 0 then 
560                C.MutInd (uri,i,exp_named_subst)
561              else
562                C.Appl 
563                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
564            in
565              (* check consistency with the actual type of term *)
566            let term',actual_type,subst,metasenv,ugraph1 = 
567              type_of_aux subst metasenv context term ugraph in
568            let expected_type',_, subst, metasenv,ugraph2 =
569              type_of_aux subst metasenv context expected_type ugraph1
570            in
571            let actual_type = CicReduction.whd ~subst context actual_type in
572            let subst,metasenv,ugraph3 =
573             try
574              fo_unif_subst subst context metasenv 
575                expected_type' actual_type ugraph2
576             with
577              exn ->
578               enrich localization_tbl term' exn
579                ~f:(function _ ->
580                  lazy ("The term " ^
581                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
582                    context ^ " has type " ^
583                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
584                    context ^ " but is here used with type " ^
585                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
586                   context))
587            in
588            let rec instantiate_prod t =
589             function
590                [] -> t
591              | he::tl ->
592                 match CicReduction.whd ~subst context t with
593                    C.Prod (_,_,t') ->
594                     instantiate_prod (CicSubstitution.subst he t') tl
595                  | _ -> assert false
596            in
597            let arity_instantiated_with_left_args =
598             instantiate_prod arity left_args in
599              (* TODO: check if the sort elimination 
600               * is allowed: [(I q1 ... qr)|B] *)
601            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
602              List.fold_right
603                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
604                   let constructor =
605                     if left_args = [] then
606                       (C.MutConstruct (uri,i,j,exp_named_subst))
607                     else
608                       (C.Appl 
609                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
610                   in
611                   let p',actual_type,subst,metasenv,ugraph1 = 
612                     type_of_aux subst metasenv context p ugraph 
613                   in
614                   let constructor',expected_type, subst, metasenv,ugraph2 = 
615                     type_of_aux subst metasenv context constructor ugraph1 
616                   in
617                   let outtypeinstance,subst,metasenv,ugraph3 =
618                    try
619                     check_branch 0 context metasenv subst
620                      no_left_params actual_type constructor' expected_type
621                      ugraph2 
622                    with
623                     exn ->
624                      enrich localization_tbl constructor'
625                       ~f:(fun _ ->
626                         lazy ("The term " ^
627                          CicMetaSubst.ppterm_in_context metasenv subst p'
628                           context ^ " has type " ^
629                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
630                           context ^ " but is here used with type " ^
631                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
632                           context)) exn
633                   in
634                     (p'::pl,j-1,
635                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
636                pl ([],List.length pl,[],subst,metasenv,ugraph3)
637            in
638            
639              (* we are left to check that the outype matches his instances.
640                 The easy case is when the outype is specified, that amount
641                 to a trivial check. Otherwise, we should guess a type from
642                 its instances 
643              *)
644              
645            let outtype,outtypety, subst, metasenv,ugraph4 =
646              type_of_aux subst metasenv context outtype ugraph4 in
647            (match outtype with
648            | C.Meta (n,l) ->
649                (let candidate,ugraph5,metasenv,subst = 
650                  let exp_name_subst, metasenv = 
651                     let o,_ = 
652                       CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri 
653                     in
654                     let uris = CicUtil.params_of_obj o in
655                     List.fold_right (
656                       fun uri (acc,metasenv) -> 
657                         let metasenv',new_meta = 
658                            CicMkImplicit.mk_implicit metasenv subst context
659                         in
660                         let irl =
661                           CicMkImplicit.identity_relocation_list_for_metavariable 
662                             context
663                         in
664                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
665                     ) uris ([],metasenv)
666                  in
667                  let ty =
668                   match left_args,right_args with
669                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
670                    | _,_ ->
671                       let rec mk_right_args =
672                        function
673                           0 -> []
674                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
675                       in
676                       let right_args_no = List.length right_args in
677                       let lifted_left_args =
678                        List.map (CicSubstitution.lift right_args_no) left_args
679                       in
680                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
681                         (lifted_left_args @ mk_right_args right_args_no))
682                  in
683                  let fresh_name = 
684                    FreshNamesGenerator.mk_fresh_name ~subst metasenv 
685                      context Cic.Anonymous ~typ:ty
686                  in
687                  match outtypeinstances with
688                  | [] -> 
689                      let extended_context = 
690                       let rec add_right_args =
691                        function
692                           Cic.Prod (name,ty,t) ->
693                            Some (name,Cic.Decl ty)::(add_right_args t)
694                         | _ -> []
695                       in
696                        (Some (fresh_name,Cic.Decl ty))::
697                        (List.rev
698                         (add_right_args arity_instantiated_with_left_args))@
699                        context
700                      in
701                      let metasenv,new_meta = 
702                        CicMkImplicit.mk_implicit metasenv subst extended_context
703                      in
704                        let irl =
705                        CicMkImplicit.identity_relocation_list_for_metavariable 
706                          extended_context
707                      in
708                      let rec add_lambdas b =
709                       function
710                          Cic.Prod (name,ty,t) ->
711                           Cic.Lambda (name,ty,(add_lambdas b t))
712                        | _ -> Cic.Lambda (fresh_name, ty, b)
713                      in
714                      let candidate = 
715                       add_lambdas (Cic.Meta (new_meta,irl))
716                        arity_instantiated_with_left_args
717                      in
718                      (Some candidate),ugraph4,metasenv,subst
719                  | (constructor_args_no,_,instance,_)::tl -> 
720                      try
721                        let instance',subst,metasenv = 
722                          CicMetaSubst.delift_rels subst metasenv
723                           constructor_args_no instance
724                        in
725                        let candidate,ugraph,metasenv,subst =
726                          List.fold_left (
727                            fun (candidate_oty,ugraph,metasenv,subst) 
728                              (constructor_args_no,_,instance,_) ->
729                                match candidate_oty with
730                                | None -> None,ugraph,metasenv,subst
731                                | Some ty ->
732                                  try 
733                                    let instance',subst,metasenv = 
734                                      CicMetaSubst.delift_rels subst metasenv
735                                       constructor_args_no instance
736                                    in
737                                    let subst,metasenv,ugraph =
738                                     fo_unif_subst subst context metasenv 
739                                       instance' ty ugraph
740                                    in
741                                     candidate_oty,ugraph,metasenv,subst
742                                  with
743                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
744                                   | RefineFailure _ | Uncertain _ ->
745                                      None,ugraph,metasenv,subst
746                          ) (Some instance',ugraph4,metasenv,subst) tl
747                        in
748                        match candidate with
749                        | None -> None, ugraph,metasenv,subst
750                        | Some t -> 
751                           let rec add_lambdas n b =
752                            function
753                               Cic.Prod (name,ty,t) ->
754                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
755                             | _ ->
756                               Cic.Lambda (fresh_name, ty,
757                                CicSubstitution.lift (n + 1) t)
758                           in
759                            Some
760                             (add_lambdas 0 t arity_instantiated_with_left_args),
761                            ugraph,metasenv,subst
762                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
763                        None,ugraph4,metasenv,subst
764                in
765                match candidate with
766                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
767                | Some candidate ->
768                    let subst,metasenv,ugraph = 
769                     try
770                      fo_unif_subst subst context metasenv 
771                        candidate outtype ugraph5
772                     with
773                      exn -> assert false(* unification against a metavariable *)
774                    in
775                      C.MutCase (uri, i, outtype, term', pl'),
776                       CicReduction.head_beta_reduce
777                        (CicMetaSubst.apply_subst subst
778                         (Cic.Appl (outtype::right_args@[term']))),
779                      subst,metasenv,ugraph)
780            | _ ->    (* easy case *)
781              let tlbody_and_type,subst,metasenv,ugraph4 =
782                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
783              in
784              let _,_,_,subst,metasenv,ugraph4 =
785                eat_prods false subst metasenv context 
786                  outtype outtypety tlbody_and_type ugraph4
787              in
788              let _,_, subst, metasenv,ugraph5 =
789                type_of_aux subst metasenv context
790                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
791              in
792              let (subst,metasenv,ugraph6) = 
793                List.fold_left2
794                  (fun (subst,metasenv,ugraph) 
795                    p (constructor_args_no,context,instance,args)
796                   ->
797                     let instance' = 
798                       let appl =
799                         let outtype' =
800                           CicSubstitution.lift constructor_args_no outtype
801                         in
802                           C.Appl (outtype'::args)
803                       in
804                         CicReduction.head_beta_reduce ~delta:false 
805                           ~upto:(List.length args) appl 
806                     in
807                      try
808                       fo_unif_subst subst context metasenv instance instance'
809                        ugraph
810                      with
811                       exn ->
812                        enrich localization_tbl p exn
813                         ~f:(function _ ->
814                           lazy ("The term " ^
815                            CicMetaSubst.ppterm_in_context ~metasenv subst p
816                             context ^ " has type " ^
817                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
818                             context ^ " but is here used with type " ^
819                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
820                             context)))
821                  (subst,metasenv,ugraph5) pl' outtypeinstances
822              in
823                C.MutCase (uri, i, outtype, term', pl'),
824                  CicReduction.head_beta_reduce
825                   (CicMetaSubst.apply_subst subst
826                    (C.Appl(outtype::right_args@[term']))),
827                  subst,metasenv,ugraph6)
828         | C.Fix (i,fl) ->
829             let fl_ty',subst,metasenv,types,ugraph1,len =
830               List.fold_left
831                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
832                    let ty',_,subst',metasenv',ugraph1 = 
833                       type_of_aux subst metasenv context ty ugraph 
834                    in
835                      fl @ [ty'],subst',metasenv', 
836                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
837                         :: types, ugraph, len+1
838                 ) ([],subst,metasenv,[],ugraph,0) fl
839             in
840             let context' = types@context in
841             let fl_bo',subst,metasenv,ugraph2 =
842               List.fold_left
843                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
844                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
845                      type_of_aux subst metasenv context' bo ugraph in
846                    let expected_ty = CicSubstitution.lift len ty in
847                    let subst',metasenv',ugraph' =
848                     try
849                      fo_unif_subst subst context' metasenv
850                        ty_of_bo expected_ty ugraph1
851                     with
852                      exn ->
853                       enrich localization_tbl bo exn
854                        ~f:(function _ ->
855                          lazy ("The term " ^
856                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
857                            context' ^ " has type " ^
858                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
859                            context' ^ " but is here used with type " ^
860                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
861                            context'))
862                    in 
863                      fl @ [bo'] , subst',metasenv',ugraph'
864                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') 
865             in
866             let ty = List.nth fl_ty' i in
867             (* now we have the new ty in fl_ty', the new bo in fl_bo',
868              * and we want the new fl with bo' and ty' injected in the right
869              * place.
870              *) 
871             let rec map3 f l1 l2 l3 =
872               match l1,l2,l3 with
873               | [],[],[] -> []
874               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
875               | _ -> assert false 
876             in
877             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') ) 
878               fl_ty' fl_bo' fl 
879             in
880               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
881         | C.CoFix (i,fl) ->
882             let fl_ty',subst,metasenv,types,ugraph1,len =
883               List.fold_left
884                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
885                    let ty',_,subst',metasenv',ugraph1 = 
886                      type_of_aux subst metasenv context ty ugraph 
887                    in
888                      fl @ [ty'],subst',metasenv', 
889                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
890                         types, ugraph1, len+1
891                 ) ([],subst,metasenv,[],ugraph,0) fl
892             in
893             let context' = types@context in
894             let fl_bo',subst,metasenv,ugraph2 =
895               List.fold_left
896                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
897                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
898                      type_of_aux subst metasenv context' bo ugraph in
899                    let expected_ty = CicSubstitution.lift len ty in
900                    let subst',metasenv',ugraph' = 
901                     try
902                      fo_unif_subst subst context' metasenv
903                        ty_of_bo expected_ty ugraph1
904                     with
905                      exn ->
906                       enrich localization_tbl bo exn
907                        ~f:(function _ ->
908                          lazy ("The term " ^
909                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
910                            context' ^ " has type " ^
911                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
912                            context' ^ " but is here used with type " ^
913                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
914                            context))
915                    in
916                      fl @ [bo'],subst',metasenv',ugraph'
917                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
918             in
919             let ty = List.nth fl_ty' i in
920             (* now we have the new ty in fl_ty', the new bo in fl_bo',
921              * and we want the new fl with bo' and ty' injected in the right
922              * place.
923              *) 
924             let rec map3 f l1 l2 l3 =
925               match l1,l2,l3 with
926               | [],[],[] -> []
927               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
928               | _ -> assert false
929             in
930             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') ) 
931               fl_ty' fl_bo' fl 
932             in
933               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
934      in
935       relocalize localization_tbl t t';
936       res
937
938   (* check_metasenv_consistency checks that the "canonical" context of a
939      metavariable is consitent - up to relocation via the relocation list l -
940      with the actual context *)
941   and check_metasenv_consistency
942     metano subst metasenv context canonical_context l ugraph
943     =
944     let module C = Cic in
945     let module R = CicReduction in
946     let module S = CicSubstitution in
947     let lifted_canonical_context = 
948       let rec aux i =
949         function
950             [] -> []
951           | (Some (n,C.Decl t))::tl ->
952               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
953           | None::tl -> None::(aux (i+1) tl)
954           | (Some (n,C.Def (t,ty)))::tl ->
955               (Some
956                (n,
957                 C.Def
958                  (S.subst_meta l (S.lift i t),
959                   S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
960       in
961         aux 1 canonical_context 
962     in
963       try
964         List.fold_left2 
965           (fun (l,subst,metasenv,ugraph) t ct -> 
966              match (t,ct) with
967                  _,None ->
968                    l @ [None],subst,metasenv,ugraph
969                | Some t,Some (_,C.Def (ct,_)) ->
970                   (*CSC: the following optimization is to avoid a possibly
971                          expensive reduction that can be easily avoided and
972                          that is quite frequent. However, this is better
973                          handled using levels to control reduction *)
974                   let optimized_t =
975                    match t with
976                       Cic.Rel n ->
977                        (try
978                          match List.nth context (n - 1) with
979                             Some (_,C.Def (te,_)) -> S.lift n te
980                           | _ -> t
981                         with
982                          Failure _ -> t)
983                     | _ -> t
984                   in
985                    let subst',metasenv',ugraph' = 
986                    (try
987 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
988  * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
989                       fo_unif_subst subst context metasenv optimized_t ct ugraph
990                     with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
991                    in
992                      l @ [Some t],subst',metasenv',ugraph'
993                | Some t,Some (_,C.Decl ct) ->
994                    let t',inferredty,subst',metasenv',ugraph1 =
995                      type_of_aux subst metasenv context t ugraph
996                    in
997                    let subst'',metasenv'',ugraph2 = 
998                      (try
999                         fo_unif_subst
1000                           subst' context metasenv' inferredty ct ugraph1
1001                       with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1002                    in
1003                      l @ [Some t'], subst'',metasenv'',ugraph2
1004                | None, Some _  ->
1005                    raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context 
1006       with
1007           Invalid_argument _ ->
1008             raise
1009             (RefineFailure
1010                (lazy (sprintf
1011                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1012                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1013                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1014
1015   and check_exp_named_subst metasubst metasenv context tl ugraph =
1016     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
1017       match tl with
1018           [] -> [],metasubst,metasenv,ugraph
1019         | (uri,t)::tl ->
1020             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
1021             let typeofvar =
1022               CicSubstitution.subst_vars substs ty_uri in
1023               (* CSC: why was this code here? it is wrong
1024                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1025                  Cic.Variable (_,Some bo,_,_) ->
1026                  raise
1027                  (RefineFailure (lazy
1028                  "A variable with a body can not be explicit substituted"))
1029                  | Cic.Variable (_,None,_,_) -> ()
1030                  | _ ->
1031                  raise
1032                  (RefineFailure (lazy
1033                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1034                  ) ;
1035               *)
1036             let t',typeoft,metasubst',metasenv',ugraph2 =
1037               type_of_aux metasubst metasenv context t ugraph1 in
1038             let subst = uri,t' in
1039             let metasubst'',metasenv'',ugraph3 =
1040               try
1041                 fo_unif_subst 
1042                   metasubst' context metasenv' typeoft typeofvar ugraph2
1043               with _ ->
1044                 raise (RefineFailure (lazy
1045                          ("Wrong Explicit Named Substitution: " ^ 
1046                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1047                           " not unifiable with " ^ 
1048                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1049             in
1050             (* FIXME: no mere tail recursive! *)
1051             let exp_name_subst, metasubst''', metasenv''', ugraph4 = 
1052               check_exp_named_subst_aux 
1053                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1054             in
1055               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1056     in
1057       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1058
1059
1060   and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1061    ugraph
1062   =
1063     let module C = Cic in
1064     let context_for_t2 = (Some (name,C.Decl s))::context in
1065     let t1'' = CicReduction.whd ~subst context t1 in
1066     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1067       match (t1'', t2'') with
1068         | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> 
1069               (* different than Coq manual!!! *)
1070               C.Sort s2,subst,metasenv,ugraph
1071         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
1072             let t' = CicUniv.fresh() in 
1073              (try
1074               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1075               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1076                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1077               with
1078                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1079         | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> 
1080             let t' = CicUniv.fresh() in 
1081              (try
1082               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1083               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1084                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1085               with
1086                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1087         | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> 
1088             let t' = CicUniv.fresh() in 
1089              (try
1090               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1091               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1092                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1093               with
1094                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1095         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
1096             let t' = CicUniv.fresh() in 
1097              (try
1098               let ugraph1 = CicUniv.add_gt t' t1 ugraph in
1099               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1100                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1101               with
1102                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1103         | (C.Sort _,C.Sort (C.Type t1)) -> 
1104             C.Sort (C.Type t1),subst,metasenv,ugraph
1105         | (C.Sort _,C.Sort (C.CProp t1)) -> 
1106             C.Sort (C.CProp t1),subst,metasenv,ugraph
1107         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1108         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1109             (* TODO how can we force the meta to become a sort? If we don't we
1110              * break the invariant that refine produce only well typed terms *)
1111             (* TODO if we check the non meta term and if it is a sort then we
1112              * are likely to know the exact value of the result e.g. if the rhs
1113              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1114             let (metasenv,idx) =
1115               CicMkImplicit.mk_implicit_sort metasenv subst in
1116             let (subst, metasenv,ugraph1) =
1117              try
1118               fo_unif_subst subst context_for_t2 metasenv 
1119                 (C.Meta (idx,[])) t2'' ugraph
1120              with _ -> assert false (* unification against a metavariable *)
1121             in
1122               t2'',subst,metasenv,ugraph1
1123         | (C.Sort _,_)
1124         | (C.Meta _,_) -> 
1125             enrich localization_tbl s
1126              (RefineFailure 
1127                (lazy 
1128                  (sprintf
1129                    "%s is supposed to be a type, but its type is %s"
1130                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1131                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1132         | _,_ -> 
1133             enrich localization_tbl t
1134              (RefineFailure 
1135                (lazy 
1136                  (sprintf
1137                    "%s is supposed to be a type, but its type is %s"
1138                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1139                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1140
1141   and avoid_double_coercion context subst metasenv ugraph t ty = 
1142    if not !pack_coercions then
1143     t,ty,subst,metasenv,ugraph
1144    else
1145     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1146     if b then
1147       let source_carr = CoercGraph.source_of c2 in
1148       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1149       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr 
1150       with
1151       | CoercGraph.SomeCoercion candidates -> 
1152          let selected =
1153            HExtlib.list_findopt
1154              (function (metasenv,last,c) ->
1155                match c with 
1156                | c when not (CoercGraph.is_composite c) -> 
1157                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1158                    None
1159                | c ->
1160                let subst,metasenv,ugraph =
1161                 fo_unif_subst subst context metasenv last head ugraph in
1162                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1163                (try
1164                  debug_print 
1165                    (lazy 
1166                      ("packing: " ^ 
1167                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1168                  let newt,_,subst,metasenv,ugraph = 
1169                    type_of_aux subst metasenv context c ugraph in
1170                  debug_print (lazy "tipa...");
1171                  let subst, metasenv, ugraph =
1172                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1173                     fo_unif_subst subst context metasenv newt t ugraph
1174                  in
1175                  debug_print (lazy "unifica...");
1176                  Some (newt, ty, subst, metasenv, ugraph)
1177                with 
1178                | RefineFailure s | Uncertain s when not !pack_coercions-> 
1179                    debug_print s; debug_print (lazy "stop\n");None
1180                | RefineFailure s | Uncertain s -> 
1181                    debug_print s;debug_print (lazy "goon\n");
1182                    try 
1183                      let old_pack_coercions = !pack_coercions in
1184                      pack_coercions := false; (* to avoid diverging *)
1185                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1186                        type_of_aux subst metasenv context c1_c2_implicit ugraph 
1187                      in
1188                      pack_coercions := old_pack_coercions;
1189                      let b, _, _, _, _ = 
1190                        is_a_double_coercion refined_c1_c2_implicit 
1191                      in 
1192                      if b then 
1193                        None 
1194                      else
1195                        let head' = 
1196                          match refined_c1_c2_implicit with
1197                          | Cic.Appl l -> HExtlib.list_last l
1198                          | _ -> assert false   
1199                        in
1200                        let subst, metasenv, ugraph =
1201                         try fo_unif_subst subst context metasenv 
1202                           head head' ugraph
1203                         with RefineFailure s| Uncertain s-> 
1204                           debug_print s;assert false 
1205                        in
1206                        let subst, metasenv, ugraph =
1207                          fo_unif_subst subst context metasenv 
1208                           refined_c1_c2_implicit t ugraph
1209                        in
1210                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1211                    with 
1212                    | RefineFailure s | Uncertain s -> 
1213                        pack_coercions := true;debug_print s;None
1214                    | exn -> pack_coercions := true; raise exn))
1215              candidates
1216          in
1217          (match selected with
1218          | Some x -> x
1219          | None -> 
1220               debug_print
1221                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1222               t, ty, subst, metasenv, ugraph)
1223       | _ -> t, ty, subst, metasenv, ugraph)
1224     else
1225       t, ty, subst, metasenv, ugraph  
1226
1227   and typeof_list subst metasenv context ugraph l =
1228     let tlbody_and_type,subst,metasenv,ugraph =
1229       List.fold_right
1230         (fun x (res,subst,metasenv,ugraph) ->
1231            let x',ty,subst',metasenv',ugraph1 =
1232              type_of_aux subst metasenv context x ugraph
1233            in
1234             (x', ty)::res,subst',metasenv',ugraph1
1235         ) l ([],subst,metasenv,ugraph)
1236     in
1237       tlbody_and_type,subst,metasenv,ugraph
1238
1239   and eat_prods
1240     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph 
1241   =
1242     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1243     let fix_arity n metasenv context subst he hetype ugraph =
1244       let hetype = CicMetaSubst.apply_subst subst hetype in
1245       let src = CoercDb.coerc_carr_of_term hetype in 
1246       let tgt = CoercDb.Fun 0 in
1247       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1248       | CoercGraph.NoCoercion -> []
1249       | CoercGraph.NotMetaClosed 
1250       | CoercGraph.NotHandled _ ->
1251          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1252       | CoercGraph.SomeCoercionToTgt candidates
1253       | CoercGraph.SomeCoercion candidates ->
1254           HExtlib.filter_map
1255             (fun (metasenv,last,coerc) -> 
1256               let pp t = 
1257                 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1258               try
1259                let subst,metasenv,ugraph =
1260                 fo_unif_subst subst context metasenv last he ugraph in
1261                 debug_print (lazy ("New head: "^ pp coerc));
1262                 let tty,ugraph =
1263                  CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1264                   ugraph
1265                 in 
1266                  debug_print (lazy (" has type: "^ pp tty));
1267                  Some (coerc,tty,subst,metasenv,ugraph)
1268               with
1269               | Uncertain _ | RefineFailure _
1270               | HExtlib.Localized (_,Uncertain _)
1271               | HExtlib.Localized (_,RefineFailure _) -> None 
1272               | exn -> assert false) 
1273             candidates
1274     in
1275     (* aux function to process the type of the head and the args in parallel *)
1276     let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1277       function
1278       | [] -> newargs,subst,metasenv,he,hetype,ugraph
1279       | (hete, hety)::tl as args ->
1280           match (CicReduction.whd ~subst context hetype) with 
1281           | Cic.Prod (n,s,t) ->
1282               let arg,subst,metasenv,ugraph =
1283                 coerce_to_something allow_coercions localization_tbl 
1284                   hete hety s subst metasenv context ugraph in
1285               eat_prods_and_args 
1286                 metasenv subst context he (CicSubstitution.subst (fst arg) t) 
1287                 ugraph (newargs@[arg]) tl
1288           | _ -> 
1289               let he = 
1290                 match he, newargs with
1291                 | _, [] -> he
1292                 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1293                 | _ -> Cic.Appl (he::List.map fst newargs)
1294               in
1295               (*{{{*) debug_print (lazy 
1296                let pp x = 
1297                 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1298                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1299                "\n but is applyed to: " ^ String.concat ";" 
1300                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1301               let possible_fixes = 
1302                fix_arity (List.length args) metasenv context subst he hetype
1303                 ugraph in
1304               match
1305                 HExtlib.list_findopt
1306                  (fun (he,hetype,subst,metasenv,ugraph) ->
1307                    (* {{{ *)debug_print (lazy ("Try fix: "^
1308                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1309                    debug_print (lazy (" of type: "^
1310                     CicMetaSubst.ppterm_in_context 
1311                     ~metasenv subst hetype context)); (* }}} *)
1312                    try      
1313                     Some (eat_prods_and_args 
1314                       metasenv subst context he hetype ugraph [] args)
1315                    with
1316                     | RefineFailure _ | Uncertain _
1317                     | HExtlib.Localized (_,RefineFailure _)
1318                     | HExtlib.Localized (_,Uncertain _) -> None)
1319                 possible_fixes
1320               with
1321               | Some x -> x
1322               | None ->
1323                  raise 
1324                   (MoreArgsThanExpected
1325                     (List.length args, RefineFailure (lazy "")))
1326     in
1327     (* first we check if we are in the simple case of a meta closed term *)
1328     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1329      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1330       (* this optimization is to postpone fix_arity (the most common case)*)
1331       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1332      else
1333        (* this (says CSC) is also useful to infer dependent types *)
1334         let pristinemenv = metasenv in
1335         let metasenv,hetype' = 
1336           mk_prod_of_metas metasenv context subst args_bo_and_ty 
1337         in
1338         try
1339           let subst,metasenv,ugraph = 
1340            fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1341           in
1342           subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1343         with RefineFailure _ | Uncertain _ ->
1344           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1345     in
1346     let coerced_args,subst,metasenv,he,t,ugraph =
1347      try
1348       eat_prods_and_args 
1349         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1350      with
1351       MoreArgsThanExpected (residuals,exn) ->
1352         more_args_than_expected localization_tbl metasenv
1353          subst he context hetype' residuals args_bo_and_ty exn
1354     in
1355     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1356
1357   and coerce_to_something 
1358     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1359   =
1360     let module CS = CicSubstitution in
1361     let module CR = CicReduction in
1362     let cs_subst = CS.subst ~avoid_beta_redexes:true in
1363     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1364       debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1365       let coer = 
1366         CoercGraph.look_for_coercion metasenv subst context infty expty
1367       in
1368       match coer with
1369       | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1370           "coerce_atom_to_something fails since not meta closed"))
1371       | CoercGraph.NoCoercion 
1372       | CoercGraph.SomeCoercionToTgt _
1373       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1374           "coerce_atom_to_something fails since no coercions found"))
1375       | CoercGraph.SomeCoercion candidates -> 
1376           debug_print (lazy (string_of_int (List.length candidates) ^ 
1377             " candidates found"));
1378           let uncertain = ref false in
1379           let selected = 
1380             let posibilities =
1381               HExtlib.filter_map
1382               (fun (metasenv,last,c) -> 
1383                try
1384                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1385                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1386                 " <==> " ^
1387                 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
1388                 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1389                 context));
1390                 debug_print (lazy ("FO_UNIF_SUBST: " ^
1391                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1392                 let subst,metasenv,ugraph =
1393                  fo_unif_subst subst context metasenv last t ugraph
1394                 in
1395                 let newt,newhety,subst,metasenv,ugraph = 
1396                  type_of_aux subst metasenv context c ugraph in
1397                 let newt, newty, subst, metasenv, ugraph = 
1398                  avoid_double_coercion context subst metasenv ugraph newt expty 
1399                 in
1400                 let subst,metasenv,ugraph = 
1401                   fo_unif_subst subst context metasenv newhety expty ugraph in
1402                  Some ((newt,newty), subst, metasenv, ugraph)
1403                with 
1404                | Uncertain _ -> uncertain := true; None
1405                | RefineFailure _ -> None)
1406               candidates
1407             in
1408             match 
1409               List.fast_sort 
1410                 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2) 
1411                 posibilities 
1412             with
1413             | [] -> None
1414             | x::_ -> Some x
1415           in
1416           match selected with
1417           | Some x -> x
1418           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1419           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1420     in
1421     let rec coerce_to_something_aux 
1422       t infty expty subst metasenv context ugraph 
1423     =
1424       try            
1425         let subst, metasenv, ugraph =
1426           fo_unif_subst subst context metasenv infty expty ugraph
1427         in
1428         (t, expty), subst, metasenv, ugraph
1429       with (Uncertain _ | RefineFailure _ as exn)
1430         when allow_coercions && !insert_coercions ->
1431           let whd = CicReduction.whd ~delta:false in
1432           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1433           let infty = clean infty subst context in
1434           let expty = clean expty subst context in
1435           let t = clean t subst context in
1436           (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1437           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1438           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1439           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1440           let (coerced,_),subst,metasenv,_ as result = 
1441            match infty, expty, t with
1442            | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1443               (*{{{*) debug_print (lazy "FIX");
1444               (match fl with
1445                   [name,i,_(* infty *),bo] ->
1446                     let context_bo =
1447                      Some (Cic.Name name,Cic.Decl expty)::context in
1448                     let (rel1, _), subst, metasenv, ugraph =
1449                      coerce_to_something_aux (Cic.Rel 1) 
1450                        (CS.lift 1 expty) (CS.lift 1 infty) subst
1451                       metasenv context_bo ugraph in
1452                     let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1453                     let (bo,_), subst, metasenv, ugraph =
1454                      coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1455                      expty) subst
1456                       metasenv context_bo ugraph
1457                     in
1458                      (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1459                 | _ -> assert false (* not implemented yet *)) (*}}}*)
1460            | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1461                (*{{{*) debug_print (lazy "CASE");
1462                (* {{{ helper functions *)
1463                let get_cl_and_left_p uri tyno outty ugraph =
1464                  match CicEnvironment.get_obj ugraph uri with
1465                  | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1466                      let count_pis t =
1467                        let rec aux ctx t = 
1468                          match CicReduction.whd ~delta:false ctx t with
1469                          | Cic.Prod (name,src,tgt) ->
1470                              let ctx = Some (name, Cic.Decl src) :: ctx in
1471                              1 + aux ctx tgt
1472                          | _ -> 0
1473                        in
1474                          aux [] t
1475                      in
1476                      let rec skip_lambda_delifting t n =
1477                        match t,n with
1478                        | _,0 -> t
1479                        | Cic.Lambda (_,_,t),n -> 
1480                            skip_lambda_delifting
1481                              (CS.subst (Cic.Implicit None) t) (n - 1)
1482                        | _ -> assert false
1483                      in
1484                      let get_l_r_p n = function
1485                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1486                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1487                            HExtlib.split_nth n args
1488                        | _ -> assert false
1489                      in
1490                      let _, _, ty, cl = List.nth tl tyno in
1491                      let pis = count_pis ty in
1492                      let rno = pis - leftno in
1493                      let t = skip_lambda_delifting outty rno in
1494                      let left_p, _ = get_l_r_p leftno t in
1495                      let instantiale_with_left cl =
1496                        List.map 
1497                          (fun ty -> 
1498                            List.fold_left 
1499                              (fun t p -> match t with
1500                                | Cic.Prod (_,_,t) ->
1501                                    cs_subst p t
1502                                | _-> assert false)
1503                              ty left_p) 
1504                          cl 
1505                      in
1506                      let cl = instantiale_with_left (List.map snd cl) in
1507                      cl, left_p, leftno, rno, ugraph
1508                  | _ -> raise exn
1509                in
1510                let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1511                  match t,n with
1512                  | _,0 ->
1513                    let rec mkr n = function 
1514                      | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1515                    in
1516                    let bo =
1517                    CicReplace.replace_lifting
1518                      ~equality:(fun _ -> CicUtil.alpha_equivalence)
1519                      ~context:ctx
1520                      ~what:(matched::right_p)
1521                      ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1522                      ~where:bo
1523                    in
1524                    bo
1525                  | Cic.Lambda (name, src, tgt),_ ->
1526                      Cic.Lambda (name, src,
1527                       keep_lambdas_and_put_expty 
1528                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1529                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1530                  | _ -> assert false
1531                in
1532                let eq_uri, eq, eq_refl = 
1533                  match LibraryObjects.eq_URI () with 
1534                  | None -> HLog.warn "no default equality"; raise exn
1535                  | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1536                in
1537                let add_params 
1538                  metasenv subst context uri tyno cty outty mty m leftno i 
1539                =
1540                  let rec aux context outty par k mty m = function
1541                    | Cic.Prod (name, src, tgt) ->
1542                        let t,k = 
1543                          aux 
1544                            (Some (name, Cic.Decl src) :: context)
1545                            (CS.lift 1 outty) (Cic.Rel k::par) (k+1) 
1546                            (CS.lift 1 mty) (CS.lift 1 m) tgt
1547                        in
1548                        Cic.Prod (name, src, t), k
1549                    | Cic.MutInd _ ->
1550                        let k = 
1551                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1552                          if par <> [] then Cic.Appl (k::par) else k
1553                        in
1554                        Cic.Prod (Cic.Name "p", 
1555                         Cic.Appl [eq; mty; m; k],
1556                         (CS.lift 1
1557                          (CR.head_beta_reduce ~delta:false 
1558                           (Cic.Appl [outty;k])))),k
1559                    | Cic.Appl (Cic.MutInd _::pl) ->
1560                        let left_p,right_p = HExtlib.split_nth leftno pl in
1561                        let has_rights = right_p <> [] in
1562                        let k = 
1563                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1564                          Cic.Appl (k::left_p@par)
1565                        in
1566                        let right_p = 
1567                          try match 
1568                            CicTypeChecker.type_of_aux' ~subst metasenv context k
1569                              CicUniv.oblivion_ugraph 
1570                          with
1571                          | Cic.Appl (Cic.MutInd _::args),_ ->
1572                              snd (HExtlib.split_nth leftno args)
1573                          | _ -> assert false
1574                          with CicTypeChecker.TypeCheckerFailure _-> assert false
1575                        in
1576                        if has_rights then
1577                          CR.head_beta_reduce ~delta:false 
1578                            (Cic.Appl (outty ::right_p @ [k])),k
1579                        else
1580                          Cic.Prod (Cic.Name "p", 
1581                           Cic.Appl [eq; mty; m; k],
1582                           (CS.lift 1
1583                            (CR.head_beta_reduce ~delta:false 
1584                             (Cic.Appl (outty ::right_p @ [k]))))),k
1585                    | _ -> assert false
1586                  in
1587                    aux context outty [] 1 mty m cty
1588                in
1589                let add_lambda_for_refl_m pbo rno mty m k cty =
1590                  (* k lives in the right context *)
1591                  if rno <> 0 then pbo else
1592                  let rec aux mty m = function 
1593                    | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1594                       Cic.Lambda (name,src,
1595                        (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1596                    | t,_ -> 
1597                        Cic.Lambda (Cic.Name "p",
1598                          Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1599                  in
1600                  aux mty m (pbo,cty)
1601                in
1602                let add_pi_for_refl_m new_outty mty m rno =
1603                  if rno <> 0 then new_outty else
1604                    let rec aux m mty = function
1605                      | Cic.Lambda (name, src, tgt) ->
1606                          Cic.Lambda (name, src, 
1607                            aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1608                      | t ->
1609                          Cic.Prod 
1610                            (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1611                            CS.lift 1 t)
1612                    in
1613                      aux m mty new_outty
1614                in (* }}} end helper functions *)
1615                (* constructors types with left params already instantiated *)
1616                let outty = CicMetaSubst.apply_subst subst outty in
1617                let cl, left_p, leftno,rno,ugraph = 
1618                  get_cl_and_left_p uri tyno outty ugraph 
1619                in
1620                let right_p, mty = 
1621                  try
1622                    match 
1623                      CicTypeChecker.type_of_aux' ~subst metasenv context m
1624                        CicUniv.oblivion_ugraph 
1625                    with
1626                    | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1627                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1628                        snd (HExtlib.split_nth leftno args), mty
1629                    | _ -> assert false
1630                  with CicTypeChecker.TypeCheckerFailure _ -> 
1631                     raise (AssertFailure(lazy "already ill-typed matched term"))
1632                in
1633                let new_outty =
1634                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1635                in
1636                debug_print 
1637                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
1638                   ~metasenv subst new_outty context));
1639                let _,pl,subst,metasenv,ugraph = 
1640                  List.fold_right2
1641                    (fun cty pbo (i, acc, s, menv, ugraph) -> 
1642                      (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
1643                       *   (new_)outty right_par (K_i left_par k_par) *)
1644                       let infty_pbo, _ = 
1645                         add_params menv s context uri tyno 
1646                           cty outty mty m leftno i in
1647                       debug_print 
1648                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1649                         ~metasenv subst infty_pbo context));
1650                       let expty_pbo, k = (* k is (K_i left_par k_par) *)
1651                         add_params menv s context uri tyno 
1652                           cty new_outty mty m leftno i in
1653                       debug_print 
1654                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1655                         ~metasenv subst expty_pbo context));
1656                       let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1657                       debug_print 
1658                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
1659                         ~metasenv subst pbo context));
1660                       let (pbo, _), subst, metasenv, ugraph =
1661                         coerce_to_something_aux pbo infty_pbo expty_pbo 
1662                           s menv context ugraph
1663                       in
1664                       debug_print 
1665                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context 
1666                         ~metasenv subst pbo context));
1667                       (i-1, pbo::acc, subst, metasenv, ugraph))
1668                    cl pl (List.length pl, [], subst, metasenv, ugraph)
1669                in
1670                let new_outty = add_pi_for_refl_m new_outty mty m rno in
1671                debug_print 
1672                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context 
1673                   ~metasenv subst new_outty context));
1674                let t = 
1675                  if rno = 0 then
1676                    let refl_m=Cic.Appl[eq_refl;mty;m]in
1677                    Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] 
1678                  else 
1679                    Cic.MutCase(uri,tyno,new_outty,m,pl)
1680                in
1681                (t, expty), subst, metasenv, ugraph (*}}}*)
1682            | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> 
1683                (*{{{*) debug_print (lazy "LAM");
1684                let name_con = 
1685                  FreshNamesGenerator.mk_fresh_name 
1686                    ~subst metasenv context ~typ:src2 Cic.Anonymous
1687                in
1688                let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1689                (* contravariant part: the argument of f:src->ty *)
1690                let (rel1, _), subst, metasenv, ugraph = 
1691                  coerce_to_something_aux
1692                   (Cic.Rel 1) (CS.lift 1 src2) 
1693                   (CS.lift 1 src) subst metasenv context_src2 ugraph
1694                in
1695                (* covariant part: the result of f(c x); x:src2; (c x):src *)
1696                let name_t, bo = 
1697                  match t with
1698                  | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1699                  | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1700                in
1701                (* we fix the possible dependency problem in the source ty *)
1702                let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1703                let (bo, _), subst, metasenv, ugraph = 
1704                  coerce_to_something_aux
1705                    bo ty ty2 subst metasenv context_src2 ugraph
1706                in
1707                let coerced = Cic.Lambda (name_t,src2, bo) in
1708                (coerced, expty), subst, metasenv, ugraph (*}}}*)
1709            | _ -> 
1710                (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1711                 ~metasenv subst infty context ^ " ==> " ^
1712                 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1713                coerce_atom_to_something
1714                t infty expty subst metasenv context ugraph (*}}}*)
1715           in
1716           debug_print (lazy ("COERCE TO SOMETHING END: "^
1717             CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1718           result
1719     in
1720     try
1721       coerce_to_something_aux t infty expty subst metasenv context ugraph
1722     with Uncertain _ | RefineFailure _ as exn ->
1723       let f _ =
1724         lazy ("The term " ^
1725           CicMetaSubst.ppterm_in_context metasenv subst t context ^ 
1726           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1727           infty context ^ " but is here used with type " ^ 
1728           CicMetaSubst.ppterm_in_context metasenv subst expty context)
1729       in
1730         enrich localization_tbl ~f t exn
1731
1732   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1733     match CicReduction.whd ~delta:false ~subst context infty with
1734     | Cic.Meta _ | Cic.Sort _ -> 
1735         t,infty, subst, metasenv, ugraph
1736     | src ->
1737        debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1738          ~metasenv subst src context));
1739        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1740        try
1741          let (t, ty_t), subst, metasenv, ugraph =
1742            coerce_to_something true
1743              localization_tbl t src tgt subst metasenv context ugraph
1744          in
1745          debug_print (lazy ("COERCE TO SORT END: "^ 
1746            CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1747          t, ty_t, subst, metasenv, ugraph
1748        with HExtlib.Localized (_, exn) -> 
1749          let f _ = 
1750            lazy ("(7)The term " ^ 
1751             CicMetaSubst.ppterm_in_context ~metasenv subst t context 
1752             ^ " is not a type since it has type " ^ 
1753             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1754             ^ " that is not a sort")
1755          in
1756            enrich localization_tbl ~f t exn
1757   in
1758   
1759   (* eat prods ends here! *)
1760   
1761   let t',ty,subst',metasenv',ugraph1 =
1762    type_of_aux [] metasenv context t ugraph
1763   in
1764   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1765   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1766     (* Andrea: ho rimesso qui l'applicazione della subst al
1767        metasenv dopo che ho droppato l'invariante che il metsaenv
1768        e' sempre istanziato *)
1769   let substituted_metasenv = 
1770     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1771     (* metasenv' *)
1772     (*  substituted_t,substituted_ty,substituted_metasenv *)
1773     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1774   let cleaned_t =
1775    if clean_dummy_dependent_types then
1776     FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1777    else substituted_t in
1778   let cleaned_ty =
1779    if clean_dummy_dependent_types then
1780     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1781    else substituted_ty in
1782   let cleaned_metasenv =
1783    if clean_dummy_dependent_types then
1784     List.map
1785       (function (n,context,ty) ->
1786          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1787          let context' =
1788            List.map
1789              (function
1790                   None -> None
1791                 | Some (n, Cic.Decl t) ->
1792                     Some (n,
1793                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1794                 | Some (n, Cic.Def (bo,ty)) ->
1795                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1796                     let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1797                     in
1798                       Some (n, Cic.Def (bo',ty'))
1799              ) context
1800          in
1801            (n,context',ty')
1802       ) substituted_metasenv
1803    else
1804     substituted_metasenv
1805   in
1806     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
1807 ;;
1808
1809 let undebrujin uri typesno tys t =
1810   snd
1811    (List.fold_right
1812      (fun (name,_,_,_) (i,t) ->
1813        (* here the explicit_named_substituion is assumed to be *)
1814        (* of length 0 *)
1815        let t' = Cic.MutInd (uri,i,[])  in
1816        let t = CicSubstitution.subst t' t in
1817         i - 1,t
1818      ) tys (typesno - 1,t)) 
1819
1820 let map_first_n n start f g l = 
1821   let rec aux acc k l =
1822     if k < n then
1823       match l with
1824       | [] -> raise (Invalid_argument "map_first_n")
1825       | hd :: tl -> f hd k (aux acc (k+1) tl)
1826     else
1827       g acc l
1828   in
1829   aux start 0 l
1830    
1831 (*CSC: this is a very rough approximation; to be finished *)
1832 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1833   let subst,metasenv,ugraph,tys = 
1834     List.fold_right
1835       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1836         let subst,metasenv,ugraph,cl = 
1837           List.fold_right
1838             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1839                let rec aux ctx k subst = function
1840                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1841                      let subst,metasenv,ugraph,tl = 
1842                        map_first_n leftno 
1843                          (subst,metasenv,ugraph,[]) 
1844                          (fun t n (subst,metasenv,ugraph,acc) ->
1845                            let subst,metasenv,ugraph = 
1846                              fo_unif_subst 
1847                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph 
1848                            in
1849                            subst,metasenv,ugraph,(t::acc)) 
1850                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl)) 
1851                          tl
1852                      in
1853                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1854                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1855                      subst,metasenv,ugraph,t 
1856                  | Cic.Prod (name,s,t) -> 
1857                      let ctx = (Some (name,Cic.Decl s))::ctx in 
1858                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1859                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1860                  | _ -> 
1861                      raise 
1862                       (RefineFailure 
1863                         (lazy "not well formed constructor type"))
1864                in
1865                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in  
1866                subst,metasenv,ugraph,(name,ty) :: acc)
1867           cl (subst,metasenv,ugraph,[])
1868         in 
1869         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1870       tys ([],metasenv,ugraph,[])
1871   in
1872   let substituted_tys = 
1873     List.map 
1874       (fun (name,ind,arity,cl) -> 
1875         let cl = 
1876           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1877         in
1878         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1879       tys 
1880   in
1881   metasenv,ugraph,substituted_tys
1882     
1883 let typecheck metasenv uri obj ~localization_tbl =
1884  let ugraph = CicUniv.oblivion_ugraph in
1885  match obj with
1886     Cic.Constant (name,Some bo,ty,args,attrs) ->
1887      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1888         since type_of_aux' destroys localization information (which are
1889         preserved by type_of_aux *)
1890      let loc exn' =
1891       try
1892        Cic.CicHash.find localization_tbl bo
1893       with Not_found ->
1894        HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1895        raise exn' in
1896      let bo',boty,metasenv,ugraph =
1897       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1898      let ty',_,metasenv,ugraph =
1899       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1900      let subst,metasenv,ugraph =
1901       try
1902        fo_unif_subst [] [] metasenv boty ty' ugraph
1903       with
1904          RefineFailure _
1905        | Uncertain _ as exn ->
1906           let msg = 
1907             lazy ("The term " ^
1908              CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1909              " has type " ^
1910              CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1911              " but is here used with type " ^
1912              CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1913           in
1914            let exn' =
1915             match exn with
1916                RefineFailure _ -> RefineFailure msg
1917              | Uncertain _ -> Uncertain msg
1918              | _ -> assert false
1919            in
1920             raise (HExtlib.Localized (loc exn',exn'))
1921      in
1922      let bo' = CicMetaSubst.apply_subst subst bo' in
1923      let ty' = CicMetaSubst.apply_subst subst ty' in
1924      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1925       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1926   | Cic.Constant (name,None,ty,args,attrs) ->
1927      let ty',_,metasenv,ugraph =
1928       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1929      in
1930       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1931   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1932      assert (metasenv' = metasenv);
1933      (* Here we do not check the metasenv for correctness *)
1934      let bo',boty,metasenv,ugraph =
1935       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1936      let ty',sort,metasenv,ugraph =
1937       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1938      begin
1939       match sort with
1940          Cic.Sort _
1941        (* instead of raising Uncertain, let's hope that the meta will become
1942           a sort *)
1943        | Cic.Meta _ -> ()
1944        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1945      end;
1946      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1947      let bo' = CicMetaSubst.apply_subst subst bo' in
1948      let ty' = CicMetaSubst.apply_subst subst ty' in
1949      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1950       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1951   | Cic.Variable _ -> assert false (* not implemented *)
1952   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1953      (*CSC: this code is greately simplified and many many checks are missing *)
1954      (*CSC: e.g. the constructors are not required to build their own types,  *)
1955      (*CSC: the arities are not required to have as type a sort, etc.         *)
1956      let uri = match uri with Some uri -> uri | None -> assert false in
1957      let typesno = List.length tys in
1958      (* first phase: we fix only the types *)
1959      let metasenv,ugraph,tys =
1960       List.fold_right
1961        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1962          let ty',_,metasenv,ugraph =
1963           (* clean_dummy_dependent_types: false to avoid cleaning the names
1964              of the left products, that must be identical to those of the
1965              constructors; however, non-left products should probably be
1966              cleaned *)
1967           type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1968            metasenv [] ty ugraph
1969          in
1970           metasenv,ugraph,(name,b,ty',cl)::res
1971        ) tys (metasenv,ugraph,[]) in
1972      let con_context =
1973       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1974      (* second phase: we fix only the constructors *)
1975      let saved_menv = metasenv in
1976      let metasenv,ugraph,tys =
1977       List.fold_right
1978        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1979          let metasenv,ugraph,cl' =
1980           List.fold_right
1981            (fun (name,ty) (metasenv,ugraph,res) ->
1982              let ty =
1983               CicTypeChecker.debrujin_constructor
1984               ~cb:(relocalize localization_tbl) uri typesno [] ty in
1985              let ty',_,metasenv,ugraph =
1986               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1987              let ty' = undebrujin uri typesno tys ty' in
1988               metasenv@saved_menv,ugraph,(name,ty')::res
1989            ) cl (metasenv,ugraph,[])
1990          in
1991           metasenv,ugraph,(name,b,ty,cl')::res
1992        ) tys (metasenv,ugraph,[]) in
1993      (* third phase: we check the positivity condition *)
1994      let metasenv,ugraph,tys = 
1995        are_all_occurrences_positive metasenv ugraph uri tys paramsno 
1996      in
1997      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1998 ;;
1999
2000 (* sara' piu' veloce che raffinare da zero? mah.... *)
2001 let pack_coercion metasenv ctx t =
2002  let module C = Cic in
2003  let rec merge_coercions ctx =
2004    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2005    function
2006    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2007    | C.Meta (n,subst) ->
2008       let subst' =
2009        List.map
2010         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2011       in
2012        C.Meta (n,subst')
2013    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2014    | C.Prod (name,so,dest) -> 
2015        let ctx' = (Some (name,C.Decl so))::ctx in
2016        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) 
2017    | C.Lambda (name,so,dest) -> 
2018        let ctx' = (Some (name,C.Decl so))::ctx in
2019        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2020    | C.LetIn (name,so,ty,dest) -> 
2021        let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2022        C.LetIn
2023         (name, merge_coercions ctx so, merge_coercions ctx ty,
2024          merge_coercions ctx' dest)
2025    | C.Appl l -> 
2026       let l = List.map (merge_coercions ctx) l in
2027       let t = C.Appl l in
2028        let b,_,_,_,_ = is_a_double_coercion t in
2029        if b then
2030          let ugraph = CicUniv.oblivion_ugraph in
2031          let old_insert_coercions = !insert_coercions in
2032          insert_coercions := false;
2033          let newt, _, menv, _ = 
2034            try 
2035              type_of_aux' metasenv ctx t ugraph 
2036            with RefineFailure _ | Uncertain _ -> 
2037              t, t, [], ugraph 
2038          in
2039          insert_coercions := old_insert_coercions;
2040          if metasenv <> [] || menv = [] then 
2041            newt 
2042          else 
2043            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2044        else
2045          t
2046    | C.Var (uri,exp_named_subst) -> 
2047        let exp_named_subst = List.map aux exp_named_subst in
2048        C.Var (uri, exp_named_subst)
2049    | C.Const (uri,exp_named_subst) ->
2050        let exp_named_subst = List.map aux exp_named_subst in
2051        C.Const (uri, exp_named_subst)
2052    | C.MutInd (uri,tyno,exp_named_subst) ->
2053        let exp_named_subst = List.map aux exp_named_subst in
2054        C.MutInd (uri,tyno,exp_named_subst)
2055    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2056        let exp_named_subst = List.map aux exp_named_subst in
2057        C.MutConstruct (uri,tyno,consno,exp_named_subst)  
2058    | C.MutCase (uri,tyno,out,te,pl) ->
2059        let pl = List.map (merge_coercions ctx) pl in
2060        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2061    | C.Fix (fno, fl) ->
2062        let ctx' =
2063          List.fold_left
2064            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
2065            ctx fl
2066        in 
2067        let fl = 
2068          List.map 
2069            (fun (name,idx,ty,bo) -> 
2070              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) 
2071          fl
2072        in
2073        C.Fix (fno, fl)
2074    | C.CoFix (fno, fl) ->
2075        let ctx' =
2076          List.fold_left
2077            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
2078            ctx fl
2079        in 
2080        let fl = 
2081          List.map 
2082            (fun (name,ty,bo) -> 
2083              (name, merge_coercions ctx ty, merge_coercions ctx' bo)) 
2084          fl 
2085        in
2086        C.CoFix (fno, fl)
2087  in
2088   merge_coercions ctx t
2089 ;;
2090
2091 let pack_coercion_metasenv conjectures = conjectures (*
2092
2093   TASSI: this code war written when coercions were a toy,
2094          now packing coercions involves unification thus
2095          the metasenv may change, and this pack coercion 
2096          does not handle that.
2097
2098   let module C = Cic in
2099   List.map 
2100     (fun (i, ctx, ty) -> 
2101        let ctx = 
2102          List.fold_right 
2103            (fun item ctx ->
2104               let item' =
2105                 match item with
2106                     Some (name, C.Decl t) -> 
2107                       Some (name, C.Decl (pack_coercion conjectures ctx t))
2108                   | Some (name, C.Def (t,None)) -> 
2109                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
2110                   | Some (name, C.Def (t,Some ty)) -> 
2111                       Some (name, C.Def (pack_coercion conjectures ctx t, 
2112                                          Some (pack_coercion conjectures ctx ty)))
2113                   | None -> None
2114               in
2115                 item'::ctx
2116            ) ctx []
2117        in
2118          ((i,ctx,pack_coercion conjectures ctx ty))
2119     ) conjectures
2120     *)
2121 ;;
2122
2123 let pack_coercion_obj obj = obj (*
2124
2125   TASSI: this code war written when coercions were a toy,
2126          now packing coercions involves unification thus
2127          the metasenv may change, and this pack coercion 
2128          does not handle that.
2129
2130   let module C = Cic in
2131   match obj with
2132   | C.Constant (id, body, ty, params, attrs) -> 
2133       let body = 
2134         match body with 
2135         | None -> None 
2136         | Some body -> Some (pack_coercion [] [] body) 
2137       in
2138       let ty = pack_coercion [] [] ty in
2139         C.Constant (id, body, ty, params, attrs)
2140   | C.Variable (name, body, ty, params, attrs) ->
2141       let body = 
2142         match body with 
2143         | None -> None 
2144         | Some body -> Some (pack_coercion [] [] body) 
2145       in
2146       let ty = pack_coercion [] [] ty in
2147         C.Variable (name, body, ty, params, attrs)
2148   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2149       let conjectures = pack_coercion_metasenv conjectures in
2150       let body = pack_coercion conjectures [] body in
2151       let ty = pack_coercion conjectures [] ty in
2152       C.CurrentProof (name, conjectures, body, ty, params, attrs)
2153   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2154       let indtys = 
2155         List.map 
2156           (fun (name, ind, arity, cl) -> 
2157             let arity = pack_coercion [] [] arity in
2158             let cl = 
2159               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl 
2160             in
2161             (name, ind, arity, cl))
2162           indtys
2163       in
2164         C.InductiveDefinition (indtys, params, leftno, attrs) *)
2165 ;;
2166
2167
2168 (* DEBUGGING ONLY 
2169 let type_of_aux' metasenv context term =
2170  try
2171   let (t,ty,m) = 
2172       type_of_aux' metasenv context term in
2173     debug_print (lazy
2174      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2175    debug_print (lazy
2176     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2177    (t,ty,m)
2178  with
2179  | RefineFailure msg as e ->
2180      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2181      raise e
2182  | Uncertain msg as e ->
2183      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2184      raise e
2185 ;; *)
2186
2187 let profiler2 = HExtlib.profile "CicRefine"
2188
2189 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2190  profiler2.HExtlib.profile
2191   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2192
2193 let typecheck ~localization_tbl metasenv uri obj =
2194  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2195
2196 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2197 (* vim:set foldmethod=marker: *)