helm/software/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 (* for internal use only; the integer is the number of surplus arguments *)
  35 exception MoreArgsThanExpected of int * exn;;
  36
  37 let insert_coercions = ref true
  38 let pack_coercions = ref true
  39
  40 let debug = false;;
  41
  42 let debug_print =
  43   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
  44
  45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
  46
  47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
  48   try
  49 let foo () =
  50     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  51 in profiler_eat_prods2.HExtlib.profile foo ()
  52   with
  53       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  54     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  55 ;;
  56
  57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
  58
  59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
  60   try
  61 let foo () =
  62     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  63 in profiler_eat_prods.HExtlib.profile foo ()
  64   with
  65       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  66     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  67 ;;
  68
  69 let profiler = HExtlib.profile "CicRefine.fo_unif"
  70
  71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
  72   try
  73 let foo () =
  74     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  75 in profiler.HExtlib.profile foo ()
  76   with
  77       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  78     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  79 ;;
  80
  81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
  82  let exn' =
  83   match exn with
  84      RefineFailure msg -> RefineFailure (f msg)
  85    | Uncertain msg -> Uncertain (f msg)
  86    | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
  87    | Sys.Break -> raise exn
  88    | _ -> prerr_endline (Printexc.to_string exn); assert false
  89  in
  90  let loc =
  91   try
  92    Cic.CicHash.find localization_tbl t
  93   with Not_found ->
  94    HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
  95    raise exn'
  96  in
  97   raise (HExtlib.Localized (loc,exn'))
  98
  99 let relocalize localization_tbl oldt newt =
 100  try
 101   let infos = Cic.CicHash.find localization_tbl oldt in
 102    Cic.CicHash.remove localization_tbl oldt;
 103    Cic.CicHash.add localization_tbl newt infos;
 104  with
 105   Not_found -> ()
 106 ;;
 107
 108 let rec split l n =
 109  match (l,n) with
 110     (l,0) -> ([], l)
 111   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
 112   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
 113 ;;
 114
 115 let exp_impl metasenv subst context =
 116  function
 117   | Some `Type ->
 118       let (metasenv', idx) =
 119         CicMkImplicit.mk_implicit_type metasenv subst context in
 120       let irl =
 121         CicMkImplicit.identity_relocation_list_for_metavariable context in
 122       metasenv', Cic.Meta (idx, irl)
 123   | Some `Closed ->
 124       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
 125       metasenv', Cic.Meta (idx, [])
 126   | None ->
 127       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
 128       let irl =
 129         CicMkImplicit.identity_relocation_list_for_metavariable context in
 130       metasenv', Cic.Meta (idx, irl)
 131   | _ -> assert false
 132 ;;
 133
 134 let is_a_double_coercion t =
 135   let rec subst_nth n x l =
 136     match n,l with
 137     | _, [] -> []
 138     | 0, _::tl -> x :: tl
 139     | n, hd::tl -> hd :: subst_nth (n-1) x tl
 140   in
 141   let imp = Cic.Implicit None in
 142   let dummyres = false,imp, imp,imp,imp in
 143   match t with
 144   | Cic.Appl l1 ->
 145      (match CoercGraph.coerced_arg l1 with
 146      | Some (Cic.Appl l2, pos1) ->
 147          (match CoercGraph.coerced_arg l2 with
 148          | Some (x, pos2) ->
 149              true, List.hd l1, List.hd l2, x,
 150               Cic.Appl (subst_nth (pos1 + 1)
 151                 (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
 152          | _ -> dummyres)
 153       | _ -> dummyres)
 154   | _ -> dummyres
 155 ;;
 156
 157 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 158 =
 159   let len = List.length tlbody_and_type in
 160   let msg =
 161     lazy ("The term " ^
 162       CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
 163       " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
 164       ") is here applied to " ^ string_of_int len ^
 165       " arguments but here it can handle only up to " ^
 166       string_of_int (len - residuals) ^ " arguments")
 167   in
 168   enrich localization_tbl he ~f:(fun _-> msg) exn
 169 ;;
 170
 171 let mk_prod_of_metas metasenv context subst args =
 172   let rec mk_prod metasenv context' = function
 173     | [] ->
 174         let (metasenv, idx) =
 175           CicMkImplicit.mk_implicit_type metasenv subst context'
 176         in
 177         let irl =
 178           CicMkImplicit.identity_relocation_list_for_metavariable context'
 179         in
 180           metasenv,Cic.Meta (idx, irl)
 181     | (_,argty)::tl ->
 182         let (metasenv, idx) =
 183           CicMkImplicit.mk_implicit_type metasenv subst context'
 184         in
 185         let irl =
 186           CicMkImplicit.identity_relocation_list_for_metavariable context'
 187         in
 188         let meta = Cic.Meta (idx,irl) in
 189         let name =
 190           (* The name must be fresh for context.                 *)
 191           (* Nevertheless, argty is well-typed only in context.  *)
 192           (* Thus I generate a name (name_hint) in context and   *)
 193           (* then I generate a name --- using the hint name_hint *)
 194           (* --- that is fresh in context'.                      *)
 195           let name_hint =
 196             FreshNamesGenerator.mk_fresh_name ~subst metasenv
 197               (CicMetaSubst.apply_subst_context subst context)
 198               Cic.Anonymous
 199               ~typ:(CicMetaSubst.apply_subst subst argty)
 200           in
 201             FreshNamesGenerator.mk_fresh_name ~subst
 202               [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
 203         in
 204         let metasenv,target =
 205           mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
 206         in
 207           metasenv,Cic.Prod (name,meta,target)
 208   in
 209   mk_prod metasenv context args
 210 ;;
 211
 212 let rec type_of_constant uri ugraph =
 213  let module C = Cic in
 214  let module R = CicReduction in
 215  let module U = UriManager in
 216   let _ = CicTypeChecker.typecheck uri in
 217   let obj,u =
 218    try
 219     CicEnvironment.get_cooked_obj ugraph uri
 220    with Not_found -> assert false
 221   in
 222    match obj with
 223       C.Constant (_,_,ty,_,_) -> ty,u
 224     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
 225     | _ ->
 226        raise
 227         (RefineFailure
 228           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 229
 230 and type_of_variable uri ugraph =
 231   let module C = Cic in
 232   let module R = CicReduction in
 233   let module U = UriManager in
 234   let _ = CicTypeChecker.typecheck uri in
 235   let obj,u =
 236    try
 237     CicEnvironment.get_cooked_obj ugraph uri
 238     with Not_found -> assert false
 239   in
 240    match obj with
 241       C.Variable (_,_,ty,_,_) -> ty,u
 242     | _ ->
 243         raise
 244          (RefineFailure
 245           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
 246
 247 and type_of_mutual_inductive_defs uri i ugraph =
 248   let module C = Cic in
 249   let module R = CicReduction in
 250   let module U = UriManager in
 251   let _ = CicTypeChecker.typecheck uri in
 252   let obj,u =
 253    try
 254     CicEnvironment.get_cooked_obj ugraph uri
 255    with Not_found -> assert false
 256   in
 257    match obj with
 258       C.InductiveDefinition (dl,_,_,_) ->
 259         let (_,_,arity,_) = List.nth dl i in
 260          arity,u
 261     | _ ->
 262        raise
 263         (RefineFailure
 264          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
 265
 266 and type_of_mutual_inductive_constr uri i j ugraph =
 267   let module C = Cic in
 268   let module R = CicReduction in
 269   let module U = UriManager in
 270   let _ = CicTypeChecker.typecheck uri in
 271    let obj,u =
 272     try
 273      CicEnvironment.get_cooked_obj ugraph uri
 274     with Not_found -> assert false
 275    in
 276     match obj with
 277         C.InductiveDefinition (dl,_,_,_) ->
 278           let (_,_,_,cl) = List.nth dl i in
 279           let (_,ty) = List.nth cl (j-1) in
 280             ty,u
 281       | _ ->
 282           raise
 283                   (RefineFailure
 284               (lazy
 285                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 286
 287
 288 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 289
 290 (* the check_branch function checks if a branch of a case is refinable.
 291    It returns a pair (outype_instance,args), a subst and a metasenv.
 292    outype_instance is the expected result of applying the case outtype
 293    to args.
 294    The problem is that outype is in general unknown, and we should
 295    try to synthesize it from the above information, that is in general
 296    a second order unification problem. *)
 297
 298 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 299   let module C = Cic in
 300   let module R = CicReduction in
 301     match R.whd ~subst context expectedtype with
 302         C.MutInd (_,_,_) ->
 303           (n,context,actualtype, [term]), subst, metasenv, ugraph
 304       | C.Appl (C.MutInd (_,_,_)::tl) ->
 305           let (_,arguments) = split tl left_args_no in
 306             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 307       | C.Prod (_,so,de) ->
 308           (* we expect that the actual type of the branch has the due
 309              number of Prod *)
 310           (match R.whd ~subst context actualtype with
 311                C.Prod (name',so',de') ->
 312                  let subst, metasenv, ugraph1 =
 313                    fo_unif_subst subst context metasenv so so' ugraph in
 314                  let term' =
 315                    (match CicSubstitution.lift 1 term with
 316                         C.Appl l -> C.Appl (l@[C.Rel 1])
 317                       | t -> C.Appl [t ; C.Rel 1]) in
 318                    (* we should also check that the name variable is anonymous in
 319                       the actual type de' ?? *)
 320                    check_branch (n+1)
 321                      ((Some (name',(C.Decl so)))::context)
 322                        metasenv subst left_args_no de' term' de ugraph1
 323              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
 324       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 325
 326 and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 327      ugraph
 328 =
 329   let rec type_of_aux subst metasenv context t ugraph =
 330     let module C = Cic in
 331     let module S = CicSubstitution in
 332     let module U = UriManager in
 333      let (t',_,_,_,_) as res =
 334       match t with
 335           (*    function *)
 336           C.Rel n ->
 337             (try
 338                match List.nth context (n - 1) with
 339                    Some (_,C.Decl ty) ->
 340                      t,S.lift n ty,subst,metasenv, ugraph
 341                  | Some (_,C.Def (_,ty)) ->
 342                      t,S.lift n ty,subst,metasenv, ugraph
 343                  | None ->
 344                     enrich localization_tbl t
 345                      (RefineFailure (lazy "Rel to hidden hypothesis"))
 346              with
 347               Failure _ ->
 348                enrich localization_tbl t
 349                 (RefineFailure (lazy "Not a closed term")))
 350         | C.Var (uri,exp_named_subst) ->
 351             let exp_named_subst',subst',metasenv',ugraph1 =
 352               check_exp_named_subst
 353                 subst metasenv context exp_named_subst ugraph
 354             in
 355             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 356             let ty =
 357               CicSubstitution.subst_vars exp_named_subst' ty_uri
 358             in
 359               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 360         | C.Meta (n,l) ->
 361             (try
 362                let (canonical_context, term,ty) =
 363                  CicUtil.lookup_subst n subst
 364                in
 365                let l',subst',metasenv',ugraph1 =
 366                  check_metasenv_consistency n subst metasenv context
 367                    canonical_context l ugraph
 368                in
 369                  (* trust or check ??? *)
 370                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 371                    subst', metasenv', ugraph1
 372                    (* type_of_aux subst metasenv
 373                       context (CicSubstitution.subst_meta l term) *)
 374              with CicUtil.Subst_not_found _ ->
 375                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 376                let l',subst',metasenv', ugraph1 =
 377                  check_metasenv_consistency n subst metasenv context
 378                    canonical_context l ugraph
 379                in
 380                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 381                    subst', metasenv',ugraph1)
 382         | C.Sort (C.Type tno) ->
 383             let tno' = CicUniv.fresh() in
 384              (try
 385                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 386                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 387               with
 388                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
 389         | C.Sort (C.CProp tno) ->
 390             let tno' = CicUniv.fresh() in
 391              (try
 392                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 393                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 394               with
 395                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
 396         | C.Sort (C.Prop|C.Set) ->
 397             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 398         | C.Implicit infos ->
 399            let metasenv',t' = exp_impl metasenv subst context infos in
 400             type_of_aux subst metasenv' context t' ugraph
 401         | C.Cast (te,ty) ->
 402             let ty',_,subst',metasenv',ugraph1 =
 403               type_of_aux subst metasenv context ty ugraph
 404             in
 405             let te',inferredty,subst'',metasenv'',ugraph2 =
 406               type_of_aux subst' metasenv' context te ugraph1
 407             in
 408             let (te', ty'), subst''',metasenv''',ugraph3 =
 409               coerce_to_something true localization_tbl te' inferredty ty'
 410                 subst'' metasenv'' context ugraph2
 411             in
 412              C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 413         | C.Prod (name,s,t) ->
 414             let s',sort1,subst',metasenv',ugraph1 =
 415               type_of_aux subst metasenv context s ugraph
 416             in
 417             let s',sort1,subst', metasenv',ugraph1 =
 418               coerce_to_sort localization_tbl
 419               s' sort1 subst' context metasenv' ugraph1
 420             in
 421             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 422             let t',sort2,subst'',metasenv'',ugraph2 =
 423               type_of_aux subst' metasenv'
 424                 context_for_t t ugraph1
 425             in
 426             let t',sort2,subst'',metasenv'',ugraph2 =
 427               coerce_to_sort localization_tbl
 428               t' sort2 subst'' context_for_t metasenv'' ugraph2
 429             in
 430               let sop,subst''',metasenv''',ugraph3 =
 431                 sort_of_prod localization_tbl subst'' metasenv''
 432                   context (name,s') t' (sort1,sort2) ugraph2
 433               in
 434                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 435         | C.Lambda (n,s,t) ->
 436             let s',sort1,subst',metasenv',ugraph1 =
 437               type_of_aux subst metasenv context s ugraph
 438             in
 439             let s',sort1,subst',metasenv',ugraph1 =
 440               coerce_to_sort localization_tbl
 441               s' sort1 subst' context metasenv' ugraph1
 442             in
 443             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 444             let t',type2,subst'',metasenv'',ugraph2 =
 445               type_of_aux subst' metasenv' context_for_t t ugraph1
 446             in
 447               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 448                 subst'',metasenv'',ugraph2
 449         | C.LetIn (n,s,ty,t) ->
 450            (* only to check if s is well-typed *)
 451            let s',ty',subst',metasenv',ugraph1 =
 452              type_of_aux subst metasenv context s ugraph in
 453            let ty,_,subst',metasenv',ugraph1 =
 454              type_of_aux subst' metasenv' context ty ugraph1 in
 455            let subst',metasenv',ugraph1 =
 456             try
 457              fo_unif_subst subst' context metasenv'
 458                ty ty' ugraph1
 459             with
 460              exn ->
 461               enrich localization_tbl s' exn
 462                ~f:(function _ ->
 463                  lazy ("The term " ^
 464                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
 465                    context ^ " has type " ^
 466                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
 467                    context ^ " but is here used with type " ^
 468                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
 469                    context))
 470            in
 471            let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
 472
 473             let t',inferredty,subst'',metasenv'',ugraph2 =
 474               type_of_aux subst' metasenv'
 475                 context_for_t t ugraph1
 476             in
 477               (* One-step LetIn reduction.
 478                * Even faster than the previous solution.
 479                * Moreover the inferred type is closer to the expected one.
 480                *)
 481               C.LetIn (n,s',ty,t'),
 482                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
 483                subst'',metasenv'',ugraph2
 484         | C.Appl (he::((_::_) as tl)) ->
 485             let he',hetype,subst',metasenv',ugraph1 =
 486               type_of_aux subst metasenv context he ugraph
 487             in
 488             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 489                typeof_list subst' metasenv' context ugraph1 tl
 490             in
 491             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
 492               eat_prods true subst'' metasenv'' context
 493                 he' hetype tlbody_and_type ugraph2
 494             in
 495             let newappl = (C.Appl (coerced_he::coerced_args)) in
 496             avoid_double_coercion
 497               context subst''' metasenv''' ugraph3 newappl applty
 498         | C.Appl _ -> assert false
 499         | C.Const (uri,exp_named_subst) ->
 500             let exp_named_subst',subst',metasenv',ugraph1 =
 501               check_exp_named_subst subst metasenv context
 502                 exp_named_subst ugraph in
 503             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 504             let cty =
 505               CicSubstitution.subst_vars exp_named_subst' ty_uri
 506             in
 507               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 508         | C.MutInd (uri,i,exp_named_subst) ->
 509             let exp_named_subst',subst',metasenv',ugraph1 =
 510               check_exp_named_subst subst metasenv context
 511                 exp_named_subst ugraph
 512             in
 513             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 514             let cty =
 515               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 516               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 517         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 518             let exp_named_subst',subst',metasenv',ugraph1 =
 519               check_exp_named_subst subst metasenv context
 520                 exp_named_subst ugraph
 521             in
 522             let ty_uri,ugraph2 =
 523               type_of_mutual_inductive_constr uri i j ugraph1
 524             in
 525             let cty =
 526               CicSubstitution.subst_vars exp_named_subst' ty_uri
 527             in
 528               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 529                 metasenv',ugraph2
 530         | C.MutCase (uri, i, outtype, term, pl) ->
 531             (* first, get the inductive type (and noparams)
 532              * in the environment  *)
 533             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 534               let _ = CicTypeChecker.typecheck uri in
 535               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 536               match obj with
 537                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 538                     List.nth l i , expl_params, parsno, u
 539                 | _ ->
 540                     enrich localization_tbl t
 541                      (RefineFailure
 542                        (lazy ("Unkown mutual inductive definition " ^
 543                          U.string_of_uri uri)))
 544            in
 545            if List.length constructors <> List.length pl then
 546             enrich localization_tbl t
 547              (RefineFailure
 548                (lazy "Wrong number of cases")) ;
 549            let rec count_prod t =
 550              match CicReduction.whd ~subst context t with
 551                  C.Prod (_, _, t) -> 1 + (count_prod t)
 552                | _ -> 0
 553            in
 554            let no_args = count_prod arity in
 555              (* now, create a "generic" MutInd *)
 556            let metasenv,left_args =
 557              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 558            in
 559            let metasenv,right_args =
 560              let no_right_params = no_args - no_left_params in
 561                if no_right_params < 0 then assert false
 562                else CicMkImplicit.n_fresh_metas
 563                       metasenv subst context no_right_params
 564            in
 565            let metasenv,exp_named_subst =
 566              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 567            let expected_type =
 568              if no_args = 0 then
 569                C.MutInd (uri,i,exp_named_subst)
 570              else
 571                C.Appl
 572                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 573            in
 574              (* check consistency with the actual type of term *)
 575            let term',actual_type,subst,metasenv,ugraph1 =
 576              type_of_aux subst metasenv context term ugraph in
 577            let expected_type',_, subst, metasenv,ugraph2 =
 578              type_of_aux subst metasenv context expected_type ugraph1
 579            in
 580            let actual_type = CicReduction.whd ~subst context actual_type in
 581            let subst,metasenv,ugraph3 =
 582             try
 583              fo_unif_subst subst context metasenv
 584                expected_type' actual_type ugraph2
 585             with
 586              exn ->
 587               enrich localization_tbl term' exn
 588                ~f:(function _ ->
 589                  lazy ("The term " ^
 590                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
 591                    context ^ " has type " ^
 592                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
 593                    context ^ " but is here used with type " ^
 594                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
 595                   context))
 596            in
 597            let rec instantiate_prod t =
 598             function
 599                [] -> t
 600              | he::tl ->
 601                 match CicReduction.whd ~subst context t with
 602                    C.Prod (_,_,t') ->
 603                     instantiate_prod (CicSubstitution.subst he t') tl
 604                  | _ -> assert false
 605            in
 606            let arity_instantiated_with_left_args =
 607             instantiate_prod arity left_args in
 608              (* TODO: check if the sort elimination
 609               * is allowed: [(I q1 ... qr)|B] *)
 610            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 611              List.fold_right
 612                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
 613                   let constructor =
 614                     if left_args = [] then
 615                       (C.MutConstruct (uri,i,j,exp_named_subst))
 616                     else
 617                       (C.Appl
 618                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 619                   in
 620                   let p',actual_type,subst,metasenv,ugraph1 =
 621                     type_of_aux subst metasenv context p ugraph
 622                   in
 623                   let constructor',expected_type, subst, metasenv,ugraph2 =
 624                     type_of_aux subst metasenv context constructor ugraph1
 625                   in
 626                   let outtypeinstance,subst,metasenv,ugraph3 =
 627                    try
 628                     check_branch 0 context metasenv subst
 629                      no_left_params actual_type constructor' expected_type
 630                      ugraph2
 631                    with
 632                     exn ->
 633                      enrich localization_tbl constructor'
 634                       ~f:(fun _ ->
 635                         lazy ("The term " ^
 636                          CicMetaSubst.ppterm_in_context metasenv subst p'
 637                           context ^ " has type " ^
 638                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
 639                           context ^ " but is here used with type " ^
 640                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
 641                           context)) exn
 642                   in
 643                     (p'::pl,j-1,
 644                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 645                pl ([],List.length pl,[],subst,metasenv,ugraph3)
 646            in
 647
 648              (* we are left to check that the outype matches his instances.
 649                 The easy case is when the outype is specified, that amount
 650                 to a trivial check. Otherwise, we should guess a type from
 651                 its instances
 652              *)
 653
 654            let outtype,outtypety, subst, metasenv,ugraph4 =
 655              type_of_aux subst metasenv context outtype ugraph4 in
 656            (match outtype with
 657            | C.Meta (n,l) ->
 658                (let candidate,ugraph5,metasenv,subst =
 659                  let exp_name_subst, metasenv =
 660                     let o,_ =
 661                       CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
 662                     in
 663                     let uris = CicUtil.params_of_obj o in
 664                     List.fold_right (
 665                       fun uri (acc,metasenv) ->
 666                         let metasenv',new_meta =
 667                            CicMkImplicit.mk_implicit metasenv subst context
 668                         in
 669                         let irl =
 670                           CicMkImplicit.identity_relocation_list_for_metavariable
 671                             context
 672                         in
 673                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 674                     ) uris ([],metasenv)
 675                  in
 676                  let ty =
 677                   match left_args,right_args with
 678                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 679                    | _,_ ->
 680                       let rec mk_right_args =
 681                        function
 682                           0 -> []
 683                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 684                       in
 685                       let right_args_no = List.length right_args in
 686                       let lifted_left_args =
 687                        List.map (CicSubstitution.lift right_args_no) left_args
 688                       in
 689                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 690                         (lifted_left_args @ mk_right_args right_args_no))
 691                  in
 692                  let fresh_name =
 693                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 694                      context Cic.Anonymous ~typ:ty
 695                  in
 696                  match outtypeinstances with
 697                  | [] ->
 698                      let extended_context =
 699                       let rec add_right_args =
 700                        function
 701                           Cic.Prod (name,ty,t) ->
 702                            Some (name,Cic.Decl ty)::(add_right_args t)
 703                         | _ -> []
 704                       in
 705                        (Some (fresh_name,Cic.Decl ty))::
 706                        (List.rev
 707                         (add_right_args arity_instantiated_with_left_args))@
 708                        context
 709                      in
 710                      let metasenv,new_meta =
 711                        CicMkImplicit.mk_implicit metasenv subst extended_context
 712                      in
 713                        let irl =
 714                        CicMkImplicit.identity_relocation_list_for_metavariable
 715                          extended_context
 716                      in
 717                      let rec add_lambdas b =
 718                       function
 719                          Cic.Prod (name,ty,t) ->
 720                           Cic.Lambda (name,ty,(add_lambdas b t))
 721                        | _ -> Cic.Lambda (fresh_name, ty, b)
 722                      in
 723                      let candidate =
 724                       add_lambdas (Cic.Meta (new_meta,irl))
 725                        arity_instantiated_with_left_args
 726                      in
 727                      (Some candidate),ugraph4,metasenv,subst
 728                  | (constructor_args_no,_,instance,_)::tl ->
 729                      try
 730                        let instance',subst,metasenv =
 731                          CicMetaSubst.delift_rels subst metasenv
 732                           constructor_args_no instance
 733                        in
 734                        let candidate,ugraph,metasenv,subst =
 735                          List.fold_left (
 736                            fun (candidate_oty,ugraph,metasenv,subst)
 737                              (constructor_args_no,_,instance,_) ->
 738                                match candidate_oty with
 739                                | None -> None,ugraph,metasenv,subst
 740                                | Some ty ->
 741                                  try
 742                                    let instance',subst,metasenv =
 743                                      CicMetaSubst.delift_rels subst metasenv
 744                                       constructor_args_no instance
 745                                    in
 746                                    let subst,metasenv,ugraph =
 747                                     fo_unif_subst subst context metasenv
 748                                       instance' ty ugraph
 749                                    in
 750                                     candidate_oty,ugraph,metasenv,subst
 751                                  with
 752                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 753                                   | RefineFailure _ | Uncertain _ ->
 754                                      None,ugraph,metasenv,subst
 755                          ) (Some instance',ugraph4,metasenv,subst) tl
 756                        in
 757                        match candidate with
 758                        | None -> None, ugraph,metasenv,subst
 759                        | Some t ->
 760                           let rec add_lambdas n b =
 761                            function
 762                               Cic.Prod (name,ty,t) ->
 763                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 764                             | _ ->
 765                               Cic.Lambda (fresh_name, ty,
 766                                CicSubstitution.lift (n + 1) t)
 767                           in
 768                            Some
 769                             (add_lambdas 0 t arity_instantiated_with_left_args),
 770                            ugraph,metasenv,subst
 771                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 772                        None,ugraph4,metasenv,subst
 773                in
 774                match candidate with
 775                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 776                | Some candidate ->
 777                    let subst,metasenv,ugraph =
 778                     try
 779                      fo_unif_subst subst context metasenv
 780                        candidate outtype ugraph5
 781                     with
 782                      exn -> assert false(* unification against a metavariable *)
 783                    in
 784                      C.MutCase (uri, i, outtype, term', pl'),
 785                       CicReduction.head_beta_reduce
 786                        (CicMetaSubst.apply_subst subst
 787                         (Cic.Appl (outtype::right_args@[term']))),
 788                      subst,metasenv,ugraph)
 789            | _ ->    (* easy case *)
 790              let tlbody_and_type,subst,metasenv,ugraph4 =
 791                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
 792              in
 793              let _,_,_,subst,metasenv,ugraph4 =
 794                eat_prods false subst metasenv context
 795                  outtype outtypety tlbody_and_type ugraph4
 796              in
 797              let _,_, subst, metasenv,ugraph5 =
 798                type_of_aux subst metasenv context
 799                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 800              in
 801              let (subst,metasenv,ugraph6) =
 802                List.fold_left2
 803                  (fun (subst,metasenv,ugraph)
 804                    p (constructor_args_no,context,instance,args)
 805                   ->
 806                     let instance' =
 807                       let appl =
 808                         let outtype' =
 809                           CicSubstitution.lift constructor_args_no outtype
 810                         in
 811                           C.Appl (outtype'::args)
 812                       in
 813                         CicReduction.head_beta_reduce ~delta:false
 814                           ~upto:(List.length args) appl
 815                     in
 816                      try
 817                       fo_unif_subst subst context metasenv instance instance'
 818                        ugraph
 819                      with
 820                       exn ->
 821                        enrich localization_tbl p exn
 822                         ~f:(function _ ->
 823                           lazy ("The term " ^
 824                            CicMetaSubst.ppterm_in_context ~metasenv subst p
 825                             context ^ " has type " ^
 826                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
 827                             context ^ " but is here used with type " ^
 828                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
 829                             context)))
 830                  (subst,metasenv,ugraph5) pl' outtypeinstances
 831              in
 832                C.MutCase (uri, i, outtype, term', pl'),
 833                  CicReduction.head_beta_reduce
 834                   (CicMetaSubst.apply_subst subst
 835                    (C.Appl(outtype::right_args@[term']))),
 836                  subst,metasenv,ugraph6)
 837         | C.Fix (i,fl) ->
 838             let fl_ty',subst,metasenv,types,ugraph1,len =
 839               List.fold_left
 840                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
 841                    let ty',_,subst',metasenv',ugraph1 =
 842                       type_of_aux subst metasenv context ty ugraph
 843                    in
 844                      fl @ [ty'],subst',metasenv',
 845                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
 846                         :: types, ugraph, len+1
 847                 ) ([],subst,metasenv,[],ugraph,0) fl
 848             in
 849             let context' = types@context in
 850             let fl_bo',subst,metasenv,ugraph2 =
 851               List.fold_left
 852                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 853                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 854                      type_of_aux subst metasenv context' bo ugraph in
 855                    let expected_ty = CicSubstitution.lift len ty in
 856                    let subst',metasenv',ugraph' =
 857                     try
 858                      fo_unif_subst subst context' metasenv
 859                        ty_of_bo expected_ty ugraph1
 860                     with
 861                      exn ->
 862                       enrich localization_tbl bo exn
 863                        ~f:(function _ ->
 864                          lazy ("The term " ^
 865                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 866                            context' ^ " has type " ^
 867                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 868                            context' ^ " but is here used with type " ^
 869                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 870                            context'))
 871                    in
 872                      fl @ [bo'] , subst',metasenv',ugraph'
 873                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 874             in
 875             let ty = List.nth fl_ty' i in
 876             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 877              * and we want the new fl with bo' and ty' injected in the right
 878              * place.
 879              *)
 880             let rec map3 f l1 l2 l3 =
 881               match l1,l2,l3 with
 882               | [],[],[] -> []
 883               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 884               | _ -> assert false
 885             in
 886             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 887               fl_ty' fl_bo' fl
 888             in
 889               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 890         | C.CoFix (i,fl) ->
 891             let fl_ty',subst,metasenv,types,ugraph1,len =
 892               List.fold_left
 893                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
 894                    let ty',_,subst',metasenv',ugraph1 =
 895                      type_of_aux subst metasenv context ty ugraph
 896                    in
 897                      fl @ [ty'],subst',metasenv',
 898                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
 899                         types, ugraph1, len+1
 900                 ) ([],subst,metasenv,[],ugraph,0) fl
 901             in
 902             let context' = types@context in
 903             let fl_bo',subst,metasenv,ugraph2 =
 904               List.fold_left
 905                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 906                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 907                      type_of_aux subst metasenv context' bo ugraph in
 908                    let expected_ty = CicSubstitution.lift len ty in
 909                    let subst',metasenv',ugraph' =
 910                     try
 911                      fo_unif_subst subst context' metasenv
 912                        ty_of_bo expected_ty ugraph1
 913                     with
 914                      exn ->
 915                       enrich localization_tbl bo exn
 916                        ~f:(function _ ->
 917                          lazy ("The term " ^
 918                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 919                            context' ^ " has type " ^
 920                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 921                            context' ^ " but is here used with type " ^
 922                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 923                            context))
 924                    in
 925                      fl @ [bo'],subst',metasenv',ugraph'
 926                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 927             in
 928             let ty = List.nth fl_ty' i in
 929             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 930              * and we want the new fl with bo' and ty' injected in the right
 931              * place.
 932              *)
 933             let rec map3 f l1 l2 l3 =
 934               match l1,l2,l3 with
 935               | [],[],[] -> []
 936               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 937               | _ -> assert false
 938             in
 939             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 940               fl_ty' fl_bo' fl
 941             in
 942               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 943      in
 944       relocalize localization_tbl t t';
 945       res
 946
 947   (* check_metasenv_consistency checks that the "canonical" context of a
 948      metavariable is consitent - up to relocation via the relocation list l -
 949      with the actual context *)
 950   and check_metasenv_consistency
 951     metano subst metasenv context canonical_context l ugraph
 952     =
 953     let module C = Cic in
 954     let module R = CicReduction in
 955     let module S = CicSubstitution in
 956     let lifted_canonical_context =
 957       let rec aux i =
 958         function
 959             [] -> []
 960           | (Some (n,C.Decl t))::tl ->
 961               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 962           | None::tl -> None::(aux (i+1) tl)
 963           | (Some (n,C.Def (t,ty)))::tl ->
 964               (Some
 965                (n,
 966                 C.Def
 967                  (S.subst_meta l (S.lift i t),
 968                   S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
 969       in
 970         aux 1 canonical_context
 971     in
 972       try
 973         List.fold_left2
 974           (fun (l,subst,metasenv,ugraph) t ct ->
 975              match (t,ct) with
 976                  _,None ->
 977                    l @ [None],subst,metasenv,ugraph
 978                | Some t,Some (_,C.Def (ct,_)) ->
 979                   (*CSC: the following optimization is to avoid a possibly
 980                          expensive reduction that can be easily avoided and
 981                          that is quite frequent. However, this is better
 982                          handled using levels to control reduction *)
 983                   let optimized_t =
 984                    match t with
 985                       Cic.Rel n ->
 986                        (try
 987                          match List.nth context (n - 1) with
 988                             Some (_,C.Def (te,_)) -> S.lift n te
 989                           | _ -> t
 990                         with
 991                          Failure _ -> t)
 992                     | _ -> t
 993                   in
 994                    let subst',metasenv',ugraph' =
 995                    (try
 996 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
 997  * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
 998                       fo_unif_subst subst context metasenv optimized_t ct ugraph
 999                     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 ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1000                    in
1001                      l @ [Some t],subst',metasenv',ugraph'
1002                | Some t,Some (_,C.Decl ct) ->
1003                    let t',inferredty,subst',metasenv',ugraph1 =
1004                      type_of_aux subst metasenv context t ugraph
1005                    in
1006                    let subst'',metasenv'',ugraph2 =
1007                      (try
1008                         fo_unif_subst
1009                           subst' context metasenv' inferredty ct ugraph1
1010                       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 metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1011                    in
1012                      l @ [Some t'], subst'',metasenv'',ugraph2
1013                | None, Some _  ->
1014                    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 ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
1015       with
1016           Invalid_argument _ ->
1017             raise
1018             (RefineFailure
1019                (lazy (sprintf
1020                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1021                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1022                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1023
1024   and check_exp_named_subst metasubst metasenv context tl ugraph =
1025     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
1026       match tl with
1027           [] -> [],metasubst,metasenv,ugraph
1028         | (uri,t)::tl ->
1029             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
1030             let typeofvar =
1031               CicSubstitution.subst_vars substs ty_uri in
1032               (* CSC: why was this code here? it is wrong
1033                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1034                  Cic.Variable (_,Some bo,_,_) ->
1035                  raise
1036                  (RefineFailure (lazy
1037                  "A variable with a body can not be explicit substituted"))
1038                  | Cic.Variable (_,None,_,_) -> ()
1039                  | _ ->
1040                  raise
1041                  (RefineFailure (lazy
1042                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1043                  ) ;
1044               *)
1045             let t',typeoft,metasubst',metasenv',ugraph2 =
1046               type_of_aux metasubst metasenv context t ugraph1 in
1047             let subst = uri,t' in
1048             let metasubst'',metasenv'',ugraph3 =
1049               try
1050                 fo_unif_subst
1051                   metasubst' context metasenv' typeoft typeofvar ugraph2
1052               with _ ->
1053                 raise (RefineFailure (lazy
1054                          ("Wrong Explicit Named Substitution: " ^
1055                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1056                           " not unifiable with " ^
1057                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1058             in
1059             (* FIXME: no mere tail recursive! *)
1060             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1061               check_exp_named_subst_aux
1062                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1063             in
1064               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1065     in
1066       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1067
1068
1069   and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1070    ugraph
1071   =
1072     let module C = Cic in
1073     let context_for_t2 = (Some (name,C.Decl s))::context in
1074     let t1'' = CicReduction.whd ~subst context t1 in
1075     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1076       match (t1'', t2'') with
1077         | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1078               (* different than Coq manual!!! *)
1079               C.Sort s2,subst,metasenv,ugraph
1080         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1081             let t' = CicUniv.fresh() in
1082              (try
1083               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1084               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1085                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1086               with
1087                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1088         | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1089             let t' = CicUniv.fresh() in
1090              (try
1091               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1092               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1093                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1094               with
1095                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1096         | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1097             let t' = CicUniv.fresh() in
1098              (try
1099               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1100               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1101                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1102               with
1103                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1104         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1105             let t' = CicUniv.fresh() in
1106              (try
1107               let ugraph1 = CicUniv.add_gt t' t1 ugraph in
1108               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1109                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1110               with
1111                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1112         | (C.Sort _,C.Sort (C.Type t1)) ->
1113             C.Sort (C.Type t1),subst,metasenv,ugraph
1114         | (C.Sort _,C.Sort (C.CProp t1)) ->
1115             C.Sort (C.CProp t1),subst,metasenv,ugraph
1116         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1117         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1118             (* TODO how can we force the meta to become a sort? If we don't we
1119              * break the invariant that refine produce only well typed terms *)
1120             (* TODO if we check the non meta term and if it is a sort then we
1121              * are likely to know the exact value of the result e.g. if the rhs
1122              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1123             let (metasenv,idx) =
1124               CicMkImplicit.mk_implicit_sort metasenv subst in
1125             let (subst, metasenv,ugraph1) =
1126              try
1127               fo_unif_subst subst context_for_t2 metasenv
1128                 (C.Meta (idx,[])) t2'' ugraph
1129              with _ -> assert false (* unification against a metavariable *)
1130             in
1131               t2'',subst,metasenv,ugraph1
1132         | (C.Sort _,_)
1133         | (C.Meta _,_) ->
1134             enrich localization_tbl s
1135              (RefineFailure
1136                (lazy
1137                  (sprintf
1138                    "%s is supposed to be a type, but its type is %s"
1139                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1140                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1141         | _,_ ->
1142             enrich localization_tbl t
1143              (RefineFailure
1144                (lazy
1145                  (sprintf
1146                    "%s is supposed to be a type, but its type is %s"
1147                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1148                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1149
1150   and avoid_double_coercion context subst metasenv ugraph t ty =
1151    if not !pack_coercions then
1152     t,ty,subst,metasenv,ugraph
1153    else
1154     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1155     if b then
1156       let source_carr = CoercGraph.source_of c2 in
1157       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1158       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1159       with
1160       | CoercGraph.SomeCoercion candidates ->
1161          let selected =
1162            HExtlib.list_findopt
1163              (function (metasenv,last,c) ->
1164                match c with
1165                | c when not (CoercGraph.is_composite c) ->
1166                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1167                    None
1168                | c ->
1169                let subst,metasenv,ugraph =
1170                 fo_unif_subst subst context metasenv last head ugraph in
1171                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1172                (try
1173                  debug_print
1174                    (lazy
1175                      ("packing: " ^
1176                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1177                  let newt,_,subst,metasenv,ugraph =
1178                    type_of_aux subst metasenv context c ugraph in
1179                  debug_print (lazy "tipa...");
1180                  let subst, metasenv, ugraph =
1181                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1182                     fo_unif_subst subst context metasenv newt t ugraph
1183                  in
1184                  debug_print (lazy "unifica...");
1185                  Some (newt, ty, subst, metasenv, ugraph)
1186                with
1187                | RefineFailure s | Uncertain s when not !pack_coercions->
1188                    debug_print s; debug_print (lazy "stop\n");None
1189                | RefineFailure s | Uncertain s ->
1190                    debug_print s;debug_print (lazy "goon\n");
1191                    try
1192                      let old_pack_coercions = !pack_coercions in
1193                      pack_coercions := false; (* to avoid diverging *)
1194                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1195                        type_of_aux subst metasenv context c1_c2_implicit ugraph
1196                      in
1197                      pack_coercions := old_pack_coercions;
1198                      let b, _, _, _, _ =
1199                        is_a_double_coercion refined_c1_c2_implicit
1200                      in
1201                      if b then
1202                        None
1203                      else
1204                        let head' =
1205                          match refined_c1_c2_implicit with
1206                          | Cic.Appl l -> HExtlib.list_last l
1207                          | _ -> assert false
1208                        in
1209                        let subst, metasenv, ugraph =
1210                         try fo_unif_subst subst context metasenv
1211                           head head' ugraph
1212                         with RefineFailure s| Uncertain s->
1213                           debug_print s;assert false
1214                        in
1215                        let subst, metasenv, ugraph =
1216                          fo_unif_subst subst context metasenv
1217                           refined_c1_c2_implicit t ugraph
1218                        in
1219                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1220                    with
1221                    | RefineFailure s | Uncertain s ->
1222                        pack_coercions := true;debug_print s;None
1223                    | exn -> pack_coercions := true; raise exn))
1224              candidates
1225          in
1226          (match selected with
1227          | Some x -> x
1228          | None ->
1229               debug_print
1230                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1231               t, ty, subst, metasenv, ugraph)
1232       | _ -> t, ty, subst, metasenv, ugraph)
1233     else
1234       t, ty, subst, metasenv, ugraph
1235
1236   and typeof_list subst metasenv context ugraph l =
1237     let tlbody_and_type,subst,metasenv,ugraph =
1238       List.fold_right
1239         (fun x (res,subst,metasenv,ugraph) ->
1240            let x',ty,subst',metasenv',ugraph1 =
1241              type_of_aux subst metasenv context x ugraph
1242            in
1243             (x', ty)::res,subst',metasenv',ugraph1
1244         ) l ([],subst,metasenv,ugraph)
1245     in
1246       tlbody_and_type,subst,metasenv,ugraph
1247
1248   and eat_prods
1249     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1250   =
1251     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1252     let fix_arity n metasenv context subst he hetype ugraph =
1253       let hetype = CicMetaSubst.apply_subst subst hetype in
1254       let src = CoercDb.coerc_carr_of_term hetype 0 in
1255       let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
1256       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1257       | CoercGraph.NoCoercion -> []
1258       | CoercGraph.NotHandled ->
1259          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1260       | CoercGraph.SomeCoercionToTgt candidates
1261       | CoercGraph.SomeCoercion candidates ->
1262           HExtlib.filter_map
1263             (fun (metasenv,last,coerc) ->
1264               let pp t =
1265                 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1266               try
1267                let subst,metasenv,ugraph =
1268                 fo_unif_subst subst context metasenv last he ugraph in
1269                 debug_print (lazy ("New head: "^ pp coerc));
1270                 let tty,ugraph =
1271                  CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1272                   ugraph
1273                 in
1274                  debug_print (lazy (" has type: "^ pp tty));
1275                  Some (coerc,tty,subst,metasenv,ugraph)
1276               with
1277               | Uncertain _ | RefineFailure _
1278               | HExtlib.Localized (_,Uncertain _)
1279               | HExtlib.Localized (_,RefineFailure _) -> None
1280               | exn -> assert false)
1281             candidates
1282     in
1283     (* aux function to process the type of the head and the args in parallel *)
1284     let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1285       function
1286       | [] -> newargs,subst,metasenv,he,hetype,ugraph
1287       | (hete, hety)::tl as args ->
1288           match (CicReduction.whd ~subst context hetype) with
1289           | Cic.Prod (n,s,t) ->
1290               let arg,subst,metasenv,ugraph =
1291                 coerce_to_something allow_coercions localization_tbl
1292                   hete hety s subst metasenv context ugraph in
1293               eat_prods_and_args
1294                 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1295                 ugraph (newargs@[arg]) tl
1296           | _ ->
1297               let he =
1298                 match he, newargs with
1299                 | _, [] -> he
1300                 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1301                 | _ -> Cic.Appl (he::List.map fst newargs)
1302               in
1303               (*{{{*) debug_print (lazy
1304                let pp x =
1305                 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1306                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1307                "\n but is applyed to: " ^ String.concat ";"
1308                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1309               let possible_fixes =
1310                fix_arity (List.length args) metasenv context subst he hetype
1311                 ugraph in
1312               match
1313                 HExtlib.list_findopt
1314                  (fun (he,hetype,subst,metasenv,ugraph) ->
1315                    (* {{{ *)debug_print (lazy ("Try fix: "^
1316                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1317                    debug_print (lazy (" of type: "^
1318                     CicMetaSubst.ppterm_in_context
1319                     ~metasenv subst hetype context)); (* }}} *)
1320                    try
1321                     Some (eat_prods_and_args
1322                       metasenv subst context he hetype ugraph [] args)
1323                    with
1324                     | RefineFailure _ | Uncertain _
1325                     | HExtlib.Localized (_,RefineFailure _)
1326                     | HExtlib.Localized (_,Uncertain _) -> None)
1327                 possible_fixes
1328               with
1329               | Some x -> x
1330               | None ->
1331                  raise
1332                   (MoreArgsThanExpected
1333                     (List.length args, RefineFailure (lazy "")))
1334     in
1335     (* first we check if we are in the simple case of a meta closed term *)
1336     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1337      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1338       (* this optimization is to postpone fix_arity (the most common case)*)
1339       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1340      else
1341        (* this (says CSC) is also useful to infer dependent types *)
1342         let pristinemenv = metasenv in
1343         let metasenv,hetype' =
1344           mk_prod_of_metas metasenv context subst args_bo_and_ty
1345         in
1346         try
1347           let subst,metasenv,ugraph =
1348            fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1349           in
1350           subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1351         with RefineFailure _ | Uncertain _ ->
1352           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1353     in
1354     let coerced_args,subst,metasenv,he,t,ugraph =
1355      try
1356       eat_prods_and_args
1357         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1358      with
1359       MoreArgsThanExpected (residuals,exn) ->
1360         more_args_than_expected localization_tbl metasenv
1361          subst he context hetype' residuals args_bo_and_ty exn
1362     in
1363     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1364
1365   and coerce_to_something
1366     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1367   =
1368     let module CS = CicSubstitution in
1369     let module CR = CicReduction in
1370     let cs_subst = CS.subst ~avoid_beta_redexes:true in
1371     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1372       debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1373       let coer =
1374         CoercGraph.look_for_coercion metasenv subst context infty expty
1375       in
1376       match coer with
1377       | CoercGraph.NoCoercion
1378       | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1379           "coerce_atom_to_something fails since no coercions found"))
1380       | CoercGraph.NotHandled when
1381           not (CicUtil.is_meta_closed infty) ||
1382           not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1383           "coerce_atom_to_something fails since carriers have metas"))
1384       | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1385           "coerce_atom_to_something fails since no coercions found"))
1386       | CoercGraph.SomeCoercion candidates ->
1387           debug_print (lazy (string_of_int (List.length candidates) ^
1388             " candidates found"));
1389           let uncertain = ref false in
1390           let selected =
1391             let posibilities =
1392               HExtlib.filter_map
1393               (fun (metasenv,last,c) ->
1394                try
1395                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1396                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1397                 " <==> " ^
1398                 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1399                 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1400                 context));
1401                 debug_print (lazy ("FO_UNIF_SUBST: " ^
1402                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1403                 let subst,metasenv,ugraph =
1404                  fo_unif_subst subst context metasenv last t ugraph
1405                 in
1406                 let newt,newhety,subst,metasenv,ugraph =
1407                  type_of_aux subst metasenv context c ugraph in
1408                 let newt, newty, subst, metasenv, ugraph =
1409                  avoid_double_coercion context subst metasenv ugraph newt expty
1410                 in
1411                 let subst,metasenv,ugraph =
1412                   fo_unif_subst subst context metasenv newhety expty ugraph in
1413                  Some ((newt,newty), subst, metasenv, ugraph)
1414                with
1415                | Uncertain _ -> uncertain := true; None
1416                | RefineFailure _ -> None)
1417               candidates
1418             in
1419             match
1420               List.fast_sort
1421                 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1422                 posibilities
1423             with
1424             | [] -> None
1425             | x::_ -> Some x
1426           in
1427           match selected with
1428           | Some x -> x
1429           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1430           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1431     in
1432     let rec coerce_to_something_aux
1433       t infty expty subst metasenv context ugraph
1434     =
1435       try
1436         let subst, metasenv, ugraph =
1437           fo_unif_subst subst context metasenv infty expty ugraph
1438         in
1439         (t, expty), subst, metasenv, ugraph
1440       with (Uncertain _ | RefineFailure _ as exn)
1441         when allow_coercions && !insert_coercions ->
1442           let whd = CicReduction.whd ~delta:false in
1443           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1444           let infty = clean infty subst context in
1445           let expty = clean expty subst context in
1446           let t = clean t subst context in
1447           (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1448           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1449           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1450           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1451           let (coerced,_),subst,metasenv,_ as result =
1452            match infty, expty, t with
1453            | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1454               (*{{{*) debug_print (lazy "FIX");
1455               (match fl with
1456                   [name,i,_(* infty *),bo] ->
1457                     let context_bo =
1458                      Some (Cic.Name name,Cic.Decl expty)::context in
1459                     let (rel1, _), subst, metasenv, ugraph =
1460                      coerce_to_something_aux (Cic.Rel 1)
1461                        (CS.lift 1 expty) (CS.lift 1 infty) subst
1462                       metasenv context_bo ugraph in
1463                     let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1464                     let (bo,_), subst, metasenv, ugraph =
1465                      coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1466                      expty) subst
1467                       metasenv context_bo ugraph
1468                     in
1469                      (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1470                 | _ -> assert false (* not implemented yet *)) (*}}}*)
1471            | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1472                (*{{{*) debug_print (lazy "CASE");
1473                (* {{{ helper functions *)
1474                let get_cl_and_left_p uri tyno outty ugraph =
1475                  match CicEnvironment.get_obj ugraph uri with
1476                  | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1477                      let count_pis t =
1478                        let rec aux ctx t =
1479                          match CicReduction.whd ~delta:false ctx t with
1480                          | Cic.Prod (name,src,tgt) ->
1481                              let ctx = Some (name, Cic.Decl src) :: ctx in
1482                              1 + aux ctx tgt
1483                          | _ -> 0
1484                        in
1485                          aux [] t
1486                      in
1487                      let rec skip_lambda_delifting t n =
1488                        match t,n with
1489                        | _,0 -> t
1490                        | Cic.Lambda (_,_,t),n ->
1491                            skip_lambda_delifting
1492                              (CS.subst (Cic.Implicit None) t) (n - 1)
1493                        | _ -> assert false
1494                      in
1495                      let get_l_r_p n = function
1496                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1497                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1498                            HExtlib.split_nth n args
1499                        | _ -> assert false
1500                      in
1501                      let _, _, ty, cl = List.nth tl tyno in
1502                      let pis = count_pis ty in
1503                      let rno = pis - leftno in
1504                      let t = skip_lambda_delifting outty rno in
1505                      let left_p, _ = get_l_r_p leftno t in
1506                      let instantiale_with_left cl =
1507                        List.map
1508                          (fun ty ->
1509                            List.fold_left
1510                              (fun t p -> match t with
1511                                | Cic.Prod (_,_,t) ->
1512                                    cs_subst p t
1513                                | _-> assert false)
1514                              ty left_p)
1515                          cl
1516                      in
1517                      let cl = instantiale_with_left (List.map snd cl) in
1518                      cl, left_p, leftno, rno, ugraph
1519                  | _ -> raise exn
1520                in
1521                let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1522                  match t,n with
1523                  | _,0 ->
1524                    let rec mkr n = function
1525                      | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1526                    in
1527                    let bo =
1528                    CicReplace.replace_lifting
1529                      ~equality:(fun _ -> CicUtil.alpha_equivalence)
1530                      ~context:ctx
1531                      ~what:(matched::right_p)
1532                      ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1533                      ~where:bo
1534                    in
1535                    bo
1536                  | Cic.Lambda (name, src, tgt),_ ->
1537                      Cic.Lambda (name, src,
1538                       keep_lambdas_and_put_expty
1539                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1540                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1541                  | _ -> assert false
1542                in
1543                let eq_uri, eq, eq_refl =
1544                  match LibraryObjects.eq_URI () with
1545                  | None -> HLog.warn "no default equality"; raise exn
1546                  | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1547                in
1548                let add_params
1549                  metasenv subst context uri tyno cty outty mty m leftno i
1550                =
1551                  let rec aux context outty par k mty m = function
1552                    | Cic.Prod (name, src, tgt) ->
1553                        let t,k =
1554                          aux
1555                            (Some (name, Cic.Decl src) :: context)
1556                            (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1557                            (CS.lift 1 mty) (CS.lift 1 m) tgt
1558                        in
1559                        Cic.Prod (name, src, t), k
1560                    | Cic.MutInd _ ->
1561                        let k =
1562                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1563                          if par <> [] then Cic.Appl (k::par) else k
1564                        in
1565                        Cic.Prod (Cic.Name "p",
1566                         Cic.Appl [eq; mty; m; k],
1567                         (CS.lift 1
1568                          (CR.head_beta_reduce ~delta:false
1569                           (Cic.Appl [outty;k])))),k
1570                    | Cic.Appl (Cic.MutInd _::pl) ->
1571                        let left_p,right_p = HExtlib.split_nth leftno pl in
1572                        let has_rights = right_p <> [] in
1573                        let k =
1574                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1575                          Cic.Appl (k::left_p@par)
1576                        in
1577                        let right_p =
1578                          try match
1579                            CicTypeChecker.type_of_aux' ~subst metasenv context k
1580                              CicUniv.oblivion_ugraph
1581                          with
1582                          | Cic.Appl (Cic.MutInd _::args),_ ->
1583                              snd (HExtlib.split_nth leftno args)
1584                          | _ -> assert false
1585                          with CicTypeChecker.TypeCheckerFailure _-> assert false
1586                        in
1587                        if has_rights then
1588                          CR.head_beta_reduce ~delta:false
1589                            (Cic.Appl (outty ::right_p @ [k])),k
1590                        else
1591                          Cic.Prod (Cic.Name "p",
1592                           Cic.Appl [eq; mty; m; k],
1593                           (CS.lift 1
1594                            (CR.head_beta_reduce ~delta:false
1595                             (Cic.Appl (outty ::right_p @ [k]))))),k
1596                    | _ -> assert false
1597                  in
1598                    aux context outty [] 1 mty m cty
1599                in
1600                let add_lambda_for_refl_m pbo rno mty m k cty =
1601                  (* k lives in the right context *)
1602                  if rno <> 0 then pbo else
1603                  let rec aux mty m = function
1604                    | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1605                       Cic.Lambda (name,src,
1606                        (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1607                    | t,_ ->
1608                        Cic.Lambda (Cic.Name "p",
1609                          Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1610                  in
1611                  aux mty m (pbo,cty)
1612                in
1613                let add_pi_for_refl_m new_outty mty m rno =
1614                  if rno <> 0 then new_outty else
1615                    let rec aux m mty = function
1616                      | Cic.Lambda (name, src, tgt) ->
1617                          Cic.Lambda (name, src,
1618                            aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1619                      | t ->
1620                          Cic.Prod
1621                            (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1622                            CS.lift 1 t)
1623                    in
1624                      aux m mty new_outty
1625                in (* }}} end helper functions *)
1626                (* constructors types with left params already instantiated *)
1627                let outty = CicMetaSubst.apply_subst subst outty in
1628                let cl, left_p, leftno,rno,ugraph =
1629                  get_cl_and_left_p uri tyno outty ugraph
1630                in
1631                let right_p, mty =
1632                  try
1633                    match
1634                      CicTypeChecker.type_of_aux' ~subst metasenv context m
1635                        CicUniv.oblivion_ugraph
1636                    with
1637                    | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
1638                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
1639                        snd (HExtlib.split_nth leftno args), mty
1640                    | _ -> assert false
1641                  with CicTypeChecker.TypeCheckerFailure _ ->
1642                     raise (AssertFailure(lazy "already ill-typed matched term"))
1643                in
1644                let new_outty =
1645                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1646                in
1647                debug_print
1648                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1649                   ~metasenv subst new_outty context));
1650                let _,pl,subst,metasenv,ugraph =
1651                  List.fold_right2
1652                    (fun cty pbo (i, acc, s, menv, ugraph) ->
1653                      (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1654                       *   (new_)outty right_par (K_i left_par k_par) *)
1655                       let infty_pbo, _ =
1656                         add_params menv s context uri tyno
1657                           cty outty mty m leftno i in
1658                       debug_print
1659                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1660                         ~metasenv subst infty_pbo context));
1661                       let expty_pbo, k = (* k is (K_i left_par k_par) *)
1662                         add_params menv s context uri tyno
1663                           cty new_outty mty m leftno i in
1664                       debug_print
1665                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1666                         ~metasenv subst expty_pbo context));
1667                       let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1668                       debug_print
1669                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1670                         ~metasenv subst pbo context));
1671                       let (pbo, _), subst, metasenv, ugraph =
1672                         coerce_to_something_aux pbo infty_pbo expty_pbo
1673                           s menv context ugraph
1674                       in
1675                       debug_print
1676                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1677                         ~metasenv subst pbo context));
1678                       (i-1, pbo::acc, subst, metasenv, ugraph))
1679                    cl pl (List.length pl, [], subst, metasenv, ugraph)
1680                in
1681                let new_outty = add_pi_for_refl_m new_outty mty m rno in
1682                debug_print
1683                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1684                   ~metasenv subst new_outty context));
1685                let t =
1686                  if rno = 0 then
1687                    let refl_m=Cic.Appl[eq_refl;mty;m]in
1688                    Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1689                  else
1690                    Cic.MutCase(uri,tyno,new_outty,m,pl)
1691                in
1692                (t, expty), subst, metasenv, ugraph (*}}}*)
1693            | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1694                (*{{{*) debug_print (lazy "LAM");
1695                let name_con =
1696                  FreshNamesGenerator.mk_fresh_name
1697                    ~subst metasenv context ~typ:src2 Cic.Anonymous
1698                in
1699                let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1700                (* contravariant part: the argument of f:src->ty *)
1701                let (rel1, _), subst, metasenv, ugraph =
1702                  coerce_to_something_aux
1703                   (Cic.Rel 1) (CS.lift 1 src2)
1704                   (CS.lift 1 src) subst metasenv context_src2 ugraph
1705                in
1706                (* covariant part: the result of f(c x); x:src2; (c x):src *)
1707                let name_t, bo =
1708                  match t with
1709                  | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1710                  | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1711                in
1712                (* we fix the possible dependency problem in the source ty *)
1713                let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1714                let (bo, _), subst, metasenv, ugraph =
1715                  coerce_to_something_aux
1716                    bo ty ty2 subst metasenv context_src2 ugraph
1717                in
1718                let coerced = Cic.Lambda (name_t,src2, bo) in
1719                (coerced, expty), subst, metasenv, ugraph (*}}}*)
1720            | _ ->
1721                (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1722                 ~metasenv subst infty context ^ " ==> " ^
1723                 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1724                coerce_atom_to_something
1725                t infty expty subst metasenv context ugraph (*}}}*)
1726           in
1727           debug_print (lazy ("COERCE TO SOMETHING END: "^
1728             CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1729           result
1730     in
1731     try
1732       coerce_to_something_aux t infty expty subst metasenv context ugraph
1733     with Uncertain _ | RefineFailure _ as exn ->
1734       let f _ =
1735         lazy ("The term " ^
1736           CicMetaSubst.ppterm_in_context metasenv subst t context ^
1737           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1738           infty context ^ " but is here used with type " ^
1739           CicMetaSubst.ppterm_in_context metasenv subst expty context)
1740       in
1741         enrich localization_tbl ~f t exn
1742
1743   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1744     match CicReduction.whd ~delta:false ~subst context infty with
1745     | Cic.Meta _ | Cic.Sort _ ->
1746         t,infty, subst, metasenv, ugraph
1747     | src ->
1748        debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1749          ~metasenv subst src context));
1750        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1751        try
1752          let (t, ty_t), subst, metasenv, ugraph =
1753            coerce_to_something true
1754              localization_tbl t src tgt subst metasenv context ugraph
1755          in
1756          debug_print (lazy ("COERCE TO SORT END: "^
1757            CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1758          t, ty_t, subst, metasenv, ugraph
1759        with HExtlib.Localized (_, exn) ->
1760          let f _ =
1761            lazy ("(7)The term " ^
1762             CicMetaSubst.ppterm_in_context ~metasenv subst t context
1763             ^ " is not a type since it has type " ^
1764             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1765             ^ " that is not a sort")
1766          in
1767            enrich localization_tbl ~f t exn
1768   in
1769
1770   (* eat prods ends here! *)
1771
1772   let t',ty,subst',metasenv',ugraph1 =
1773    type_of_aux [] metasenv context t ugraph
1774   in
1775   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1776   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1777     (* Andrea: ho rimesso qui l'applicazione della subst al
1778        metasenv dopo che ho droppato l'invariante che il metsaenv
1779        e' sempre istanziato *)
1780   let substituted_metasenv =
1781     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1782     (* metasenv' *)
1783     (*  substituted_t,substituted_ty,substituted_metasenv *)
1784     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1785   let cleaned_t =
1786    if clean_dummy_dependent_types then
1787     FreshNamesGenerator.clean_dummy_dependent_types substituted_t
1788    else substituted_t in
1789   let cleaned_ty =
1790    if clean_dummy_dependent_types then
1791     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
1792    else substituted_ty in
1793   let cleaned_metasenv =
1794    if clean_dummy_dependent_types then
1795     List.map
1796       (function (n,context,ty) ->
1797          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1798          let context' =
1799            List.map
1800              (function
1801                   None -> None
1802                 | Some (n, Cic.Decl t) ->
1803                     Some (n,
1804                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1805                 | Some (n, Cic.Def (bo,ty)) ->
1806                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1807                     let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
1808                     in
1809                       Some (n, Cic.Def (bo',ty'))
1810              ) context
1811          in
1812            (n,context',ty')
1813       ) substituted_metasenv
1814    else
1815     substituted_metasenv
1816   in
1817     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1818 ;;
1819
1820 let undebrujin uri typesno tys t =
1821   snd
1822    (List.fold_right
1823      (fun (name,_,_,_) (i,t) ->
1824        (* here the explicit_named_substituion is assumed to be *)
1825        (* of length 0 *)
1826        let t' = Cic.MutInd (uri,i,[])  in
1827        let t = CicSubstitution.subst t' t in
1828         i - 1,t
1829      ) tys (typesno - 1,t))
1830
1831 let map_first_n n start f g l =
1832   let rec aux acc k l =
1833     if k < n then
1834       match l with
1835       | [] -> raise (Invalid_argument "map_first_n")
1836       | hd :: tl -> f hd k (aux acc (k+1) tl)
1837     else
1838       g acc l
1839   in
1840   aux start 0 l
1841
1842 (*CSC: this is a very rough approximation; to be finished *)
1843 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1844   let subst,metasenv,ugraph,tys =
1845     List.fold_right
1846       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1847         let subst,metasenv,ugraph,cl =
1848           List.fold_right
1849             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1850                let rec aux ctx k subst = function
1851                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1852                      let subst,metasenv,ugraph,tl =
1853                        map_first_n leftno
1854                          (subst,metasenv,ugraph,[])
1855                          (fun t n (subst,metasenv,ugraph,acc) ->
1856                            let subst,metasenv,ugraph =
1857                              fo_unif_subst
1858                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1859                            in
1860                            subst,metasenv,ugraph,(t::acc))
1861                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1862                          tl
1863                      in
1864                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1865                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1866                      subst,metasenv,ugraph,t
1867                  | Cic.Prod (name,s,t) ->
1868                      let ctx = (Some (name,Cic.Decl s))::ctx in
1869                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1870                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1871                  | _ ->
1872                      raise
1873                       (RefineFailure
1874                         (lazy "not well formed constructor type"))
1875                in
1876                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1877                subst,metasenv,ugraph,(name,ty) :: acc)
1878           cl (subst,metasenv,ugraph,[])
1879         in
1880         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1881       tys ([],metasenv,ugraph,[])
1882   in
1883   let substituted_tys =
1884     List.map
1885       (fun (name,ind,arity,cl) ->
1886         let cl =
1887           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1888         in
1889         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1890       tys
1891   in
1892   metasenv,ugraph,substituted_tys
1893
1894 let typecheck metasenv uri obj ~localization_tbl =
1895  let ugraph = CicUniv.oblivion_ugraph in
1896  match obj with
1897     Cic.Constant (name,Some bo,ty,args,attrs) ->
1898      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
1899         since type_of_aux' destroys localization information (which are
1900         preserved by type_of_aux *)
1901      let loc exn' =
1902       try
1903        Cic.CicHash.find localization_tbl bo
1904       with Not_found ->
1905        HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
1906        raise exn' in
1907      let bo',boty,metasenv,ugraph =
1908       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1909      let ty',_,metasenv,ugraph =
1910       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1911      let subst,metasenv,ugraph =
1912       try
1913        fo_unif_subst [] [] metasenv boty ty' ugraph
1914       with
1915          RefineFailure _
1916        | Uncertain _ as exn ->
1917           let msg =
1918             lazy ("The term " ^
1919              CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
1920              " has type " ^
1921              CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
1922              " but is here used with type " ^
1923              CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
1924           in
1925            let exn' =
1926             match exn with
1927                RefineFailure _ -> RefineFailure msg
1928              | Uncertain _ -> Uncertain msg
1929              | _ -> assert false
1930            in
1931             raise (HExtlib.Localized (loc exn',exn'))
1932      in
1933      let bo' = CicMetaSubst.apply_subst subst bo' in
1934      let ty' = CicMetaSubst.apply_subst subst ty' in
1935      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1936       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1937   | Cic.Constant (name,None,ty,args,attrs) ->
1938      let ty',_,metasenv,ugraph =
1939       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1940      in
1941       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1942   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1943      assert (metasenv' = metasenv);
1944      (* Here we do not check the metasenv for correctness *)
1945      let bo',boty,metasenv,ugraph =
1946       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1947      let ty',sort,metasenv,ugraph =
1948       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1949      begin
1950       match sort with
1951          Cic.Sort _
1952        (* instead of raising Uncertain, let's hope that the meta will become
1953           a sort *)
1954        | Cic.Meta _ -> ()
1955        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1956      end;
1957      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1958      let bo' = CicMetaSubst.apply_subst subst bo' in
1959      let ty' = CicMetaSubst.apply_subst subst ty' in
1960      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1961       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1962   | Cic.Variable _ -> assert false (* not implemented *)
1963   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1964      (*CSC: this code is greately simplified and many many checks are missing *)
1965      (*CSC: e.g. the constructors are not required to build their own types,  *)
1966      (*CSC: the arities are not required to have as type a sort, etc.         *)
1967      let uri = match uri with Some uri -> uri | None -> assert false in
1968      let typesno = List.length tys in
1969      (* first phase: we fix only the types *)
1970      let metasenv,ugraph,tys =
1971       List.fold_right
1972        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1973          let ty',_,metasenv,ugraph =
1974           (* clean_dummy_dependent_types: false to avoid cleaning the names
1975              of the left products, that must be identical to those of the
1976              constructors; however, non-left products should probably be
1977              cleaned *)
1978           type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
1979            metasenv [] ty ugraph
1980          in
1981           metasenv,ugraph,(name,b,ty',cl)::res
1982        ) tys (metasenv,ugraph,[]) in
1983      let con_context =
1984       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1985      (* second phase: we fix only the constructors *)
1986      let saved_menv = metasenv in
1987      let metasenv,ugraph,tys =
1988       List.fold_right
1989        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1990          let metasenv,ugraph,cl' =
1991           List.fold_right
1992            (fun (name,ty) (metasenv,ugraph,res) ->
1993              let ty =
1994               CicTypeChecker.debrujin_constructor
1995               ~cb:(relocalize localization_tbl) uri typesno [] ty in
1996              let ty',_,metasenv,ugraph =
1997               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1998              let ty' = undebrujin uri typesno tys ty' in
1999               metasenv@saved_menv,ugraph,(name,ty')::res
2000            ) cl (metasenv,ugraph,[])
2001          in
2002           metasenv,ugraph,(name,b,ty,cl')::res
2003        ) tys (metasenv,ugraph,[]) in
2004      (* third phase: we check the positivity condition *)
2005      let metasenv,ugraph,tys =
2006        are_all_occurrences_positive metasenv ugraph uri tys paramsno
2007      in
2008      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2009 ;;
2010
2011 (* sara' piu' veloce che raffinare da zero? mah.... *)
2012 let pack_coercion metasenv ctx t =
2013  let module C = Cic in
2014  let rec merge_coercions ctx =
2015    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2016    function
2017    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2018    | C.Meta (n,subst) ->
2019       let subst' =
2020        List.map
2021         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2022       in
2023        C.Meta (n,subst')
2024    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2025    | C.Prod (name,so,dest) ->
2026        let ctx' = (Some (name,C.Decl so))::ctx in
2027        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2028    | C.Lambda (name,so,dest) ->
2029        let ctx' = (Some (name,C.Decl so))::ctx in
2030        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2031    | C.LetIn (name,so,ty,dest) ->
2032        let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2033        C.LetIn
2034         (name, merge_coercions ctx so, merge_coercions ctx ty,
2035          merge_coercions ctx' dest)
2036    | C.Appl l ->
2037       let l = List.map (merge_coercions ctx) l in
2038       let t = C.Appl l in
2039        let b,_,_,_,_ = is_a_double_coercion t in
2040        if b then
2041          let ugraph = CicUniv.oblivion_ugraph in
2042          let old_insert_coercions = !insert_coercions in
2043          insert_coercions := false;
2044          let newt, _, menv, _ =
2045            try
2046              type_of_aux' metasenv ctx t ugraph
2047            with RefineFailure _ | Uncertain _ ->
2048              t, t, [], ugraph
2049          in
2050          insert_coercions := old_insert_coercions;
2051          if metasenv <> [] || menv = [] then
2052            newt
2053          else
2054            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2055        else
2056          t
2057    | C.Var (uri,exp_named_subst) ->
2058        let exp_named_subst = List.map aux exp_named_subst in
2059        C.Var (uri, exp_named_subst)
2060    | C.Const (uri,exp_named_subst) ->
2061        let exp_named_subst = List.map aux exp_named_subst in
2062        C.Const (uri, exp_named_subst)
2063    | C.MutInd (uri,tyno,exp_named_subst) ->
2064        let exp_named_subst = List.map aux exp_named_subst in
2065        C.MutInd (uri,tyno,exp_named_subst)
2066    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2067        let exp_named_subst = List.map aux exp_named_subst in
2068        C.MutConstruct (uri,tyno,consno,exp_named_subst)
2069    | C.MutCase (uri,tyno,out,te,pl) ->
2070        let pl = List.map (merge_coercions ctx) pl in
2071        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2072    | C.Fix (fno, fl) ->
2073        let ctx' =
2074          List.fold_left
2075            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2076            ctx fl
2077        in
2078        let fl =
2079          List.map
2080            (fun (name,idx,ty,bo) ->
2081              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2082          fl
2083        in
2084        C.Fix (fno, fl)
2085    | C.CoFix (fno, fl) ->
2086        let ctx' =
2087          List.fold_left
2088            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2089            ctx fl
2090        in
2091        let fl =
2092          List.map
2093            (fun (name,ty,bo) ->
2094              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2095          fl
2096        in
2097        C.CoFix (fno, fl)
2098  in
2099   merge_coercions ctx t
2100 ;;
2101
2102 let pack_coercion_metasenv conjectures = conjectures (*
2103
2104   TASSI: this code war written when coercions were a toy,
2105          now packing coercions involves unification thus
2106          the metasenv may change, and this pack coercion
2107          does not handle that.
2108
2109   let module C = Cic in
2110   List.map
2111     (fun (i, ctx, ty) ->
2112        let ctx =
2113          List.fold_right
2114            (fun item ctx ->
2115               let item' =
2116                 match item with
2117                     Some (name, C.Decl t) ->
2118                       Some (name, C.Decl (pack_coercion conjectures ctx t))
2119                   | Some (name, C.Def (t,None)) ->
2120                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
2121                   | Some (name, C.Def (t,Some ty)) ->
2122                       Some (name, C.Def (pack_coercion conjectures ctx t,
2123                                          Some (pack_coercion conjectures ctx ty)))
2124                   | None -> None
2125               in
2126                 item'::ctx
2127            ) ctx []
2128        in
2129          ((i,ctx,pack_coercion conjectures ctx ty))
2130     ) conjectures
2131     *)
2132 ;;
2133
2134 let pack_coercion_obj obj = obj (*
2135
2136   TASSI: this code war written when coercions were a toy,
2137          now packing coercions involves unification thus
2138          the metasenv may change, and this pack coercion
2139          does not handle that.
2140
2141   let module C = Cic in
2142   match obj with
2143   | C.Constant (id, body, ty, params, attrs) ->
2144       let body =
2145         match body with
2146         | None -> None
2147         | Some body -> Some (pack_coercion [] [] body)
2148       in
2149       let ty = pack_coercion [] [] ty in
2150         C.Constant (id, body, ty, params, attrs)
2151   | C.Variable (name, body, ty, params, attrs) ->
2152       let body =
2153         match body with
2154         | None -> None
2155         | Some body -> Some (pack_coercion [] [] body)
2156       in
2157       let ty = pack_coercion [] [] ty in
2158         C.Variable (name, body, ty, params, attrs)
2159   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2160       let conjectures = pack_coercion_metasenv conjectures in
2161       let body = pack_coercion conjectures [] body in
2162       let ty = pack_coercion conjectures [] ty in
2163       C.CurrentProof (name, conjectures, body, ty, params, attrs)
2164   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2165       let indtys =
2166         List.map
2167           (fun (name, ind, arity, cl) ->
2168             let arity = pack_coercion [] [] arity in
2169             let cl =
2170               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2171             in
2172             (name, ind, arity, cl))
2173           indtys
2174       in
2175         C.InductiveDefinition (indtys, params, leftno, attrs) *)
2176 ;;
2177
2178
2179 (* DEBUGGING ONLY
2180 let type_of_aux' metasenv context term =
2181  try
2182   let (t,ty,m) =
2183       type_of_aux' metasenv context term in
2184     debug_print (lazy
2185      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2186    debug_print (lazy
2187     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2188    (t,ty,m)
2189  with
2190  | RefineFailure msg as e ->
2191      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2192      raise e
2193  | Uncertain msg as e ->
2194      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2195      raise e
2196 ;; *)
2197
2198 let profiler2 = HExtlib.profile "CicRefine"
2199
2200 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2201  profiler2.HExtlib.profile
2202   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2203
2204 let typecheck ~localization_tbl metasenv uri obj =
2205  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2206
2207 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2208 (* vim:set foldmethod=marker: *)