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