components/cic_unification/cicRefine.ml

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