helm/software/components/cic_unification/cicRefine.ml

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