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                            CicReduction.whd ~delta:false
1186                              context (CicMetaSubst.apply_subst subst t )
1187                          in
1188                          let c_hety = carr hety subst context in
1189                          let c_s = carr s subst context in
1190                          CoercGraph.look_for_coercion c_hety c_s, c_s
1191                        in
1192                        (match coer with
1193                        | CoercGraph.NoCoercion
1194                        | CoercGraph.NotHandled _ ->
1195                            enrich localization_tbl hete
1196                             (RefineFailure
1197                               (lazy ("The term " ^
1198                                 CicMetaSubst.ppterm_in_context subst hete
1199                                  context ^ " has type " ^
1200                                 CicMetaSubst.ppterm_in_context subst hety
1201                                  context ^ " but is here used with type " ^
1202                                 CicMetaSubst.ppterm_in_context subst s context
1203                                  (* "\nReason: " ^ Lazy.force e*))))
1204                        | CoercGraph.NotMetaClosed ->
1205                            enrich localization_tbl hete
1206                             (Uncertain
1207                               (lazy ("The term " ^
1208                                 CicMetaSubst.ppterm_in_context subst hete
1209                                  context ^ " has type " ^
1210                                 CicMetaSubst.ppterm_in_context subst hety
1211                                  context ^ " but is here used with type " ^
1212                                 CicMetaSubst.ppterm_in_context subst s context
1213                                  (* "\nReason: " ^ Lazy.force e*))))
1214                        | CoercGraph.SomeCoercion c ->
1215                           try
1216                            let newt,newhety,subst,metasenv,ugraph =
1217                             type_of_aux subst metasenv context
1218                              (Cic.Appl[c;hete]) ugraph in
1219                            let newt, _, subst, metasenv, ugraph =
1220                             avoid_double_coercion context subst metasenv
1221                              ugraph newt tgt_carr in
1222                             let subst,metasenv,ugraph1 =
1223                              fo_unif_subst subst context metasenv
1224                                 newhety s ugraph
1225                             in
1226                              newt, subst, metasenv, ugraph
1227                           with _ ->
1228                            enrich localization_tbl hete
1229                              ~f:(fun _ ->
1230                                (lazy ("The term " ^
1231                                  CicMetaSubst.ppterm_in_context subst hete
1232                                   context ^ " has type " ^
1233                                  CicMetaSubst.ppterm_in_context subst hety
1234                                   context ^ " but is here used with type " ^
1235                                  CicMetaSubst.ppterm_in_context subst s context
1236                                   (* "\nReason: " ^ Lazy.force e*)))) exn)
1237                      | exn ->
1238                         enrich localization_tbl hete
1239                          ~f:(fun _ ->
1240                            (lazy ("The term " ^
1241                              CicMetaSubst.ppterm_in_context subst hete
1242                               context ^ " has type " ^
1243                              CicMetaSubst.ppterm_in_context subst hety
1244                               context ^ " but is here used with type " ^
1245                              CicMetaSubst.ppterm_in_context subst s context
1246                               (* "\nReason: " ^ Lazy.force e*)))) exn
1247                    in
1248                    let coerced_args,metasenv',subst',t',ugraph2 =
1249                      eat_prods metasenv subst context
1250                        (CicSubstitution.subst arg t) ugraph1 tl
1251                    in
1252                      arg::coerced_args,metasenv',subst',t',ugraph2
1253                | _ -> assert false
1254             )
1255     in
1256     let coerced_args,metasenv,subst,t,ugraph2 =
1257       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1258     in
1259       coerced_args,t,subst,metasenv,ugraph2
1260   in
1261
1262   (* eat prods ends here! *)
1263
1264   let t',ty,subst',metasenv',ugraph1 =
1265    type_of_aux [] metasenv context t ugraph
1266   in
1267   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1268   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1269     (* Andrea: ho rimesso qui l'applicazione della subst al
1270        metasenv dopo che ho droppato l'invariante che il metsaenv
1271        e' sempre istanziato *)
1272   let substituted_metasenv =
1273     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1274     (* metasenv' *)
1275     (*  substituted_t,substituted_ty,substituted_metasenv *)
1276     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1277   let cleaned_t =
1278     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1279   let cleaned_ty =
1280     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1281   let cleaned_metasenv =
1282     List.map
1283       (function (n,context,ty) ->
1284          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1285          let context' =
1286            List.map
1287              (function
1288                   None -> None
1289                 | Some (n, Cic.Decl t) ->
1290                     Some (n,
1291                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1292                 | Some (n, Cic.Def (bo,ty)) ->
1293                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1294                     let ty' =
1295                       match ty with
1296                           None -> None
1297                         | Some ty ->
1298                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1299                     in
1300                       Some (n, Cic.Def (bo',ty'))
1301              ) context
1302          in
1303            (n,context',ty')
1304       ) substituted_metasenv
1305   in
1306     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1307 ;;
1308
1309 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1310   try
1311     type_of_aux' ?localization_tbl metasenv context term ugraph
1312   with
1313     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1314
1315 let undebrujin uri typesno tys t =
1316   snd
1317    (List.fold_right
1318      (fun (name,_,_,_) (i,t) ->
1319        (* here the explicit_named_substituion is assumed to be *)
1320        (* of length 0 *)
1321        let t' = Cic.MutInd (uri,i,[])  in
1322        let t = CicSubstitution.subst t' t in
1323         i - 1,t
1324      ) tys (typesno - 1,t))
1325
1326 let map_first_n n start f g l =
1327   let rec aux acc k l =
1328     if k < n then
1329       match l with
1330       | [] -> raise (Invalid_argument "map_first_n")
1331       | hd :: tl -> f hd k (aux acc (k+1) tl)
1332     else
1333       g acc l
1334   in
1335   aux start 0 l
1336
1337 (*CSC: this is a very rough approximation; to be finished *)
1338 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1339   let subst,metasenv,ugraph,tys =
1340     List.fold_right
1341       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1342         let subst,metasenv,ugraph,cl =
1343           List.fold_right
1344             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1345                let rec aux ctx k subst = function
1346                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1347                      let subst,metasenv,ugraph,tl =
1348                        map_first_n leftno
1349                          (subst,metasenv,ugraph,[])
1350                          (fun t n (subst,metasenv,ugraph,acc) ->
1351                            let subst,metasenv,ugraph =
1352                              fo_unif_subst
1353                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1354                            in
1355                            subst,metasenv,ugraph,(t::acc))
1356                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1357                          tl
1358                      in
1359                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1360                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1361                      subst,metasenv,ugraph,t
1362                  | Cic.Prod (name,s,t) ->
1363                      let ctx = (Some (name,Cic.Decl s))::ctx in
1364                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1365                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1366                  | _ ->
1367                      raise
1368                       (RefineFailure
1369                         (lazy "not well formed constructor type"))
1370                in
1371                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1372                subst,metasenv,ugraph,(name,ty) :: acc)
1373           cl (subst,metasenv,ugraph,[])
1374         in
1375         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1376       tys ([],metasenv,ugraph,[])
1377   in
1378   let substituted_tys =
1379     List.map
1380       (fun (name,ind,arity,cl) ->
1381         let cl =
1382           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1383         in
1384         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1385       tys
1386   in
1387   metasenv,ugraph,substituted_tys
1388
1389 let typecheck metasenv uri obj ~localization_tbl =
1390  let ugraph = CicUniv.empty_ugraph in
1391  match obj with
1392     Cic.Constant (name,Some bo,ty,args,attrs) ->
1393      let bo',boty,metasenv,ugraph =
1394       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1395      let ty',_,metasenv,ugraph =
1396       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1397      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1398      let bo' = CicMetaSubst.apply_subst subst bo' in
1399      let ty' = CicMetaSubst.apply_subst subst ty' in
1400      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1401       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1402   | Cic.Constant (name,None,ty,args,attrs) ->
1403      let ty',_,metasenv,ugraph =
1404       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1405      in
1406       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1407   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1408      assert (metasenv' = metasenv);
1409      (* Here we do not check the metasenv for correctness *)
1410      let bo',boty,metasenv,ugraph =
1411       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1412      let ty',sort,metasenv,ugraph =
1413       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1414      begin
1415       match sort with
1416          Cic.Sort _
1417        (* instead of raising Uncertain, let's hope that the meta will become
1418           a sort *)
1419        | Cic.Meta _ -> ()
1420        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1421      end;
1422      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1423      let bo' = CicMetaSubst.apply_subst subst bo' in
1424      let ty' = CicMetaSubst.apply_subst subst ty' in
1425      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1426       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1427   | Cic.Variable _ -> assert false (* not implemented *)
1428   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1429      (*CSC: this code is greately simplified and many many checks are missing *)
1430      (*CSC: e.g. the constructors are not required to build their own types,  *)
1431      (*CSC: the arities are not required to have as type a sort, etc.         *)
1432      let uri = match uri with Some uri -> uri | None -> assert false in
1433      let typesno = List.length tys in
1434      (* first phase: we fix only the types *)
1435      let metasenv,ugraph,tys =
1436       List.fold_right
1437        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1438          let ty',_,metasenv,ugraph =
1439           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1440          in
1441           metasenv,ugraph,(name,b,ty',cl)::res
1442        ) tys (metasenv,ugraph,[]) in
1443      let con_context =
1444       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1445      (* second phase: we fix only the constructors *)
1446      let metasenv,ugraph,tys =
1447       List.fold_right
1448        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1449          let metasenv,ugraph,cl' =
1450           List.fold_right
1451            (fun (name,ty) (metasenv,ugraph,res) ->
1452              let ty =
1453               CicTypeChecker.debrujin_constructor
1454                ~cb:(relocalize localization_tbl) uri typesno ty in
1455              let ty',_,metasenv,ugraph =
1456               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1457              let ty' = undebrujin uri typesno tys ty' in
1458               metasenv,ugraph,(name,ty')::res
1459            ) cl (metasenv,ugraph,[])
1460          in
1461           metasenv,ugraph,(name,b,ty,cl')::res
1462        ) tys (metasenv,ugraph,[]) in
1463      (* third phase: we check the positivity condition *)
1464      let metasenv,ugraph,tys =
1465        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1466      in
1467      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1468 ;;
1469
1470 (* sara' piu' veloce che raffinare da zero? mah.... *)
1471 let pack_coercion metasenv ctx t =
1472  let module C = Cic in
1473  let rec merge_coercions ctx =
1474    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1475    function
1476    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1477    | C.Meta (n,subst) ->
1478       let subst' =
1479        List.map
1480         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1481       in
1482        C.Meta (n,subst')
1483    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1484    | C.Prod (name,so,dest) ->
1485        let ctx' = (Some (name,C.Decl so))::ctx in
1486        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1487    | C.Lambda (name,so,dest) ->
1488        let ctx' = (Some (name,C.Decl so))::ctx in
1489        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1490    | C.LetIn (name,so,dest) ->
1491        let ctx' = Some (name,(C.Def (so,None)))::ctx in
1492        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1493    | C.Appl l ->
1494       let l = List.map (merge_coercions ctx) l in
1495       let t = C.Appl l in
1496        let b,_,_,_ = is_a_double_coercion t in
1497        (* prerr_endline "CANDIDATO!!!!"; *)
1498        if b then
1499          let ugraph = CicUniv.empty_ugraph in
1500          let old_insert_coercions = !insert_coercions in
1501          insert_coercions := false;
1502          let newt, _, menv, _ =
1503            try
1504              type_of_aux' metasenv ctx t ugraph
1505            with RefineFailure _ | Uncertain _ ->
1506              prerr_endline (CicPp.ppterm t);
1507              t, t, [], ugraph
1508          in
1509          insert_coercions := old_insert_coercions;
1510          if metasenv <> [] || menv = [] then
1511            newt
1512          else
1513            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1514        else
1515          t
1516    | C.Var (uri,exp_named_subst) ->
1517        let exp_named_subst = List.map aux exp_named_subst in
1518        C.Var (uri, exp_named_subst)
1519    | C.Const (uri,exp_named_subst) ->
1520        let exp_named_subst = List.map aux exp_named_subst in
1521        C.Const (uri, exp_named_subst)
1522    | C.MutInd (uri,tyno,exp_named_subst) ->
1523        let exp_named_subst = List.map aux exp_named_subst in
1524        C.MutInd (uri,tyno,exp_named_subst)
1525    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1526        let exp_named_subst = List.map aux exp_named_subst in
1527        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1528    | C.MutCase (uri,tyno,out,te,pl) ->
1529        let pl = List.map (merge_coercions ctx) pl in
1530        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1531    | C.Fix (fno, fl) ->
1532        let ctx' =
1533          List.fold_left
1534            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1535            ctx fl
1536        in
1537        let fl =
1538          List.map
1539            (fun (name,idx,ty,bo) ->
1540              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1541          fl
1542        in
1543        C.Fix (fno, fl)
1544    | C.CoFix (fno, fl) ->
1545        let ctx' =
1546          List.fold_left
1547            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1548            ctx fl
1549        in
1550        let fl =
1551          List.map
1552            (fun (name,ty,bo) ->
1553              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1554          fl
1555        in
1556        C.CoFix (fno, fl)
1557  in
1558   merge_coercions ctx t
1559 ;;
1560
1561 let pack_coercion_obj obj =
1562   let module C = Cic in
1563   match obj with
1564   | C.Constant (id, body, ty, params, attrs) ->
1565       let body =
1566         match body with
1567         | None -> None
1568         | Some body -> Some (pack_coercion [] [] body)
1569       in
1570       let ty = pack_coercion [] [] ty in
1571         C.Constant (id, body, ty, params, attrs)
1572   | C.Variable (name, body, ty, params, attrs) ->
1573       let body =
1574         match body with
1575         | None -> None
1576         | Some body -> Some (pack_coercion [] [] body)
1577       in
1578       let ty = pack_coercion [] [] ty in
1579         C.Variable (name, body, ty, params, attrs)
1580   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1581       let conjectures =
1582         List.map
1583           (fun (i, ctx, ty) ->
1584             let ctx =
1585               List.fold_right
1586                 (fun item ctx ->
1587                   let item' =
1588                    match item with
1589                       Some (name, C.Decl t) ->
1590                         Some (name, C.Decl (pack_coercion conjectures ctx t))
1591                     | Some (name, C.Def (t,None)) ->
1592                         Some (name,C.Def (pack_coercion conjectures ctx t,None))
1593                     | Some (name, C.Def (t,Some ty)) ->
1594                         Some (name, C.Def (pack_coercion conjectures ctx t,
1595                                        Some (pack_coercion conjectures ctx ty)))
1596                     | None -> None
1597                   in
1598                    item'::ctx
1599                 ) ctx []
1600             in
1601              ((i,ctx,pack_coercion conjectures ctx ty))
1602           ) conjectures
1603       in
1604       let body = pack_coercion conjectures [] body in
1605       let ty = pack_coercion conjectures [] ty in
1606       C.CurrentProof (name, conjectures, body, ty, params, attrs)
1607   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1608       let indtys =
1609         List.map
1610           (fun (name, ind, arity, cl) ->
1611             let arity = pack_coercion [] [] arity in
1612             let cl =
1613               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1614             in
1615             (name, ind, arity, cl))
1616           indtys
1617       in
1618         C.InductiveDefinition (indtys, params, leftno, attrs)
1619 ;;
1620
1621
1622 (* DEBUGGING ONLY
1623 let type_of_aux' metasenv context term =
1624  try
1625   let (t,ty,m) =
1626       type_of_aux' metasenv context term in
1627     debug_print (lazy
1628      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1629    debug_print (lazy
1630     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1631    (t,ty,m)
1632  with
1633  | RefineFailure msg as e ->
1634      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1635      raise e
1636  | Uncertain msg as e ->
1637      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1638      raise e
1639 ;; *)
1640
1641 let profiler2 = HExtlib.profile "CicRefine"
1642
1643 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1644  profiler2.HExtlib.profile
1645   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1646
1647 let typecheck ~localization_tbl metasenv uri obj =
1648  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1649
1650 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;