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.SomeCoercionToTgt _
 458                     | CoercGraph.NotHandled _ ->
 459                        enrich localization_tbl t
 460                         (RefineFailure
 461                           (lazy ("(4)The term " ^
 462                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
 463                           " is not a type since it has type " ^
 464                           CicMetaSubst.ppterm_in_context ~metasenv
 465                            subst coercion_src context ^ " that is not a sort")))
 466                     | CoercGraph.NotMetaClosed ->
 467                        enrich localization_tbl t
 468                         (Uncertain
 469                           (lazy ("(5)The term " ^
 470                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
 471                           " is not a type since it has type " ^
 472                           CicMetaSubst.ppterm_in_context ~metasenv
 473                            subst coercion_src context ^ " that is not a sort")))
 474                     | CoercGraph.SomeCoercion candidates ->
 475                         let selected =
 476                           HExtlib.list_findopt
 477                             (try_coercion t subst context ugraph coercion_tgt)
 478                             candidates
 479                         in
 480                         match selected with
 481                         | Some x -> x
 482                         | None ->
 483                             enrich localization_tbl t
 484                               (RefineFailure
 485                                 (lazy ("(6)The term " ^
 486                                 CicMetaSubst.ppterm_in_context ~metasenv
 487                                   subst t context ^
 488                                   " is not a type since it has type " ^
 489                                   CicMetaSubst.ppterm_in_context ~metasenv
 490                                   subst coercion_src context ^
 491                                   " that is not a sort"))))
 492             in
 493             let s',sort1,subst',metasenv',ugraph1 =
 494               type_of_aux subst metasenv context s ugraph
 495             in
 496             let s',sort1,subst', metasenv',ugraph1 =
 497               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 498               s' sort1 subst' context metasenv' ugraph1
 499             in
 500             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 501             let t',sort2,subst'',metasenv'',ugraph2 =
 502               type_of_aux subst' metasenv'
 503                 context_for_t t ugraph1
 504             in
 505             let t',sort2,subst'',metasenv'',ugraph2 =
 506               coerce_to_sort false (Cic.Type(CicUniv.fresh()))
 507               t' sort2 subst'' context_for_t metasenv'' ugraph2
 508             in
 509               let sop,subst''',metasenv''',ugraph3 =
 510                 sort_of_prod localization_tbl subst'' metasenv''
 511                   context (name,s') t' (sort1,sort2) ugraph2
 512               in
 513                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 514         | C.Lambda (n,s,t) ->
 515             let s',sort1,subst',metasenv',ugraph1 =
 516               type_of_aux subst metasenv context s ugraph in
 517             let s',sort1,subst',metasenv',ugraph1 =
 518               if not !insert_coercions then
 519                 s',sort1, subst', metasenv', ugraph1
 520               else
 521                 match CicReduction.whd ~subst:subst' context sort1 with
 522                   | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
 523                   | coercion_src ->
 524                      let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
 525                      let boh =
 526                       CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
 527                      in
 528                       match boh with
 529                       | CoercGraph.NoCoercion
 530                       | CoercGraph.SomeCoercionToTgt _
 531                       |  CoercGraph.NotHandled _ ->
 532                         enrich localization_tbl s'
 533                          (RefineFailure
 534                           (lazy ("(7)The term " ^
 535                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
 536                           " is not a type since it has type " ^
 537                           CicMetaSubst.ppterm_in_context ~metasenv
 538                            subst coercion_src context ^ " that is not a sort")))
 539                       | CoercGraph.NotMetaClosed ->
 540                         enrich localization_tbl s'
 541                          (Uncertain
 542                           (lazy ("(8)The term " ^
 543                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
 544                           " is not a type since it has type " ^
 545                           CicMetaSubst.ppterm_in_context ~metasenv
 546                            subst coercion_src context ^ " that is not a sort")))
 547                       | CoercGraph.SomeCoercion candidates ->
 548                         let selected =
 549                           HExtlib.list_findopt
 550                            (try_coercion s' subst' context ugraph1 coercion_tgt)
 551                            candidates
 552                         in
 553                         match selected with
 554                         | Some x -> x
 555                         | None ->
 556                            enrich localization_tbl s'
 557                             (RefineFailure
 558                              (lazy ("(9)The term " ^
 559                               CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^
 560                               " is not a type since it has type " ^
 561                               CicMetaSubst.ppterm_in_context ~metasenv
 562                               subst coercion_src context ^
 563                               " that is not a sort")))
 564             in
 565             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 566             let t',type2,subst'',metasenv'',ugraph2 =
 567               type_of_aux subst' metasenv' context_for_t t ugraph1
 568             in
 569               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 570                 subst'',metasenv'',ugraph2
 571         | C.LetIn (n,s,t) ->
 572             (* only to check if s is well-typed *)
 573             let s',ty,subst',metasenv',ugraph1 =
 574               type_of_aux subst metasenv context s ugraph
 575             in
 576            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 577
 578             let t',inferredty,subst'',metasenv'',ugraph2 =
 579               type_of_aux subst' metasenv'
 580                 context_for_t t ugraph1
 581             in
 582               (* One-step LetIn reduction.
 583                * Even faster than the previous solution.
 584                * Moreover the inferred type is closer to the expected one.
 585                *)
 586               C.LetIn (n,s',t'),
 587                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
 588                subst'',metasenv'',ugraph2
 589         | C.Appl (he::((_::_) as tl)) ->
 590             let he',hetype,subst',metasenv',ugraph1 =
 591               type_of_aux subst metasenv context he ugraph
 592             in
 593             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 594                typeof_list subst' metasenv' context ugraph1 tl
 595             in
 596             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
 597               eat_prods true subst'' metasenv'' context
 598                 he' hetype tlbody_and_type ugraph2
 599             in
 600             let newappl = (C.Appl (coerced_he::coerced_args)) in
 601             avoid_double_coercion
 602               context subst''' metasenv''' ugraph3 newappl applty
 603         | C.Appl _ -> assert false
 604         | C.Const (uri,exp_named_subst) ->
 605             let exp_named_subst',subst',metasenv',ugraph1 =
 606               check_exp_named_subst subst metasenv context
 607                 exp_named_subst ugraph in
 608             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 609             let cty =
 610               CicSubstitution.subst_vars exp_named_subst' ty_uri
 611             in
 612               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 613         | C.MutInd (uri,i,exp_named_subst) ->
 614             let exp_named_subst',subst',metasenv',ugraph1 =
 615               check_exp_named_subst subst metasenv context
 616                 exp_named_subst ugraph
 617             in
 618             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 619             let cty =
 620               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 621               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 622         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 623             let exp_named_subst',subst',metasenv',ugraph1 =
 624               check_exp_named_subst subst metasenv context
 625                 exp_named_subst ugraph
 626             in
 627             let ty_uri,ugraph2 =
 628               type_of_mutual_inductive_constr uri i j ugraph1
 629             in
 630             let cty =
 631               CicSubstitution.subst_vars exp_named_subst' ty_uri
 632             in
 633               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 634                 metasenv',ugraph2
 635         | C.MutCase (uri, i, outtype, term, pl) ->
 636             (* first, get the inductive type (and noparams)
 637              * in the environment  *)
 638             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 639               let _ = CicTypeChecker.typecheck uri in
 640               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 641               match obj with
 642                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 643                     List.nth l i , expl_params, parsno, u
 644                 | _ ->
 645                     enrich localization_tbl t
 646                      (RefineFailure
 647                        (lazy ("Unkown mutual inductive definition " ^
 648                          U.string_of_uri uri)))
 649            in
 650            let rec count_prod t =
 651              match CicReduction.whd ~subst context t with
 652                  C.Prod (_, _, t) -> 1 + (count_prod t)
 653                | _ -> 0
 654            in
 655            let no_args = count_prod arity in
 656              (* now, create a "generic" MutInd *)
 657            let metasenv,left_args =
 658              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 659            in
 660            let metasenv,right_args =
 661              let no_right_params = no_args - no_left_params in
 662                if no_right_params < 0 then assert false
 663                else CicMkImplicit.n_fresh_metas
 664                       metasenv subst context no_right_params
 665            in
 666            let metasenv,exp_named_subst =
 667              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 668            let expected_type =
 669              if no_args = 0 then
 670                C.MutInd (uri,i,exp_named_subst)
 671              else
 672                C.Appl
 673                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 674            in
 675              (* check consistency with the actual type of term *)
 676            let term',actual_type,subst,metasenv,ugraph1 =
 677              type_of_aux subst metasenv context term ugraph in
 678            let expected_type',_, subst, metasenv,ugraph2 =
 679              type_of_aux subst metasenv context expected_type ugraph1
 680            in
 681            let actual_type = CicReduction.whd ~subst context actual_type in
 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.SomeCoercionToTgt candidates
1369         | CoercGraph.SomeCoercion candidates ->
1370             match
1371             HExtlib.list_findopt
1372               (fun (metasenv,last,coerc) ->
1373                 let subst,metasenv,ugraph =
1374                  fo_unif_subst subst context metasenv last x ugraph in
1375                 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1376                 try
1377                   (* we want this to be available in the error handler fo the
1378                    * following (so it has its own try. *)
1379                   let t,tty,subst,metasenv,ugraph =
1380                     type_of_aux subst metasenv context coerc ugraph
1381                   in
1382                   try
1383                     let metasenv, hetype' =
1384                       mk_prod_of_metas metasenv context subst remainder
1385                     in
1386                     debug_print (lazy
1387                       ("  unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1388                        CicMetaSubst.ppterm ~metasenv subst hetype'));
1389                     let subst,metasenv,ugraph =
1390                       fo_unif_subst_eat_prods
1391                         subst context metasenv tty hetype' ugraph
1392                     in
1393                     debug_print (lazy " success!");
1394                     Some (subst,metasenv,ugraph,tty,t,remainder)
1395                   with
1396                   | Uncertain _ | RefineFailure _
1397                   | CicUnification.UnificationFailure _
1398                   | CicUnification.Uncertain _ ->
1399                       try
1400                         let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1401                           fix_arity
1402                             metasenv context subst t tty remainder ugraph
1403                         in
1404                         Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1405                       with Uncertain _ | RefineFailure _ -> None
1406                 with
1407                    Uncertain _
1408                  | RefineFailure _
1409                  | HExtlib.Localized (_,Uncertain _)
1410                  | HExtlib.Localized (_,RefineFailure _) -> None
1411                  | exn -> assert false) (* ritornare None, e' un localized *)
1412               candidates
1413            with
1414            | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1415                subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1416            | None ->
1417                more_args_than_expected localization_tbl metasenv
1418                  subst he context hetype args_bo_and_ty exn
1419       (* }}} end coercion to funclass stuff *)
1420       (* }}} end fix_arity *)
1421     in
1422     (* aux function to process the type of the head and the args in parallel *)
1423     let rec eat_prods_and_args
1424       pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1425     =
1426       (* {{{ body *)
1427       function
1428         | [] -> newargs,subst,metasenv,he,hetype,ugraph
1429         | (hete, hety)::tl ->
1430             match (CicReduction.whd ~subst context hetype) with
1431             | Cic.Prod (n,s,t) ->
1432                 let arg,subst,metasenv,ugraph1 =
1433                   try
1434                     let subst,metasenv,ugraph1 =
1435                       fo_unif_subst_eat_prods2
1436                         subst context metasenv hety s ugraph
1437                     in
1438                       (hete,hety),subst,metasenv,ugraph1
1439                   (* {{{ we search a coercion from hety to s if fails *)
1440                   with RefineFailure _ | Uncertain _ as exn
1441                   when allow_coercions && !insert_coercions ->
1442                     let coer, tgt_carr =
1443                       let carr t subst context =
1444                         CicReduction.whd ~delta:false
1445                           context (CicMetaSubst.apply_subst subst t )
1446                       in
1447                       let c_hety = carr hety subst context in
1448                       let c_s = carr s subst context in
1449                       CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
1450                     in
1451                     (match coer with
1452                     | CoercGraph.NoCoercion
1453                     | CoercGraph.SomeCoercionToTgt _
1454                     | CoercGraph.NotHandled _ ->
1455                         enrich localization_tbl hete exn
1456                          ~f:(fun _ ->
1457                            (lazy ("(15)The term " ^
1458                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
1459                               context ^ " has type " ^
1460                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
1461                               context ^ " but is here used with type " ^
1462                              CicMetaSubst.ppterm_in_context ~metasenv subst s context
1463                               (* "\nReason: " ^ Lazy.force e*))))
1464                     | CoercGraph.NotMetaClosed ->
1465                         enrich localization_tbl hete exn
1466                          ~f:(fun _ ->
1467                            (lazy ("(16)The term " ^
1468                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
1469                               context ^ " has type " ^
1470                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
1471                               context ^ " but is here used with type " ^
1472                              CicMetaSubst.ppterm_in_context ~metasenv subst s context
1473                               (* "\nReason: " ^ Lazy.force e*))))
1474                     | CoercGraph.SomeCoercion candidates ->
1475                         let selected =
1476                           HExtlib.list_findopt
1477                             (fun (metasenv,last,c) ->
1478                              try
1479                               let subst,metasenv,ugraph =
1480                                fo_unif_subst subst context metasenv last hete
1481                                 ugraph in
1482                               let newt,newhety,subst,metasenv,ugraph =
1483                                type_of_aux subst metasenv context
1484                                 c ugraph
1485                               in
1486                               let newt, newty, subst, metasenv, ugraph =
1487                                avoid_double_coercion context subst metasenv
1488                                 ugraph newt tgt_carr
1489                               in
1490                               let subst,metasenv,ugraph1 =
1491                                 fo_unif_subst subst context metasenv
1492                                    newhety s ugraph
1493                               in
1494                                Some ((newt,newty), subst, metasenv, ugraph)
1495                              with Uncertain _ | RefineFailure _ -> None)
1496                             candidates
1497                         in
1498                         (match selected with
1499                         | Some x -> x
1500                         | None ->
1501                            enrich localization_tbl hete
1502                             ~f:(fun _ ->
1503                              (lazy ("(1)The term " ^
1504                               CicMetaSubst.ppterm_in_context ~metasenv subst hete
1505                                context ^ " has type " ^
1506                               CicMetaSubst.ppterm_in_context ~metasenv subst hety
1507                                context ^ " but is here used with type " ^
1508                               CicMetaSubst.ppterm_in_context ~metasenv subst s context
1509                                (* "\nReason: " ^ Lazy.force e*)))) exn))
1510                   | exn ->
1511                      enrich localization_tbl hete
1512                       ~f:(fun _ ->
1513                         (lazy ("(2)The term " ^
1514                           CicMetaSubst.ppterm_in_context ~metasenv subst hete
1515                            context ^ " has type " ^
1516                           CicMetaSubst.ppterm_in_context ~metasenv subst hety
1517                            context ^ " but is here used with type " ^
1518                           CicMetaSubst.ppterm_in_context ~metasenv subst s context
1519                            (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1520                   (* }}} end coercion stuff *)
1521                 in
1522                   eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1523                     (CicSubstitution.subst (fst arg) t)
1524                     ugraph1 (newargs@[arg]) tl
1525             | _ ->
1526                 try
1527                   let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1528                     fix_arity
1529                       pristinemenv context subst he hetype
1530                        (newargs@[hete,hety]@tl) ugraph
1531                   in
1532                   eat_prods_and_args metasenv
1533                     metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1534                 with RefineFailure _ | Uncertain _ as exn ->
1535                   (* unable to fix arity *)
1536                    more_args_than_expected localization_tbl metasenv
1537                      subst he context hetype args_bo_and_ty exn
1538       (* }}} *)
1539     in
1540     (* first we check if we are in the simple case of a meta closed term *)
1541     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1542      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1543       (* this optimization is to postpone fix_arity (the most common case)*)
1544       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1545      else
1546        (* this (says CSC) is also useful to infer dependent types *)
1547        try
1548         fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1549        with RefineFailure _ | Uncertain _ as exn ->
1550          (* unable to fix arity *)
1551           more_args_than_expected localization_tbl metasenv
1552             subst he context hetype args_bo_and_ty exn
1553     in
1554     let coerced_args,subst,metasenv,he,t,ugraph =
1555       eat_prods_and_args
1556         metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1557     in
1558     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1559   in
1560
1561   (* eat prods ends here! *)
1562
1563   let t',ty,subst',metasenv',ugraph1 =
1564    type_of_aux [] metasenv context t ugraph
1565   in
1566   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1567   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1568     (* Andrea: ho rimesso qui l'applicazione della subst al
1569        metasenv dopo che ho droppato l'invariante che il metsaenv
1570        e' sempre istanziato *)
1571   let substituted_metasenv =
1572     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1573     (* metasenv' *)
1574     (*  substituted_t,substituted_ty,substituted_metasenv *)
1575     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1576   let cleaned_t =
1577     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1578   let cleaned_ty =
1579     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1580   let cleaned_metasenv =
1581     List.map
1582       (function (n,context,ty) ->
1583          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1584          let context' =
1585            List.map
1586              (function
1587                   None -> None
1588                 | Some (n, Cic.Decl t) ->
1589                     Some (n,
1590                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1591                 | Some (n, Cic.Def (bo,ty)) ->
1592                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1593                     let ty' =
1594                       match ty with
1595                           None -> None
1596                         | Some ty ->
1597                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1598                     in
1599                       Some (n, Cic.Def (bo',ty'))
1600              ) context
1601          in
1602            (n,context',ty')
1603       ) substituted_metasenv
1604   in
1605     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1606 ;;
1607
1608 let undebrujin uri typesno tys t =
1609   snd
1610    (List.fold_right
1611      (fun (name,_,_,_) (i,t) ->
1612        (* here the explicit_named_substituion is assumed to be *)
1613        (* of length 0 *)
1614        let t' = Cic.MutInd (uri,i,[])  in
1615        let t = CicSubstitution.subst t' t in
1616         i - 1,t
1617      ) tys (typesno - 1,t))
1618
1619 let map_first_n n start f g l =
1620   let rec aux acc k l =
1621     if k < n then
1622       match l with
1623       | [] -> raise (Invalid_argument "map_first_n")
1624       | hd :: tl -> f hd k (aux acc (k+1) tl)
1625     else
1626       g acc l
1627   in
1628   aux start 0 l
1629
1630 (*CSC: this is a very rough approximation; to be finished *)
1631 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1632   let subst,metasenv,ugraph,tys =
1633     List.fold_right
1634       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1635         let subst,metasenv,ugraph,cl =
1636           List.fold_right
1637             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1638                let rec aux ctx k subst = function
1639                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1640                      let subst,metasenv,ugraph,tl =
1641                        map_first_n leftno
1642                          (subst,metasenv,ugraph,[])
1643                          (fun t n (subst,metasenv,ugraph,acc) ->
1644                            let subst,metasenv,ugraph =
1645                              fo_unif_subst
1646                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1647                            in
1648                            subst,metasenv,ugraph,(t::acc))
1649                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1650                          tl
1651                      in
1652                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1653                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1654                      subst,metasenv,ugraph,t
1655                  | Cic.Prod (name,s,t) ->
1656                      let ctx = (Some (name,Cic.Decl s))::ctx in
1657                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1658                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1659                  | _ ->
1660                      raise
1661                       (RefineFailure
1662                         (lazy "not well formed constructor type"))
1663                in
1664                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1665                subst,metasenv,ugraph,(name,ty) :: acc)
1666           cl (subst,metasenv,ugraph,[])
1667         in
1668         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1669       tys ([],metasenv,ugraph,[])
1670   in
1671   let substituted_tys =
1672     List.map
1673       (fun (name,ind,arity,cl) ->
1674         let cl =
1675           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1676         in
1677         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1678       tys
1679   in
1680   metasenv,ugraph,substituted_tys
1681
1682 let typecheck metasenv uri obj ~localization_tbl =
1683  let ugraph = CicUniv.empty_ugraph in
1684  match obj with
1685     Cic.Constant (name,Some bo,ty,args,attrs) ->
1686      let bo',boty,metasenv,ugraph =
1687       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1688      let ty',_,metasenv,ugraph =
1689       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1690      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1691      let bo' = CicMetaSubst.apply_subst subst bo' in
1692      let ty' = CicMetaSubst.apply_subst subst ty' in
1693      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1694       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1695   | Cic.Constant (name,None,ty,args,attrs) ->
1696      let ty',_,metasenv,ugraph =
1697       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1698      in
1699       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1700   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1701      assert (metasenv' = metasenv);
1702      (* Here we do not check the metasenv for correctness *)
1703      let bo',boty,metasenv,ugraph =
1704       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1705      let ty',sort,metasenv,ugraph =
1706       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1707      begin
1708       match sort with
1709          Cic.Sort _
1710        (* instead of raising Uncertain, let's hope that the meta will become
1711           a sort *)
1712        | Cic.Meta _ -> ()
1713        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1714      end;
1715      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1716      let bo' = CicMetaSubst.apply_subst subst bo' in
1717      let ty' = CicMetaSubst.apply_subst subst ty' in
1718      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1719       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1720   | Cic.Variable _ -> assert false (* not implemented *)
1721   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1722      (*CSC: this code is greately simplified and many many checks are missing *)
1723      (*CSC: e.g. the constructors are not required to build their own types,  *)
1724      (*CSC: the arities are not required to have as type a sort, etc.         *)
1725      let uri = match uri with Some uri -> uri | None -> assert false in
1726      let typesno = List.length tys in
1727      (* first phase: we fix only the types *)
1728      let metasenv,ugraph,tys =
1729       List.fold_right
1730        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1731          let ty',_,metasenv,ugraph =
1732           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1733          in
1734           metasenv,ugraph,(name,b,ty',cl)::res
1735        ) tys (metasenv,ugraph,[]) in
1736      let con_context =
1737       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1738      (* second phase: we fix only the constructors *)
1739      let saved_menv = metasenv in
1740      let metasenv,ugraph,tys =
1741       List.fold_right
1742        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1743          let metasenv,ugraph,cl' =
1744           List.fold_right
1745            (fun (name,ty) (metasenv,ugraph,res) ->
1746              let ty =
1747               CicTypeChecker.debrujin_constructor
1748                ~cb:(relocalize localization_tbl) uri typesno ty in
1749              let ty',_,metasenv,ugraph =
1750               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1751              let ty' = undebrujin uri typesno tys ty' in
1752               metasenv@saved_menv,ugraph,(name,ty')::res
1753            ) cl (metasenv,ugraph,[])
1754          in
1755           metasenv,ugraph,(name,b,ty,cl')::res
1756        ) tys (metasenv,ugraph,[]) in
1757      (* third phase: we check the positivity condition *)
1758      let metasenv,ugraph,tys =
1759        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1760      in
1761      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1762 ;;
1763
1764 (* sara' piu' veloce che raffinare da zero? mah.... *)
1765 let pack_coercion metasenv ctx t =
1766  let module C = Cic in
1767  let rec merge_coercions ctx =
1768    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1769    function
1770    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1771    | C.Meta (n,subst) ->
1772       let subst' =
1773        List.map
1774         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1775       in
1776        C.Meta (n,subst')
1777    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1778    | C.Prod (name,so,dest) ->
1779        let ctx' = (Some (name,C.Decl so))::ctx in
1780        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1781    | C.Lambda (name,so,dest) ->
1782        let ctx' = (Some (name,C.Decl so))::ctx in
1783        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1784    | C.LetIn (name,so,dest) ->
1785        let _,ty,metasenv,ugraph =
1786         pack_coercions := false;
1787         type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1788         pack_coercions := true;
1789        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1790        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1791    | C.Appl l ->
1792       let l = List.map (merge_coercions ctx) l in
1793       let t = C.Appl l in
1794        let b,_,_,_,_ = is_a_double_coercion t in
1795        (* prerr_endline "CANDIDATO!!!!"; *)
1796        if b then
1797          let ugraph = CicUniv.oblivion_ugraph in
1798          let old_insert_coercions = !insert_coercions in
1799          insert_coercions := false;
1800          let newt, _, menv, _ =
1801            try
1802              type_of_aux' metasenv ctx t ugraph
1803            with RefineFailure _ | Uncertain _ ->
1804              t, t, [], ugraph
1805          in
1806          insert_coercions := old_insert_coercions;
1807          if metasenv <> [] || menv = [] then
1808            newt
1809          else
1810            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1811        else
1812          t
1813    | C.Var (uri,exp_named_subst) ->
1814        let exp_named_subst = List.map aux exp_named_subst in
1815        C.Var (uri, exp_named_subst)
1816    | C.Const (uri,exp_named_subst) ->
1817        let exp_named_subst = List.map aux exp_named_subst in
1818        C.Const (uri, exp_named_subst)
1819    | C.MutInd (uri,tyno,exp_named_subst) ->
1820        let exp_named_subst = List.map aux exp_named_subst in
1821        C.MutInd (uri,tyno,exp_named_subst)
1822    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1823        let exp_named_subst = List.map aux exp_named_subst in
1824        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1825    | C.MutCase (uri,tyno,out,te,pl) ->
1826        let pl = List.map (merge_coercions ctx) pl in
1827        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1828    | C.Fix (fno, fl) ->
1829        let ctx' =
1830          List.fold_left
1831            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1832            ctx fl
1833        in
1834        let fl =
1835          List.map
1836            (fun (name,idx,ty,bo) ->
1837              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1838          fl
1839        in
1840        C.Fix (fno, fl)
1841    | C.CoFix (fno, fl) ->
1842        let ctx' =
1843          List.fold_left
1844            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1845            ctx fl
1846        in
1847        let fl =
1848          List.map
1849            (fun (name,ty,bo) ->
1850              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1851          fl
1852        in
1853        C.CoFix (fno, fl)
1854  in
1855   merge_coercions ctx t
1856 ;;
1857
1858 let pack_coercion_metasenv conjectures =
1859   let module C = Cic in
1860   List.map
1861     (fun (i, ctx, ty) ->
1862        let ctx =
1863          List.fold_right
1864            (fun item ctx ->
1865               let item' =
1866                 match item with
1867                     Some (name, C.Decl t) ->
1868                       Some (name, C.Decl (pack_coercion conjectures ctx t))
1869                   | Some (name, C.Def (t,None)) ->
1870                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
1871                   | Some (name, C.Def (t,Some ty)) ->
1872                       Some (name, C.Def (pack_coercion conjectures ctx t,
1873                                          Some (pack_coercion conjectures ctx ty)))
1874                   | None -> None
1875               in
1876                 item'::ctx
1877            ) ctx []
1878        in
1879          ((i,ctx,pack_coercion conjectures ctx ty))
1880     ) conjectures
1881 ;;
1882
1883 let pack_coercion_obj obj =
1884   let module C = Cic in
1885   match obj with
1886   | C.Constant (id, body, ty, params, attrs) ->
1887       let body =
1888         match body with
1889         | None -> None
1890         | Some body -> Some (pack_coercion [] [] body)
1891       in
1892       let ty = pack_coercion [] [] ty in
1893         C.Constant (id, body, ty, params, attrs)
1894   | C.Variable (name, body, ty, params, attrs) ->
1895       let body =
1896         match body with
1897         | None -> None
1898         | Some body -> Some (pack_coercion [] [] body)
1899       in
1900       let ty = pack_coercion [] [] ty in
1901         C.Variable (name, body, ty, params, attrs)
1902   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1903       let conjectures = pack_coercion_metasenv conjectures in
1904       let body = pack_coercion conjectures [] body in
1905       let ty = pack_coercion conjectures [] ty in
1906       C.CurrentProof (name, conjectures, body, ty, params, attrs)
1907   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1908       let indtys =
1909         List.map
1910           (fun (name, ind, arity, cl) ->
1911             let arity = pack_coercion [] [] arity in
1912             let cl =
1913               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1914             in
1915             (name, ind, arity, cl))
1916           indtys
1917       in
1918         C.InductiveDefinition (indtys, params, leftno, attrs)
1919 ;;
1920
1921
1922 (* DEBUGGING ONLY
1923 let type_of_aux' metasenv context term =
1924  try
1925   let (t,ty,m) =
1926       type_of_aux' metasenv context term in
1927     debug_print (lazy
1928      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1929    debug_print (lazy
1930     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1931    (t,ty,m)
1932  with
1933  | RefineFailure msg as e ->
1934      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1935      raise e
1936  | Uncertain msg as e ->
1937      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1938      raise e
1939 ;; *)
1940
1941 let profiler2 = HExtlib.profile "CicRefine"
1942
1943 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1944  profiler2.HExtlib.profile
1945   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1946
1947 let typecheck ~localization_tbl metasenv uri obj =
1948  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1949
1950 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1951 (* vim:set foldmethod=marker: *)