helm/software/components/cic_unification/cicRefine.ml

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