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