components/cic_unification/cicRefine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 exception RefineFailure of string Lazy.t;;
  31 exception Uncertain of string Lazy.t;;
  32 exception AssertFailure of string Lazy.t;;
  33
  34 (* for internal use only; the integer is the number of surplus arguments *)
  35 exception MoreArgsThanExpected of int * exn;;
  36
  37 let insert_coercions = ref true
  38 let pack_coercions = ref true
  39
  40 let debug = false;;
  41
  42 let debug_print =
  43   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
  44
  45 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
  46
  47 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
  48   try
  49 let foo () =
  50     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  51 in profiler_eat_prods2.HExtlib.profile foo ()
  52   with
  53       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  54     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  55 ;;
  56
  57 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
  58
  59 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
  60   try
  61 let foo () =
  62     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  63 in profiler_eat_prods.HExtlib.profile foo ()
  64   with
  65       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  66     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  67 ;;
  68
  69 let profiler = HExtlib.profile "CicRefine.fo_unif"
  70
  71 let fo_unif_subst subst context metasenv t1 t2 ugraph =
  72   try
  73 let foo () =
  74     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  75 in profiler.HExtlib.profile foo ()
  76   with
  77       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  78     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  79 ;;
  80
  81 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
  82  let exn' =
  83   match exn with
  84      RefineFailure msg -> RefineFailure (f msg)
  85    | Uncertain msg -> Uncertain (f msg)
  86    | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
  87    | Sys.Break -> raise exn
  88    | _ -> prerr_endline (Printexc.to_string exn); assert false
  89  in
  90  let loc =
  91   try
  92    Cic.CicHash.find localization_tbl t
  93   with Not_found ->
  94    HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
  95    raise exn'
  96  in
  97   raise (HExtlib.Localized (loc,exn'))
  98
  99 let relocalize localization_tbl oldt newt =
 100  try
 101   let infos = Cic.CicHash.find localization_tbl oldt in
 102    Cic.CicHash.remove localization_tbl oldt;
 103    Cic.CicHash.add localization_tbl newt infos;
 104  with
 105   Not_found -> ()
 106 ;;
 107
 108 let rec split l n =
 109  match (l,n) with
 110     (l,0) -> ([], l)
 111   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
 112   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
 113 ;;
 114
 115 let exp_impl metasenv subst context =
 116  function
 117   | Some `Type ->
 118       let (metasenv', idx) =
 119         CicMkImplicit.mk_implicit_type metasenv subst context in
 120       let irl =
 121         CicMkImplicit.identity_relocation_list_for_metavariable context in
 122       metasenv', Cic.Meta (idx, irl)
 123   | Some `Closed ->
 124       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
 125       metasenv', Cic.Meta (idx, [])
 126   | None ->
 127       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
 128       let irl =
 129         CicMkImplicit.identity_relocation_list_for_metavariable context in
 130       metasenv', Cic.Meta (idx, irl)
 131   | _ -> assert false
 132 ;;
 133
 134 let is_a_double_coercion t =
 135   let last_of l =
 136     let rec aux acc = function
 137       | x::[] -> acc,x
 138       | x::tl -> aux (acc@[x]) tl
 139       | [] -> assert false
 140     in
 141     aux [] l
 142   in
 143   let imp = Cic.Implicit None in
 144   let dummyres = false,imp, imp,imp,imp in
 145   match t with
 146   | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
 147       (match last_of tl with
 148       | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
 149           let sib2,head = last_of tl2 in
 150           true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
 151             (c2::sib2@[imp])])
 152       | _ -> dummyres)
 153   | _ -> dummyres
 154
 155 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 156 =
 157   let len = List.length tlbody_and_type in
 158   let msg =
 159     lazy ("The term " ^
 160       CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
 161       " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
 162       ") is here applied to " ^ string_of_int len ^
 163       " arguments but here it can handle only up to " ^
 164       string_of_int (len - residuals) ^ " arguments")
 165   in
 166   enrich localization_tbl he ~f:(fun _-> msg) exn
 167 ;;
 168
 169 let mk_prod_of_metas metasenv context' subst args =
 170   let rec mk_prod metasenv context' = function
 171     | [] ->
 172         let (metasenv, idx) =
 173           CicMkImplicit.mk_implicit_type metasenv subst context'
 174         in
 175         let irl =
 176           CicMkImplicit.identity_relocation_list_for_metavariable context'
 177         in
 178           metasenv,Cic.Meta (idx, irl)
 179     | (_,argty)::tl ->
 180         let (metasenv, idx) =
 181           CicMkImplicit.mk_implicit_type metasenv subst context'
 182         in
 183         let irl =
 184           CicMkImplicit.identity_relocation_list_for_metavariable context'
 185         in
 186         let meta = Cic.Meta (idx,irl) in
 187         let name =
 188           (* The name must be fresh for context.                 *)
 189           (* Nevertheless, argty is well-typed only in context.  *)
 190           (* Thus I generate a name (name_hint) in context and   *)
 191           (* then I generate a name --- using the hint name_hint *)
 192           (* --- that is fresh in context'.                      *)
 193           let name_hint =
 194             (* Cic.Name "pippo" *)
 195             FreshNamesGenerator.mk_fresh_name ~subst metasenv
 196               (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
 197               (CicMetaSubst.apply_subst_context subst context')
 198               Cic.Anonymous
 199               ~typ:(CicMetaSubst.apply_subst subst argty)
 200           in
 201             (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 202             FreshNamesGenerator.mk_fresh_name ~subst
 203               [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
 204         in
 205         let metasenv,target =
 206           mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
 207         in
 208           metasenv,Cic.Prod (name,meta,target)
 209   in
 210   mk_prod metasenv context' args
 211 ;;
 212
 213 let rec type_of_constant uri ugraph =
 214  let module C = Cic in
 215  let module R = CicReduction in
 216  let module U = UriManager in
 217   let _ = CicTypeChecker.typecheck uri in
 218   let obj,u =
 219    try
 220     CicEnvironment.get_cooked_obj ugraph uri
 221    with Not_found -> assert false
 222   in
 223    match obj with
 224       C.Constant (_,_,ty,_,_) -> ty,u
 225     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
 226     | _ ->
 227        raise
 228         (RefineFailure
 229           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 230
 231 and type_of_variable uri ugraph =
 232   let module C = Cic in
 233   let module R = CicReduction in
 234   let module U = UriManager in
 235   let _ = CicTypeChecker.typecheck uri in
 236   let obj,u =
 237    try
 238     CicEnvironment.get_cooked_obj ugraph uri
 239     with Not_found -> assert false
 240   in
 241    match obj with
 242       C.Variable (_,_,ty,_,_) -> ty,u
 243     | _ ->
 244         raise
 245          (RefineFailure
 246           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
 247
 248 and type_of_mutual_inductive_defs uri i ugraph =
 249   let module C = Cic in
 250   let module R = CicReduction in
 251   let module U = UriManager in
 252   let _ = CicTypeChecker.typecheck uri in
 253   let obj,u =
 254    try
 255     CicEnvironment.get_cooked_obj ugraph uri
 256    with Not_found -> assert false
 257   in
 258    match obj with
 259       C.InductiveDefinition (dl,_,_,_) ->
 260         let (_,_,arity,_) = List.nth dl i in
 261          arity,u
 262     | _ ->
 263        raise
 264         (RefineFailure
 265          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
 266
 267 and type_of_mutual_inductive_constr uri i j ugraph =
 268   let module C = Cic in
 269   let module R = CicReduction in
 270   let module U = UriManager in
 271   let _ = CicTypeChecker.typecheck uri in
 272    let obj,u =
 273     try
 274      CicEnvironment.get_cooked_obj ugraph uri
 275     with Not_found -> assert false
 276    in
 277     match obj with
 278         C.InductiveDefinition (dl,_,_,_) ->
 279           let (_,_,_,cl) = List.nth dl i in
 280           let (_,ty) = List.nth cl (j-1) in
 281             ty,u
 282       | _ ->
 283           raise
 284                   (RefineFailure
 285               (lazy
 286                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 287
 288
 289 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 290
 291 (* the check_branch function checks if a branch of a case is refinable.
 292    It returns a pair (outype_instance,args), a subst and a metasenv.
 293    outype_instance is the expected result of applying the case outtype
 294    to args.
 295    The problem is that outype is in general unknown, and we should
 296    try to synthesize it from the above information, that is in general
 297    a second order unification problem. *)
 298
 299 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 300   let module C = Cic in
 301     (* let module R = CicMetaSubst in *)
 302   let module R = CicReduction in
 303     match R.whd ~subst context expectedtype with
 304         C.MutInd (_,_,_) ->
 305           (n,context,actualtype, [term]), subst, metasenv, ugraph
 306       | C.Appl (C.MutInd (_,_,_)::tl) ->
 307           let (_,arguments) = split tl left_args_no in
 308             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 309       | C.Prod (name,so,de) ->
 310           (* we expect that the actual type of the branch has the due
 311              number of Prod *)
 312           (match R.whd ~subst context actualtype with
 313                C.Prod (name',so',de') ->
 314                  let subst, metasenv, ugraph1 =
 315                    fo_unif_subst subst context metasenv so so' ugraph in
 316                  let term' =
 317                    (match CicSubstitution.lift 1 term with
 318                         C.Appl l -> C.Appl (l@[C.Rel 1])
 319                       | t -> C.Appl [t ; C.Rel 1]) in
 320                    (* we should also check that the name variable is anonymous in
 321                       the actual type de' ?? *)
 322                    check_branch (n+1)
 323                      ((Some (name,(C.Decl so)))::context)
 324                        metasenv subst left_args_no de' term' de ugraph1
 325              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
 326       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 327
 328 and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 329      ugraph
 330 =
 331   let rec type_of_aux subst metasenv context t ugraph =
 332     let module C = Cic in
 333     let module S = CicSubstitution in
 334     let module U = UriManager in
 335      let (t',_,_,_,_) as res =
 336       match t with
 337           (*    function *)
 338           C.Rel n ->
 339             (try
 340                match List.nth context (n - 1) with
 341                    Some (_,C.Decl ty) ->
 342                      t,S.lift n ty,subst,metasenv, ugraph
 343                  | Some (_,C.Def (_,Some ty)) ->
 344                      t,S.lift n ty,subst,metasenv, ugraph
 345                  | Some (_,C.Def (bo,None)) ->
 346                      let ty,ugraph =
 347                       (* if it is in the context it must be already well-typed*)
 348                       CicTypeChecker.type_of_aux' ~subst metasenv context
 349                        (S.lift n bo) ugraph
 350                      in
 351                       t,ty,subst,metasenv,ugraph
 352                  | None ->
 353                     enrich localization_tbl t
 354                      (RefineFailure (lazy "Rel to hidden hypothesis"))
 355              with
 356               Failure _ ->
 357                enrich localization_tbl t
 358                 (RefineFailure (lazy "Not a closed term")))
 359         | C.Var (uri,exp_named_subst) ->
 360             let exp_named_subst',subst',metasenv',ugraph1 =
 361               check_exp_named_subst
 362                 subst metasenv context exp_named_subst ugraph
 363             in
 364             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 365             let ty =
 366               CicSubstitution.subst_vars exp_named_subst' ty_uri
 367             in
 368               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 369         | C.Meta (n,l) ->
 370             (try
 371                let (canonical_context, term,ty) =
 372                  CicUtil.lookup_subst n subst
 373                in
 374                let l',subst',metasenv',ugraph1 =
 375                  check_metasenv_consistency n subst metasenv context
 376                    canonical_context l ugraph
 377                in
 378                  (* trust or check ??? *)
 379                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 380                    subst', metasenv', ugraph1
 381                    (* type_of_aux subst metasenv
 382                       context (CicSubstitution.subst_meta l term) *)
 383              with CicUtil.Subst_not_found _ ->
 384                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 385                let l',subst',metasenv', ugraph1 =
 386                  check_metasenv_consistency n subst metasenv context
 387                    canonical_context l ugraph
 388                in
 389                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 390                    subst', metasenv',ugraph1)
 391         | C.Sort (C.Type tno) ->
 392             let tno' = CicUniv.fresh() in
 393              (try
 394                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 395                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 396               with
 397                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
 398         | C.Sort _ ->
 399             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 400         | C.Implicit infos ->
 401            let metasenv',t' = exp_impl metasenv subst context infos in
 402             type_of_aux subst metasenv' context t' ugraph
 403         | C.Cast (te,ty) ->
 404             let ty',_,subst',metasenv',ugraph1 =
 405               type_of_aux subst metasenv context ty ugraph
 406             in
 407             let te',inferredty,subst'',metasenv'',ugraph2 =
 408               type_of_aux subst' metasenv' context te ugraph1
 409             in
 410             let (te', ty'), subst''',metasenv''',ugraph3 =
 411               coerce_to_something true localization_tbl te' inferredty ty'
 412                 subst'' metasenv'' context ugraph2
 413             in
 414              C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 415         | C.Prod (name,s,t) ->
 416             let s',sort1,subst',metasenv',ugraph1 =
 417               type_of_aux subst metasenv context s ugraph
 418             in
 419             let s',sort1,subst', metasenv',ugraph1 =
 420               coerce_to_sort localization_tbl
 421               s' sort1 subst' context metasenv' ugraph1
 422             in
 423             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 424             let t',sort2,subst'',metasenv'',ugraph2 =
 425               type_of_aux subst' metasenv'
 426                 context_for_t t ugraph1
 427             in
 428             let t',sort2,subst'',metasenv'',ugraph2 =
 429               coerce_to_sort localization_tbl
 430               t' sort2 subst'' context_for_t metasenv'' ugraph2
 431             in
 432               let sop,subst''',metasenv''',ugraph3 =
 433                 sort_of_prod localization_tbl subst'' metasenv''
 434                   context (name,s') t' (sort1,sort2) ugraph2
 435               in
 436                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 437         | C.Lambda (n,s,t) ->
 438             let s',sort1,subst',metasenv',ugraph1 =
 439               type_of_aux subst metasenv context s ugraph
 440             in
 441             let s',sort1,subst',metasenv',ugraph1 =
 442               coerce_to_sort localization_tbl
 443               s' sort1 subst' context metasenv' ugraph1
 444             in
 445             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 446             let t',type2,subst'',metasenv'',ugraph2 =
 447               type_of_aux subst' metasenv' context_for_t t ugraph1
 448             in
 449               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 450                 subst'',metasenv'',ugraph2
 451         | C.LetIn (n,s,t) ->
 452             (* only to check if s is well-typed *)
 453             let s',ty,subst',metasenv',ugraph1 =
 454               type_of_aux subst metasenv context s ugraph
 455             in
 456            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 457
 458             let t',inferredty,subst'',metasenv'',ugraph2 =
 459               type_of_aux subst' metasenv'
 460                 context_for_t t ugraph1
 461             in
 462               (* One-step LetIn reduction.
 463                * Even faster than the previous solution.
 464                * Moreover the inferred type is closer to the expected one.
 465                *)
 466               C.LetIn (n,s',t'),
 467                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
 468                subst'',metasenv'',ugraph2
 469         | C.Appl (he::((_::_) as tl)) ->
 470             let he',hetype,subst',metasenv',ugraph1 =
 471               type_of_aux subst metasenv context he ugraph
 472             in
 473             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 474                typeof_list subst' metasenv' context ugraph1 tl
 475             in
 476             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
 477               eat_prods true subst'' metasenv'' context
 478                 he' hetype tlbody_and_type ugraph2
 479             in
 480             let newappl = (C.Appl (coerced_he::coerced_args)) in
 481             avoid_double_coercion
 482               context subst''' metasenv''' ugraph3 newappl applty
 483         | C.Appl _ -> assert false
 484         | C.Const (uri,exp_named_subst) ->
 485             let exp_named_subst',subst',metasenv',ugraph1 =
 486               check_exp_named_subst subst metasenv context
 487                 exp_named_subst ugraph in
 488             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 489             let cty =
 490               CicSubstitution.subst_vars exp_named_subst' ty_uri
 491             in
 492               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 493         | C.MutInd (uri,i,exp_named_subst) ->
 494             let exp_named_subst',subst',metasenv',ugraph1 =
 495               check_exp_named_subst subst metasenv context
 496                 exp_named_subst ugraph
 497             in
 498             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 499             let cty =
 500               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 501               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 502         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 503             let exp_named_subst',subst',metasenv',ugraph1 =
 504               check_exp_named_subst subst metasenv context
 505                 exp_named_subst ugraph
 506             in
 507             let ty_uri,ugraph2 =
 508               type_of_mutual_inductive_constr uri i j ugraph1
 509             in
 510             let cty =
 511               CicSubstitution.subst_vars exp_named_subst' ty_uri
 512             in
 513               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 514                 metasenv',ugraph2
 515         | C.MutCase (uri, i, outtype, term, pl) ->
 516             (* first, get the inductive type (and noparams)
 517              * in the environment  *)
 518             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 519               let _ = CicTypeChecker.typecheck uri in
 520               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 521               match obj with
 522                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 523                     List.nth l i , expl_params, parsno, u
 524                 | _ ->
 525                     enrich localization_tbl t
 526                      (RefineFailure
 527                        (lazy ("Unkown mutual inductive definition " ^
 528                          U.string_of_uri uri)))
 529            in
 530            if List.length constructors <> List.length pl then
 531             enrich localization_tbl t
 532              (RefineFailure
 533                (lazy "Wrong number of cases")) ;
 534            let rec count_prod t =
 535              match CicReduction.whd ~subst context t with
 536                  C.Prod (_, _, t) -> 1 + (count_prod t)
 537                | _ -> 0
 538            in
 539            let no_args = count_prod arity in
 540              (* now, create a "generic" MutInd *)
 541            let metasenv,left_args =
 542              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 543            in
 544            let metasenv,right_args =
 545              let no_right_params = no_args - no_left_params in
 546                if no_right_params < 0 then assert false
 547                else CicMkImplicit.n_fresh_metas
 548                       metasenv subst context no_right_params
 549            in
 550            let metasenv,exp_named_subst =
 551              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 552            let expected_type =
 553              if no_args = 0 then
 554                C.MutInd (uri,i,exp_named_subst)
 555              else
 556                C.Appl
 557                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 558            in
 559              (* check consistency with the actual type of term *)
 560            let term',actual_type,subst,metasenv,ugraph1 =
 561              type_of_aux subst metasenv context term ugraph in
 562            let expected_type',_, subst, metasenv,ugraph2 =
 563              type_of_aux subst metasenv context expected_type ugraph1
 564            in
 565            let actual_type = CicReduction.whd ~subst context actual_type in
 566            let subst,metasenv,ugraph3 =
 567             try
 568              fo_unif_subst subst context metasenv
 569                expected_type' actual_type ugraph2
 570             with
 571              exn ->
 572               enrich localization_tbl term' exn
 573                ~f:(function _ ->
 574                  lazy ("(10)The term " ^
 575                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
 576                    context ^ " has type " ^
 577                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
 578                    context ^ " but is here used with type " ^
 579                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
 580            in
 581            let rec instantiate_prod t =
 582             function
 583                [] -> t
 584              | he::tl ->
 585                 match CicReduction.whd ~subst context t with
 586                    C.Prod (_,_,t') ->
 587                     instantiate_prod (CicSubstitution.subst he t') tl
 588                  | _ -> assert false
 589            in
 590            let arity_instantiated_with_left_args =
 591             instantiate_prod arity left_args in
 592              (* TODO: check if the sort elimination
 593               * is allowed: [(I q1 ... qr)|B] *)
 594            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 595              List.fold_right
 596                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
 597                   let constructor =
 598                     if left_args = [] then
 599                       (C.MutConstruct (uri,i,j,exp_named_subst))
 600                     else
 601                       (C.Appl
 602                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 603                   in
 604                   let p',actual_type,subst,metasenv,ugraph1 =
 605                     type_of_aux subst metasenv context p ugraph
 606                   in
 607                   let constructor',expected_type, subst, metasenv,ugraph2 =
 608                     type_of_aux subst metasenv context constructor ugraph1
 609                   in
 610                   let outtypeinstance,subst,metasenv,ugraph3 =
 611                    try
 612                     check_branch 0 context metasenv subst
 613                      no_left_params actual_type constructor' expected_type
 614                      ugraph2
 615                    with
 616                     exn ->
 617                      enrich localization_tbl constructor'
 618                       ~f:(fun _ ->
 619                         lazy ("(11)The term " ^
 620                          CicMetaSubst.ppterm_in_context metasenv subst p'
 621                           context ^ " has type " ^
 622                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
 623                           context ^ " but is here used with type " ^
 624                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
 625                           context)) exn
 626                   in
 627                     (p'::pl,j-1,
 628                      outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
 629                pl ([],List.length pl,[],subst,metasenv,ugraph3)
 630            in
 631
 632              (* we are left to check that the outype matches his instances.
 633                 The easy case is when the outype is specified, that amount
 634                 to a trivial check. Otherwise, we should guess a type from
 635                 its instances
 636              *)
 637
 638            let outtype,outtypety, subst, metasenv,ugraph4 =
 639              type_of_aux subst metasenv context outtype ugraph4 in
 640            (match outtype with
 641            | C.Meta (n,l) ->
 642                (let candidate,ugraph5,metasenv,subst =
 643                  let exp_name_subst, metasenv =
 644                     let o,_ =
 645                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 646                     in
 647                     let uris = CicUtil.params_of_obj o in
 648                     List.fold_right (
 649                       fun uri (acc,metasenv) ->
 650                         let metasenv',new_meta =
 651                            CicMkImplicit.mk_implicit metasenv subst context
 652                         in
 653                         let irl =
 654                           CicMkImplicit.identity_relocation_list_for_metavariable
 655                             context
 656                         in
 657                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 658                     ) uris ([],metasenv)
 659                  in
 660                  let ty =
 661                   match left_args,right_args with
 662                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 663                    | _,_ ->
 664                       let rec mk_right_args =
 665                        function
 666                           0 -> []
 667                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 668                       in
 669                       let right_args_no = List.length right_args in
 670                       let lifted_left_args =
 671                        List.map (CicSubstitution.lift right_args_no) left_args
 672                       in
 673                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 674                         (lifted_left_args @ mk_right_args right_args_no))
 675                  in
 676                  let fresh_name =
 677                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 678                      context Cic.Anonymous ~typ:ty
 679                  in
 680                  match outtypeinstances with
 681                  | [] ->
 682                      let extended_context =
 683                       let rec add_right_args =
 684                        function
 685                           Cic.Prod (name,ty,t) ->
 686                            Some (name,Cic.Decl ty)::(add_right_args t)
 687                         | _ -> []
 688                       in
 689                        (Some (fresh_name,Cic.Decl ty))::
 690                        (List.rev
 691                         (add_right_args arity_instantiated_with_left_args))@
 692                        context
 693                      in
 694                      let metasenv,new_meta =
 695                        CicMkImplicit.mk_implicit metasenv subst extended_context
 696                      in
 697                        let irl =
 698                        CicMkImplicit.identity_relocation_list_for_metavariable
 699                          extended_context
 700                      in
 701                      let rec add_lambdas b =
 702                       function
 703                          Cic.Prod (name,ty,t) ->
 704                           Cic.Lambda (name,ty,(add_lambdas b t))
 705                        | _ -> Cic.Lambda (fresh_name, ty, b)
 706                      in
 707                      let candidate =
 708                       add_lambdas (Cic.Meta (new_meta,irl))
 709                        arity_instantiated_with_left_args
 710                      in
 711                      (Some candidate),ugraph4,metasenv,subst
 712                  | (constructor_args_no,_,instance,_)::tl ->
 713                      try
 714                        let instance',subst,metasenv =
 715                          CicMetaSubst.delift_rels subst metasenv
 716                           constructor_args_no instance
 717                        in
 718                        let candidate,ugraph,metasenv,subst =
 719                          List.fold_left (
 720                            fun (candidate_oty,ugraph,metasenv,subst)
 721                              (constructor_args_no,_,instance,_) ->
 722                                match candidate_oty with
 723                                | None -> None,ugraph,metasenv,subst
 724                                | Some ty ->
 725                                  try
 726                                    let instance',subst,metasenv =
 727                                      CicMetaSubst.delift_rels subst metasenv
 728                                       constructor_args_no instance
 729                                    in
 730                                    let subst,metasenv,ugraph =
 731                                     fo_unif_subst subst context metasenv
 732                                       instance' ty ugraph
 733                                    in
 734                                     candidate_oty,ugraph,metasenv,subst
 735                                  with
 736                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 737                                   | RefineFailure _ | Uncertain _ ->
 738                                      None,ugraph,metasenv,subst
 739                          ) (Some instance',ugraph4,metasenv,subst) tl
 740                        in
 741                        match candidate with
 742                        | None -> None, ugraph,metasenv,subst
 743                        | Some t ->
 744                           let rec add_lambdas n b =
 745                            function
 746                               Cic.Prod (name,ty,t) ->
 747                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 748                             | _ ->
 749                               Cic.Lambda (fresh_name, ty,
 750                                CicSubstitution.lift (n + 1) t)
 751                           in
 752                            Some
 753                             (add_lambdas 0 t arity_instantiated_with_left_args),
 754                            ugraph,metasenv,subst
 755                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 756                        None,ugraph4,metasenv,subst
 757                in
 758                match candidate with
 759                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 760                | Some candidate ->
 761                    let subst,metasenv,ugraph =
 762                     try
 763                      fo_unif_subst subst context metasenv
 764                        candidate outtype ugraph5
 765                     with
 766                      exn -> assert false(* unification against a metavariable *)
 767                    in
 768                      C.MutCase (uri, i, outtype, term', pl'),
 769                       CicReduction.head_beta_reduce
 770                        (CicMetaSubst.apply_subst subst
 771                         (Cic.Appl (outtype::right_args@[term']))),
 772                      subst,metasenv,ugraph)
 773            | _ ->    (* easy case *)
 774              let tlbody_and_type,subst,metasenv,ugraph4 =
 775                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
 776              in
 777              let _,_,_,subst,metasenv,ugraph4 =
 778                eat_prods false subst metasenv context
 779                  outtype outtypety tlbody_and_type ugraph4
 780              in
 781              let _,_, subst, metasenv,ugraph5 =
 782                type_of_aux subst metasenv context
 783                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 784              in
 785              let (subst,metasenv,ugraph6) =
 786                List.fold_left2
 787                  (fun (subst,metasenv,ugraph)
 788                    p (constructor_args_no,context,instance,args)
 789                   ->
 790                     let instance' =
 791                       let appl =
 792                         let outtype' =
 793                           CicSubstitution.lift constructor_args_no outtype
 794                         in
 795                           C.Appl (outtype'::args)
 796                       in
 797                         CicReduction.whd ~subst context appl
 798                     in
 799                      try
 800                       fo_unif_subst subst context metasenv instance instance'
 801                        ugraph
 802                      with
 803                       exn ->
 804                        enrich localization_tbl p exn
 805                         ~f:(function _ ->
 806                           lazy ("(12)The term " ^
 807                            CicMetaSubst.ppterm_in_context ~metasenv subst p
 808                             context ^ " has type " ^
 809                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
 810                             context ^ " but is here used with type " ^
 811                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
 812                             context)))
 813                  (subst,metasenv,ugraph5) pl' outtypeinstances
 814              in
 815                C.MutCase (uri, i, outtype, term', pl'),
 816                  CicReduction.head_beta_reduce
 817                   (CicMetaSubst.apply_subst subst
 818                    (C.Appl(outtype::right_args@[term]))),
 819                  subst,metasenv,ugraph6)
 820         | C.Fix (i,fl) ->
 821             let fl_ty',subst,metasenv,types,ugraph1,len =
 822               List.fold_left
 823                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
 824                    let ty',_,subst',metasenv',ugraph1 =
 825                       type_of_aux subst metasenv context ty ugraph
 826                    in
 827                      fl @ [ty'],subst',metasenv',
 828                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
 829                         :: types, ugraph, len+1
 830                 ) ([],subst,metasenv,[],ugraph,0) fl
 831             in
 832             let context' = types@context in
 833             let fl_bo',subst,metasenv,ugraph2 =
 834               List.fold_left
 835                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 836                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 837                      type_of_aux subst metasenv context' bo ugraph in
 838                    let expected_ty = CicSubstitution.lift len ty in
 839                    let subst',metasenv',ugraph' =
 840                     try
 841                      fo_unif_subst subst context' metasenv
 842                        ty_of_bo expected_ty ugraph1
 843                     with
 844                      exn ->
 845                       enrich localization_tbl bo exn
 846                        ~f:(function _ ->
 847                          lazy ("(13)The term " ^
 848                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 849                            context' ^ " has type " ^
 850                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 851                            context' ^ " but is here used with type " ^
 852                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 853                            context))
 854                    in
 855                      fl @ [bo'] , subst',metasenv',ugraph'
 856                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 857             in
 858             let ty = List.nth fl_ty' i in
 859             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 860              * and we want the new fl with bo' and ty' injected in the right
 861              * place.
 862              *)
 863             let rec map3 f l1 l2 l3 =
 864               match l1,l2,l3 with
 865               | [],[],[] -> []
 866               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 867               | _ -> assert false
 868             in
 869             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 870               fl_ty' fl_bo' fl
 871             in
 872               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 873         | C.CoFix (i,fl) ->
 874             let fl_ty',subst,metasenv,types,ugraph1,len =
 875               List.fold_left
 876                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
 877                    let ty',_,subst',metasenv',ugraph1 =
 878                      type_of_aux subst metasenv context ty ugraph
 879                    in
 880                      fl @ [ty'],subst',metasenv',
 881                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
 882                         types, ugraph1, len+1
 883                 ) ([],subst,metasenv,[],ugraph,0) fl
 884             in
 885             let context' = types@context in
 886             let fl_bo',subst,metasenv,ugraph2 =
 887               List.fold_left
 888                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 889                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 890                      type_of_aux subst metasenv context' bo ugraph in
 891                    let expected_ty = CicSubstitution.lift len ty in
 892                    let subst',metasenv',ugraph' =
 893                     try
 894                      fo_unif_subst subst context' metasenv
 895                        ty_of_bo expected_ty ugraph1
 896                     with
 897                      exn ->
 898                       enrich localization_tbl bo exn
 899                        ~f:(function _ ->
 900                          lazy ("(14)The term " ^
 901                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 902                            context' ^ " has type " ^
 903                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 904                            context' ^ " but is here used with type " ^
 905                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 906                            context))
 907                    in
 908                      fl @ [bo'],subst',metasenv',ugraph'
 909                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 910             in
 911             let ty = List.nth fl_ty' i in
 912             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 913              * and we want the new fl with bo' and ty' injected in the right
 914              * place.
 915              *)
 916             let rec map3 f l1 l2 l3 =
 917               match l1,l2,l3 with
 918               | [],[],[] -> []
 919               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 920               | _ -> assert false
 921             in
 922             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 923               fl_ty' fl_bo' fl
 924             in
 925               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 926      in
 927       relocalize localization_tbl t t';
 928       res
 929
 930   (* check_metasenv_consistency checks that the "canonical" context of a
 931      metavariable is consitent - up to relocation via the relocation list l -
 932      with the actual context *)
 933   and check_metasenv_consistency
 934     metano subst metasenv context canonical_context l ugraph
 935     =
 936     let module C = Cic in
 937     let module R = CicReduction in
 938     let module S = CicSubstitution in
 939     let lifted_canonical_context =
 940       let rec aux i =
 941         function
 942             [] -> []
 943           | (Some (n,C.Decl t))::tl ->
 944               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 945           | (Some (n,C.Def (t,None)))::tl ->
 946               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 947           | None::tl -> None::(aux (i+1) tl)
 948           | (Some (n,C.Def (t,Some ty)))::tl ->
 949               (Some (n,
 950                      C.Def ((S.subst_meta l (S.lift i t)),
 951                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 952       in
 953         aux 1 canonical_context
 954     in
 955       try
 956         List.fold_left2
 957           (fun (l,subst,metasenv,ugraph) t ct ->
 958              match (t,ct) with
 959                  _,None ->
 960                    l @ [None],subst,metasenv,ugraph
 961                | Some t,Some (_,C.Def (ct,_)) ->
 962                    let subst',metasenv',ugraph' =
 963                    (try
 964 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
 965  * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
 966                       fo_unif_subst subst context metasenv t ct ugraph
 967                     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 ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
 968                    in
 969                      l @ [Some t],subst',metasenv',ugraph'
 970                | Some t,Some (_,C.Decl ct) ->
 971                    let t',inferredty,subst',metasenv',ugraph1 =
 972                      type_of_aux subst metasenv context t ugraph
 973                    in
 974                    let subst'',metasenv'',ugraph2 =
 975                      (try
 976                         fo_unif_subst
 977                           subst' context metasenv' inferredty ct ugraph1
 978                       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 metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
 979                    in
 980                      l @ [Some t'], subst'',metasenv'',ugraph2
 981                | None, Some _  ->
 982                    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 ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
 983       with
 984           Invalid_argument _ ->
 985             raise
 986             (RefineFailure
 987                (lazy (sprintf
 988                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 989                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
 990                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
 991
 992   and check_exp_named_subst metasubst metasenv context tl ugraph =
 993     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 994       match tl with
 995           [] -> [],metasubst,metasenv,ugraph
 996         | (uri,t)::tl ->
 997             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 998             let typeofvar =
 999               CicSubstitution.subst_vars substs ty_uri in
1000               (* CSC: why was this code here? it is wrong
1001                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1002                  Cic.Variable (_,Some bo,_,_) ->
1003                  raise
1004                  (RefineFailure (lazy
1005                  "A variable with a body can not be explicit substituted"))
1006                  | Cic.Variable (_,None,_,_) -> ()
1007                  | _ ->
1008                  raise
1009                  (RefineFailure (lazy
1010                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1011                  ) ;
1012               *)
1013             let t',typeoft,metasubst',metasenv',ugraph2 =
1014               type_of_aux metasubst metasenv context t ugraph1 in
1015             let subst = uri,t' in
1016             let metasubst'',metasenv'',ugraph3 =
1017               try
1018                 fo_unif_subst
1019                   metasubst' context metasenv' typeoft typeofvar ugraph2
1020               with _ ->
1021                 raise (RefineFailure (lazy
1022                          ("Wrong Explicit Named Substitution: " ^
1023                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1024                           " not unifiable with " ^
1025                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1026             in
1027             (* FIXME: no mere tail recursive! *)
1028             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1029               check_exp_named_subst_aux
1030                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1031             in
1032               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1033     in
1034       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1035
1036
1037   and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1038    ugraph
1039   =
1040     let module C = Cic in
1041     let context_for_t2 = (Some (name,C.Decl s))::context in
1042     let t1'' = CicReduction.whd ~subst context t1 in
1043     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1044       match (t1'', t2'') with
1045           (C.Sort s1, C.Sort s2)
1046             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1047               (* different than Coq manual!!! *)
1048               C.Sort s2,subst,metasenv,ugraph
1049         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1050             let t' = CicUniv.fresh() in
1051              (try
1052               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1053               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1054                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1055               with
1056                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1057         | (C.Sort _,C.Sort (C.Type t1)) ->
1058             C.Sort (C.Type t1),subst,metasenv,ugraph
1059         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1060         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1061             (* TODO how can we force the meta to become a sort? If we don't we
1062              * break the invariant that refine produce only well typed terms *)
1063             (* TODO if we check the non meta term and if it is a sort then we
1064              * are likely to know the exact value of the result e.g. if the rhs
1065              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1066             let (metasenv,idx) =
1067               CicMkImplicit.mk_implicit_sort metasenv subst in
1068             let (subst, metasenv,ugraph1) =
1069              try
1070               fo_unif_subst subst context_for_t2 metasenv
1071                 (C.Meta (idx,[])) t2'' ugraph
1072              with _ -> assert false (* unification against a metavariable *)
1073             in
1074               t2'',subst,metasenv,ugraph1
1075         | (C.Sort _,_)
1076         | (C.Meta _,_) ->
1077             enrich localization_tbl s
1078              (RefineFailure
1079                (lazy
1080                  (sprintf
1081                    "%s is supposed to be a type, but its type is %s"
1082                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1083                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1084         | _,_ ->
1085             enrich localization_tbl t
1086              (RefineFailure
1087                (lazy
1088                  (sprintf
1089                    "%s is supposed to be a type, but its type is %s"
1090                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1091                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1092
1093   and avoid_double_coercion context subst metasenv ugraph t ty =
1094    if not !pack_coercions then
1095     t,ty,subst,metasenv,ugraph
1096    else
1097     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1098     if b then
1099       let source_carr = CoercGraph.source_of c2 in
1100       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1101       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1102       with
1103       | CoercGraph.SomeCoercion candidates ->
1104          let selected =
1105            HExtlib.list_findopt
1106              (function (metasenv,last,c) ->
1107                match c with
1108                | c when not (CoercGraph.is_composite c) ->
1109                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1110                    None
1111                | c ->
1112                let subst,metasenv,ugraph =
1113                 fo_unif_subst subst context metasenv last head ugraph in
1114                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1115                (try
1116                  debug_print
1117                    (lazy
1118                      ("packing: " ^
1119                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1120                  let newt,_,subst,metasenv,ugraph =
1121                    type_of_aux subst metasenv context c ugraph in
1122                  debug_print (lazy "tipa...");
1123                  let subst, metasenv, ugraph =
1124                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1125                     fo_unif_subst subst context metasenv newt t ugraph
1126                  in
1127                  debug_print (lazy "unifica...");
1128                  Some (newt, ty, subst, metasenv, ugraph)
1129                with
1130                | RefineFailure s | Uncertain s when not !pack_coercions->
1131                    debug_print s; debug_print (lazy "stop\n");None
1132                | RefineFailure s | Uncertain s ->
1133                    debug_print s;debug_print (lazy "goon\n");
1134                    try
1135                      let old_pack_coercions = !pack_coercions in
1136                      pack_coercions := false; (* to avoid diverging *)
1137                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1138                        type_of_aux subst metasenv context c1_c2_implicit ugraph
1139                      in
1140                      pack_coercions := old_pack_coercions;
1141                      let b, _, _, _, _ =
1142                        is_a_double_coercion refined_c1_c2_implicit
1143                      in
1144                      if b then
1145                        None
1146                      else
1147                        let head' =
1148                          match refined_c1_c2_implicit with
1149                          | Cic.Appl l -> HExtlib.list_last l
1150                          | _ -> assert false
1151                        in
1152                        let subst, metasenv, ugraph =
1153                         try fo_unif_subst subst context metasenv
1154                           head head' ugraph
1155                         with RefineFailure s| Uncertain s->
1156                           debug_print s;assert false
1157                        in
1158                        let subst, metasenv, ugraph =
1159                          fo_unif_subst subst context metasenv
1160                           refined_c1_c2_implicit t ugraph
1161                        in
1162                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1163                    with
1164                    | RefineFailure s | Uncertain s ->
1165                        pack_coercions := true;debug_print s;None
1166                    | exn -> pack_coercions := true; raise exn))
1167              candidates
1168          in
1169          (match selected with
1170          | Some x -> x
1171          | None ->
1172               debug_print
1173                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1174               t, ty, subst, metasenv, ugraph)
1175       | _ -> t, ty, subst, metasenv, ugraph)
1176     else
1177       t, ty, subst, metasenv, ugraph
1178
1179   and typeof_list subst metasenv context ugraph l =
1180     let tlbody_and_type,subst,metasenv,ugraph =
1181       List.fold_right
1182         (fun x (res,subst,metasenv,ugraph) ->
1183            let x',ty,subst',metasenv',ugraph1 =
1184              type_of_aux subst metasenv context x ugraph
1185            in
1186             (x', ty)::res,subst',metasenv',ugraph1
1187         ) l ([],subst,metasenv,ugraph)
1188     in
1189       tlbody_and_type,subst,metasenv,ugraph
1190
1191   and eat_prods
1192     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1193   =
1194     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1195     let fix_arity n metasenv context subst he hetype ugraph =
1196       let hetype = CicMetaSubst.apply_subst subst hetype in
1197       let src = CoercDb.coerc_carr_of_term hetype in
1198       let tgt = CoercDb.Fun 0 in
1199       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1200       | CoercGraph.NoCoercion -> []
1201       | CoercGraph.NotMetaClosed
1202       | CoercGraph.NotHandled _ ->
1203          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1204       | CoercGraph.SomeCoercionToTgt candidates
1205       | CoercGraph.SomeCoercion candidates ->
1206           HExtlib.filter_map
1207             (fun (metasenv,last,coerc) ->
1208               let pp t =
1209                 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1210               let subst,metasenv,ugraph =
1211                fo_unif_subst subst context metasenv last he ugraph in
1212               debug_print (lazy ("New head: "^ pp coerc));
1213               try
1214                 let tty,ugraph =
1215                  CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
1216                 debug_print (lazy (" has type: "^ pp tty));
1217                 Some (coerc,tty,subst,metasenv,ugraph)
1218               with
1219               | Uncertain _ | RefineFailure _
1220               | HExtlib.Localized (_,Uncertain _)
1221               | HExtlib.Localized (_,RefineFailure _) -> None
1222               | exn -> assert false)
1223             candidates
1224     in
1225     (* aux function to process the type of the head and the args in parallel *)
1226     let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1227       function
1228       | [] -> newargs,subst,metasenv,he,hetype,ugraph
1229       | (hete, hety)::tl as args ->
1230           match (CicReduction.whd ~subst context hetype) with
1231           | Cic.Prod (n,s,t) ->
1232               let arg,subst,metasenv,ugraph =
1233                 coerce_to_something allow_coercions localization_tbl
1234                   hete hety s subst metasenv context ugraph in
1235               eat_prods_and_args
1236                 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1237                 ugraph (newargs@[arg]) tl
1238           | _ ->
1239               let he =
1240                 match he, newargs with
1241                 | _, [] -> he
1242                 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1243                 | _ -> Cic.Appl (he::List.map fst newargs)
1244               in
1245               (*{{{*) debug_print (lazy
1246                let pp x =
1247                 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1248                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1249                "\n but is applyed to: " ^ String.concat ";"
1250                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1251               let possible_fixes =
1252                fix_arity (List.length args) metasenv context subst he hetype
1253                 ugraph in
1254               match
1255                 HExtlib.list_findopt
1256                  (fun (he,hetype,subst,metasenv,ugraph) ->
1257                    (* {{{ *)debug_print (lazy ("Try fix: "^
1258                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1259                    debug_print (lazy (" of type: "^
1260                     CicMetaSubst.ppterm_in_context
1261                     ~metasenv subst hetype context)); (* }}} *)
1262                    try
1263                     Some (eat_prods_and_args
1264                       metasenv subst context he hetype ugraph [] args)
1265                    with
1266                     | RefineFailure _ | Uncertain _
1267                     | HExtlib.Localized (_,RefineFailure _)
1268                     | HExtlib.Localized (_,Uncertain _) -> None)
1269                 possible_fixes
1270               with
1271               | Some x -> x
1272               | None ->
1273                  raise
1274                   (MoreArgsThanExpected
1275                     (List.length args, RefineFailure (lazy "")))
1276     in
1277     (* first we check if we are in the simple case of a meta closed term *)
1278     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1279      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1280       (* this optimization is to postpone fix_arity (the most common case)*)
1281       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1282      else
1283        (* this (says CSC) is also useful to infer dependent types *)
1284         let pristinemenv = metasenv in
1285         let metasenv,hetype' =
1286           mk_prod_of_metas metasenv context subst args_bo_and_ty
1287         in
1288         try
1289           let subst,metasenv,ugraph =
1290            fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1291           in
1292           subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1293         with RefineFailure _ | Uncertain _ ->
1294           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1295     in
1296     let coerced_args,subst,metasenv,he,t,ugraph =
1297      try
1298       eat_prods_and_args
1299         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1300      with
1301       MoreArgsThanExpected (residuals,exn) ->
1302         more_args_than_expected localization_tbl metasenv
1303          subst he context hetype' residuals args_bo_and_ty exn
1304     in
1305     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1306
1307   and coerce_to_something
1308     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1309   =
1310     let module CS = CicSubstitution in
1311     let module CR = CicReduction in
1312     let cs_subst = CS.subst ~avoid_beta_redexes:true in
1313     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1314       debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1315       let coer =
1316         CoercGraph.look_for_coercion metasenv subst context infty expty
1317       in
1318       match coer with
1319       | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1320           "coerce_atom_to_something fails since not meta closed"))
1321       | CoercGraph.NoCoercion
1322       | CoercGraph.SomeCoercionToTgt _
1323       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1324           "coerce_atom_to_something fails since no coercions found"))
1325       | CoercGraph.SomeCoercion candidates ->
1326           debug_print (lazy (string_of_int (List.length candidates) ^
1327             " candidates found"));
1328           let uncertain = ref false in
1329           let selected =
1330             let posibilities =
1331               HExtlib.filter_map
1332               (fun (metasenv,last,c) ->
1333                try
1334                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1335                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1336                 " <==> " ^
1337                 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1338                 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1339                 context));
1340                 debug_print (lazy ("FO_UNIF_SUBST: " ^
1341                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1342                 let subst,metasenv,ugraph =
1343                  fo_unif_subst subst context metasenv last t ugraph
1344                 in
1345                 let newt,newhety,subst,metasenv,ugraph =
1346                  type_of_aux subst metasenv context c ugraph in
1347                 let newt, newty, subst, metasenv, ugraph =
1348                  avoid_double_coercion context subst metasenv ugraph newt expty
1349                 in
1350                 let subst,metasenv,ugraph =
1351                   fo_unif_subst subst context metasenv newhety expty ugraph in
1352                  Some ((newt,newty), subst, metasenv, ugraph)
1353                with
1354                | Uncertain _ -> uncertain := true; None
1355                | RefineFailure _ -> None)
1356               candidates
1357             in
1358             match
1359               List.fast_sort
1360                 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1361                 posibilities
1362             with
1363             | [] -> None
1364             | x::_ -> Some x
1365           in
1366           match selected with
1367           | Some x -> x
1368           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1369           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1370     in
1371     let rec coerce_to_something_aux
1372       t infty expty subst metasenv context ugraph
1373     =
1374       try
1375         let subst, metasenv, ugraph =
1376           fo_unif_subst subst context metasenv infty expty ugraph
1377         in
1378         (t, expty), subst, metasenv, ugraph
1379       with Uncertain _ | RefineFailure _ as exn ->
1380         if not allow_coercions || not !insert_coercions then
1381           enrich localization_tbl t exn
1382         else
1383           let whd = CicReduction.whd ~delta:false in
1384           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1385           let infty = clean infty subst context in
1386           let expty = clean expty subst context in
1387           let t = clean t subst context in
1388           (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1389           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1390           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1391           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1392           let (coerced,_),subst,metasenv,_ as result =
1393            match infty, expty, t with
1394            | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1395               (*{{{*) debug_print (lazy "FIX");
1396               (match fl with
1397                   [name,i,_(* infty *),bo] ->
1398                     let context_bo =
1399                      Some (Cic.Name name,Cic.Decl expty)::context in
1400                     let (rel1, _), subst, metasenv, ugraph =
1401                      coerce_to_something_aux (Cic.Rel 1)
1402                        (CS.lift 1 expty) (CS.lift 1 infty) subst
1403                       metasenv context_bo ugraph in
1404                     let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1405                     let (bo,_), subst, metasenv, ugraph =
1406                      coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1407                      expty) subst
1408                       metasenv context_bo ugraph
1409                     in
1410                      (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1411                 | _ -> assert false (* not implemented yet *)) (*}}}*)
1412            | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1413                (*{{{*) debug_print (lazy "CASE");
1414                (* {{{ helper functions *)
1415                let get_cl_and_left_p uri tyno outty ugraph =
1416                  match CicEnvironment.get_obj ugraph uri with
1417                  | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1418                      let count_pis t =
1419                        let rec aux ctx t =
1420                          match CicReduction.whd ~delta:false ctx t with
1421                          | Cic.Prod (name,src,tgt) ->
1422                              let ctx = Some (name, Cic.Decl src) :: ctx in
1423                              1 + aux ctx tgt
1424                          | _ -> 0
1425                        in
1426                          aux [] t
1427                      in
1428                      let rec skip_lambda_delifting t n =
1429                        match t,n with
1430                        | _,0 -> t
1431                        | Cic.Lambda (_,_,t),n ->
1432                            skip_lambda_delifting
1433                              (CS.subst (Cic.Implicit None) t) (n - 1)
1434                        | _ -> assert false
1435                      in
1436                      let get_l_r_p n = function
1437                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1438                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1439                            HExtlib.split_nth n args
1440                        | _ -> assert false
1441                      in
1442                      let _, _, ty, cl = List.nth tl tyno in
1443                      let pis = count_pis ty in
1444                      let rno = pis - leftno in
1445                      let t = skip_lambda_delifting outty rno in
1446                      let left_p, _ = get_l_r_p leftno t in
1447                      let instantiale_with_left cl =
1448                        List.map
1449                          (fun ty ->
1450                            List.fold_left
1451                              (fun t p -> match t with
1452                                | Cic.Prod (_,_,t) ->
1453                                    cs_subst p t
1454                                | _-> assert false)
1455                              ty left_p)
1456                          cl
1457                      in
1458                      let cl = instantiale_with_left (List.map snd cl) in
1459                      cl, left_p, leftno, rno, ugraph
1460                  | _ -> raise exn
1461                in
1462                let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1463                  match t,n with
1464                  | _,0 ->
1465                    let rec mkr n = function
1466                      | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1467                    in
1468                    let bo =
1469                    CicReplace.replace_lifting
1470                      ~equality:(fun _ -> CicUtil.alpha_equivalence)
1471                      ~context:ctx
1472                      ~what:(matched::right_p)
1473                      ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1474                      ~where:bo
1475                    in
1476                    bo
1477                  | Cic.Lambda (name, src, tgt),_ ->
1478                      Cic.Lambda (name, src,
1479                       keep_lambdas_and_put_expty
1480                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1481                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1482                  | _ -> assert false
1483                in
1484                let eq_uri, eq, eq_refl =
1485                  match LibraryObjects.eq_URI () with
1486                  | None -> HLog.warn "no default equality"; raise exn
1487                  | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1488                in
1489                let add_params
1490                  metasenv subst context uri tyno cty outty mty m leftno i
1491                =
1492                  let rec aux context outty par k mty m = function
1493                    | Cic.Prod (name, src, tgt) ->
1494                        let t,k =
1495                          aux
1496                            (Some (name, Cic.Decl src) :: context)
1497                            (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1498                            (CS.lift 1 mty) (CS.lift 1 m) tgt
1499                        in
1500                        Cic.Prod (name, src, t), k
1501                    | Cic.MutInd _ ->
1502                        let k =
1503                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1504                          if par <> [] then Cic.Appl (k::par) else k
1505                        in
1506                        Cic.Prod (Cic.Name "p",
1507                         Cic.Appl [eq; mty; m; k],
1508                         (CS.lift 1
1509                          (CR.head_beta_reduce ~delta:false
1510                           (Cic.Appl [outty;k])))),k
1511                    | Cic.Appl (Cic.MutInd _::pl) ->
1512                        let left_p,right_p = HExtlib.split_nth leftno pl in
1513                        let has_rights = right_p <> [] in
1514                        let k =
1515                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1516                          Cic.Appl (k::left_p@par)
1517                        in
1518                        let right_p =
1519                          try match
1520                            CicTypeChecker.type_of_aux' ~subst metasenv context k
1521                              CicUniv.oblivion_ugraph
1522                          with
1523                          | Cic.Appl (Cic.MutInd _::args),_ ->
1524                              snd (HExtlib.split_nth leftno args)
1525                          | _ -> assert false
1526                          with CicTypeChecker.TypeCheckerFailure _-> assert false
1527                        in
1528                        if has_rights then
1529                          CR.head_beta_reduce ~delta:false
1530                            (Cic.Appl (outty ::right_p @ [k])),k
1531                        else
1532                          Cic.Prod (Cic.Name "p",
1533                           Cic.Appl [eq; mty; m; k],
1534                           (CS.lift 1
1535                            (CR.head_beta_reduce ~delta:false
1536                             (Cic.Appl (outty ::right_p @ [k]))))),k
1537                    | _ -> assert false
1538                  in
1539                    aux context outty [] 1 mty m cty
1540                in
1541                let add_lambda_for_refl_m pbo rno mty m k cty =
1542                  (* k lives in the right context *)
1543                  if rno <> 0 then pbo else
1544                  let rec aux mty m = function
1545                    | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1546                       Cic.Lambda (name,src,
1547                        (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1548                    | t,_ ->
1549                        Cic.Lambda (Cic.Name "p",
1550                          Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1551                  in
1552                  aux mty m (pbo,cty)
1553                in
1554                let add_pi_for_refl_m new_outty mty m rno =
1555                  if rno <> 0 then new_outty else
1556                    let rec aux m mty = function
1557                      | Cic.Lambda (name, src, tgt) ->
1558                          Cic.Lambda (name, src,
1559                            aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1560                      | t ->
1561                          Cic.Prod
1562                            (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1563                            CS.lift 1 t)
1564                    in
1565                      aux m mty new_outty
1566                in (* }}} end helper functions *)
1567                (* constructors types with left params already instantiated *)
1568                let outty = CicMetaSubst.apply_subst subst outty in
1569                let cl, left_p, leftno,rno,ugraph =
1570                  get_cl_and_left_p uri tyno outty ugraph
1571                in
1572                let right_p, mty =
1573                  try
1574                    match
1575                      CicTypeChecker.type_of_aux' ~subst metasenv context m
1576                        CicUniv.oblivion_ugraph
1577                    with
1578                    | Cic.MutInd _ as mty,_ -> [], mty
1579                    | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1580                        snd (HExtlib.split_nth leftno args), mty
1581                    | _ -> assert false
1582                  with CicTypeChecker.TypeCheckerFailure _ -> assert false
1583                in
1584                let new_outty =
1585                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1586                in
1587                debug_print
1588                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1589                   ~metasenv subst new_outty context));
1590                let _,pl,subst,metasenv,ugraph =
1591                  List.fold_right2
1592                    (fun cty pbo (i, acc, s, menv, ugraph) ->
1593                      (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1594                       *   (new_)outty right_par (K_i left_par k_par) *)
1595                       let infty_pbo, _ =
1596                         add_params menv s context uri tyno
1597                           cty outty mty m leftno i in
1598                       debug_print
1599                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1600                         ~metasenv subst infty_pbo context));
1601                       let expty_pbo, k = (* k is (K_i left_par k_par) *)
1602                         add_params menv s context uri tyno
1603                           cty new_outty mty m leftno i in
1604                       debug_print
1605                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1606                         ~metasenv subst expty_pbo context));
1607                       let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1608                       debug_print
1609                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1610                         ~metasenv subst pbo context));
1611                       let (pbo, _), subst, metasenv, ugraph =
1612                         coerce_to_something_aux pbo infty_pbo expty_pbo
1613                           s menv context ugraph
1614                       in
1615                       debug_print
1616                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1617                         ~metasenv subst pbo context));
1618                       (i-1, pbo::acc, subst, metasenv, ugraph))
1619                    cl pl (List.length pl, [], subst, metasenv, ugraph)
1620                in
1621                let new_outty = add_pi_for_refl_m new_outty mty m rno in
1622                debug_print
1623                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1624                   ~metasenv subst new_outty context));
1625                let t =
1626                  if rno = 0 then
1627                    let refl_m=Cic.Appl[eq_refl;mty;m]in
1628                    Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1629                  else
1630                    Cic.MutCase(uri,tyno,new_outty,m,pl)
1631                in
1632                (t, expty), subst, metasenv, ugraph (*}}}*)
1633            | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1634                (*{{{*) debug_print (lazy "LAM");
1635                let name_con =
1636                  FreshNamesGenerator.mk_fresh_name
1637                    ~subst metasenv context ~typ:src2 Cic.Anonymous
1638                in
1639                let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1640                (* contravariant part: the argument of f:src->ty *)
1641                let (rel1, _), subst, metasenv, ugraph =
1642                  coerce_to_something_aux
1643                   (Cic.Rel 1) (CS.lift 1 src2)
1644                   (CS.lift 1 src) subst metasenv context_src2 ugraph
1645                in
1646                (* covariant part: the result of f(c x); x:src2; (c x):src *)
1647                let name_t, bo =
1648                  match t with
1649                  | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1650                  | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1651                in
1652                (* we fix the possible dependency problem in the source ty *)
1653                let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1654                let (bo, _), subst, metasenv, ugraph =
1655                  coerce_to_something_aux
1656                    bo ty ty2 subst metasenv context_src2 ugraph
1657                in
1658                let coerced = Cic.Lambda (name_t,src2, bo) in
1659                (coerced, expty), subst, metasenv, ugraph (*}}}*)
1660            | _ ->
1661                (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1662                 ~metasenv subst infty context ^ " ==> " ^
1663                 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1664                coerce_atom_to_something
1665                t infty expty subst metasenv context ugraph (*}}}*)
1666           in
1667           debug_print (lazy ("COERCE TO SOMETHING END: "^
1668             CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1669           result
1670     in
1671     try
1672       coerce_to_something_aux t infty expty subst metasenv context ugraph
1673     with Uncertain _ | RefineFailure _ as exn ->
1674       let f _ =
1675         lazy ("The term " ^
1676           CicMetaSubst.ppterm_in_context metasenv subst t context ^
1677           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1678           infty context ^ " but is here used with type " ^
1679           CicMetaSubst.ppterm_in_context metasenv subst expty context)
1680       in
1681         enrich localization_tbl ~f t exn
1682
1683   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1684     match CicReduction.whd ~delta:false ~subst context infty with
1685     | Cic.Meta _ | Cic.Sort _ ->
1686         t,infty, subst, metasenv, ugraph
1687     | src ->
1688        debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1689          ~metasenv subst src context));
1690        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1691        try
1692          let (t, ty_t), subst, metasenv, ugraph =
1693            coerce_to_something true
1694              localization_tbl t src tgt subst metasenv context ugraph
1695          in
1696          debug_print (lazy ("COERCE TO SORT END: "^
1697            CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1698          t, ty_t, subst, metasenv, ugraph
1699        with HExtlib.Localized (_, exn) ->
1700          let f _ =
1701            lazy ("(7)The term " ^
1702             CicMetaSubst.ppterm_in_context ~metasenv subst t context
1703             ^ " is not a type since it has type " ^
1704             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1705             ^ " that is not a sort")
1706          in
1707            enrich localization_tbl ~f t exn
1708   in
1709
1710   (* eat prods ends here! *)
1711
1712   let t',ty,subst',metasenv',ugraph1 =
1713    type_of_aux [] metasenv context t ugraph
1714   in
1715   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1716   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1717     (* Andrea: ho rimesso qui l'applicazione della subst al
1718        metasenv dopo che ho droppato l'invariante che il metsaenv
1719        e' sempre istanziato *)
1720   let substituted_metasenv =
1721     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1722     (* metasenv' *)
1723     (*  substituted_t,substituted_ty,substituted_metasenv *)
1724     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1725   let cleaned_t =
1726     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1727   let cleaned_ty =
1728     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1729   let cleaned_metasenv =
1730     List.map
1731       (function (n,context,ty) ->
1732          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1733          let context' =
1734            List.map
1735              (function
1736                   None -> None
1737                 | Some (n, Cic.Decl t) ->
1738                     Some (n,
1739                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1740                 | Some (n, Cic.Def (bo,ty)) ->
1741                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1742                     let ty' =
1743                       match ty with
1744                           None -> None
1745                         | Some ty ->
1746                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1747                     in
1748                       Some (n, Cic.Def (bo',ty'))
1749              ) context
1750          in
1751            (n,context',ty')
1752       ) substituted_metasenv
1753   in
1754     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1755 ;;
1756
1757 let undebrujin uri typesno tys t =
1758   snd
1759    (List.fold_right
1760      (fun (name,_,_,_) (i,t) ->
1761        (* here the explicit_named_substituion is assumed to be *)
1762        (* of length 0 *)
1763        let t' = Cic.MutInd (uri,i,[])  in
1764        let t = CicSubstitution.subst t' t in
1765         i - 1,t
1766      ) tys (typesno - 1,t))
1767
1768 let map_first_n n start f g l =
1769   let rec aux acc k l =
1770     if k < n then
1771       match l with
1772       | [] -> raise (Invalid_argument "map_first_n")
1773       | hd :: tl -> f hd k (aux acc (k+1) tl)
1774     else
1775       g acc l
1776   in
1777   aux start 0 l
1778
1779 (*CSC: this is a very rough approximation; to be finished *)
1780 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1781   let subst,metasenv,ugraph,tys =
1782     List.fold_right
1783       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1784         let subst,metasenv,ugraph,cl =
1785           List.fold_right
1786             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1787                let rec aux ctx k subst = function
1788                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1789                      let subst,metasenv,ugraph,tl =
1790                        map_first_n leftno
1791                          (subst,metasenv,ugraph,[])
1792                          (fun t n (subst,metasenv,ugraph,acc) ->
1793                            let subst,metasenv,ugraph =
1794                              fo_unif_subst
1795                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1796                            in
1797                            subst,metasenv,ugraph,(t::acc))
1798                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1799                          tl
1800                      in
1801                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1802                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1803                      subst,metasenv,ugraph,t
1804                  | Cic.Prod (name,s,t) ->
1805                      let ctx = (Some (name,Cic.Decl s))::ctx in
1806                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1807                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1808                  | _ ->
1809                      raise
1810                       (RefineFailure
1811                         (lazy "not well formed constructor type"))
1812                in
1813                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1814                subst,metasenv,ugraph,(name,ty) :: acc)
1815           cl (subst,metasenv,ugraph,[])
1816         in
1817         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1818       tys ([],metasenv,ugraph,[])
1819   in
1820   let substituted_tys =
1821     List.map
1822       (fun (name,ind,arity,cl) ->
1823         let cl =
1824           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1825         in
1826         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1827       tys
1828   in
1829   metasenv,ugraph,substituted_tys
1830
1831 let typecheck metasenv uri obj ~localization_tbl =
1832  let ugraph = CicUniv.empty_ugraph in
1833  match obj with
1834     Cic.Constant (name,Some bo,ty,args,attrs) ->
1835      let bo',boty,metasenv,ugraph =
1836       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1837      let ty',_,metasenv,ugraph =
1838       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1839      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1840      let bo' = CicMetaSubst.apply_subst subst bo' in
1841      let ty' = CicMetaSubst.apply_subst subst ty' in
1842      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1843       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1844   | Cic.Constant (name,None,ty,args,attrs) ->
1845      let ty',_,metasenv,ugraph =
1846       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1847      in
1848       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1849   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1850      assert (metasenv' = metasenv);
1851      (* Here we do not check the metasenv for correctness *)
1852      let bo',boty,metasenv,ugraph =
1853       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1854      let ty',sort,metasenv,ugraph =
1855       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1856      begin
1857       match sort with
1858          Cic.Sort _
1859        (* instead of raising Uncertain, let's hope that the meta will become
1860           a sort *)
1861        | Cic.Meta _ -> ()
1862        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1863      end;
1864      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1865      let bo' = CicMetaSubst.apply_subst subst bo' in
1866      let ty' = CicMetaSubst.apply_subst subst ty' in
1867      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1868       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1869   | Cic.Variable _ -> assert false (* not implemented *)
1870   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1871      (*CSC: this code is greately simplified and many many checks are missing *)
1872      (*CSC: e.g. the constructors are not required to build their own types,  *)
1873      (*CSC: the arities are not required to have as type a sort, etc.         *)
1874      let uri = match uri with Some uri -> uri | None -> assert false in
1875      let typesno = List.length tys in
1876      (* first phase: we fix only the types *)
1877      let metasenv,ugraph,tys =
1878       List.fold_right
1879        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1880          let ty',_,metasenv,ugraph =
1881           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1882          in
1883           metasenv,ugraph,(name,b,ty',cl)::res
1884        ) tys (metasenv,ugraph,[]) in
1885      let con_context =
1886       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1887      (* second phase: we fix only the constructors *)
1888      let saved_menv = metasenv in
1889      let metasenv,ugraph,tys =
1890       List.fold_right
1891        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1892          let metasenv,ugraph,cl' =
1893           List.fold_right
1894            (fun (name,ty) (metasenv,ugraph,res) ->
1895              let ty =
1896               CicTypeChecker.debrujin_constructor
1897                ~cb:(relocalize localization_tbl) uri typesno ty in
1898              let ty',_,metasenv,ugraph =
1899               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1900              let ty' = undebrujin uri typesno tys ty' in
1901               metasenv@saved_menv,ugraph,(name,ty')::res
1902            ) cl (metasenv,ugraph,[])
1903          in
1904           metasenv,ugraph,(name,b,ty,cl')::res
1905        ) tys (metasenv,ugraph,[]) in
1906      (* third phase: we check the positivity condition *)
1907      let metasenv,ugraph,tys =
1908        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1909      in
1910      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1911 ;;
1912
1913 (* sara' piu' veloce che raffinare da zero? mah.... *)
1914 let pack_coercion metasenv ctx t =
1915  let module C = Cic in
1916  let rec merge_coercions ctx =
1917    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1918    function
1919    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1920    | C.Meta (n,subst) ->
1921       let subst' =
1922        List.map
1923         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1924       in
1925        C.Meta (n,subst')
1926    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1927    | C.Prod (name,so,dest) ->
1928        let ctx' = (Some (name,C.Decl so))::ctx in
1929        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1930    | C.Lambda (name,so,dest) ->
1931        let ctx' = (Some (name,C.Decl so))::ctx in
1932        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1933    | C.LetIn (name,so,dest) ->
1934        let _,ty,metasenv,ugraph =
1935         pack_coercions := false;
1936         type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1937         pack_coercions := true;
1938        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1939        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1940    | C.Appl l ->
1941       let l = List.map (merge_coercions ctx) l in
1942       let t = C.Appl l in
1943        let b,_,_,_,_ = is_a_double_coercion t in
1944        if b then
1945          let ugraph = CicUniv.oblivion_ugraph in
1946          let old_insert_coercions = !insert_coercions in
1947          insert_coercions := false;
1948          let newt, _, menv, _ =
1949            try
1950              type_of_aux' metasenv ctx t ugraph
1951            with RefineFailure _ | Uncertain _ ->
1952              t, t, [], ugraph
1953          in
1954          insert_coercions := old_insert_coercions;
1955          if metasenv <> [] || menv = [] then
1956            newt
1957          else
1958            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1959        else
1960          t
1961    | C.Var (uri,exp_named_subst) ->
1962        let exp_named_subst = List.map aux exp_named_subst in
1963        C.Var (uri, exp_named_subst)
1964    | C.Const (uri,exp_named_subst) ->
1965        let exp_named_subst = List.map aux exp_named_subst in
1966        C.Const (uri, exp_named_subst)
1967    | C.MutInd (uri,tyno,exp_named_subst) ->
1968        let exp_named_subst = List.map aux exp_named_subst in
1969        C.MutInd (uri,tyno,exp_named_subst)
1970    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1971        let exp_named_subst = List.map aux exp_named_subst in
1972        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1973    | C.MutCase (uri,tyno,out,te,pl) ->
1974        let pl = List.map (merge_coercions ctx) pl in
1975        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1976    | C.Fix (fno, fl) ->
1977        let ctx' =
1978          List.fold_left
1979            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1980            ctx fl
1981        in
1982        let fl =
1983          List.map
1984            (fun (name,idx,ty,bo) ->
1985              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1986          fl
1987        in
1988        C.Fix (fno, fl)
1989    | C.CoFix (fno, fl) ->
1990        let ctx' =
1991          List.fold_left
1992            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1993            ctx fl
1994        in
1995        let fl =
1996          List.map
1997            (fun (name,ty,bo) ->
1998              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1999          fl
2000        in
2001        C.CoFix (fno, fl)
2002  in
2003   merge_coercions ctx t
2004 ;;
2005
2006 let pack_coercion_metasenv conjectures = conjectures (*
2007
2008   TASSI: this code war written when coercions were a toy,
2009          now packing coercions involves unification thus
2010          the metasenv may change, and this pack coercion
2011          does not handle that.
2012
2013   let module C = Cic in
2014   List.map
2015     (fun (i, ctx, ty) ->
2016        let ctx =
2017          List.fold_right
2018            (fun item ctx ->
2019               let item' =
2020                 match item with
2021                     Some (name, C.Decl t) ->
2022                       Some (name, C.Decl (pack_coercion conjectures ctx t))
2023                   | Some (name, C.Def (t,None)) ->
2024                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
2025                   | Some (name, C.Def (t,Some ty)) ->
2026                       Some (name, C.Def (pack_coercion conjectures ctx t,
2027                                          Some (pack_coercion conjectures ctx ty)))
2028                   | None -> None
2029               in
2030                 item'::ctx
2031            ) ctx []
2032        in
2033          ((i,ctx,pack_coercion conjectures ctx ty))
2034     ) conjectures
2035     *)
2036 ;;
2037
2038 let pack_coercion_obj obj = obj (*
2039
2040   TASSI: this code war written when coercions were a toy,
2041          now packing coercions involves unification thus
2042          the metasenv may change, and this pack coercion
2043          does not handle that.
2044
2045   let module C = Cic in
2046   match obj with
2047   | C.Constant (id, body, ty, params, attrs) ->
2048       let body =
2049         match body with
2050         | None -> None
2051         | Some body -> Some (pack_coercion [] [] body)
2052       in
2053       let ty = pack_coercion [] [] ty in
2054         C.Constant (id, body, ty, params, attrs)
2055   | C.Variable (name, body, ty, params, attrs) ->
2056       let body =
2057         match body with
2058         | None -> None
2059         | Some body -> Some (pack_coercion [] [] body)
2060       in
2061       let ty = pack_coercion [] [] ty in
2062         C.Variable (name, body, ty, params, attrs)
2063   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2064       let conjectures = pack_coercion_metasenv conjectures in
2065       let body = pack_coercion conjectures [] body in
2066       let ty = pack_coercion conjectures [] ty in
2067       C.CurrentProof (name, conjectures, body, ty, params, attrs)
2068   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2069       let indtys =
2070         List.map
2071           (fun (name, ind, arity, cl) ->
2072             let arity = pack_coercion [] [] arity in
2073             let cl =
2074               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2075             in
2076             (name, ind, arity, cl))
2077           indtys
2078       in
2079         C.InductiveDefinition (indtys, params, leftno, attrs) *)
2080 ;;
2081
2082
2083 (* DEBUGGING ONLY
2084 let type_of_aux' metasenv context term =
2085  try
2086   let (t,ty,m) =
2087       type_of_aux' metasenv context term in
2088     debug_print (lazy
2089      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2090    debug_print (lazy
2091     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2092    (t,ty,m)
2093  with
2094  | RefineFailure msg as e ->
2095      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2096      raise e
2097  | Uncertain msg as e ->
2098      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2099      raise e
2100 ;; *)
2101
2102 let profiler2 = HExtlib.profile "CicRefine"
2103
2104 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2105  profiler2.HExtlib.profile
2106   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2107
2108 let typecheck ~localization_tbl metasenv uri obj =
2109  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2110
2111 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2112 (* vim:set foldmethod=marker: *)