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]) ]) 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'.                      *)
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 in
1119                            try
1120                             let newty,newhety,subst,metasenv,ugraph =
1121                               type_of_aux subst metasenv context newt ugraph in
1122                             let subst,metasenv,ugraph1 =
1123                              fo_unif_subst subst context metasenv
1124                                 newhety s ugraph
1125                             in
1126                              newt, subst, metasenv, ugraph
1127                            with exn ->
1128                             enrich localization_tbl hete
1129                              ~f:(fun _ ->
1130                                (lazy ("The term " ^
1131                                  CicMetaSubst.ppterm_in_context subst hete
1132                                   context ^ " has type " ^
1133                                  CicMetaSubst.ppterm_in_context subst hety
1134                                   context ^ " but is here used with type " ^
1135                                  CicMetaSubst.ppterm_in_context subst s context
1136                                   (* "\nReason: " ^ Lazy.force e*)))) exn)
1137                      | exn ->
1138                         enrich localization_tbl hete
1139                          ~f:(fun _ ->
1140                            (lazy ("The term " ^
1141                              CicMetaSubst.ppterm_in_context subst hete
1142                               context ^ " has type " ^
1143                              CicMetaSubst.ppterm_in_context subst hety
1144                               context ^ " but is here used with type " ^
1145                              CicMetaSubst.ppterm_in_context subst s context
1146                               (* "\nReason: " ^ Lazy.force e*)))) exn
1147                    in
1148                    let coerced_args,metasenv',subst',t',ugraph2 =
1149                      eat_prods metasenv subst context
1150                        (CicSubstitution.subst arg t) ugraph1 tl
1151                    in
1152                      arg::coerced_args,metasenv',subst',t',ugraph2
1153                | _ -> assert false
1154             )
1155     in
1156     let coerced_args,metasenv,subst,t,ugraph2 =
1157       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1158     in
1159       coerced_args,t,subst,metasenv,ugraph2
1160   in
1161
1162   (* eat prods ends here! *)
1163
1164   let t',ty,subst',metasenv',ugraph1 =
1165    type_of_aux [] metasenv context t ugraph
1166   in
1167   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1168   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1169     (* Andrea: ho rimesso qui l'applicazione della subst al
1170        metasenv dopo che ho droppato l'invariante che il metsaenv
1171        e' sempre istanziato *)
1172   let substituted_metasenv =
1173     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1174     (* metasenv' *)
1175     (*  substituted_t,substituted_ty,substituted_metasenv *)
1176     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1177   let cleaned_t =
1178     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1179   let cleaned_ty =
1180     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1181   let cleaned_metasenv =
1182     List.map
1183       (function (n,context,ty) ->
1184          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1185          let context' =
1186            List.map
1187              (function
1188                   None -> None
1189                 | Some (n, Cic.Decl t) ->
1190                     Some (n,
1191                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1192                 | Some (n, Cic.Def (bo,ty)) ->
1193                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1194                     let ty' =
1195                       match ty with
1196                           None -> None
1197                         | Some ty ->
1198                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1199                     in
1200                       Some (n, Cic.Def (bo',ty'))
1201              ) context
1202          in
1203            (n,context',ty')
1204       ) substituted_metasenv
1205   in
1206     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1207 ;;
1208
1209 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1210   try
1211     type_of_aux' ?localization_tbl metasenv context term ugraph
1212   with
1213     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1214
1215 let undebrujin uri typesno tys t =
1216   snd
1217    (List.fold_right
1218      (fun (name,_,_,_) (i,t) ->
1219        (* here the explicit_named_substituion is assumed to be *)
1220        (* of length 0 *)
1221        let t' = Cic.MutInd (uri,i,[])  in
1222        let t = CicSubstitution.subst t' t in
1223         i - 1,t
1224      ) tys (typesno - 1,t))
1225
1226 let map_first_n n start f g l =
1227   let rec aux acc k l =
1228     if k < n then
1229       match l with
1230       | [] -> raise (Invalid_argument "map_first_n")
1231       | hd :: tl -> f hd k (aux acc (k+1) tl)
1232     else
1233       g acc l
1234   in
1235   aux start 0 l
1236
1237 (*CSC: this is a very rough approximation; to be finished *)
1238 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1239   let subst,metasenv,ugraph,tys =
1240     List.fold_right
1241       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1242         let subst,metasenv,ugraph,cl =
1243           List.fold_right
1244             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1245                let rec aux ctx k subst = function
1246                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1247                      let subst,metasenv,ugraph,tl =
1248                        map_first_n leftno
1249                          (subst,metasenv,ugraph,[])
1250                          (fun t n (subst,metasenv,ugraph,acc) ->
1251                            let subst,metasenv,ugraph =
1252                              fo_unif_subst
1253                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1254                            in
1255                            subst,metasenv,ugraph,(t::acc))
1256                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1257                          tl
1258                      in
1259                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1260                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1261                      subst,metasenv,ugraph,t
1262                  | Cic.Prod (name,s,t) ->
1263                      let ctx = (Some (name,Cic.Decl s))::ctx in
1264                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1265                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1266                  | _ ->
1267                      raise
1268                       (RefineFailure
1269                         (lazy "not well formed constructor type"))
1270                in
1271                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1272                subst,metasenv,ugraph,(name,ty) :: acc)
1273           cl (subst,metasenv,ugraph,[])
1274         in
1275         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1276       tys ([],metasenv,ugraph,[])
1277   in
1278   let substituted_tys =
1279     List.map
1280       (fun (name,ind,arity,cl) ->
1281         let cl =
1282           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1283         in
1284         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1285       tys
1286   in
1287   metasenv,ugraph,substituted_tys
1288
1289 let typecheck metasenv uri obj ~localization_tbl =
1290  let ugraph = CicUniv.empty_ugraph in
1291  match obj with
1292     Cic.Constant (name,Some bo,ty,args,attrs) ->
1293      let bo',boty,metasenv,ugraph =
1294       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1295      let ty',_,metasenv,ugraph =
1296       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1297      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1298      let bo' = CicMetaSubst.apply_subst subst bo' in
1299      let ty' = CicMetaSubst.apply_subst subst ty' in
1300      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1301       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1302   | Cic.Constant (name,None,ty,args,attrs) ->
1303      let ty',_,metasenv,ugraph =
1304       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1305      in
1306       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1307   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1308      assert (metasenv' = metasenv);
1309      (* Here we do not check the metasenv for correctness *)
1310      let bo',boty,metasenv,ugraph =
1311       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1312      let ty',sort,metasenv,ugraph =
1313       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1314      begin
1315       match sort with
1316          Cic.Sort _
1317        (* instead of raising Uncertain, let's hope that the meta will become
1318           a sort *)
1319        | Cic.Meta _ -> ()
1320        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1321      end;
1322      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1323      let bo' = CicMetaSubst.apply_subst subst bo' in
1324      let ty' = CicMetaSubst.apply_subst subst ty' in
1325      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1326       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1327   | Cic.Variable _ -> assert false (* not implemented *)
1328   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1329      (*CSC: this code is greately simplified and many many checks are missing *)
1330      (*CSC: e.g. the constructors are not required to build their own types,  *)
1331      (*CSC: the arities are not required to have as type a sort, etc.         *)
1332      let uri = match uri with Some uri -> uri | None -> assert false in
1333      let typesno = List.length tys in
1334      (* first phase: we fix only the types *)
1335      let metasenv,ugraph,tys =
1336       List.fold_right
1337        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1338          let ty',_,metasenv,ugraph =
1339           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1340          in
1341           metasenv,ugraph,(name,b,ty',cl)::res
1342        ) tys (metasenv,ugraph,[]) in
1343      let con_context =
1344       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1345      (* second phase: we fix only the constructors *)
1346      let metasenv,ugraph,tys =
1347       List.fold_right
1348        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1349          let metasenv,ugraph,cl' =
1350           List.fold_right
1351            (fun (name,ty) (metasenv,ugraph,res) ->
1352              let ty =
1353               CicTypeChecker.debrujin_constructor
1354                ~cb:(relocalize localization_tbl) uri typesno ty in
1355              let ty',_,metasenv,ugraph =
1356               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1357              let ty' = undebrujin uri typesno tys ty' in
1358               metasenv,ugraph,(name,ty')::res
1359            ) cl (metasenv,ugraph,[])
1360          in
1361           metasenv,ugraph,(name,b,ty,cl')::res
1362        ) tys (metasenv,ugraph,[]) in
1363      (* third phase: we check the positivity condition *)
1364      let metasenv,ugraph,tys =
1365        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1366      in
1367      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1368
1369 (* DEBUGGING ONLY
1370 let type_of_aux' metasenv context term =
1371  try
1372   let (t,ty,m) =
1373       type_of_aux' metasenv context term in
1374     debug_print (lazy
1375      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1376    debug_print (lazy
1377     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1378    (t,ty,m)
1379  with
1380  | RefineFailure msg as e ->
1381      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1382      raise e
1383  | Uncertain msg as e ->
1384      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1385      raise e
1386 ;; *)
1387
1388 let profiler2 = HExtlib.profile "CicRefine"
1389
1390 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1391  profiler2.HExtlib.profile
1392   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1393
1394 let typecheck ~localization_tbl metasenv uri obj =
1395  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj