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