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