helm/software/components/cic_unification/cicRefine.ml

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