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