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