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