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