components/cic_unification/cicRefine.ml

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