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