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