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