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