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