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