components/cic_unification/cicRefine.ml

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