components/cic_unification/cicRefine.ml

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