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