components/cic_unification/cicRefine.ml

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