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 avoid_double_coercion context subst metasenv ugraph t ty =
 122   let arity_of con =
 123     try
 124       let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
 125       let rec count_pi = function
 126         | Cic.Prod (_,_,t) -> 1 + count_pi t
 127         | _ -> 0
 128       in
 129       count_pi ty
 130     with Invalid_argument _ -> assert false (* all coercions have an uri *)
 131   in
 132   let rec mk_implicits tail = function
 133     | 0 -> [tail]
 134     | n -> Cic.Implicit None :: mk_implicits tail (n-1)
 135   in
 136   let b, c1, c2, head = is_a_double_coercion t in
 137   if b then
 138     let source_carr = CoercGraph.source_of c2 in
 139     let tgt_carr = CicMetaSubst.apply_subst subst ty in
 140     (match CoercGraph.look_for_coercion source_carr tgt_carr
 141     with
 142     | CoercGraph.SomeCoercion c ->
 143         let arity = arity_of c in
 144         let args = mk_implicits head (arity - 1) in
 145         let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
 146         let newt = Cic.Appl (c_bo::args) in
 147         (try
 148           let subst, metasenv, ugraph =
 149            fo_unif_subst subst context metasenv newt t ugraph
 150           in
 151           debug_print
 152             (lazy
 153               ("packing: " ^
 154                 CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
 155           Cic.Appl (c::args), ty, subst, metasenv, ugraph
 156          with
 157             RefineFailure _ ->
 158              prerr_endline ("#### Coercion not packed (Refine_failure): " ^
 159               CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
 160              assert false
 161           | Uncertain _ ->
 162              prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
 163               CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
 164              assert false)
 165     | _ -> assert false) (* the composite coercion must exist *)
 166   else
 167     t, ty, subst, metasenv, ugraph
 168
 169 let rec type_of_constant uri ugraph =
 170  let module C = Cic in
 171  let module R = CicReduction in
 172  let module U = UriManager in
 173   let _ = CicTypeChecker.typecheck uri in
 174   let obj,u =
 175    try
 176     CicEnvironment.get_cooked_obj ugraph uri
 177    with Not_found -> assert false
 178   in
 179    match obj with
 180       C.Constant (_,_,ty,_,_) -> ty,u
 181     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
 182     | _ ->
 183        raise
 184         (RefineFailure
 185           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 186
 187 and type_of_variable uri ugraph =
 188   let module C = Cic in
 189   let module R = CicReduction in
 190   let module U = UriManager in
 191   let _ = CicTypeChecker.typecheck uri in
 192   let obj,u =
 193    try
 194     CicEnvironment.get_cooked_obj ugraph uri
 195     with Not_found -> assert false
 196   in
 197    match obj with
 198       C.Variable (_,_,ty,_,_) -> ty,u
 199     | _ ->
 200         raise
 201          (RefineFailure
 202           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
 203
 204 and type_of_mutual_inductive_defs uri i ugraph =
 205   let module C = Cic in
 206   let module R = CicReduction in
 207   let module U = UriManager in
 208   let _ = CicTypeChecker.typecheck uri in
 209   let obj,u =
 210    try
 211     CicEnvironment.get_cooked_obj ugraph uri
 212    with Not_found -> assert false
 213   in
 214    match obj with
 215       C.InductiveDefinition (dl,_,_,_) ->
 216         let (_,_,arity,_) = List.nth dl i in
 217          arity,u
 218     | _ ->
 219        raise
 220         (RefineFailure
 221          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
 222
 223 and type_of_mutual_inductive_constr uri i j ugraph =
 224   let module C = Cic in
 225   let module R = CicReduction in
 226   let module U = UriManager in
 227   let _ = CicTypeChecker.typecheck uri in
 228    let obj,u =
 229     try
 230      CicEnvironment.get_cooked_obj ugraph uri
 231     with Not_found -> assert false
 232    in
 233     match obj with
 234         C.InductiveDefinition (dl,_,_,_) ->
 235           let (_,_,_,cl) = List.nth dl i in
 236           let (_,ty) = List.nth cl (j-1) in
 237             ty,u
 238       | _ ->
 239           raise
 240                   (RefineFailure
 241               (lazy
 242                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 243
 244
 245 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 246
 247 (* the check_branch function checks if a branch of a case is refinable.
 248    It returns a pair (outype_instance,args), a subst and a metasenv.
 249    outype_instance is the expected result of applying the case outtype
 250    to args.
 251    The problem is that outype is in general unknown, and we should
 252    try to synthesize it from the above information, that is in general
 253    a second order unification problem. *)
 254
 255 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 256   let module C = Cic in
 257     (* let module R = CicMetaSubst in *)
 258   let module R = CicReduction in
 259     match R.whd ~subst context expectedtype with
 260         C.MutInd (_,_,_) ->
 261           (n,context,actualtype, [term]), subst, metasenv, ugraph
 262       | C.Appl (C.MutInd (_,_,_)::tl) ->
 263           let (_,arguments) = split tl left_args_no in
 264             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 265       | C.Prod (name,so,de) ->
 266           (* we expect that the actual type of the branch has the due
 267              number of Prod *)
 268           (match R.whd ~subst context actualtype with
 269                C.Prod (name',so',de') ->
 270                  let subst, metasenv, ugraph1 =
 271                    fo_unif_subst subst context metasenv so so' ugraph in
 272                  let term' =
 273                    (match CicSubstitution.lift 1 term with
 274                         C.Appl l -> C.Appl (l@[C.Rel 1])
 275                       | t -> C.Appl [t ; C.Rel 1]) in
 276                    (* we should also check that the name variable is anonymous in
 277                       the actual type de' ?? *)
 278                    check_branch (n+1)
 279                      ((Some (name,(C.Decl so)))::context)
 280                        metasenv subst left_args_no de' term' de ugraph1
 281              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
 282       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 283
 284 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 285      ugraph
 286 =
 287   let rec type_of_aux subst metasenv context t ugraph =
 288     let module C = Cic in
 289     let module S = CicSubstitution in
 290     let module U = UriManager in
 291      let (t',_,_,_,_) as res =
 292       match t with
 293           (*    function *)
 294           C.Rel n ->
 295             (try
 296                match List.nth context (n - 1) with
 297                    Some (_,C.Decl ty) ->
 298                      t,S.lift n ty,subst,metasenv, ugraph
 299                  | Some (_,C.Def (_,Some ty)) ->
 300                      t,S.lift n ty,subst,metasenv, ugraph
 301                  | Some (_,C.Def (bo,None)) ->
 302                      let ty,ugraph =
 303                       (* if it is in the context it must be already well-typed*)
 304                       CicTypeChecker.type_of_aux' ~subst metasenv context
 305                        (S.lift n bo) ugraph
 306                      in
 307                       t,ty,subst,metasenv,ugraph
 308                  | None ->
 309                     enrich localization_tbl t
 310                      (RefineFailure (lazy "Rel to hidden hypothesis"))
 311              with
 312               _ ->
 313                enrich localization_tbl t
 314                 (RefineFailure (lazy "Not a close term")))
 315         | C.Var (uri,exp_named_subst) ->
 316             let exp_named_subst',subst',metasenv',ugraph1 =
 317               check_exp_named_subst
 318                 subst metasenv context exp_named_subst ugraph
 319             in
 320             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 321             let ty =
 322               CicSubstitution.subst_vars exp_named_subst' ty_uri
 323             in
 324               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 325         | C.Meta (n,l) ->
 326             (try
 327                let (canonical_context, term,ty) =
 328                  CicUtil.lookup_subst n subst
 329                in
 330                let l',subst',metasenv',ugraph1 =
 331                  check_metasenv_consistency n subst metasenv context
 332                    canonical_context l ugraph
 333                in
 334                  (* trust or check ??? *)
 335                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 336                    subst', metasenv', ugraph1
 337                    (* type_of_aux subst metasenv
 338                       context (CicSubstitution.subst_meta l term) *)
 339              with CicUtil.Subst_not_found _ ->
 340                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 341                let l',subst',metasenv', ugraph1 =
 342                  check_metasenv_consistency n subst metasenv context
 343                    canonical_context l ugraph
 344                in
 345                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 346                    subst', metasenv',ugraph1)
 347         | C.Sort (C.Type tno) ->
 348             let tno' = CicUniv.fresh() in
 349             let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 350               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 351         | C.Sort _ ->
 352             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 353         | C.Implicit infos ->
 354            let metasenv',t' = exp_impl metasenv subst context infos in
 355             type_of_aux subst metasenv' context t' ugraph
 356         | C.Cast (te,ty) ->
 357             let ty',_,subst',metasenv',ugraph1 =
 358               type_of_aux subst metasenv context ty ugraph
 359             in
 360             let te',inferredty,subst'',metasenv'',ugraph2 =
 361               type_of_aux subst' metasenv' context te ugraph1
 362             in
 363              (try
 364                let subst''',metasenv''',ugraph3 =
 365                  fo_unif_subst subst'' context metasenv''
 366                    inferredty ty' ugraph2
 367                in
 368                 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 369               with
 370                exn ->
 371                 enrich localization_tbl te'
 372                  ~f:(fun _ ->
 373                    lazy ("The term " ^
 374                     CicMetaSubst.ppterm_in_context subst'' te'
 375                      context ^ " has type " ^
 376                     CicMetaSubst.ppterm_in_context subst'' inferredty
 377                      context ^ " but is here used with type " ^
 378                     CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
 379              )
 380         | C.Prod (name,s,t) ->
 381             let carr t subst context = CicMetaSubst.apply_subst subst t in
 382             let coerce_to_sort in_source tgt_sort t type_to_coerce
 383                  subst context metasenv uragph
 384             =
 385               if not !insert_coercions then
 386                 t,type_to_coerce,subst,metasenv,ugraph
 387               else
 388                 let coercion_src = carr type_to_coerce subst context in
 389                 match coercion_src with
 390                 | Cic.Sort _ ->
 391                     t,type_to_coerce,subst,metasenv,ugraph
 392                 | Cic.Meta _ as meta ->
 393                     t, meta, subst, metasenv, ugraph
 394                 | Cic.Cast _ as cast ->
 395                     t, cast, subst, metasenv, ugraph
 396                 | term ->
 397                     let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
 398                     let search = CoercGraph.look_for_coercion in
 399                     let boh = search coercion_src coercion_tgt in
 400                     (match boh with
 401                     | CoercGraph.NoCoercion
 402                     | CoercGraph.NotHandled _ ->
 403                        enrich localization_tbl t
 404                         (RefineFailure
 405                           (lazy ("The term " ^
 406                           CicMetaSubst.ppterm_in_context subst t context ^
 407                           " is not a type since it has type " ^
 408                           CicMetaSubst.ppterm_in_context
 409                            subst coercion_src context ^ " that is not a sort")))
 410                     | CoercGraph.NotMetaClosed ->
 411                        enrich localization_tbl t
 412                         (Uncertain
 413                           (lazy ("The term " ^
 414                           CicMetaSubst.ppterm_in_context subst t context ^
 415                           " is not a type since it has type " ^
 416                           CicMetaSubst.ppterm_in_context
 417                            subst coercion_src context ^ " that is not a sort")))
 418                     | CoercGraph.SomeCoercion c ->
 419                        let newt, tty, subst, metasenv, ugraph =
 420                          avoid_double_coercion context
 421                           subst metasenv ugraph
 422                             (Cic.Appl[c;t]) coercion_tgt
 423                        in
 424                         newt, tty, subst, metasenv, ugraph)
 425             in
 426             let s',sort1,subst',metasenv',ugraph1 =
 427               type_of_aux subst metasenv context s ugraph
 428             in
 429             let s',sort1,subst', metasenv',ugraph1 =
 430               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 431               s' sort1 subst' context metasenv' ugraph1
 432             in
 433             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 434             let t',sort2,subst'',metasenv'',ugraph2 =
 435               type_of_aux subst' metasenv'
 436                 context_for_t t ugraph1
 437             in
 438             let t',sort2,subst'',metasenv'',ugraph2 =
 439               coerce_to_sort false (Cic.Type(CicUniv.fresh()))
 440               t' sort2 subst'' context_for_t metasenv'' ugraph2
 441             in
 442               let sop,subst''',metasenv''',ugraph3 =
 443                 sort_of_prod subst'' metasenv''
 444                   context (name,s') (sort1,sort2) ugraph2
 445               in
 446                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 447         | C.Lambda (n,s,t) ->
 448
 449             let s',sort1,subst',metasenv',ugraph1 =
 450               type_of_aux subst metasenv context s ugraph in
 451             let s',sort1,subst',metasenv',ugraph1 =
 452               if not !insert_coercions then
 453                 s',sort1, subst', metasenv', ugraph1
 454               else
 455                 match CicReduction.whd ~subst:subst' context sort1 with
 456                   | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
 457                   | coercion_src ->
 458                      let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
 459                      let search = CoercGraph.look_for_coercion in
 460                      let boh = search coercion_src coercion_tgt in
 461                       match boh with
 462                       | CoercGraph.SomeCoercion c ->
 463                         let newt, tty, subst', metasenv', ugraph1 =
 464                           avoid_double_coercion context
 465                            subst' metasenv' ugraph1
 466                              (Cic.Appl[c;s']) coercion_tgt
 467                         in
 468                          newt, tty, subst', metasenv', ugraph1
 469                       | CoercGraph.NoCoercion
 470                       |  CoercGraph.NotHandled _ ->
 471                         enrich localization_tbl s'
 472                          (RefineFailure
 473                           (lazy ("The term " ^
 474                           CicMetaSubst.ppterm_in_context subst s' context ^
 475                           " is not a type since it has type " ^
 476                           CicMetaSubst.ppterm_in_context
 477                            subst coercion_src context ^ " that is not a sort")))
 478                       | CoercGraph.NotMetaClosed ->
 479                         enrich localization_tbl s'
 480                          (Uncertain
 481                           (lazy ("The term " ^
 482                           CicMetaSubst.ppterm_in_context subst s' context ^
 483                           " is not a type since it has type " ^
 484                           CicMetaSubst.ppterm_in_context
 485                            subst coercion_src context ^ " that is not a sort")))
 486             in
 487             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 488             let t',type2,subst'',metasenv'',ugraph2 =
 489               type_of_aux subst' metasenv' context_for_t t ugraph1
 490             in
 491               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 492                 subst'',metasenv'',ugraph2
 493         | C.LetIn (n,s,t) ->
 494             (* only to check if s is well-typed *)
 495             let s',ty,subst',metasenv',ugraph1 =
 496               type_of_aux subst metasenv context s ugraph
 497             in
 498            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 499
 500             let t',inferredty,subst'',metasenv'',ugraph2 =
 501               type_of_aux subst' metasenv'
 502                 context_for_t t ugraph1
 503             in
 504               (* One-step LetIn reduction.
 505                * Even faster than the previous solution.
 506                * Moreover the inferred type is closer to the expected one.
 507                *)
 508               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
 509                 subst'',metasenv'',ugraph2
 510         | C.Appl (he::((_::_) as tl)) ->
 511             let he',hetype,subst',metasenv',ugraph1 =
 512               type_of_aux subst metasenv context he ugraph
 513             in
 514             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 515               List.fold_right
 516                 (fun x (res,subst,metasenv,ugraph) ->
 517                    let x',ty,subst',metasenv',ugraph1 =
 518                      type_of_aux subst metasenv context x ugraph
 519                    in
 520                     (x', ty)::res,subst',metasenv',ugraph1
 521                 ) tl ([],subst',metasenv',ugraph1)
 522             in
 523             let tl',applty,subst''',metasenv''',ugraph3 =
 524               eat_prods true subst'' metasenv'' context
 525                 hetype tlbody_and_type ugraph2
 526             in
 527               avoid_double_coercion context
 528                 subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
 529         | C.Appl _ -> assert false
 530         | C.Const (uri,exp_named_subst) ->
 531             let exp_named_subst',subst',metasenv',ugraph1 =
 532               check_exp_named_subst subst metasenv context
 533                 exp_named_subst ugraph in
 534             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 535             let cty =
 536               CicSubstitution.subst_vars exp_named_subst' ty_uri
 537             in
 538               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 539         | C.MutInd (uri,i,exp_named_subst) ->
 540             let exp_named_subst',subst',metasenv',ugraph1 =
 541               check_exp_named_subst subst metasenv context
 542                 exp_named_subst ugraph
 543             in
 544             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 545             let cty =
 546               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 547               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 548         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 549             let exp_named_subst',subst',metasenv',ugraph1 =
 550               check_exp_named_subst subst metasenv context
 551                 exp_named_subst ugraph
 552             in
 553             let ty_uri,ugraph2 =
 554               type_of_mutual_inductive_constr uri i j ugraph1
 555             in
 556             let cty =
 557               CicSubstitution.subst_vars exp_named_subst' ty_uri
 558             in
 559               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 560                 metasenv',ugraph2
 561         | C.MutCase (uri, i, outtype, term, pl) ->
 562             (* first, get the inductive type (and noparams)
 563              * in the environment  *)
 564             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 565               let _ = CicTypeChecker.typecheck uri in
 566               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 567               match obj with
 568                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 569                     List.nth l i , expl_params, parsno, u
 570                 | _ ->
 571                     enrich localization_tbl t
 572                      (RefineFailure
 573                        (lazy ("Unkown mutual inductive definition " ^
 574                          U.string_of_uri uri)))
 575            in
 576            let rec count_prod t =
 577              match CicReduction.whd ~subst context t with
 578                  C.Prod (_, _, t) -> 1 + (count_prod t)
 579                | _ -> 0
 580            in
 581            let no_args = count_prod arity in
 582              (* now, create a "generic" MutInd *)
 583            let metasenv,left_args =
 584              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 585            in
 586            let metasenv,right_args =
 587              let no_right_params = no_args - no_left_params in
 588                if no_right_params < 0 then assert false
 589                else CicMkImplicit.n_fresh_metas
 590                       metasenv subst context no_right_params
 591            in
 592            let metasenv,exp_named_subst =
 593              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 594            let expected_type =
 595              if no_args = 0 then
 596                C.MutInd (uri,i,exp_named_subst)
 597              else
 598                C.Appl
 599                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 600            in
 601              (* check consistency with the actual type of term *)
 602            let term',actual_type,subst,metasenv,ugraph1 =
 603              type_of_aux subst metasenv context term ugraph in
 604            let expected_type',_, subst, metasenv,ugraph2 =
 605              type_of_aux subst metasenv context expected_type ugraph1
 606            in
 607            let actual_type = CicReduction.whd ~subst context actual_type in
 608            let subst,metasenv,ugraph3 =
 609             try
 610              fo_unif_subst subst context metasenv
 611                expected_type' actual_type ugraph2
 612             with
 613              exn ->
 614               enrich localization_tbl term' exn
 615                ~f:(function _ ->
 616                  lazy ("The term " ^
 617                   CicMetaSubst.ppterm_in_context subst term'
 618                    context ^ " has type " ^
 619                   CicMetaSubst.ppterm_in_context subst actual_type
 620                    context ^ " but is here used with type " ^
 621                   CicMetaSubst.ppterm_in_context subst expected_type' context))
 622            in
 623            let rec instantiate_prod t =
 624             function
 625                [] -> t
 626              | he::tl ->
 627                 match CicReduction.whd ~subst context t with
 628                    C.Prod (_,_,t') ->
 629                     instantiate_prod (CicSubstitution.subst he t') tl
 630                  | _ -> assert false
 631            in
 632            let arity_instantiated_with_left_args =
 633             instantiate_prod arity left_args in
 634              (* TODO: check if the sort elimination
 635               * is allowed: [(I q1 ... qr)|B] *)
 636            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 637              List.fold_left
 638                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 639                   let constructor =
 640                     if left_args = [] then
 641                       (C.MutConstruct (uri,i,j,exp_named_subst))
 642                     else
 643                       (C.Appl
 644                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 645                   in
 646                   let p',actual_type,subst,metasenv,ugraph1 =
 647                     type_of_aux subst metasenv context p ugraph
 648                   in
 649                   let constructor',expected_type, subst, metasenv,ugraph2 =
 650                     type_of_aux subst metasenv context constructor ugraph1
 651                   in
 652                   let outtypeinstance,subst,metasenv,ugraph3 =
 653                     check_branch 0 context metasenv subst no_left_params
 654                       actual_type constructor' expected_type ugraph2
 655                   in
 656                     (pl @ [p'],j+1,
 657                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 658                ([],1,[],subst,metasenv,ugraph3) pl
 659            in
 660
 661              (* we are left to check that the outype matches his instances.
 662                 The easy case is when the outype is specified, that amount
 663                 to a trivial check. Otherwise, we should guess a type from
 664                 its instances
 665              *)
 666
 667            let outtype,outtypety, subst, metasenv,ugraph4 =
 668              type_of_aux subst metasenv context outtype ugraph4 in
 669            (match outtype with
 670            | C.Meta (n,l) ->
 671                (let candidate,ugraph5,metasenv,subst =
 672                  let exp_name_subst, metasenv =
 673                     let o,_ =
 674                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 675                     in
 676                     let uris = CicUtil.params_of_obj o in
 677                     List.fold_right (
 678                       fun uri (acc,metasenv) ->
 679                         let metasenv',new_meta =
 680                            CicMkImplicit.mk_implicit metasenv subst context
 681                         in
 682                         let irl =
 683                           CicMkImplicit.identity_relocation_list_for_metavariable
 684                             context
 685                         in
 686                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 687                     ) uris ([],metasenv)
 688                  in
 689                  let ty =
 690                   match left_args,right_args with
 691                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 692                    | _,_ ->
 693                       let rec mk_right_args =
 694                        function
 695                           0 -> []
 696                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 697                       in
 698                       let right_args_no = List.length right_args in
 699                       let lifted_left_args =
 700                        List.map (CicSubstitution.lift right_args_no) left_args
 701                       in
 702                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 703                         (lifted_left_args @ mk_right_args right_args_no))
 704                  in
 705                  let fresh_name =
 706                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 707                      context Cic.Anonymous ~typ:ty
 708                  in
 709                  match outtypeinstances with
 710                  | [] ->
 711                      let extended_context =
 712                       let rec add_right_args =
 713                        function
 714                           Cic.Prod (name,ty,t) ->
 715                            Some (name,Cic.Decl ty)::(add_right_args t)
 716                         | _ -> []
 717                       in
 718                        (Some (fresh_name,Cic.Decl ty))::
 719                        (List.rev
 720                         (add_right_args arity_instantiated_with_left_args))@
 721                        context
 722                      in
 723                      let metasenv,new_meta =
 724                        CicMkImplicit.mk_implicit metasenv subst extended_context
 725                      in
 726                        let irl =
 727                        CicMkImplicit.identity_relocation_list_for_metavariable
 728                          extended_context
 729                      in
 730                      let rec add_lambdas b =
 731                       function
 732                          Cic.Prod (name,ty,t) ->
 733                           Cic.Lambda (name,ty,(add_lambdas b t))
 734                        | _ -> Cic.Lambda (fresh_name, ty, b)
 735                      in
 736                      let candidate =
 737                       add_lambdas (Cic.Meta (new_meta,irl))
 738                        arity_instantiated_with_left_args
 739                      in
 740                      (Some candidate),ugraph4,metasenv,subst
 741                  | (constructor_args_no,_,instance,_)::tl ->
 742                      try
 743                        let instance',subst,metasenv =
 744                          CicMetaSubst.delift_rels subst metasenv
 745                           constructor_args_no instance
 746                        in
 747                        let candidate,ugraph,metasenv,subst =
 748                          List.fold_left (
 749                            fun (candidate_oty,ugraph,metasenv,subst)
 750                              (constructor_args_no,_,instance,_) ->
 751                                match candidate_oty with
 752                                | None -> None,ugraph,metasenv,subst
 753                                | Some ty ->
 754                                  try
 755                                    let instance',subst,metasenv =
 756                                      CicMetaSubst.delift_rels subst metasenv
 757                                       constructor_args_no instance
 758                                    in
 759                                    let subst,metasenv,ugraph =
 760                                     fo_unif_subst subst context metasenv
 761                                       instance' ty ugraph
 762                                    in
 763                                     candidate_oty,ugraph,metasenv,subst
 764                                  with
 765                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 766                                   | CicUnification.UnificationFailure _
 767                                   | CicUnification.Uncertain _ ->
 768                                      None,ugraph,metasenv,subst
 769                          ) (Some instance',ugraph4,metasenv,subst) tl
 770                        in
 771                        match candidate with
 772                        | None -> None, ugraph,metasenv,subst
 773                        | Some t ->
 774                           let rec add_lambdas n b =
 775                            function
 776                               Cic.Prod (name,ty,t) ->
 777                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 778                             | _ ->
 779                               Cic.Lambda (fresh_name, ty,
 780                                CicSubstitution.lift (n + 1) t)
 781                           in
 782                            Some
 783                             (add_lambdas 0 t arity_instantiated_with_left_args),
 784                            ugraph,metasenv,subst
 785                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 786                        None,ugraph4,metasenv,subst
 787                in
 788                match candidate with
 789                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 790                | Some candidate ->
 791                    let subst,metasenv,ugraph =
 792                     try
 793                      fo_unif_subst subst context metasenv
 794                        candidate outtype ugraph5
 795                     with
 796                      exn -> assert false(* unification against a metavariable *)
 797                    in
 798                      C.MutCase (uri, i, outtype, term', pl'),
 799                       CicReduction.head_beta_reduce
 800                        (CicMetaSubst.apply_subst subst
 801                         (Cic.Appl (outtype::right_args@[term']))),
 802                      subst,metasenv,ugraph)
 803            | _ ->    (* easy case *)
 804              let tlbody_and_type,subst,metasenv,ugraph4 =
 805                List.fold_right
 806                  (fun x (res,subst,metasenv,ugraph) ->
 807                     let x',ty,subst',metasenv',ugraph1 =
 808                       type_of_aux subst metasenv context x ugraph
 809                     in
 810                       (x', ty)::res,subst',metasenv',ugraph1
 811                  ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
 812              in
 813              let _,_,subst,metasenv,ugraph4 =
 814                eat_prods false subst metasenv context
 815                  outtypety tlbody_and_type ugraph4
 816              in
 817              let _,_, subst, metasenv,ugraph5 =
 818                type_of_aux subst metasenv context
 819                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 820              in
 821              let (subst,metasenv,ugraph6) =
 822                List.fold_left2
 823                  (fun (subst,metasenv,ugraph)
 824                    p (constructor_args_no,context,instance,args)
 825                   ->
 826                     let instance' =
 827                       let appl =
 828                         let outtype' =
 829                           CicSubstitution.lift constructor_args_no outtype
 830                         in
 831                           C.Appl (outtype'::args)
 832                       in
 833                         CicReduction.whd ~subst context appl
 834                     in
 835                      try
 836                       fo_unif_subst subst context metasenv instance instance'
 837                        ugraph
 838                      with
 839                       exn ->
 840                        enrich localization_tbl p exn
 841                         ~f:(function _ ->
 842                           lazy ("The term " ^
 843                            CicMetaSubst.ppterm_in_context subst p
 844                             context ^ " has type " ^
 845                            CicMetaSubst.ppterm_in_context subst instance'
 846                             context ^ " but is here used with type " ^
 847                            CicMetaSubst.ppterm_in_context subst instance
 848                             context)))
 849                  (subst,metasenv,ugraph5) pl' outtypeinstances
 850              in
 851                C.MutCase (uri, i, outtype, term', pl'),
 852                  CicReduction.head_beta_reduce
 853                   (CicMetaSubst.apply_subst subst
 854                    (C.Appl(outtype::right_args@[term]))),
 855                  subst,metasenv,ugraph6)
 856         | C.Fix (i,fl) ->
 857             let fl_ty',subst,metasenv,types,ugraph1 =
 858               List.fold_left
 859                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 860                    let ty',_,subst',metasenv',ugraph1 =
 861                       type_of_aux subst metasenv context ty ugraph
 862                    in
 863                      fl @ [ty'],subst',metasenv',
 864                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 865                 ) ([],subst,metasenv,[],ugraph) fl
 866             in
 867             let len = List.length types in
 868             let context' = types@context in
 869             let fl_bo',subst,metasenv,ugraph2 =
 870               List.fold_left
 871                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 872                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 873                      type_of_aux subst metasenv context' bo ugraph in
 874                    let expected_ty = CicSubstitution.lift len ty in
 875                    let subst',metasenv',ugraph' =
 876                     try
 877                      fo_unif_subst subst context' metasenv
 878                        ty_of_bo expected_ty ugraph1
 879                     with
 880                      exn ->
 881                       enrich localization_tbl bo exn
 882                        ~f:(function _ ->
 883                          lazy ("The term " ^
 884                           CicMetaSubst.ppterm_in_context subst bo
 885                            context' ^ " has type " ^
 886                           CicMetaSubst.ppterm_in_context subst ty_of_bo
 887                            context' ^ " but is here used with type " ^
 888                           CicMetaSubst.ppterm_in_context subst expected_ty
 889                            context))
 890                    in
 891                      fl @ [bo'] , subst',metasenv',ugraph'
 892                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 893             in
 894             let ty = List.nth fl_ty' i in
 895             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 896              * and we want the new fl with bo' and ty' injected in the right
 897              * place.
 898              *)
 899             let rec map3 f l1 l2 l3 =
 900               match l1,l2,l3 with
 901               | [],[],[] -> []
 902               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 903               | _ -> assert false
 904             in
 905             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 906               fl_ty' fl_bo' fl
 907             in
 908               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 909         | C.CoFix (i,fl) ->
 910             let fl_ty',subst,metasenv,types,ugraph1 =
 911               List.fold_left
 912                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 913                    let ty',_,subst',metasenv',ugraph1 =
 914                      type_of_aux subst metasenv context ty ugraph
 915                    in
 916                      fl @ [ty'],subst',metasenv',
 917                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 918                 ) ([],subst,metasenv,[],ugraph) fl
 919             in
 920             let len = List.length types in
 921             let context' = types@context in
 922             let fl_bo',subst,metasenv,ugraph2 =
 923               List.fold_left
 924                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 925                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 926                      type_of_aux subst metasenv context' bo ugraph in
 927                    let expected_ty = CicSubstitution.lift len ty in
 928                    let subst',metasenv',ugraph' =
 929                     try
 930                      fo_unif_subst subst context' metasenv
 931                        ty_of_bo expected_ty ugraph1
 932                     with
 933                      exn ->
 934                       enrich localization_tbl bo exn
 935                        ~f:(function _ ->
 936                          lazy ("The term " ^
 937                           CicMetaSubst.ppterm_in_context subst bo
 938                            context' ^ " has type " ^
 939                           CicMetaSubst.ppterm_in_context subst ty_of_bo
 940                            context' ^ " but is here used with type " ^
 941                           CicMetaSubst.ppterm_in_context subst expected_ty
 942                            context))
 943                    in
 944                      fl @ [bo'],subst',metasenv',ugraph'
 945                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 946             in
 947             let ty = List.nth fl_ty' i in
 948             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 949              * and we want the new fl with bo' and ty' injected in the right
 950              * place.
 951              *)
 952             let rec map3 f l1 l2 l3 =
 953               match l1,l2,l3 with
 954               | [],[],[] -> []
 955               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 956               | _ -> assert false
 957             in
 958             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 959               fl_ty' fl_bo' fl
 960             in
 961               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 962      in
 963       relocalize localization_tbl t t';
 964       res
 965
 966   (* check_metasenv_consistency checks that the "canonical" context of a
 967      metavariable is consitent - up to relocation via the relocation list l -
 968      with the actual context *)
 969   and check_metasenv_consistency
 970     metano subst metasenv context canonical_context l ugraph
 971     =
 972     let module C = Cic in
 973     let module R = CicReduction in
 974     let module S = CicSubstitution in
 975     let lifted_canonical_context =
 976       let rec aux i =
 977         function
 978             [] -> []
 979           | (Some (n,C.Decl t))::tl ->
 980               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 981           | (Some (n,C.Def (t,None)))::tl ->
 982               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 983           | None::tl -> None::(aux (i+1) tl)
 984           | (Some (n,C.Def (t,Some ty)))::tl ->
 985               (Some (n,
 986                      C.Def ((S.subst_meta l (S.lift i t)),
 987                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 988       in
 989         aux 1 canonical_context
 990     in
 991       try
 992         List.fold_left2
 993           (fun (l,subst,metasenv,ugraph) t ct ->
 994              match (t,ct) with
 995                  _,None ->
 996                    l @ [None],subst,metasenv,ugraph
 997                | Some t,Some (_,C.Def (ct,_)) ->
 998                    let subst',metasenv',ugraph' =
 999                    (try
1000                       fo_unif_subst subst context metasenv t ct ugraph
1001                     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))))))
1002                    in
1003                      l @ [Some t],subst',metasenv',ugraph'
1004                | Some t,Some (_,C.Decl ct) ->
1005                    let t',inferredty,subst',metasenv',ugraph1 =
1006                      type_of_aux subst metasenv context t ugraph
1007                    in
1008                    let subst'',metasenv'',ugraph2 =
1009                      (try
1010                         fo_unif_subst
1011                           subst' context metasenv' inferredty ct ugraph1
1012                       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))))))
1013                    in
1014                      l @ [Some t'], subst'',metasenv'',ugraph2
1015                | None, Some _  ->
1016                    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
1017       with
1018           Invalid_argument _ ->
1019             raise
1020             (RefineFailure
1021                (lazy (sprintf
1022                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1023                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
1024                   (CicMetaSubst.ppcontext subst canonical_context))))
1025
1026   and check_exp_named_subst metasubst metasenv context tl ugraph =
1027     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
1028       match tl with
1029           [] -> [],metasubst,metasenv,ugraph
1030         | (uri,t)::tl ->
1031             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
1032             let typeofvar =
1033               CicSubstitution.subst_vars substs ty_uri in
1034               (* CSC: why was this code here? it is wrong
1035                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1036                  Cic.Variable (_,Some bo,_,_) ->
1037                  raise
1038                  (RefineFailure (lazy
1039                  "A variable with a body can not be explicit substituted"))
1040                  | Cic.Variable (_,None,_,_) -> ()
1041                  | _ ->
1042                  raise
1043                  (RefineFailure (lazy
1044                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1045                  ) ;
1046               *)
1047             let t',typeoft,metasubst',metasenv',ugraph2 =
1048               type_of_aux metasubst metasenv context t ugraph1 in
1049             let subst = uri,t' in
1050             let metasubst'',metasenv'',ugraph3 =
1051               try
1052                 fo_unif_subst
1053                   metasubst' context metasenv' typeoft typeofvar ugraph2
1054               with _ ->
1055                 raise (RefineFailure (lazy
1056                          ("Wrong Explicit Named Substitution: " ^
1057                            CicMetaSubst.ppterm metasubst' typeoft ^
1058                           " not unifiable with " ^
1059                           CicMetaSubst.ppterm metasubst' typeofvar)))
1060             in
1061             (* FIXME: no mere tail recursive! *)
1062             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1063               check_exp_named_subst_aux
1064                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1065             in
1066               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1067     in
1068       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1069
1070
1071   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
1072     let module C = Cic in
1073     let context_for_t2 = (Some (name,C.Decl s))::context in
1074     let t1'' = CicReduction.whd ~subst context t1 in
1075     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1076       match (t1'', t2'') with
1077           (C.Sort s1, C.Sort s2)
1078             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1079               (* different than Coq manual!!! *)
1080               C.Sort s2,subst,metasenv,ugraph
1081         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1082             let t' = CicUniv.fresh() in
1083             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1084             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1085               C.Sort (C.Type t'),subst,metasenv,ugraph2
1086         | (C.Sort _,C.Sort (C.Type t1)) ->
1087             C.Sort (C.Type t1),subst,metasenv,ugraph
1088         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1089         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1090             (* TODO how can we force the meta to become a sort? If we don't we
1091              * break the invariant that refine produce only well typed terms *)
1092             (* TODO if we check the non meta term and if it is a sort then we
1093              * are likely to know the exact value of the result e.g. if the rhs
1094              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1095             let (metasenv,idx) =
1096               CicMkImplicit.mk_implicit_sort metasenv subst in
1097             let (subst, metasenv,ugraph1) =
1098               fo_unif_subst subst context_for_t2 metasenv
1099                 (C.Meta (idx,[])) t2'' ugraph
1100             in
1101               t2'',subst,metasenv,ugraph1
1102         | _,_ ->
1103             raise
1104               (RefineFailure
1105                 (lazy
1106                   (sprintf
1107                     ("Two sorts were expected, found %s " ^^
1108                      "(that reduces to %s) and %s (that reduces to %s)")
1109                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1110                 (CicPp.ppterm t2''))))
1111
1112   and eat_prods
1113     allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1114   =
1115     let rec mk_prod metasenv context' =
1116       function
1117           [] ->
1118             let (metasenv, idx) =
1119               CicMkImplicit.mk_implicit_type metasenv subst context'
1120             in
1121             let irl =
1122               CicMkImplicit.identity_relocation_list_for_metavariable context'
1123             in
1124               metasenv,Cic.Meta (idx, irl)
1125         | (_,argty)::tl ->
1126             let (metasenv, idx) =
1127               CicMkImplicit.mk_implicit_type metasenv subst context'
1128             in
1129             let irl =
1130               CicMkImplicit.identity_relocation_list_for_metavariable context'
1131             in
1132             let meta = Cic.Meta (idx,irl) in
1133             let name =
1134               (* The name must be fresh for context.                 *)
1135               (* Nevertheless, argty is well-typed only in context.  *)
1136               (* Thus I generate a name (name_hint) in context and   *)
1137               (* then I generate a name --- using the hint name_hint *)
1138               (* --- that is fresh in context'.                      *)
1139               let name_hint =
1140                 (* Cic.Name "pippo" *)
1141                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1142                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1143                   (CicMetaSubst.apply_subst_context subst context)
1144                   Cic.Anonymous
1145                   ~typ:(CicMetaSubst.apply_subst subst argty)
1146               in
1147                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1148                 FreshNamesGenerator.mk_fresh_name ~subst
1149                   [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
1150             in
1151             let metasenv,target =
1152               mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
1153             in
1154               metasenv,Cic.Prod (name,meta,target)
1155     in
1156     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1157     let (subst, metasenv,ugraph1) =
1158       try
1159         fo_unif_subst subst context metasenv hetype hetype' ugraph
1160       with exn ->
1161         debug_print
1162           (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1163                          (CicPp.ppterm hetype)
1164                          (CicPp.ppterm hetype')
1165                          (CicMetaSubst.ppmetasenv [] metasenv)
1166                          (CicMetaSubst.ppsubst subst)));
1167         raise exn
1168
1169     in
1170     let rec eat_prods metasenv subst context hetype ugraph =
1171       function
1172         | [] -> [],metasenv,subst,hetype,ugraph
1173         | (hete, hety)::tl ->
1174             (match hetype with
1175                  Cic.Prod (n,s,t) ->
1176                    let arg,subst,metasenv,ugraph1 =
1177                      try
1178                        let subst,metasenv,ugraph1 =
1179                          fo_unif_subst subst context metasenv hety s ugraph
1180                        in
1181                          hete,subst,metasenv,ugraph1
1182                      with exn when allow_coercions && !insert_coercions ->
1183                        (* we search a coercion from hety to s *)
1184                        let coer, tgt_carr =
1185                          let carr t subst context =
1186                            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                            let newt, _, subst, metasenv, ugraph =
1216                              avoid_double_coercion context
1217                               subst metasenv ugraph
1218                                 (Cic.Appl[c;hete]) tgt_carr in
1219                            try
1220                             let newty,newhety,subst,metasenv,ugraph =
1221                               type_of_aux subst metasenv context newt ugraph 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 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 as t ->
1494        let b,_,_,_ = is_a_double_coercion t in
1495        (* prerr_endline "CANDIDATO!!!!"; *)
1496        let newt =
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        in
1516        (match newt with
1517        | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
1518        | _ -> assert false)
1519    | C.Var (uri,exp_named_subst) ->
1520        let exp_named_subst = List.map aux exp_named_subst in
1521        C.Var (uri, exp_named_subst)
1522    | C.Const (uri,exp_named_subst) ->
1523        let exp_named_subst = List.map aux exp_named_subst in
1524        C.Const (uri, exp_named_subst)
1525    | C.MutInd (uri,tyno,exp_named_subst) ->
1526        let exp_named_subst = List.map aux exp_named_subst in
1527        C.MutInd (uri,tyno,exp_named_subst)
1528    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1529        let exp_named_subst = List.map aux exp_named_subst in
1530        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1531    | C.MutCase (uri,tyno,out,te,pl) ->
1532        let pl = List.map (merge_coercions ctx) pl in
1533        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1534    | C.Fix (fno, fl) ->
1535        let ctx =
1536          List.fold_left
1537            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1538            ctx fl
1539        in
1540        let fl =
1541          List.map
1542            (fun (name,idx,ty,bo) ->
1543              (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
1544          fl
1545        in
1546        C.Fix (fno, fl)
1547    | C.CoFix (fno, fl) ->
1548        let ctx =
1549          List.fold_left
1550            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1551            ctx fl
1552        in
1553        let fl =
1554          List.map
1555            (fun (name,ty,bo) ->
1556              (name, merge_coercions ctx ty, merge_coercions ctx bo))
1557          fl
1558        in
1559        C.CoFix (fno, fl)
1560  in
1561  merge_coercions [] t
1562 ;;
1563
1564 let pack_coercion_obj obj =
1565   let module C = Cic in
1566   match obj with
1567   | C.Constant (id, body, ty, params, attrs) ->
1568       let body =
1569         match body with
1570         | None -> None
1571         | Some body -> Some (pack_coercion [] body)
1572       in
1573       let ty = pack_coercion [] ty in
1574         C.Constant (id, body, ty, params, attrs)
1575   | C.Variable (name, body, ty, params, attrs) ->
1576       let body =
1577         match body with
1578         | None -> None
1579         | Some body -> Some (pack_coercion [] body)
1580       in
1581       let ty = pack_coercion [] ty in
1582         C.Variable (name, body, ty, params, attrs)
1583   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1584       let conjectures =
1585         List.map
1586           (fun (i, ctx, ty) ->
1587             let ctx =
1588               List.map
1589                 (function
1590                 | Some (name, C.Decl t) ->
1591                     Some (name, C.Decl (pack_coercion conjectures t))
1592                 | Some (name, C.Def (t,None)) ->
1593                     Some (name, C.Def (pack_coercion conjectures t, None))
1594                 | Some (name, C.Def (t,Some ty)) ->
1595                     Some (name, C.Def (pack_coercion conjectures t,
1596                                     Some (pack_coercion conjectures ty)))
1597                 | None -> None)
1598                 ctx
1599             in
1600             ((i,ctx,pack_coercion conjectures 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