helm/software/components/cic_unification/cicRefine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 exception RefineFailure of string Lazy.t;;
  31 exception Uncertain of string Lazy.t;;
  32 exception AssertFailure of string Lazy.t;;
  33
  34 let insert_coercions = ref true
  35
  36 let debug_print = fun _ -> ()
  37
  38 let profiler = HExtlib.profile "CicRefine.fo_unif"
  39
  40 let fo_unif_subst subst context metasenv t1 t2 ugraph =
  41   try
  42 let foo () =
  43     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  44 in profiler.HExtlib.profile foo ()
  45   with
  46       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  47     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  48 ;;
  49
  50 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
  51  let exn' =
  52   match exn with
  53      RefineFailure msg -> RefineFailure (f msg)
  54    | Uncertain msg -> Uncertain (f msg)
  55    | _ -> assert false in
  56  let loc =
  57   try
  58    Cic.CicHash.find localization_tbl t
  59   with Not_found ->
  60    prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
  61    raise exn'
  62  in
  63   raise (HExtlib.Localized (loc,exn'))
  64
  65 let relocalize localization_tbl oldt newt =
  66  try
  67   let infos = Cic.CicHash.find localization_tbl oldt in
  68    Cic.CicHash.remove localization_tbl oldt;
  69    Cic.CicHash.add localization_tbl newt infos;
  70  with
  71   Not_found -> ()
  72 ;;
  73
  74 let rec split l n =
  75  match (l,n) with
  76     (l,0) -> ([], l)
  77   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  78   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
  79 ;;
  80
  81 let exp_impl metasenv subst context =
  82  function
  83   | Some `Type ->
  84       let (metasenv', idx) =
  85         CicMkImplicit.mk_implicit_type metasenv subst context in
  86       let irl =
  87         CicMkImplicit.identity_relocation_list_for_metavariable context in
  88       metasenv', Cic.Meta (idx, irl)
  89   | Some `Closed ->
  90       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
  91       metasenv', Cic.Meta (idx, [])
  92   | None ->
  93       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
  94       let irl =
  95         CicMkImplicit.identity_relocation_list_for_metavariable context in
  96       metasenv', Cic.Meta (idx, irl)
  97   | _ -> assert false
  98 ;;
  99
 100 let is_a_double_coercion t =
 101   let last_of l =
 102     let rec aux = function
 103       | x::[] -> x
 104       | x::tl -> aux tl
 105       | [] -> assert false
 106     in
 107     aux l
 108   in
 109   let dummyres =
 110     false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
 111   in
 112   match t with
 113   | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
 114       (match last_of tl with
 115       | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
 116           let head = last_of tl2 in
 117           true, c1, c2, head
 118       | _ -> dummyres)
 119   | _ -> dummyres
 120
 121 let rec type_of_constant uri ugraph =
 122  let module C = Cic in
 123  let module R = CicReduction in
 124  let module U = UriManager in
 125   let _ = CicTypeChecker.typecheck uri in
 126   let obj,u =
 127    try
 128     CicEnvironment.get_cooked_obj ugraph uri
 129    with Not_found -> assert false
 130   in
 131    match obj with
 132       C.Constant (_,_,ty,_,_) -> ty,u
 133     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
 134     | _ ->
 135        raise
 136         (RefineFailure
 137           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 138
 139 and type_of_variable uri ugraph =
 140   let module C = Cic in
 141   let module R = CicReduction in
 142   let module U = UriManager in
 143   let _ = CicTypeChecker.typecheck uri in
 144   let obj,u =
 145    try
 146     CicEnvironment.get_cooked_obj ugraph uri
 147     with Not_found -> assert false
 148   in
 149    match obj with
 150       C.Variable (_,_,ty,_,_) -> ty,u
 151     | _ ->
 152         raise
 153          (RefineFailure
 154           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
 155
 156 and type_of_mutual_inductive_defs uri i ugraph =
 157   let module C = Cic in
 158   let module R = CicReduction in
 159   let module U = UriManager in
 160   let _ = CicTypeChecker.typecheck uri in
 161   let obj,u =
 162    try
 163     CicEnvironment.get_cooked_obj ugraph uri
 164    with Not_found -> assert false
 165   in
 166    match obj with
 167       C.InductiveDefinition (dl,_,_,_) ->
 168         let (_,_,arity,_) = List.nth dl i in
 169          arity,u
 170     | _ ->
 171        raise
 172         (RefineFailure
 173          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
 174
 175 and type_of_mutual_inductive_constr uri i j ugraph =
 176   let module C = Cic in
 177   let module R = CicReduction in
 178   let module U = UriManager in
 179   let _ = CicTypeChecker.typecheck uri in
 180    let obj,u =
 181     try
 182      CicEnvironment.get_cooked_obj ugraph uri
 183     with Not_found -> assert false
 184    in
 185     match obj with
 186         C.InductiveDefinition (dl,_,_,_) ->
 187           let (_,_,_,cl) = List.nth dl i in
 188           let (_,ty) = List.nth cl (j-1) in
 189             ty,u
 190       | _ ->
 191           raise
 192                   (RefineFailure
 193               (lazy
 194                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 195
 196
 197 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 198
 199 (* the check_branch function checks if a branch of a case is refinable.
 200    It returns a pair (outype_instance,args), a subst and a metasenv.
 201    outype_instance is the expected result of applying the case outtype
 202    to args.
 203    The problem is that outype is in general unknown, and we should
 204    try to synthesize it from the above information, that is in general
 205    a second order unification problem. *)
 206
 207 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 208   let module C = Cic in
 209     (* let module R = CicMetaSubst in *)
 210   let module R = CicReduction in
 211     match R.whd ~subst context expectedtype with
 212         C.MutInd (_,_,_) ->
 213           (n,context,actualtype, [term]), subst, metasenv, ugraph
 214       | C.Appl (C.MutInd (_,_,_)::tl) ->
 215           let (_,arguments) = split tl left_args_no in
 216             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 217       | C.Prod (name,so,de) ->
 218           (* we expect that the actual type of the branch has the due
 219              number of Prod *)
 220           (match R.whd ~subst context actualtype with
 221                C.Prod (name',so',de') ->
 222                  let subst, metasenv, ugraph1 =
 223                    fo_unif_subst subst context metasenv so so' ugraph in
 224                  let term' =
 225                    (match CicSubstitution.lift 1 term with
 226                         C.Appl l -> C.Appl (l@[C.Rel 1])
 227                       | t -> C.Appl [t ; C.Rel 1]) in
 228                    (* we should also check that the name variable is anonymous in
 229                       the actual type de' ?? *)
 230                    check_branch (n+1)
 231                      ((Some (name,(C.Decl so)))::context)
 232                        metasenv subst left_args_no de' term' de ugraph1
 233              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
 234       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 235
 236 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 237      ugraph
 238 =
 239   let rec type_of_aux subst metasenv context t ugraph =
 240     let module C = Cic in
 241     let module S = CicSubstitution in
 242     let module U = UriManager in
 243      let (t',_,_,_,_) as res =
 244       match t with
 245           (*    function *)
 246           C.Rel n ->
 247             (try
 248                match List.nth context (n - 1) with
 249                    Some (_,C.Decl ty) ->
 250                      t,S.lift n ty,subst,metasenv, ugraph
 251                  | Some (_,C.Def (_,Some ty)) ->
 252                      t,S.lift n ty,subst,metasenv, ugraph
 253                  | Some (_,C.Def (bo,None)) ->
 254                      let ty,ugraph =
 255                       (* if it is in the context it must be already well-typed*)
 256                       CicTypeChecker.type_of_aux' ~subst metasenv context
 257                        (S.lift n bo) ugraph
 258                      in
 259                       t,ty,subst,metasenv,ugraph
 260                  | None ->
 261                     enrich localization_tbl t
 262                      (RefineFailure (lazy "Rel to hidden hypothesis"))
 263              with
 264               _ ->
 265                enrich localization_tbl t
 266                 (RefineFailure (lazy "Not a close term")))
 267         | C.Var (uri,exp_named_subst) ->
 268             let exp_named_subst',subst',metasenv',ugraph1 =
 269               check_exp_named_subst
 270                 subst metasenv context exp_named_subst ugraph
 271             in
 272             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 273             let ty =
 274               CicSubstitution.subst_vars exp_named_subst' ty_uri
 275             in
 276               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 277         | C.Meta (n,l) ->
 278             (try
 279                let (canonical_context, term,ty) =
 280                  CicUtil.lookup_subst n subst
 281                in
 282                let l',subst',metasenv',ugraph1 =
 283                  check_metasenv_consistency n subst metasenv context
 284                    canonical_context l ugraph
 285                in
 286                  (* trust or check ??? *)
 287                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 288                    subst', metasenv', ugraph1
 289                    (* type_of_aux subst metasenv
 290                       context (CicSubstitution.subst_meta l term) *)
 291              with CicUtil.Subst_not_found _ ->
 292                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 293                let l',subst',metasenv', ugraph1 =
 294                  check_metasenv_consistency n subst metasenv context
 295                    canonical_context l ugraph
 296                in
 297                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 298                    subst', metasenv',ugraph1)
 299         | C.Sort (C.Type tno) ->
 300             let tno' = CicUniv.fresh() in
 301             let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 302               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 303         | C.Sort _ ->
 304             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 305         | C.Implicit infos ->
 306            let metasenv',t' = exp_impl metasenv subst context infos in
 307             type_of_aux subst metasenv' context t' ugraph
 308         | C.Cast (te,ty) ->
 309             let ty',_,subst',metasenv',ugraph1 =
 310               type_of_aux subst metasenv context ty ugraph
 311             in
 312             let te',inferredty,subst'',metasenv'',ugraph2 =
 313               type_of_aux subst' metasenv' context te ugraph1
 314             in
 315              (try
 316                let subst''',metasenv''',ugraph3 =
 317                  fo_unif_subst subst'' context metasenv''
 318                    inferredty ty' ugraph2
 319                in
 320                 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 321               with
 322                exn ->
 323                 enrich localization_tbl te'
 324                  ~f:(fun _ ->
 325                    lazy ("The term " ^
 326                     CicMetaSubst.ppterm_in_context subst'' te'
 327                      context ^ " has type " ^
 328                     CicMetaSubst.ppterm_in_context subst'' inferredty
 329                      context ^ " but is here used with type " ^
 330                     CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
 331              )
 332         | C.Prod (name,s,t) ->
 333             let carr t subst context = CicMetaSubst.apply_subst subst t in
 334             let coerce_to_sort in_source tgt_sort t type_to_coerce
 335                  subst context metasenv uragph
 336             =
 337               if not !insert_coercions then
 338                 t,type_to_coerce,subst,metasenv,ugraph
 339               else
 340                 let coercion_src = carr type_to_coerce subst context in
 341                 match coercion_src with
 342                 | Cic.Sort _ ->
 343                     t,type_to_coerce,subst,metasenv,ugraph
 344                 | Cic.Meta _ as meta ->
 345                     t, meta, subst, metasenv, ugraph
 346                 | Cic.Cast _ as cast ->
 347                     t, cast, subst, metasenv, ugraph
 348                 | term ->
 349                     let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
 350                     let boh =
 351                      CoercGraph.look_for_coercion coercion_src coercion_tgt
 352                     in
 353                     (match boh with
 354                     | CoercGraph.NoCoercion
 355                     | CoercGraph.NotHandled _ ->
 356                        enrich localization_tbl t
 357                         (RefineFailure
 358                           (lazy ("The term " ^
 359                           CicMetaSubst.ppterm_in_context subst t context ^
 360                           " is not a type since it has type " ^
 361                           CicMetaSubst.ppterm_in_context
 362                            subst coercion_src context ^ " that is not a sort")))
 363                     | CoercGraph.NotMetaClosed ->
 364                        enrich localization_tbl t
 365                         (Uncertain
 366                           (lazy ("The term " ^
 367                           CicMetaSubst.ppterm_in_context subst t context ^
 368                           " is not a type since it has type " ^
 369                           CicMetaSubst.ppterm_in_context
 370                            subst coercion_src context ^ " that is not a sort")))
 371                     | CoercGraph.SomeCoercion c ->
 372                        let newt,_,subst,metasenv,ugraph =
 373                          type_of_aux subst metasenv context (Cic.Appl[c;t])
 374                           ugraph in
 375                        let newt, tty, subst, metasenv, ugraph =
 376                          avoid_double_coercion context subst metasenv ugraph
 377                           newt coercion_tgt
 378                        in
 379                         newt, tty, subst, metasenv, ugraph)
 380             in
 381             let s',sort1,subst',metasenv',ugraph1 =
 382               type_of_aux subst metasenv context s ugraph
 383             in
 384             let s',sort1,subst', metasenv',ugraph1 =
 385               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 386               s' sort1 subst' context metasenv' ugraph1
 387             in
 388             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 389             let t',sort2,subst'',metasenv'',ugraph2 =
 390               type_of_aux subst' metasenv'
 391                 context_for_t t ugraph1
 392             in
 393             let t',sort2,subst'',metasenv'',ugraph2 =
 394               coerce_to_sort false (Cic.Type(CicUniv.fresh()))
 395               t' sort2 subst'' context_for_t metasenv'' ugraph2
 396             in
 397               let sop,subst''',metasenv''',ugraph3 =
 398                 sort_of_prod subst'' metasenv''
 399                   context (name,s') (sort1,sort2) ugraph2
 400               in
 401                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 402         | C.Lambda (n,s,t) ->
 403
 404             let s',sort1,subst',metasenv',ugraph1 =
 405               type_of_aux subst metasenv context s ugraph in
 406             let s',sort1,subst',metasenv',ugraph1 =
 407               if not !insert_coercions then
 408                 s',sort1, subst', metasenv', ugraph1
 409               else
 410                 match CicReduction.whd ~subst:subst' context sort1 with
 411                   | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
 412                   | coercion_src ->
 413                      let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
 414                      let boh =
 415                       CoercGraph.look_for_coercion coercion_src coercion_tgt
 416                      in
 417                       match boh with
 418                       | CoercGraph.SomeCoercion c ->
 419                         let newt,_,subst',metasenv',ugraph1 =
 420                          type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
 421                           ugraph1 in
 422                         let newt, tty, subst', metasenv', ugraph1 =
 423                           avoid_double_coercion context subst' metasenv'
 424                            ugraph1 newt coercion_tgt
 425                         in
 426                          newt, tty, subst', metasenv', ugraph1
 427                       | CoercGraph.NoCoercion
 428                       |  CoercGraph.NotHandled _ ->
 429                         enrich localization_tbl s'
 430                          (RefineFailure
 431                           (lazy ("The term " ^
 432                           CicMetaSubst.ppterm_in_context subst s' context ^
 433                           " is not a type since it has type " ^
 434                           CicMetaSubst.ppterm_in_context
 435                            subst coercion_src context ^ " that is not a sort")))
 436                       | CoercGraph.NotMetaClosed ->
 437                         enrich localization_tbl s'
 438                          (Uncertain
 439                           (lazy ("The term " ^
 440                           CicMetaSubst.ppterm_in_context subst s' context ^
 441                           " is not a type since it has type " ^
 442                           CicMetaSubst.ppterm_in_context
 443                            subst coercion_src context ^ " that is not a sort")))
 444             in
 445             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 446             let t',type2,subst'',metasenv'',ugraph2 =
 447               type_of_aux subst' metasenv' context_for_t t ugraph1
 448             in
 449               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 450                 subst'',metasenv'',ugraph2
 451         | C.LetIn (n,s,t) ->
 452             (* only to check if s is well-typed *)
 453             let s',ty,subst',metasenv',ugraph1 =
 454               type_of_aux subst metasenv context s ugraph
 455             in
 456            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 457
 458             let t',inferredty,subst'',metasenv'',ugraph2 =
 459               type_of_aux subst' metasenv'
 460                 context_for_t t ugraph1
 461             in
 462               (* One-step LetIn reduction.
 463                * Even faster than the previous solution.
 464                * Moreover the inferred type is closer to the expected one.
 465                *)
 466               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
 467                 subst'',metasenv'',ugraph2
 468         | C.Appl (he::((_::_) as tl)) ->
 469             let he',hetype,subst',metasenv',ugraph1 =
 470               type_of_aux subst metasenv context he ugraph
 471             in
 472             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 473               List.fold_right
 474                 (fun x (res,subst,metasenv,ugraph) ->
 475                    let x',ty,subst',metasenv',ugraph1 =
 476                      type_of_aux subst metasenv context x ugraph
 477                    in
 478                     (x', ty)::res,subst',metasenv',ugraph1
 479                 ) tl ([],subst',metasenv',ugraph1)
 480             in
 481             let tl',applty,subst''',metasenv''',ugraph3 =
 482               eat_prods true subst'' metasenv'' context
 483                 he' hetype tlbody_and_type ugraph2
 484             in
 485               avoid_double_coercion context
 486                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
 487         | C.Appl _ -> assert false
 488         | C.Const (uri,exp_named_subst) ->
 489             let exp_named_subst',subst',metasenv',ugraph1 =
 490               check_exp_named_subst subst metasenv context
 491                 exp_named_subst ugraph in
 492             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 493             let cty =
 494               CicSubstitution.subst_vars exp_named_subst' ty_uri
 495             in
 496               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 497         | C.MutInd (uri,i,exp_named_subst) ->
 498             let exp_named_subst',subst',metasenv',ugraph1 =
 499               check_exp_named_subst subst metasenv context
 500                 exp_named_subst ugraph
 501             in
 502             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 503             let cty =
 504               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 505               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 506         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 507             let exp_named_subst',subst',metasenv',ugraph1 =
 508               check_exp_named_subst subst metasenv context
 509                 exp_named_subst ugraph
 510             in
 511             let ty_uri,ugraph2 =
 512               type_of_mutual_inductive_constr uri i j ugraph1
 513             in
 514             let cty =
 515               CicSubstitution.subst_vars exp_named_subst' ty_uri
 516             in
 517               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 518                 metasenv',ugraph2
 519         | C.MutCase (uri, i, outtype, term, pl) ->
 520             (* first, get the inductive type (and noparams)
 521              * in the environment  *)
 522             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 523               let _ = CicTypeChecker.typecheck uri in
 524               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 525               match obj with
 526                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 527                     List.nth l i , expl_params, parsno, u
 528                 | _ ->
 529                     enrich localization_tbl t
 530                      (RefineFailure
 531                        (lazy ("Unkown mutual inductive definition " ^
 532                          U.string_of_uri uri)))
 533            in
 534            let rec count_prod t =
 535              match CicReduction.whd ~subst context t with
 536                  C.Prod (_, _, t) -> 1 + (count_prod t)
 537                | _ -> 0
 538            in
 539            let no_args = count_prod arity in
 540              (* now, create a "generic" MutInd *)
 541            let metasenv,left_args =
 542              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 543            in
 544            let metasenv,right_args =
 545              let no_right_params = no_args - no_left_params in
 546                if no_right_params < 0 then assert false
 547                else CicMkImplicit.n_fresh_metas
 548                       metasenv subst context no_right_params
 549            in
 550            let metasenv,exp_named_subst =
 551              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 552            let expected_type =
 553              if no_args = 0 then
 554                C.MutInd (uri,i,exp_named_subst)
 555              else
 556                C.Appl
 557                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 558            in
 559              (* check consistency with the actual type of term *)
 560            let term',actual_type,subst,metasenv,ugraph1 =
 561              type_of_aux subst metasenv context term ugraph in
 562            let expected_type',_, subst, metasenv,ugraph2 =
 563              type_of_aux subst metasenv context expected_type ugraph1
 564            in
 565            let actual_type = CicReduction.whd ~subst context actual_type in
 566            let subst,metasenv,ugraph3 =
 567             try
 568              fo_unif_subst subst context metasenv
 569                expected_type' actual_type ugraph2
 570             with
 571              exn ->
 572               enrich localization_tbl term' exn
 573                ~f:(function _ ->
 574                  lazy ("The term " ^
 575                   CicMetaSubst.ppterm_in_context subst term'
 576                    context ^ " has type " ^
 577                   CicMetaSubst.ppterm_in_context subst actual_type
 578                    context ^ " but is here used with type " ^
 579                   CicMetaSubst.ppterm_in_context subst expected_type' context))
 580            in
 581            let rec instantiate_prod t =
 582             function
 583                [] -> t
 584              | he::tl ->
 585                 match CicReduction.whd ~subst context t with
 586                    C.Prod (_,_,t') ->
 587                     instantiate_prod (CicSubstitution.subst he t') tl
 588                  | _ -> assert false
 589            in
 590            let arity_instantiated_with_left_args =
 591             instantiate_prod arity left_args in
 592              (* TODO: check if the sort elimination
 593               * is allowed: [(I q1 ... qr)|B] *)
 594            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 595              List.fold_left
 596                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 597                   let constructor =
 598                     if left_args = [] then
 599                       (C.MutConstruct (uri,i,j,exp_named_subst))
 600                     else
 601                       (C.Appl
 602                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 603                   in
 604                   let p',actual_type,subst,metasenv,ugraph1 =
 605                     type_of_aux subst metasenv context p ugraph
 606                   in
 607                   let constructor',expected_type, subst, metasenv,ugraph2 =
 608                     type_of_aux subst metasenv context constructor ugraph1
 609                   in
 610                   let outtypeinstance,subst,metasenv,ugraph3 =
 611                     check_branch 0 context metasenv subst no_left_params
 612                       actual_type constructor' expected_type ugraph2
 613                   in
 614                     (pl @ [p'],j+1,
 615                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 616                ([],1,[],subst,metasenv,ugraph3) pl
 617            in
 618
 619              (* we are left to check that the outype matches his instances.
 620                 The easy case is when the outype is specified, that amount
 621                 to a trivial check. Otherwise, we should guess a type from
 622                 its instances
 623              *)
 624
 625            let outtype,outtypety, subst, metasenv,ugraph4 =
 626              type_of_aux subst metasenv context outtype ugraph4 in
 627            (match outtype with
 628            | C.Meta (n,l) ->
 629                (let candidate,ugraph5,metasenv,subst =
 630                  let exp_name_subst, metasenv =
 631                     let o,_ =
 632                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 633                     in
 634                     let uris = CicUtil.params_of_obj o in
 635                     List.fold_right (
 636                       fun uri (acc,metasenv) ->
 637                         let metasenv',new_meta =
 638                            CicMkImplicit.mk_implicit metasenv subst context
 639                         in
 640                         let irl =
 641                           CicMkImplicit.identity_relocation_list_for_metavariable
 642                             context
 643                         in
 644                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 645                     ) uris ([],metasenv)
 646                  in
 647                  let ty =
 648                   match left_args,right_args with
 649                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 650                    | _,_ ->
 651                       let rec mk_right_args =
 652                        function
 653                           0 -> []
 654                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 655                       in
 656                       let right_args_no = List.length right_args in
 657                       let lifted_left_args =
 658                        List.map (CicSubstitution.lift right_args_no) left_args
 659                       in
 660                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 661                         (lifted_left_args @ mk_right_args right_args_no))
 662                  in
 663                  let fresh_name =
 664                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 665                      context Cic.Anonymous ~typ:ty
 666                  in
 667                  match outtypeinstances with
 668                  | [] ->
 669                      let extended_context =
 670                       let rec add_right_args =
 671                        function
 672                           Cic.Prod (name,ty,t) ->
 673                            Some (name,Cic.Decl ty)::(add_right_args t)
 674                         | _ -> []
 675                       in
 676                        (Some (fresh_name,Cic.Decl ty))::
 677                        (List.rev
 678                         (add_right_args arity_instantiated_with_left_args))@
 679                        context
 680                      in
 681                      let metasenv,new_meta =
 682                        CicMkImplicit.mk_implicit metasenv subst extended_context
 683                      in
 684                        let irl =
 685                        CicMkImplicit.identity_relocation_list_for_metavariable
 686                          extended_context
 687                      in
 688                      let rec add_lambdas b =
 689                       function
 690                          Cic.Prod (name,ty,t) ->
 691                           Cic.Lambda (name,ty,(add_lambdas b t))
 692                        | _ -> Cic.Lambda (fresh_name, ty, b)
 693                      in
 694                      let candidate =
 695                       add_lambdas (Cic.Meta (new_meta,irl))
 696                        arity_instantiated_with_left_args
 697                      in
 698                      (Some candidate),ugraph4,metasenv,subst
 699                  | (constructor_args_no,_,instance,_)::tl ->
 700                      try
 701                        let instance',subst,metasenv =
 702                          CicMetaSubst.delift_rels subst metasenv
 703                           constructor_args_no instance
 704                        in
 705                        let candidate,ugraph,metasenv,subst =
 706                          List.fold_left (
 707                            fun (candidate_oty,ugraph,metasenv,subst)
 708                              (constructor_args_no,_,instance,_) ->
 709                                match candidate_oty with
 710                                | None -> None,ugraph,metasenv,subst
 711                                | Some ty ->
 712                                  try
 713                                    let instance',subst,metasenv =
 714                                      CicMetaSubst.delift_rels subst metasenv
 715                                       constructor_args_no instance
 716                                    in
 717                                    let subst,metasenv,ugraph =
 718                                     fo_unif_subst subst context metasenv
 719                                       instance' ty ugraph
 720                                    in
 721                                     candidate_oty,ugraph,metasenv,subst
 722                                  with
 723                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 724                                   | CicUnification.UnificationFailure _
 725                                   | CicUnification.Uncertain _ ->
 726                                      None,ugraph,metasenv,subst
 727                          ) (Some instance',ugraph4,metasenv,subst) tl
 728                        in
 729                        match candidate with
 730                        | None -> None, ugraph,metasenv,subst
 731                        | Some t ->
 732                           let rec add_lambdas n b =
 733                            function
 734                               Cic.Prod (name,ty,t) ->
 735                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 736                             | _ ->
 737                               Cic.Lambda (fresh_name, ty,
 738                                CicSubstitution.lift (n + 1) t)
 739                           in
 740                            Some
 741                             (add_lambdas 0 t arity_instantiated_with_left_args),
 742                            ugraph,metasenv,subst
 743                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 744                        None,ugraph4,metasenv,subst
 745                in
 746                match candidate with
 747                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 748                | Some candidate ->
 749                    let subst,metasenv,ugraph =
 750                     try
 751                      fo_unif_subst subst context metasenv
 752                        candidate outtype ugraph5
 753                     with
 754                      exn -> assert false(* unification against a metavariable *)
 755                    in
 756                      C.MutCase (uri, i, outtype, term', pl'),
 757                       CicReduction.head_beta_reduce
 758                        (CicMetaSubst.apply_subst subst
 759                         (Cic.Appl (outtype::right_args@[term']))),
 760                      subst,metasenv,ugraph)
 761            | _ ->    (* easy case *)
 762              let tlbody_and_type,subst,metasenv,ugraph4 =
 763                List.fold_right
 764                  (fun x (res,subst,metasenv,ugraph) ->
 765                     let x',ty,subst',metasenv',ugraph1 =
 766                       type_of_aux subst metasenv context x ugraph
 767                     in
 768                       (x', ty)::res,subst',metasenv',ugraph1
 769                  ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
 770              in
 771              let _,_,subst,metasenv,ugraph4 =
 772                eat_prods false subst metasenv context
 773                  outtype outtypety tlbody_and_type ugraph4
 774              in
 775              let _,_, subst, metasenv,ugraph5 =
 776                type_of_aux subst metasenv context
 777                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 778              in
 779              let (subst,metasenv,ugraph6) =
 780                List.fold_left2
 781                  (fun (subst,metasenv,ugraph)
 782                    p (constructor_args_no,context,instance,args)
 783                   ->
 784                     let instance' =
 785                       let appl =
 786                         let outtype' =
 787                           CicSubstitution.lift constructor_args_no outtype
 788                         in
 789                           C.Appl (outtype'::args)
 790                       in
 791                         CicReduction.whd ~subst context appl
 792                     in
 793                      try
 794                       fo_unif_subst subst context metasenv instance instance'
 795                        ugraph
 796                      with
 797                       exn ->
 798                        enrich localization_tbl p exn
 799                         ~f:(function _ ->
 800                           lazy ("The term " ^
 801                            CicMetaSubst.ppterm_in_context subst p
 802                             context ^ " has type " ^
 803                            CicMetaSubst.ppterm_in_context subst instance'
 804                             context ^ " but is here used with type " ^
 805                            CicMetaSubst.ppterm_in_context subst instance
 806                             context)))
 807                  (subst,metasenv,ugraph5) pl' outtypeinstances
 808              in
 809                C.MutCase (uri, i, outtype, term', pl'),
 810                  CicReduction.head_beta_reduce
 811                   (CicMetaSubst.apply_subst subst
 812                    (C.Appl(outtype::right_args@[term]))),
 813                  subst,metasenv,ugraph6)
 814         | C.Fix (i,fl) ->
 815             let fl_ty',subst,metasenv,types,ugraph1 =
 816               List.fold_left
 817                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 818                    let ty',_,subst',metasenv',ugraph1 =
 819                       type_of_aux subst metasenv context ty ugraph
 820                    in
 821                      fl @ [ty'],subst',metasenv',
 822                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 823                 ) ([],subst,metasenv,[],ugraph) fl
 824             in
 825             let len = List.length types in
 826             let context' = types@context in
 827             let fl_bo',subst,metasenv,ugraph2 =
 828               List.fold_left
 829                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 830                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 831                      type_of_aux subst metasenv context' bo ugraph in
 832                    let expected_ty = CicSubstitution.lift len ty in
 833                    let subst',metasenv',ugraph' =
 834                     try
 835                      fo_unif_subst subst context' metasenv
 836                        ty_of_bo expected_ty ugraph1
 837                     with
 838                      exn ->
 839                       enrich localization_tbl bo exn
 840                        ~f:(function _ ->
 841                          lazy ("The term " ^
 842                           CicMetaSubst.ppterm_in_context subst bo
 843                            context' ^ " has type " ^
 844                           CicMetaSubst.ppterm_in_context subst ty_of_bo
 845                            context' ^ " but is here used with type " ^
 846                           CicMetaSubst.ppterm_in_context subst expected_ty
 847                            context))
 848                    in
 849                      fl @ [bo'] , subst',metasenv',ugraph'
 850                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 851             in
 852             let ty = List.nth fl_ty' i in
 853             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 854              * and we want the new fl with bo' and ty' injected in the right
 855              * place.
 856              *)
 857             let rec map3 f l1 l2 l3 =
 858               match l1,l2,l3 with
 859               | [],[],[] -> []
 860               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 861               | _ -> assert false
 862             in
 863             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 864               fl_ty' fl_bo' fl
 865             in
 866               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 867         | C.CoFix (i,fl) ->
 868             let fl_ty',subst,metasenv,types,ugraph1 =
 869               List.fold_left
 870                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 871                    let ty',_,subst',metasenv',ugraph1 =
 872                      type_of_aux subst metasenv context ty ugraph
 873                    in
 874                      fl @ [ty'],subst',metasenv',
 875                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 876                 ) ([],subst,metasenv,[],ugraph) fl
 877             in
 878             let len = List.length types in
 879             let context' = types@context in
 880             let fl_bo',subst,metasenv,ugraph2 =
 881               List.fold_left
 882                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 883                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 884                      type_of_aux subst metasenv context' bo ugraph in
 885                    let expected_ty = CicSubstitution.lift len ty in
 886                    let subst',metasenv',ugraph' =
 887                     try
 888                      fo_unif_subst subst context' metasenv
 889                        ty_of_bo expected_ty ugraph1
 890                     with
 891                      exn ->
 892                       enrich localization_tbl bo exn
 893                        ~f:(function _ ->
 894                          lazy ("The term " ^
 895                           CicMetaSubst.ppterm_in_context subst bo
 896                            context' ^ " has type " ^
 897                           CicMetaSubst.ppterm_in_context subst ty_of_bo
 898                            context' ^ " but is here used with type " ^
 899                           CicMetaSubst.ppterm_in_context subst expected_ty
 900                            context))
 901                    in
 902                      fl @ [bo'],subst',metasenv',ugraph'
 903                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 904             in
 905             let ty = List.nth fl_ty' i in
 906             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 907              * and we want the new fl with bo' and ty' injected in the right
 908              * place.
 909              *)
 910             let rec map3 f l1 l2 l3 =
 911               match l1,l2,l3 with
 912               | [],[],[] -> []
 913               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 914               | _ -> assert false
 915             in
 916             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 917               fl_ty' fl_bo' fl
 918             in
 919               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 920      in
 921       relocalize localization_tbl t t';
 922       res
 923
 924   (* check_metasenv_consistency checks that the "canonical" context of a
 925      metavariable is consitent - up to relocation via the relocation list l -
 926      with the actual context *)
 927   and check_metasenv_consistency
 928     metano subst metasenv context canonical_context l ugraph
 929     =
 930     let module C = Cic in
 931     let module R = CicReduction in
 932     let module S = CicSubstitution in
 933     let lifted_canonical_context =
 934       let rec aux i =
 935         function
 936             [] -> []
 937           | (Some (n,C.Decl t))::tl ->
 938               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 939           | (Some (n,C.Def (t,None)))::tl ->
 940               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 941           | None::tl -> None::(aux (i+1) tl)
 942           | (Some (n,C.Def (t,Some ty)))::tl ->
 943               (Some (n,
 944                      C.Def ((S.subst_meta l (S.lift i t)),
 945                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 946       in
 947         aux 1 canonical_context
 948     in
 949       try
 950         List.fold_left2
 951           (fun (l,subst,metasenv,ugraph) t ct ->
 952              match (t,ct) with
 953                  _,None ->
 954                    l @ [None],subst,metasenv,ugraph
 955                | Some t,Some (_,C.Def (ct,_)) ->
 956                    let subst',metasenv',ugraph' =
 957                    (try
 958                       fo_unif_subst subst context metasenv t ct ugraph
 959                     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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
 960                    in
 961                      l @ [Some t],subst',metasenv',ugraph'
 962                | Some t,Some (_,C.Decl ct) ->
 963                    let t',inferredty,subst',metasenv',ugraph1 =
 964                      type_of_aux subst metasenv context t ugraph
 965                    in
 966                    let subst'',metasenv'',ugraph2 =
 967                      (try
 968                         fo_unif_subst
 969                           subst' context metasenv' inferredty ct ugraph1
 970                       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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
 971                    in
 972                      l @ [Some t'], subst'',metasenv'',ugraph2
 973                | None, Some _  ->
 974                    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 subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
 975       with
 976           Invalid_argument _ ->
 977             raise
 978             (RefineFailure
 979                (lazy (sprintf
 980                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 981                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 982                   (CicMetaSubst.ppcontext subst canonical_context))))
 983
 984   and check_exp_named_subst metasubst metasenv context tl ugraph =
 985     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 986       match tl with
 987           [] -> [],metasubst,metasenv,ugraph
 988         | (uri,t)::tl ->
 989             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 990             let typeofvar =
 991               CicSubstitution.subst_vars substs ty_uri in
 992               (* CSC: why was this code here? it is wrong
 993                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 994                  Cic.Variable (_,Some bo,_,_) ->
 995                  raise
 996                  (RefineFailure (lazy
 997                  "A variable with a body can not be explicit substituted"))
 998                  | Cic.Variable (_,None,_,_) -> ()
 999                  | _ ->
1000                  raise
1001                  (RefineFailure (lazy
1002                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1003                  ) ;
1004               *)
1005             let t',typeoft,metasubst',metasenv',ugraph2 =
1006               type_of_aux metasubst metasenv context t ugraph1 in
1007             let subst = uri,t' in
1008             let metasubst'',metasenv'',ugraph3 =
1009               try
1010                 fo_unif_subst
1011                   metasubst' context metasenv' typeoft typeofvar ugraph2
1012               with _ ->
1013                 raise (RefineFailure (lazy
1014                          ("Wrong Explicit Named Substitution: " ^
1015                            CicMetaSubst.ppterm metasubst' typeoft ^
1016                           " not unifiable with " ^
1017                           CicMetaSubst.ppterm metasubst' typeofvar)))
1018             in
1019             (* FIXME: no mere tail recursive! *)
1020             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1021               check_exp_named_subst_aux
1022                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1023             in
1024               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1025     in
1026       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1027
1028
1029   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1030     let module C = Cic in
1031     let context_for_t2 = (Some (name,C.Decl s))::context in
1032     let t1'' = CicReduction.whd ~subst context t1 in
1033     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1034       match (t1'', t2'') with
1035           (C.Sort s1, C.Sort s2)
1036             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1037               (* different than Coq manual!!! *)
1038               C.Sort s2,subst,metasenv,ugraph
1039         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1040             let t' = CicUniv.fresh() in
1041             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1042             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1043               C.Sort (C.Type t'),subst,metasenv,ugraph2
1044         | (C.Sort _,C.Sort (C.Type t1)) ->
1045             C.Sort (C.Type t1),subst,metasenv,ugraph
1046         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1047         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1048             (* TODO how can we force the meta to become a sort? If we don't we
1049              * break the invariant that refine produce only well typed terms *)
1050             (* TODO if we check the non meta term and if it is a sort then we
1051              * are likely to know the exact value of the result e.g. if the rhs
1052              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1053             let (metasenv,idx) =
1054               CicMkImplicit.mk_implicit_sort metasenv subst in
1055             let (subst, metasenv,ugraph1) =
1056              try
1057               fo_unif_subst subst context_for_t2 metasenv
1058                 (C.Meta (idx,[])) t2'' ugraph
1059              with _ -> assert false (* unification against a metavariable *)
1060             in
1061               t2'',subst,metasenv,ugraph1
1062         | _,_ ->
1063             raise
1064               (RefineFailure
1065                 (lazy
1066                   (sprintf
1067                     ("Two sorts were expected, found %s " ^^
1068                      "(that reduces to %s) and %s (that reduces to %s)")
1069                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1070                 (CicPp.ppterm t2''))))
1071
1072   and avoid_double_coercion context subst metasenv ugraph t ty =
1073     let b, c1, c2, head = is_a_double_coercion t in
1074     if b then
1075       let source_carr = CoercGraph.source_of c2 in
1076       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1077       (match CoercGraph.look_for_coercion source_carr tgt_carr
1078       with
1079       | CoercGraph.SomeCoercion c ->
1080          let newt =
1081           match c with
1082              Cic.Appl l -> Cic.Appl (l @ [head])
1083            | _ -> Cic.Appl [c;head]
1084          in
1085           (try
1086             let newt,_,subst,metasenv,ugraph =
1087               type_of_aux subst metasenv context newt ugraph in
1088             let subst, metasenv, ugraph =
1089              fo_unif_subst subst context metasenv newt t ugraph
1090             in
1091             debug_print
1092               (lazy
1093                 ("packing: " ^
1094                   CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
1095             newt, ty, subst, metasenv, ugraph
1096            with
1097               RefineFailure _ ->
1098                prerr_endline ("#### Coercion not packed (Refine_failure): " ^
1099                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
1100                assert false
1101             | Uncertain _ ->
1102                prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
1103                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
1104                assert false)
1105       | _ -> assert false) (* the composite coercion must exist *)
1106     else
1107       t, ty, subst, metasenv, ugraph
1108
1109   and eat_prods
1110     allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
1111   =
1112     let rec mk_prod metasenv context' =
1113       function
1114           [] ->
1115             let (metasenv, idx) =
1116               CicMkImplicit.mk_implicit_type metasenv subst context'
1117             in
1118             let irl =
1119               CicMkImplicit.identity_relocation_list_for_metavariable context'
1120             in
1121               metasenv,Cic.Meta (idx, irl)
1122         | (_,argty)::tl ->
1123             let (metasenv, idx) =
1124               CicMkImplicit.mk_implicit_type metasenv subst context'
1125             in
1126             let irl =
1127               CicMkImplicit.identity_relocation_list_for_metavariable context'
1128             in
1129             let meta = Cic.Meta (idx,irl) in
1130             let name =
1131               (* The name must be fresh for context.                 *)
1132               (* Nevertheless, argty is well-typed only in context.  *)
1133               (* Thus I generate a name (name_hint) in context and   *)
1134               (* then I generate a name --- using the hint name_hint *)
1135               (* --- that is fresh in context'.                      *)
1136               let name_hint =
1137                 (* Cic.Name "pippo" *)
1138                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1139                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1140                   (CicMetaSubst.apply_subst_context subst context)
1141                   Cic.Anonymous
1142                   ~typ:(CicMetaSubst.apply_subst subst argty)
1143               in
1144                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1145                 FreshNamesGenerator.mk_fresh_name ~subst
1146                   [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1147             in
1148             let metasenv,target =
1149               mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1150             in
1151               metasenv,Cic.Prod (name,meta,target)
1152     in
1153     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1154     let (subst, metasenv,ugraph1) =
1155       try
1156         fo_unif_subst subst context metasenv hetype hetype' ugraph
1157       with exn ->
1158        enrich localization_tbl he
1159         ~f:(fun _ ->
1160           (lazy ("The term " ^
1161             CicMetaSubst.ppterm_in_context subst he
1162              context ^ " (that has type " ^
1163             CicMetaSubst.ppterm_in_context subst hetype
1164              context ^ ") is here applied to " ^
1165             string_of_int (List.length tlbody_and_type) ^
1166             " arguments that are more than expected"
1167              (* "\nReason: " ^ Lazy.force exn*)))) exn
1168     in
1169     let rec eat_prods metasenv subst context hetype ugraph =
1170       function
1171         | [] -> [],metasenv,subst,hetype,ugraph
1172         | (hete, hety)::tl ->
1173             (match hetype with
1174                  Cic.Prod (n,s,t) ->
1175                    let arg,subst,metasenv,ugraph1 =
1176                      try
1177                        let subst,metasenv,ugraph1 =
1178                          fo_unif_subst subst context metasenv hety s ugraph
1179                        in
1180                          hete,subst,metasenv,ugraph1
1181                      with exn when allow_coercions && !insert_coercions ->
1182                        (* we search a coercion from hety to s *)
1183                        let coer, tgt_carr =
1184                          let carr t subst context =
1185                            CicMetaSubst.apply_subst subst t
1186                          in
1187                          let c_hety = carr hety subst context in
1188                          let c_s = carr s subst context in
1189                          CoercGraph.look_for_coercion c_hety c_s, c_s
1190                        in
1191                        (match coer with
1192                        | CoercGraph.NoCoercion
1193                        | CoercGraph.NotHandled _ ->
1194                            enrich localization_tbl hete
1195                             (RefineFailure
1196                               (lazy ("The term " ^
1197                                 CicMetaSubst.ppterm_in_context subst hete
1198                                  context ^ " has type " ^
1199                                 CicMetaSubst.ppterm_in_context subst hety
1200                                  context ^ " but is here used with type " ^
1201                                 CicMetaSubst.ppterm_in_context subst s context
1202                                  (* "\nReason: " ^ Lazy.force e*))))
1203                        | CoercGraph.NotMetaClosed ->
1204                            enrich localization_tbl hete
1205                             (Uncertain
1206                               (lazy ("The term " ^
1207                                 CicMetaSubst.ppterm_in_context subst hete
1208                                  context ^ " has type " ^
1209                                 CicMetaSubst.ppterm_in_context subst hety
1210                                  context ^ " but is here used with type " ^
1211                                 CicMetaSubst.ppterm_in_context subst s context
1212                                  (* "\nReason: " ^ Lazy.force e*))))
1213                        | CoercGraph.SomeCoercion c ->
1214                           try
1215                            let newt,newhety,subst,metasenv,ugraph =
1216                             type_of_aux subst metasenv context
1217                              (Cic.Appl[c;hete]) ugraph in
1218                            let newt, _, subst, metasenv, ugraph =
1219                             avoid_double_coercion context subst metasenv
1220                              ugraph newt tgt_carr in
1221                             let subst,metasenv,ugraph1 =
1222                              fo_unif_subst subst context metasenv
1223                                 newhety s ugraph
1224                             in
1225                              newt, subst, metasenv, ugraph
1226                           with _ ->
1227                            enrich localization_tbl hete
1228                              ~f:(fun _ ->
1229                                (lazy ("The term " ^
1230                                  CicMetaSubst.ppterm_in_context subst hete
1231                                   context ^ " has type " ^
1232                                  CicMetaSubst.ppterm_in_context subst hety
1233                                   context ^ " but is here used with type " ^
1234                                  CicMetaSubst.ppterm_in_context subst s context
1235                                   (* "\nReason: " ^ Lazy.force e*)))) exn)
1236                      | exn ->
1237                         enrich localization_tbl hete
1238                          ~f:(fun _ ->
1239                            (lazy ("The term " ^
1240                              CicMetaSubst.ppterm_in_context subst hete
1241                               context ^ " has type " ^
1242                              CicMetaSubst.ppterm_in_context subst hety
1243                               context ^ " but is here used with type " ^
1244                              CicMetaSubst.ppterm_in_context subst s context
1245                               (* "\nReason: " ^ Lazy.force e*)))) exn
1246                    in
1247                    let coerced_args,metasenv',subst',t',ugraph2 =
1248                      eat_prods metasenv subst context
1249                        (CicSubstitution.subst arg t) ugraph1 tl
1250                    in
1251                      arg::coerced_args,metasenv',subst',t',ugraph2
1252                | _ -> assert false
1253             )
1254     in
1255     let coerced_args,metasenv,subst,t,ugraph2 =
1256       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1257     in
1258       coerced_args,t,subst,metasenv,ugraph2
1259   in
1260
1261   (* eat prods ends here! *)
1262
1263   let t',ty,subst',metasenv',ugraph1 =
1264    type_of_aux [] metasenv context t ugraph
1265   in
1266   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1267   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1268     (* Andrea: ho rimesso qui l'applicazione della subst al
1269        metasenv dopo che ho droppato l'invariante che il metsaenv
1270        e' sempre istanziato *)
1271   let substituted_metasenv =
1272     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1273     (* metasenv' *)
1274     (*  substituted_t,substituted_ty,substituted_metasenv *)
1275     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1276   let cleaned_t =
1277     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1278   let cleaned_ty =
1279     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1280   let cleaned_metasenv =
1281     List.map
1282       (function (n,context,ty) ->
1283          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1284          let context' =
1285            List.map
1286              (function
1287                   None -> None
1288                 | Some (n, Cic.Decl t) ->
1289                     Some (n,
1290                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1291                 | Some (n, Cic.Def (bo,ty)) ->
1292                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1293                     let ty' =
1294                       match ty with
1295                           None -> None
1296                         | Some ty ->
1297                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1298                     in
1299                       Some (n, Cic.Def (bo',ty'))
1300              ) context
1301          in
1302            (n,context',ty')
1303       ) substituted_metasenv
1304   in
1305     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1306 ;;
1307
1308 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1309   try
1310     type_of_aux' ?localization_tbl metasenv context term ugraph
1311   with
1312     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1313
1314 let undebrujin uri typesno tys t =
1315   snd
1316    (List.fold_right
1317      (fun (name,_,_,_) (i,t) ->
1318        (* here the explicit_named_substituion is assumed to be *)
1319        (* of length 0 *)
1320        let t' = Cic.MutInd (uri,i,[])  in
1321        let t = CicSubstitution.subst t' t in
1322         i - 1,t
1323      ) tys (typesno - 1,t))
1324
1325 let map_first_n n start f g l =
1326   let rec aux acc k l =
1327     if k < n then
1328       match l with
1329       | [] -> raise (Invalid_argument "map_first_n")
1330       | hd :: tl -> f hd k (aux acc (k+1) tl)
1331     else
1332       g acc l
1333   in
1334   aux start 0 l
1335
1336 (*CSC: this is a very rough approximation; to be finished *)
1337 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1338   let subst,metasenv,ugraph,tys =
1339     List.fold_right
1340       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1341         let subst,metasenv,ugraph,cl =
1342           List.fold_right
1343             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1344                let rec aux ctx k subst = function
1345                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1346                      let subst,metasenv,ugraph,tl =
1347                        map_first_n leftno
1348                          (subst,metasenv,ugraph,[])
1349                          (fun t n (subst,metasenv,ugraph,acc) ->
1350                            let subst,metasenv,ugraph =
1351                              fo_unif_subst
1352                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1353                            in
1354                            subst,metasenv,ugraph,(t::acc))
1355                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1356                          tl
1357                      in
1358                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1359                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1360                      subst,metasenv,ugraph,t
1361                  | Cic.Prod (name,s,t) ->
1362                      let ctx = (Some (name,Cic.Decl s))::ctx in
1363                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1364                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1365                  | _ ->
1366                      raise
1367                       (RefineFailure
1368                         (lazy "not well formed constructor type"))
1369                in
1370                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1371                subst,metasenv,ugraph,(name,ty) :: acc)
1372           cl (subst,metasenv,ugraph,[])
1373         in
1374         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1375       tys ([],metasenv,ugraph,[])
1376   in
1377   let substituted_tys =
1378     List.map
1379       (fun (name,ind,arity,cl) ->
1380         let cl =
1381           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1382         in
1383         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1384       tys
1385   in
1386   metasenv,ugraph,substituted_tys
1387
1388 let typecheck metasenv uri obj ~localization_tbl =
1389  let ugraph = CicUniv.empty_ugraph in
1390  match obj with
1391     Cic.Constant (name,Some bo,ty,args,attrs) ->
1392      let bo',boty,metasenv,ugraph =
1393       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1394      let ty',_,metasenv,ugraph =
1395       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1396      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1397      let bo' = CicMetaSubst.apply_subst subst bo' in
1398      let ty' = CicMetaSubst.apply_subst subst ty' in
1399      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1400       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1401   | Cic.Constant (name,None,ty,args,attrs) ->
1402      let ty',_,metasenv,ugraph =
1403       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1404      in
1405       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1406   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1407      assert (metasenv' = metasenv);
1408      (* Here we do not check the metasenv for correctness *)
1409      let bo',boty,metasenv,ugraph =
1410       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1411      let ty',sort,metasenv,ugraph =
1412       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1413      begin
1414       match sort with
1415          Cic.Sort _
1416        (* instead of raising Uncertain, let's hope that the meta will become
1417           a sort *)
1418        | Cic.Meta _ -> ()
1419        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1420      end;
1421      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1422      let bo' = CicMetaSubst.apply_subst subst bo' in
1423      let ty' = CicMetaSubst.apply_subst subst ty' in
1424      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1425       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1426   | Cic.Variable _ -> assert false (* not implemented *)
1427   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1428      (*CSC: this code is greately simplified and many many checks are missing *)
1429      (*CSC: e.g. the constructors are not required to build their own types,  *)
1430      (*CSC: the arities are not required to have as type a sort, etc.         *)
1431      let uri = match uri with Some uri -> uri | None -> assert false in
1432      let typesno = List.length tys in
1433      (* first phase: we fix only the types *)
1434      let metasenv,ugraph,tys =
1435       List.fold_right
1436        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1437          let ty',_,metasenv,ugraph =
1438           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1439          in
1440           metasenv,ugraph,(name,b,ty',cl)::res
1441        ) tys (metasenv,ugraph,[]) in
1442      let con_context =
1443       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1444      (* second phase: we fix only the constructors *)
1445      let metasenv,ugraph,tys =
1446       List.fold_right
1447        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1448          let metasenv,ugraph,cl' =
1449           List.fold_right
1450            (fun (name,ty) (metasenv,ugraph,res) ->
1451              let ty =
1452               CicTypeChecker.debrujin_constructor
1453                ~cb:(relocalize localization_tbl) uri typesno ty in
1454              let ty',_,metasenv,ugraph =
1455               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1456              let ty' = undebrujin uri typesno tys ty' in
1457               metasenv,ugraph,(name,ty')::res
1458            ) cl (metasenv,ugraph,[])
1459          in
1460           metasenv,ugraph,(name,b,ty,cl')::res
1461        ) tys (metasenv,ugraph,[]) in
1462      (* third phase: we check the positivity condition *)
1463      let metasenv,ugraph,tys =
1464        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1465      in
1466      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1467 ;;
1468
1469 (* sara' piu' veloce che raffinare da zero? mah.... *)
1470 let pack_coercion metasenv ctx t =
1471  let module C = Cic in
1472  let rec merge_coercions ctx =
1473    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1474    function
1475    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1476    | C.Meta (n,subst) ->
1477       let subst' =
1478        List.map
1479         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1480       in
1481        C.Meta (n,subst')
1482    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1483    | C.Prod (name,so,dest) ->
1484        let ctx' = (Some (name,C.Decl so))::ctx in
1485        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1486    | C.Lambda (name,so,dest) ->
1487        let ctx' = (Some (name,C.Decl so))::ctx in
1488        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1489    | C.LetIn (name,so,dest) ->
1490        let ctx' = Some (name,(C.Def (so,None)))::ctx in
1491        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1492    | C.Appl l ->
1493       let l = List.map (merge_coercions ctx) l in
1494       let t = C.Appl l in
1495        let b,_,_,_ = is_a_double_coercion t in
1496        (* prerr_endline "CANDIDATO!!!!"; *)
1497        if b then
1498          let ugraph = CicUniv.empty_ugraph in
1499          let old_insert_coercions = !insert_coercions in
1500          insert_coercions := false;
1501          let newt, _, menv, _ =
1502            try
1503              type_of_aux' metasenv ctx t ugraph
1504            with RefineFailure _ | Uncertain _ ->
1505              prerr_endline (CicPp.ppterm t);
1506              t, t, [], ugraph
1507          in
1508          insert_coercions := old_insert_coercions;
1509          if metasenv <> [] || menv = [] then
1510            newt
1511          else
1512            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1513        else
1514          t
1515    | C.Var (uri,exp_named_subst) ->
1516        let exp_named_subst = List.map aux exp_named_subst in
1517        C.Var (uri, exp_named_subst)
1518    | C.Const (uri,exp_named_subst) ->
1519        let exp_named_subst = List.map aux exp_named_subst in
1520        C.Const (uri, exp_named_subst)
1521    | C.MutInd (uri,tyno,exp_named_subst) ->
1522        let exp_named_subst = List.map aux exp_named_subst in
1523        C.MutInd (uri,tyno,exp_named_subst)
1524    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1525        let exp_named_subst = List.map aux exp_named_subst in
1526        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1527    | C.MutCase (uri,tyno,out,te,pl) ->
1528        let pl = List.map (merge_coercions ctx) pl in
1529        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1530    | C.Fix (fno, fl) ->
1531        let ctx' =
1532          List.fold_left
1533            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1534            ctx fl
1535        in
1536        let fl =
1537          List.map
1538            (fun (name,idx,ty,bo) ->
1539              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1540          fl
1541        in
1542        C.Fix (fno, fl)
1543    | C.CoFix (fno, fl) ->
1544        let ctx' =
1545          List.fold_left
1546            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1547            ctx fl
1548        in
1549        let fl =
1550          List.map
1551            (fun (name,ty,bo) ->
1552              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1553          fl
1554        in
1555        C.CoFix (fno, fl)
1556  in
1557   merge_coercions ctx t
1558 ;;
1559
1560 let pack_coercion_obj obj =
1561   let module C = Cic in
1562   match obj with
1563   | C.Constant (id, body, ty, params, attrs) ->
1564       let body =
1565         match body with
1566         | None -> None
1567         | Some body -> Some (pack_coercion [] [] body)
1568       in
1569       let ty = pack_coercion [] [] ty in
1570         C.Constant (id, body, ty, params, attrs)
1571   | C.Variable (name, body, ty, params, attrs) ->
1572       let body =
1573         match body with
1574         | None -> None
1575         | Some body -> Some (pack_coercion [] [] body)
1576       in
1577       let ty = pack_coercion [] [] ty in
1578         C.Variable (name, body, ty, params, attrs)
1579   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1580       let conjectures =
1581         List.map
1582           (fun (i, ctx, ty) ->
1583             let ctx =
1584               List.fold_right
1585                 (fun item ctx ->
1586                   let item' =
1587                    match item with
1588                       Some (name, C.Decl t) ->
1589                         Some (name, C.Decl (pack_coercion conjectures ctx t))
1590                     | Some (name, C.Def (t,None)) ->
1591                         Some (name,C.Def (pack_coercion conjectures ctx t,None))
1592                     | Some (name, C.Def (t,Some ty)) ->
1593                         Some (name, C.Def (pack_coercion conjectures ctx t,
1594                                        Some (pack_coercion conjectures ctx ty)))
1595                     | None -> None
1596                   in
1597                    item'::ctx
1598                 ) ctx []
1599             in
1600              ((i,ctx,pack_coercion conjectures ctx ty))
1601           ) conjectures
1602       in
1603       let body = pack_coercion conjectures [] body in
1604       let ty = pack_coercion conjectures [] ty in
1605       C.CurrentProof (name, conjectures, body, ty, params, attrs)
1606   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1607       let indtys =
1608         List.map
1609           (fun (name, ind, arity, cl) ->
1610             let arity = pack_coercion [] [] arity in
1611             let cl =
1612               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1613             in
1614             (name, ind, arity, cl))
1615           indtys
1616       in
1617         C.InductiveDefinition (indtys, params, leftno, attrs)
1618 ;;
1619
1620
1621 (* DEBUGGING ONLY
1622 let type_of_aux' metasenv context term =
1623  try
1624   let (t,ty,m) =
1625       type_of_aux' metasenv context term in
1626     debug_print (lazy
1627      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1628    debug_print (lazy
1629     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1630    (t,ty,m)
1631  with
1632  | RefineFailure msg as e ->
1633      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1634      raise e
1635  | Uncertain msg as e ->
1636      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1637      raise e
1638 ;; *)
1639
1640 let profiler2 = HExtlib.profile "CicRefine"
1641
1642 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1643  profiler2.HExtlib.profile
1644   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1645
1646 let typecheck ~localization_tbl metasenv uri obj =
1647  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj