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