helm/software/components/cic_unification/cicRefine.ml

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