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