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    prerr_endline ("!!! 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            let rec count_prod t =
 531              match CicReduction.whd ~subst context t with
 532                  C.Prod (_, _, t) -> 1 + (count_prod t)
 533                | _ -> 0
 534            in
 535            let no_args = count_prod arity in
 536              (* now, create a "generic" MutInd *)
 537            let metasenv,left_args =
 538              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 539            in
 540            let metasenv,right_args =
 541              let no_right_params = no_args - no_left_params in
 542                if no_right_params < 0 then assert false
 543                else CicMkImplicit.n_fresh_metas
 544                       metasenv subst context no_right_params
 545            in
 546            let metasenv,exp_named_subst =
 547              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 548            let expected_type =
 549              if no_args = 0 then
 550                C.MutInd (uri,i,exp_named_subst)
 551              else
 552                C.Appl
 553                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 554            in
 555              (* check consistency with the actual type of term *)
 556            let term',actual_type,subst,metasenv,ugraph1 =
 557              type_of_aux subst metasenv context term ugraph in
 558            let expected_type',_, subst, metasenv,ugraph2 =
 559              type_of_aux subst metasenv context expected_type ugraph1
 560            in
 561            let actual_type = CicReduction.whd ~subst context actual_type in
 562            let subst,metasenv,ugraph3 =
 563             try
 564              fo_unif_subst subst context metasenv
 565                expected_type' actual_type ugraph2
 566             with
 567              exn ->
 568               enrich localization_tbl term' exn
 569                ~f:(function _ ->
 570                  lazy ("(10)The term " ^
 571                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
 572                    context ^ " has type " ^
 573                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
 574                    context ^ " but is here used with type " ^
 575                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
 576            in
 577            let rec instantiate_prod t =
 578             function
 579                [] -> t
 580              | he::tl ->
 581                 match CicReduction.whd ~subst context t with
 582                    C.Prod (_,_,t') ->
 583                     instantiate_prod (CicSubstitution.subst he t') tl
 584                  | _ -> assert false
 585            in
 586            let arity_instantiated_with_left_args =
 587             instantiate_prod arity left_args in
 588              (* TODO: check if the sort elimination
 589               * is allowed: [(I q1 ... qr)|B] *)
 590            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 591              List.fold_right
 592                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
 593                   let constructor =
 594                     if left_args = [] then
 595                       (C.MutConstruct (uri,i,j,exp_named_subst))
 596                     else
 597                       (C.Appl
 598                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 599                   in
 600                   let p',actual_type,subst,metasenv,ugraph1 =
 601                     type_of_aux subst metasenv context p ugraph
 602                   in
 603                   let constructor',expected_type, subst, metasenv,ugraph2 =
 604                     type_of_aux subst metasenv context constructor ugraph1
 605                   in
 606                   let outtypeinstance,subst,metasenv,ugraph3 =
 607                    try
 608                     check_branch 0 context metasenv subst
 609                      no_left_params actual_type constructor' expected_type
 610                      ugraph2
 611                    with
 612                     exn ->
 613                      enrich localization_tbl constructor'
 614                       ~f:(fun _ ->
 615                         lazy ("(11)The term " ^
 616                          CicMetaSubst.ppterm_in_context metasenv subst p'
 617                           context ^ " has type " ^
 618                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
 619                           context ^ " but is here used with type " ^
 620                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
 621                           context)) exn
 622                   in
 623                     (p'::pl,j-1,
 624                      outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
 625                pl ([],List.length pl,[],subst,metasenv,ugraph3)
 626            in
 627
 628              (* we are left to check that the outype matches his instances.
 629                 The easy case is when the outype is specified, that amount
 630                 to a trivial check. Otherwise, we should guess a type from
 631                 its instances
 632              *)
 633
 634            let outtype,outtypety, subst, metasenv,ugraph4 =
 635              type_of_aux subst metasenv context outtype ugraph4 in
 636            (match outtype with
 637            | C.Meta (n,l) ->
 638                (let candidate,ugraph5,metasenv,subst =
 639                  let exp_name_subst, metasenv =
 640                     let o,_ =
 641                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 642                     in
 643                     let uris = CicUtil.params_of_obj o in
 644                     List.fold_right (
 645                       fun uri (acc,metasenv) ->
 646                         let metasenv',new_meta =
 647                            CicMkImplicit.mk_implicit metasenv subst context
 648                         in
 649                         let irl =
 650                           CicMkImplicit.identity_relocation_list_for_metavariable
 651                             context
 652                         in
 653                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 654                     ) uris ([],metasenv)
 655                  in
 656                  let ty =
 657                   match left_args,right_args with
 658                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 659                    | _,_ ->
 660                       let rec mk_right_args =
 661                        function
 662                           0 -> []
 663                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 664                       in
 665                       let right_args_no = List.length right_args in
 666                       let lifted_left_args =
 667                        List.map (CicSubstitution.lift right_args_no) left_args
 668                       in
 669                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 670                         (lifted_left_args @ mk_right_args right_args_no))
 671                  in
 672                  let fresh_name =
 673                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 674                      context Cic.Anonymous ~typ:ty
 675                  in
 676                  match outtypeinstances with
 677                  | [] ->
 678                      let extended_context =
 679                       let rec add_right_args =
 680                        function
 681                           Cic.Prod (name,ty,t) ->
 682                            Some (name,Cic.Decl ty)::(add_right_args t)
 683                         | _ -> []
 684                       in
 685                        (Some (fresh_name,Cic.Decl ty))::
 686                        (List.rev
 687                         (add_right_args arity_instantiated_with_left_args))@
 688                        context
 689                      in
 690                      let metasenv,new_meta =
 691                        CicMkImplicit.mk_implicit metasenv subst extended_context
 692                      in
 693                        let irl =
 694                        CicMkImplicit.identity_relocation_list_for_metavariable
 695                          extended_context
 696                      in
 697                      let rec add_lambdas b =
 698                       function
 699                          Cic.Prod (name,ty,t) ->
 700                           Cic.Lambda (name,ty,(add_lambdas b t))
 701                        | _ -> Cic.Lambda (fresh_name, ty, b)
 702                      in
 703                      let candidate =
 704                       add_lambdas (Cic.Meta (new_meta,irl))
 705                        arity_instantiated_with_left_args
 706                      in
 707                      (Some candidate),ugraph4,metasenv,subst
 708                  | (constructor_args_no,_,instance,_)::tl ->
 709                      try
 710                        let instance',subst,metasenv =
 711                          CicMetaSubst.delift_rels subst metasenv
 712                           constructor_args_no instance
 713                        in
 714                        let candidate,ugraph,metasenv,subst =
 715                          List.fold_left (
 716                            fun (candidate_oty,ugraph,metasenv,subst)
 717                              (constructor_args_no,_,instance,_) ->
 718                                match candidate_oty with
 719                                | None -> None,ugraph,metasenv,subst
 720                                | Some ty ->
 721                                  try
 722                                    let instance',subst,metasenv =
 723                                      CicMetaSubst.delift_rels subst metasenv
 724                                       constructor_args_no instance
 725                                    in
 726                                    let subst,metasenv,ugraph =
 727                                     fo_unif_subst subst context metasenv
 728                                       instance' ty ugraph
 729                                    in
 730                                     candidate_oty,ugraph,metasenv,subst
 731                                  with
 732                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 733                                   | RefineFailure _ | Uncertain _ ->
 734                                      None,ugraph,metasenv,subst
 735                          ) (Some instance',ugraph4,metasenv,subst) tl
 736                        in
 737                        match candidate with
 738                        | None -> None, ugraph,metasenv,subst
 739                        | Some t ->
 740                           let rec add_lambdas n b =
 741                            function
 742                               Cic.Prod (name,ty,t) ->
 743                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 744                             | _ ->
 745                               Cic.Lambda (fresh_name, ty,
 746                                CicSubstitution.lift (n + 1) t)
 747                           in
 748                            Some
 749                             (add_lambdas 0 t arity_instantiated_with_left_args),
 750                            ugraph,metasenv,subst
 751                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 752                        None,ugraph4,metasenv,subst
 753                in
 754                match candidate with
 755                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 756                | Some candidate ->
 757                    let subst,metasenv,ugraph =
 758                     try
 759                      fo_unif_subst subst context metasenv
 760                        candidate outtype ugraph5
 761                     with
 762                      exn -> assert false(* unification against a metavariable *)
 763                    in
 764                      C.MutCase (uri, i, outtype, term', pl'),
 765                       CicReduction.head_beta_reduce
 766                        (CicMetaSubst.apply_subst subst
 767                         (Cic.Appl (outtype::right_args@[term']))),
 768                      subst,metasenv,ugraph)
 769            | _ ->    (* easy case *)
 770              let tlbody_and_type,subst,metasenv,ugraph4 =
 771                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
 772              in
 773              let _,_,_,subst,metasenv,ugraph4 =
 774                eat_prods false subst metasenv context
 775                  outtype outtypety tlbody_and_type ugraph4
 776              in
 777              let _,_, subst, metasenv,ugraph5 =
 778                type_of_aux subst metasenv context
 779                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 780              in
 781              let (subst,metasenv,ugraph6) =
 782                List.fold_left2
 783                  (fun (subst,metasenv,ugraph)
 784                    p (constructor_args_no,context,instance,args)
 785                   ->
 786                     let instance' =
 787                       let appl =
 788                         let outtype' =
 789                           CicSubstitution.lift constructor_args_no outtype
 790                         in
 791                           C.Appl (outtype'::args)
 792                       in
 793                         CicReduction.whd ~subst context appl
 794                     in
 795                      try
 796                       fo_unif_subst subst context metasenv instance instance'
 797                        ugraph
 798                      with
 799                       exn ->
 800                        enrich localization_tbl p exn
 801                         ~f:(function _ ->
 802                           lazy ("(12)The term " ^
 803                            CicMetaSubst.ppterm_in_context ~metasenv subst p
 804                             context ^ " has type " ^
 805                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
 806                             context ^ " but is here used with type " ^
 807                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
 808                             context)))
 809                  (subst,metasenv,ugraph5) pl' outtypeinstances
 810              in
 811                C.MutCase (uri, i, outtype, term', pl'),
 812                  CicReduction.head_beta_reduce
 813                   (CicMetaSubst.apply_subst subst
 814                    (C.Appl(outtype::right_args@[term]))),
 815                  subst,metasenv,ugraph6)
 816         | C.Fix (i,fl) ->
 817             let fl_ty',subst,metasenv,types,ugraph1,len =
 818               List.fold_left
 819                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
 820                    let ty',_,subst',metasenv',ugraph1 =
 821                       type_of_aux subst metasenv context ty ugraph
 822                    in
 823                      fl @ [ty'],subst',metasenv',
 824                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
 825                         :: types, ugraph, len+1
 826                 ) ([],subst,metasenv,[],ugraph,0) fl
 827             in
 828             let context' = types@context in
 829             let fl_bo',subst,metasenv,ugraph2 =
 830               List.fold_left
 831                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 832                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 833                      type_of_aux subst metasenv context' bo ugraph in
 834                    let expected_ty = CicSubstitution.lift len ty in
 835                    let subst',metasenv',ugraph' =
 836                     try
 837                      fo_unif_subst subst context' metasenv
 838                        ty_of_bo expected_ty ugraph1
 839                     with
 840                      exn ->
 841                       enrich localization_tbl bo exn
 842                        ~f:(function _ ->
 843                          lazy ("(13)The term " ^
 844                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 845                            context' ^ " has type " ^
 846                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 847                            context' ^ " but is here used with type " ^
 848                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 849                            context))
 850                    in
 851                      fl @ [bo'] , subst',metasenv',ugraph'
 852                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 853             in
 854             let ty = List.nth fl_ty' i in
 855             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 856              * and we want the new fl with bo' and ty' injected in the right
 857              * place.
 858              *)
 859             let rec map3 f l1 l2 l3 =
 860               match l1,l2,l3 with
 861               | [],[],[] -> []
 862               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 863               | _ -> assert false
 864             in
 865             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 866               fl_ty' fl_bo' fl
 867             in
 868               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 869         | C.CoFix (i,fl) ->
 870             let fl_ty',subst,metasenv,types,ugraph1,len =
 871               List.fold_left
 872                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
 873                    let ty',_,subst',metasenv',ugraph1 =
 874                      type_of_aux subst metasenv context ty ugraph
 875                    in
 876                      fl @ [ty'],subst',metasenv',
 877                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
 878                         types, ugraph1, len+1
 879                 ) ([],subst,metasenv,[],ugraph,0) fl
 880             in
 881             let context' = types@context in
 882             let fl_bo',subst,metasenv,ugraph2 =
 883               List.fold_left
 884                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 885                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 886                      type_of_aux subst metasenv context' bo ugraph in
 887                    let expected_ty = CicSubstitution.lift len ty in
 888                    let subst',metasenv',ugraph' =
 889                     try
 890                      fo_unif_subst subst context' metasenv
 891                        ty_of_bo expected_ty ugraph1
 892                     with
 893                      exn ->
 894                       enrich localization_tbl bo exn
 895                        ~f:(function _ ->
 896                          lazy ("(14)The term " ^
 897                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 898                            context' ^ " has type " ^
 899                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 900                            context' ^ " but is here used with type " ^
 901                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 902                            context))
 903                    in
 904                      fl @ [bo'],subst',metasenv',ugraph'
 905                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 906             in
 907             let ty = List.nth fl_ty' i in
 908             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 909              * and we want the new fl with bo' and ty' injected in the right
 910              * place.
 911              *)
 912             let rec map3 f l1 l2 l3 =
 913               match l1,l2,l3 with
 914               | [],[],[] -> []
 915               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 916               | _ -> assert false
 917             in
 918             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 919               fl_ty' fl_bo' fl
 920             in
 921               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 922      in
 923       relocalize localization_tbl t t';
 924       res
 925
 926   (* check_metasenv_consistency checks that the "canonical" context of a
 927      metavariable is consitent - up to relocation via the relocation list l -
 928      with the actual context *)
 929   and check_metasenv_consistency
 930     metano subst metasenv context canonical_context l ugraph
 931     =
 932     let module C = Cic in
 933     let module R = CicReduction in
 934     let module S = CicSubstitution in
 935     let lifted_canonical_context =
 936       let rec aux i =
 937         function
 938             [] -> []
 939           | (Some (n,C.Decl t))::tl ->
 940               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 941           | (Some (n,C.Def (t,None)))::tl ->
 942               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 943           | None::tl -> None::(aux (i+1) tl)
 944           | (Some (n,C.Def (t,Some ty)))::tl ->
 945               (Some (n,
 946                      C.Def ((S.subst_meta l (S.lift i t)),
 947                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 948       in
 949         aux 1 canonical_context
 950     in
 951       try
 952         List.fold_left2
 953           (fun (l,subst,metasenv,ugraph) t ct ->
 954              match (t,ct) with
 955                  _,None ->
 956                    l @ [None],subst,metasenv,ugraph
 957                | Some t,Some (_,C.Def (ct,_)) ->
 958                    let subst',metasenv',ugraph' =
 959                    (try
 960 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
 961                       fo_unif_subst subst context metasenv t ct ugraph
 962                     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))))))
 963                    in
 964                      l @ [Some t],subst',metasenv',ugraph'
 965                | Some t,Some (_,C.Decl ct) ->
 966                    let t',inferredty,subst',metasenv',ugraph1 =
 967                      type_of_aux subst metasenv context t ugraph
 968                    in
 969                    let subst'',metasenv'',ugraph2 =
 970                      (try
 971                         fo_unif_subst
 972                           subst' context metasenv' inferredty ct ugraph1
 973                       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))))))
 974                    in
 975                      l @ [Some t'], subst'',metasenv'',ugraph2
 976                | None, Some _  ->
 977                    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
 978       with
 979           Invalid_argument _ ->
 980             raise
 981             (RefineFailure
 982                (lazy (sprintf
 983                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 984                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
 985                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
 986
 987   and check_exp_named_subst metasubst metasenv context tl ugraph =
 988     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 989       match tl with
 990           [] -> [],metasubst,metasenv,ugraph
 991         | (uri,t)::tl ->
 992             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 993             let typeofvar =
 994               CicSubstitution.subst_vars substs ty_uri in
 995               (* CSC: why was this code here? it is wrong
 996                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 997                  Cic.Variable (_,Some bo,_,_) ->
 998                  raise
 999                  (RefineFailure (lazy
1000                  "A variable with a body can not be explicit substituted"))
1001                  | Cic.Variable (_,None,_,_) -> ()
1002                  | _ ->
1003                  raise
1004                  (RefineFailure (lazy
1005                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1006                  ) ;
1007               *)
1008             let t',typeoft,metasubst',metasenv',ugraph2 =
1009               type_of_aux metasubst metasenv context t ugraph1 in
1010             let subst = uri,t' in
1011             let metasubst'',metasenv'',ugraph3 =
1012               try
1013                 fo_unif_subst
1014                   metasubst' context metasenv' typeoft typeofvar ugraph2
1015               with _ ->
1016                 raise (RefineFailure (lazy
1017                          ("Wrong Explicit Named Substitution: " ^
1018                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1019                           " not unifiable with " ^
1020                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1021             in
1022             (* FIXME: no mere tail recursive! *)
1023             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1024               check_exp_named_subst_aux
1025                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1026             in
1027               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1028     in
1029       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1030
1031
1032   and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1033    ugraph
1034   =
1035     let module C = Cic in
1036     let context_for_t2 = (Some (name,C.Decl s))::context in
1037     let t1'' = CicReduction.whd ~subst context t1 in
1038     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1039       match (t1'', t2'') with
1040           (C.Sort s1, C.Sort s2)
1041             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1042               (* different than Coq manual!!! *)
1043               C.Sort s2,subst,metasenv,ugraph
1044         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1045             let t' = CicUniv.fresh() in
1046              (try
1047               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1048               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1049                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1050               with
1051                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1052         | (C.Sort _,C.Sort (C.Type t1)) ->
1053             C.Sort (C.Type t1),subst,metasenv,ugraph
1054         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1055         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1056             (* TODO how can we force the meta to become a sort? If we don't we
1057              * break the invariant that refine produce only well typed terms *)
1058             (* TODO if we check the non meta term and if it is a sort then we
1059              * are likely to know the exact value of the result e.g. if the rhs
1060              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1061             let (metasenv,idx) =
1062               CicMkImplicit.mk_implicit_sort metasenv subst in
1063             let (subst, metasenv,ugraph1) =
1064              try
1065               fo_unif_subst subst context_for_t2 metasenv
1066                 (C.Meta (idx,[])) t2'' ugraph
1067              with _ -> assert false (* unification against a metavariable *)
1068             in
1069               t2'',subst,metasenv,ugraph1
1070         | (C.Sort _,_)
1071         | (C.Meta _,_) ->
1072             enrich localization_tbl s
1073              (RefineFailure
1074                (lazy
1075                  (sprintf
1076                    "%s is supposed to be a type, but its type is %s"
1077                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1078                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1079         | _,_ ->
1080             enrich localization_tbl t
1081              (RefineFailure
1082                (lazy
1083                  (sprintf
1084                    "%s is supposed to be a type, but its type is %s"
1085                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1086                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1087
1088   and avoid_double_coercion context subst metasenv ugraph t ty =
1089    if not !pack_coercions then
1090     t,ty,subst,metasenv,ugraph
1091    else
1092     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1093     if b then
1094       let source_carr = CoercGraph.source_of c2 in
1095       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1096       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1097       with
1098       | CoercGraph.SomeCoercion candidates ->
1099          let selected =
1100            HExtlib.list_findopt
1101              (function (metasenv,last,c) ->
1102                match c with
1103                | c when not (CoercGraph.is_composite c) ->
1104                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1105                    None
1106                | c ->
1107                let subst,metasenv,ugraph =
1108                 fo_unif_subst subst context metasenv last head ugraph in
1109                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1110                (try
1111                  debug_print
1112                    (lazy
1113                      ("packing: " ^
1114                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1115                  let newt,_,subst,metasenv,ugraph =
1116                    type_of_aux subst metasenv context c ugraph in
1117                  debug_print (lazy "tipa...");
1118                  let subst, metasenv, ugraph =
1119                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1120                     fo_unif_subst subst context metasenv newt t ugraph
1121                  in
1122                  debug_print (lazy "unifica...");
1123                  Some (newt, ty, subst, metasenv, ugraph)
1124                with
1125                | RefineFailure s | Uncertain s when not !pack_coercions->
1126                    debug_print s; debug_print (lazy "stop\n");None
1127                | RefineFailure s | Uncertain s ->
1128                    debug_print s;debug_print (lazy "goon\n");
1129                    try
1130                      let old_pack_coercions = !pack_coercions in
1131                      pack_coercions := false; (* to avoid diverging *)
1132                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1133                        type_of_aux subst metasenv context c1_c2_implicit ugraph
1134                      in
1135                      pack_coercions := old_pack_coercions;
1136                      let b, _, _, _, _ =
1137                        is_a_double_coercion refined_c1_c2_implicit
1138                      in
1139                      if b then
1140                        None
1141                      else
1142                        let head' =
1143                          match refined_c1_c2_implicit with
1144                          | Cic.Appl l -> HExtlib.list_last l
1145                          | _ -> assert false
1146                        in
1147                        let subst, metasenv, ugraph =
1148                         try fo_unif_subst subst context metasenv
1149                           head head' ugraph
1150                         with RefineFailure s| Uncertain s->
1151                           debug_print s;assert false
1152                        in
1153                        let subst, metasenv, ugraph =
1154                          fo_unif_subst subst context metasenv
1155                           refined_c1_c2_implicit t ugraph
1156                        in
1157                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1158                    with
1159                    | RefineFailure s | Uncertain s ->
1160                        pack_coercions := true;debug_print s;None
1161                    | exn -> pack_coercions := true; raise exn))
1162              candidates
1163          in
1164          (match selected with
1165          | Some x -> x
1166          | None ->
1167               debug_print
1168                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1169               t, ty, subst, metasenv, ugraph)
1170       | _ -> t, ty, subst, metasenv, ugraph)
1171     else
1172       t, ty, subst, metasenv, ugraph
1173
1174   and typeof_list subst metasenv context ugraph l =
1175     let tlbody_and_type,subst,metasenv,ugraph =
1176       List.fold_right
1177         (fun x (res,subst,metasenv,ugraph) ->
1178            let x',ty,subst',metasenv',ugraph1 =
1179              type_of_aux subst metasenv context x ugraph
1180            in
1181             (x', ty)::res,subst',metasenv',ugraph1
1182         ) l ([],subst,metasenv,ugraph)
1183     in
1184       tlbody_and_type,subst,metasenv,ugraph
1185
1186   and eat_prods
1187     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1188   =
1189     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1190     let fix_arity n metasenv context subst he hetype ugraph =
1191       let hetype = CicMetaSubst.apply_subst subst hetype in
1192       let src = CoercDb.coerc_carr_of_term hetype in
1193       let tgt = CoercDb.Fun 0 in
1194       match CoercGraph.look_for_coercion' metasenv subst context src tgt with
1195       | CoercGraph.NoCoercion -> []
1196       | CoercGraph.NotMetaClosed
1197       | CoercGraph.NotHandled _ ->
1198          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1199       | CoercGraph.SomeCoercionToTgt candidates
1200       | CoercGraph.SomeCoercion candidates ->
1201           HExtlib.filter_map
1202             (fun (metasenv,last,coerc) ->
1203               let pp t =
1204                 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1205               let subst,metasenv,ugraph =
1206                fo_unif_subst subst context metasenv last he ugraph in
1207               debug_print (lazy ("New head: "^ pp coerc));
1208               try
1209                 let tty,ugraph =
1210                  CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
1211                 debug_print (lazy (" has type: "^ pp tty));
1212                 Some (coerc,tty,subst,metasenv,ugraph)
1213               with
1214               | Uncertain _ | RefineFailure _
1215               | HExtlib.Localized (_,Uncertain _)
1216               | HExtlib.Localized (_,RefineFailure _) -> None
1217               | exn -> assert false)
1218             candidates
1219     in
1220     (* aux function to process the type of the head and the args in parallel *)
1221     let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1222       function
1223       | [] -> newargs,subst,metasenv,he,hetype,ugraph
1224       | (hete, hety)::tl as args ->
1225           match (CicReduction.whd ~subst context hetype) with
1226           | Cic.Prod (n,s,t) ->
1227               let arg,subst,metasenv,ugraph =
1228                 coerce_to_something allow_coercions localization_tbl
1229                   hete hety s subst metasenv context ugraph in
1230               eat_prods_and_args
1231                 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1232                 ugraph (newargs@[arg]) tl
1233           | _ ->
1234               let he =
1235                 match he, newargs with
1236                 | _, [] -> he
1237                 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1238                 | _ -> Cic.Appl (he::List.map fst newargs)
1239               in
1240               (*{{{*) debug_print (lazy
1241                let pp x =
1242                 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1243                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1244                "\n but is applyed to: " ^ String.concat ";"
1245                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1246               let possible_fixes =
1247                fix_arity (List.length args) metasenv context subst he hetype
1248                 ugraph in
1249               match
1250                 HExtlib.list_findopt
1251                  (fun (he,hetype,subst,metasenv,ugraph) ->
1252                    (* {{{ *)debug_print (lazy ("Try fix: "^
1253                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1254                    debug_print (lazy (" of type: "^
1255                     CicMetaSubst.ppterm_in_context
1256                     ~metasenv subst hetype context)); (* }}} *)
1257                    try
1258                     Some (eat_prods_and_args
1259                       metasenv subst context he hetype ugraph [] args)
1260                    with
1261                     | RefineFailure _ | Uncertain _
1262                     | HExtlib.Localized (_,RefineFailure _)
1263                     | HExtlib.Localized (_,Uncertain _) -> None)
1264                 possible_fixes
1265               with
1266               | Some x -> x
1267               | None ->
1268                  raise
1269                   (MoreArgsThanExpected
1270                     (List.length args, RefineFailure (lazy "")))
1271     in
1272     (* first we check if we are in the simple case of a meta closed term *)
1273     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1274      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1275       (* this optimization is to postpone fix_arity (the most common case)*)
1276       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1277      else
1278        (* this (says CSC) is also useful to infer dependent types *)
1279         let pristinemenv = metasenv in
1280         let metasenv,hetype' =
1281           mk_prod_of_metas metasenv context subst args_bo_and_ty
1282         in
1283         try
1284           let subst,metasenv,ugraph =
1285            fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1286           in
1287           subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1288         with RefineFailure _ | Uncertain _ ->
1289           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1290     in
1291     let coerced_args,subst,metasenv,he,t,ugraph =
1292      try
1293       eat_prods_and_args
1294         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1295      with
1296       MoreArgsThanExpected (residuals,exn) ->
1297         more_args_than_expected localization_tbl metasenv
1298          subst he context hetype' residuals args_bo_and_ty exn
1299     in
1300     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1301
1302   and coerce_to_something
1303     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1304   =
1305     let module CS = CicSubstitution in
1306     let module CR = CicReduction in
1307     let cs_subst = CS.subst ~avoid_beta_redexes:true in
1308     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1309       debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1310       let coer =
1311         CoercGraph.look_for_coercion metasenv subst context infty expty
1312       in
1313       match coer with
1314       | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1315           "coerce_atom_to_something fails since not meta closed"))
1316       | CoercGraph.NoCoercion
1317       | CoercGraph.SomeCoercionToTgt _
1318       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1319           "coerce_atom_to_something fails since no coercions found"))
1320       | CoercGraph.SomeCoercion candidates ->
1321           debug_print (lazy (string_of_int (List.length candidates) ^
1322             " candidates found"));
1323           let uncertain = ref false in
1324           let selected =
1325             let posibilities =
1326               HExtlib.filter_map
1327               (fun (metasenv,last,c) ->
1328                try
1329                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1330                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1331                 " <==> " ^
1332                 CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1333                 debug_print (lazy ("FO_UNIF_SUBST: " ^
1334                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1335                 let subst,metasenv,ugraph =
1336                  fo_unif_subst subst context metasenv last t ugraph
1337                 in
1338                 let newt,newhety,subst,metasenv,ugraph =
1339                  type_of_aux subst metasenv context c ugraph in
1340                 let newt, newty, subst, metasenv, ugraph =
1341                  avoid_double_coercion context subst metasenv ugraph newt expty
1342                 in
1343                 let subst,metasenv,ugraph =
1344                   fo_unif_subst subst context metasenv newhety expty ugraph in
1345                  Some ((newt,newty), subst, metasenv, ugraph)
1346                with
1347                | Uncertain _ -> uncertain := true; None
1348                | RefineFailure _ -> None)
1349               candidates
1350             in
1351             match
1352               List.fast_sort
1353                 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1354                 posibilities
1355             with
1356             | [] -> None
1357             | x::_ -> Some x
1358           in
1359           match selected with
1360           | Some x -> x
1361           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1362           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1363     in
1364     let rec coerce_to_something_aux
1365       t infty expty subst metasenv context ugraph
1366     =
1367       try
1368         let subst, metasenv, ugraph =
1369           fo_unif_subst subst context metasenv infty expty ugraph
1370         in
1371         (t, expty), subst, metasenv, ugraph
1372       with Uncertain _ | RefineFailure _ as exn ->
1373         if not allow_coercions || not !insert_coercions then
1374           enrich localization_tbl t exn
1375         else
1376           let whd = CicReduction.whd ~delta:false in
1377           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1378           let infty = clean infty subst context in
1379           let expty = clean expty subst context in
1380           let t = clean t subst context in
1381           (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1382           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1383           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1384           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1385           let (coerced,_),subst,metasenv,_ as result =
1386            match infty, expty, t with
1387            | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1388               (*{{{*) debug_print (lazy "FIX");
1389               (match fl with
1390                   [name,i,_(* infty *),bo] ->
1391                     let context_bo =
1392                      Some (Cic.Name name,Cic.Decl expty)::context in
1393                     let (rel1, _), subst, metasenv, ugraph =
1394                      coerce_to_something_aux (Cic.Rel 1)
1395                        (CS.lift 1 expty) (CS.lift 1 infty) subst
1396                       metasenv context_bo ugraph in
1397                     let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1398                     let (bo,_), subst, metasenv, ugraph =
1399                      coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1400                      expty) subst
1401                       metasenv context_bo ugraph
1402                     in
1403                      (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1404                 | _ -> assert false (* not implemented yet *)) (*}}}*)
1405            | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1406                (*{{{*) debug_print (lazy "CASE");
1407                (* {{{ helper functions *)
1408                let get_cl_and_left_p uri tyno outty ugraph =
1409                  match CicEnvironment.get_obj ugraph uri with
1410                  | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1411                      let count_pis t =
1412                        let rec aux ctx t =
1413                          match CicReduction.whd ~delta:false ctx t with
1414                          | Cic.Prod (name,src,tgt) ->
1415                              let ctx = Some (name, Cic.Decl src) :: ctx in
1416                              1 + aux ctx tgt
1417                          | _ -> 0
1418                        in
1419                          aux [] t
1420                      in
1421                      let rec skip_lambda_delifting t n =
1422                        match t,n with
1423                        | _,0 -> t
1424                        | Cic.Lambda (_,_,t),n ->
1425                            skip_lambda_delifting
1426                              (CS.subst (Cic.Implicit None) t) (n - 1)
1427                        | _ -> assert false
1428                      in
1429                      let get_l_r_p n = function
1430                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1431                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1432                            HExtlib.split_nth n args
1433                        | _ -> assert false
1434                      in
1435                      let _, _, ty, cl = List.nth tl tyno in
1436                      let pis = count_pis ty in
1437                      let rno = pis - leftno in
1438                      let t = skip_lambda_delifting outty rno in
1439                      let left_p, _ = get_l_r_p leftno t in
1440                      let instantiale_with_left cl =
1441                        List.map
1442                          (fun ty ->
1443                            List.fold_left
1444                              (fun t p -> match t with
1445                                | Cic.Prod (_,_,t) ->
1446                                    cs_subst p t
1447                                | _-> assert false)
1448                              ty left_p)
1449                          cl
1450                      in
1451                      let cl = instantiale_with_left (List.map snd cl) in
1452                      cl, left_p, leftno, rno, ugraph
1453                  | _ -> raise exn
1454                in
1455                let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1456                  match t,n with
1457                  | _,0 ->
1458                    let rec mkr n = function
1459                      | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1460                    in
1461                    let bo =
1462                    CicReplace.replace_lifting
1463                      ~equality:(fun _ -> CicUtil.alpha_equivalence)
1464                      ~context:ctx
1465                      ~what:(matched::right_p)
1466                      ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1467                      ~where:bo
1468                    in
1469                    bo
1470                  | Cic.Lambda (name, src, tgt),_ ->
1471                      Cic.Lambda (name, src,
1472                       keep_lambdas_and_put_expty
1473                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1474                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1475                  | _ -> assert false
1476                in
1477                let eq_uri, eq, eq_refl =
1478                  match LibraryObjects.eq_URI () with
1479                  | None -> HLog.warn "no default equality"; raise exn
1480                  | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1481                in
1482                let add_params
1483                  metasenv subst context uri tyno cty outty mty m leftno i
1484                =
1485                  let rec aux context outty par k mty m = function
1486                    | Cic.Prod (name, src, tgt) ->
1487                        let t,k =
1488                          aux
1489                            (Some (name, Cic.Decl src) :: context)
1490                            (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1491                            (CS.lift 1 mty) (CS.lift 1 m) tgt
1492                        in
1493                        Cic.Prod (name, src, t), k
1494                    | Cic.MutInd _ ->
1495                        let k =
1496                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1497                          if par <> [] then Cic.Appl (k::par) else k
1498                        in
1499                        Cic.Prod (Cic.Name "p",
1500                         Cic.Appl [eq; mty; m; k],
1501                         (CS.lift 1
1502                          (CR.head_beta_reduce ~delta:false
1503                           (Cic.Appl [outty;k])))),k
1504                    | Cic.Appl (Cic.MutInd _::pl) ->
1505                        let left_p,right_p = HExtlib.split_nth leftno pl in
1506                        let has_rights = right_p <> [] in
1507                        let k =
1508                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1509                          Cic.Appl (k::left_p@par)
1510                        in
1511                        let right_p =
1512                          try match
1513                            CicTypeChecker.type_of_aux' ~subst metasenv context k
1514                              CicUniv.oblivion_ugraph
1515                          with
1516                          | Cic.Appl (Cic.MutInd _::args),_ ->
1517                              snd (HExtlib.split_nth leftno args)
1518                          | _ -> assert false
1519                          with CicTypeChecker.TypeCheckerFailure _-> assert false
1520                        in
1521                        if has_rights then
1522                          CR.head_beta_reduce ~delta:false
1523                            (Cic.Appl (outty ::right_p @ [k])),k
1524                        else
1525                          Cic.Prod (Cic.Name "p",
1526                           Cic.Appl [eq; mty; m; k],
1527                           (CS.lift 1
1528                            (CR.head_beta_reduce ~delta:false
1529                             (Cic.Appl (outty ::right_p @ [k]))))),k
1530                    | _ -> assert false
1531                  in
1532                    aux context outty [] 1 mty m cty
1533                in
1534                let add_lambda_for_refl_m pbo rno mty m k cty =
1535                  (* k lives in the right context *)
1536                  if rno <> 0 then pbo else
1537                  let rec aux mty m = function
1538                    | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
1539                       Cic.Lambda (name,src,
1540                        (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
1541                    | t,_ ->
1542                        Cic.Lambda (Cic.Name "p",
1543                          Cic.Appl [eq; mty; m; k],CS.lift 1 t)
1544                  in
1545                  aux mty m (pbo,cty)
1546                in
1547                let add_pi_for_refl_m new_outty mty m rno =
1548                  if rno <> 0 then new_outty else
1549                    let rec aux m mty = function
1550                      | Cic.Lambda (name, src, tgt) ->
1551                          Cic.Lambda (name, src,
1552                            aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
1553                      | t ->
1554                          Cic.Prod
1555                            (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
1556                            CS.lift 1 t)
1557                    in
1558                      aux m mty new_outty
1559                in (* }}} end helper functions *)
1560                (* constructors types with left params already instantiated *)
1561                let outty = CicMetaSubst.apply_subst subst outty in
1562                let cl, left_p, leftno,rno,ugraph =
1563                  get_cl_and_left_p uri tyno outty ugraph
1564                in
1565                let right_p, mty =
1566                  try
1567                    match
1568                      CicTypeChecker.type_of_aux' ~subst metasenv context m
1569                        CicUniv.oblivion_ugraph
1570                    with
1571                    | Cic.MutInd _ as mty,_ -> [], mty
1572                    | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
1573                        snd (HExtlib.split_nth leftno args), mty
1574                    | _ -> assert false
1575                  with CicTypeChecker.TypeCheckerFailure _ -> assert false
1576                in
1577                let new_outty =
1578                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1579                in
1580                debug_print
1581                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1582                   ~metasenv subst new_outty context));
1583                let _,pl,subst,metasenv,ugraph =
1584                  List.fold_right2
1585                    (fun cty pbo (i, acc, s, menv, ugraph) ->
1586                      (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
1587                       *   (new_)outty right_par (K_i left_par k_par) *)
1588                       let infty_pbo, _ =
1589                         add_params menv s context uri tyno
1590                           cty outty mty m leftno i in
1591                       debug_print
1592                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
1593                         ~metasenv subst infty_pbo context));
1594                       let expty_pbo, k = (* k is (K_i left_par k_par) *)
1595                         add_params menv s context uri tyno
1596                           cty new_outty mty m leftno i in
1597                       debug_print
1598                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
1599                         ~metasenv subst expty_pbo context));
1600                       let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
1601                       debug_print
1602                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1603                         ~metasenv subst pbo context));
1604                       let (pbo, _), subst, metasenv, ugraph =
1605                         coerce_to_something_aux pbo infty_pbo expty_pbo
1606                           s menv context ugraph
1607                       in
1608                       debug_print
1609                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
1610                         ~metasenv subst pbo context));
1611                       (i-1, pbo::acc, subst, metasenv, ugraph))
1612                    cl pl (List.length pl, [], subst, metasenv, ugraph)
1613                in
1614                let new_outty = add_pi_for_refl_m new_outty mty m rno in
1615                debug_print
1616                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
1617                   ~metasenv subst new_outty context));
1618                let t =
1619                  if rno = 0 then
1620                    let refl_m=Cic.Appl[eq_refl;mty;m]in
1621                    Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
1622                  else
1623                    Cic.MutCase(uri,tyno,new_outty,m,pl)
1624                in
1625                (t, expty), subst, metasenv, ugraph (*}}}*)
1626            | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1627                (*{{{*) debug_print (lazy "LAM");
1628                let name_con =
1629                  FreshNamesGenerator.mk_fresh_name
1630                    ~subst metasenv context ~typ:src2 Cic.Anonymous
1631                in
1632                let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1633                (* contravariant part: the argument of f:src->ty *)
1634                let (rel1, _), subst, metasenv, ugraph =
1635                  coerce_to_something_aux
1636                   (Cic.Rel 1) (CS.lift 1 src2)
1637                   (CS.lift 1 src) subst metasenv context_src2 ugraph
1638                in
1639                (* covariant part: the result of f(c x); x:src2; (c x):src *)
1640                let name_t, bo =
1641                  match t with
1642                  | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
1643                  | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1644                in
1645                (* we fix the possible dependency problem in the source ty *)
1646                let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
1647                let (bo, _), subst, metasenv, ugraph =
1648                  coerce_to_something_aux
1649                    bo ty ty2 subst metasenv context_src2 ugraph
1650                in
1651                let coerced = Cic.Lambda (name_t,src2, bo) in
1652                (coerced, expty), subst, metasenv, ugraph (*}}}*)
1653            | _ ->
1654                (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
1655                 ~metasenv subst infty context ^ " ==> " ^
1656                 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
1657                coerce_atom_to_something
1658                t infty expty subst metasenv context ugraph (*}}}*)
1659           in
1660           debug_print (lazy ("COERCE TO SOMETHING END: "^
1661             CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
1662           result
1663     in
1664     try
1665       coerce_to_something_aux t infty expty subst metasenv context ugraph
1666     with Uncertain _ | RefineFailure _ as exn ->
1667       let f _ =
1668         lazy ("The term " ^
1669           CicMetaSubst.ppterm_in_context metasenv subst t context ^
1670           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1671           infty context ^ " but is here used with type " ^
1672           CicMetaSubst.ppterm_in_context metasenv subst expty context)
1673       in
1674         enrich localization_tbl ~f t exn
1675
1676   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1677     match CicReduction.whd ~delta:false ~subst context infty with
1678     | Cic.Meta _ | Cic.Sort _ ->
1679         t,infty, subst, metasenv, ugraph
1680     | src ->
1681        debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
1682          ~metasenv subst src context));
1683        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1684        try
1685          let (t, ty_t), subst, metasenv, ugraph =
1686            coerce_to_something true
1687              localization_tbl t src tgt subst metasenv context ugraph
1688          in
1689          debug_print (lazy ("COERCE TO SORT END: "^
1690            CicMetaSubst.ppterm_in_context ~metasenv subst t context));
1691          t, ty_t, subst, metasenv, ugraph
1692        with HExtlib.Localized (_, exn) ->
1693          let f _ =
1694            lazy ("(7)The term " ^
1695             CicMetaSubst.ppterm_in_context ~metasenv subst t context
1696             ^ " is not a type since it has type " ^
1697             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1698             ^ " that is not a sort")
1699          in
1700            enrich localization_tbl ~f t exn
1701   in
1702
1703   (* eat prods ends here! *)
1704
1705   let t',ty,subst',metasenv',ugraph1 =
1706    type_of_aux [] metasenv context t ugraph
1707   in
1708   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1709   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1710     (* Andrea: ho rimesso qui l'applicazione della subst al
1711        metasenv dopo che ho droppato l'invariante che il metsaenv
1712        e' sempre istanziato *)
1713   let substituted_metasenv =
1714     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1715     (* metasenv' *)
1716     (*  substituted_t,substituted_ty,substituted_metasenv *)
1717     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1718   let cleaned_t =
1719     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1720   let cleaned_ty =
1721     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1722   let cleaned_metasenv =
1723     List.map
1724       (function (n,context,ty) ->
1725          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1726          let context' =
1727            List.map
1728              (function
1729                   None -> None
1730                 | Some (n, Cic.Decl t) ->
1731                     Some (n,
1732                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1733                 | Some (n, Cic.Def (bo,ty)) ->
1734                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1735                     let ty' =
1736                       match ty with
1737                           None -> None
1738                         | Some ty ->
1739                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1740                     in
1741                       Some (n, Cic.Def (bo',ty'))
1742              ) context
1743          in
1744            (n,context',ty')
1745       ) substituted_metasenv
1746   in
1747     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1748 ;;
1749
1750 let undebrujin uri typesno tys t =
1751   snd
1752    (List.fold_right
1753      (fun (name,_,_,_) (i,t) ->
1754        (* here the explicit_named_substituion is assumed to be *)
1755        (* of length 0 *)
1756        let t' = Cic.MutInd (uri,i,[])  in
1757        let t = CicSubstitution.subst t' t in
1758         i - 1,t
1759      ) tys (typesno - 1,t))
1760
1761 let map_first_n n start f g l =
1762   let rec aux acc k l =
1763     if k < n then
1764       match l with
1765       | [] -> raise (Invalid_argument "map_first_n")
1766       | hd :: tl -> f hd k (aux acc (k+1) tl)
1767     else
1768       g acc l
1769   in
1770   aux start 0 l
1771
1772 (*CSC: this is a very rough approximation; to be finished *)
1773 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1774   let subst,metasenv,ugraph,tys =
1775     List.fold_right
1776       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1777         let subst,metasenv,ugraph,cl =
1778           List.fold_right
1779             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1780                let rec aux ctx k subst = function
1781                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1782                      let subst,metasenv,ugraph,tl =
1783                        map_first_n leftno
1784                          (subst,metasenv,ugraph,[])
1785                          (fun t n (subst,metasenv,ugraph,acc) ->
1786                            let subst,metasenv,ugraph =
1787                              fo_unif_subst
1788                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1789                            in
1790                            subst,metasenv,ugraph,(t::acc))
1791                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1792                          tl
1793                      in
1794                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1795                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1796                      subst,metasenv,ugraph,t
1797                  | Cic.Prod (name,s,t) ->
1798                      let ctx = (Some (name,Cic.Decl s))::ctx in
1799                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1800                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1801                  | _ ->
1802                      raise
1803                       (RefineFailure
1804                         (lazy "not well formed constructor type"))
1805                in
1806                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1807                subst,metasenv,ugraph,(name,ty) :: acc)
1808           cl (subst,metasenv,ugraph,[])
1809         in
1810         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1811       tys ([],metasenv,ugraph,[])
1812   in
1813   let substituted_tys =
1814     List.map
1815       (fun (name,ind,arity,cl) ->
1816         let cl =
1817           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1818         in
1819         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1820       tys
1821   in
1822   metasenv,ugraph,substituted_tys
1823
1824 let typecheck metasenv uri obj ~localization_tbl =
1825  let ugraph = CicUniv.empty_ugraph in
1826  match obj with
1827     Cic.Constant (name,Some bo,ty,args,attrs) ->
1828      let bo',boty,metasenv,ugraph =
1829       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1830      let ty',_,metasenv,ugraph =
1831       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1832      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1833      let bo' = CicMetaSubst.apply_subst subst bo' in
1834      let ty' = CicMetaSubst.apply_subst subst ty' in
1835      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1836       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1837   | Cic.Constant (name,None,ty,args,attrs) ->
1838      let ty',_,metasenv,ugraph =
1839       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1840      in
1841       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1842   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1843      assert (metasenv' = metasenv);
1844      (* Here we do not check the metasenv for correctness *)
1845      let bo',boty,metasenv,ugraph =
1846       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1847      let ty',sort,metasenv,ugraph =
1848       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1849      begin
1850       match sort with
1851          Cic.Sort _
1852        (* instead of raising Uncertain, let's hope that the meta will become
1853           a sort *)
1854        | Cic.Meta _ -> ()
1855        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1856      end;
1857      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1858      let bo' = CicMetaSubst.apply_subst subst bo' in
1859      let ty' = CicMetaSubst.apply_subst subst ty' in
1860      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1861       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1862   | Cic.Variable _ -> assert false (* not implemented *)
1863   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1864      (*CSC: this code is greately simplified and many many checks are missing *)
1865      (*CSC: e.g. the constructors are not required to build their own types,  *)
1866      (*CSC: the arities are not required to have as type a sort, etc.         *)
1867      let uri = match uri with Some uri -> uri | None -> assert false in
1868      let typesno = List.length tys in
1869      (* first phase: we fix only the types *)
1870      let metasenv,ugraph,tys =
1871       List.fold_right
1872        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1873          let ty',_,metasenv,ugraph =
1874           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1875          in
1876           metasenv,ugraph,(name,b,ty',cl)::res
1877        ) tys (metasenv,ugraph,[]) in
1878      let con_context =
1879       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1880      (* second phase: we fix only the constructors *)
1881      let saved_menv = metasenv in
1882      let metasenv,ugraph,tys =
1883       List.fold_right
1884        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1885          let metasenv,ugraph,cl' =
1886           List.fold_right
1887            (fun (name,ty) (metasenv,ugraph,res) ->
1888              let ty =
1889               CicTypeChecker.debrujin_constructor
1890                ~cb:(relocalize localization_tbl) uri typesno ty in
1891              let ty',_,metasenv,ugraph =
1892               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1893              let ty' = undebrujin uri typesno tys ty' in
1894               metasenv@saved_menv,ugraph,(name,ty')::res
1895            ) cl (metasenv,ugraph,[])
1896          in
1897           metasenv,ugraph,(name,b,ty,cl')::res
1898        ) tys (metasenv,ugraph,[]) in
1899      (* third phase: we check the positivity condition *)
1900      let metasenv,ugraph,tys =
1901        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1902      in
1903      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1904 ;;
1905
1906 (* sara' piu' veloce che raffinare da zero? mah.... *)
1907 let pack_coercion metasenv ctx t =
1908  let module C = Cic in
1909  let rec merge_coercions ctx =
1910    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1911    function
1912    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1913    | C.Meta (n,subst) ->
1914       let subst' =
1915        List.map
1916         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1917       in
1918        C.Meta (n,subst')
1919    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1920    | C.Prod (name,so,dest) ->
1921        let ctx' = (Some (name,C.Decl so))::ctx in
1922        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1923    | C.Lambda (name,so,dest) ->
1924        let ctx' = (Some (name,C.Decl so))::ctx in
1925        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1926    | C.LetIn (name,so,dest) ->
1927        let _,ty,metasenv,ugraph =
1928         pack_coercions := false;
1929         type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1930         pack_coercions := true;
1931        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1932        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1933    | C.Appl l ->
1934       let l = List.map (merge_coercions ctx) l in
1935       let t = C.Appl l in
1936        let b,_,_,_,_ = is_a_double_coercion t in
1937        if b then
1938          let ugraph = CicUniv.oblivion_ugraph in
1939          let old_insert_coercions = !insert_coercions in
1940          insert_coercions := false;
1941          let newt, _, menv, _ =
1942            try
1943              type_of_aux' metasenv ctx t ugraph
1944            with RefineFailure _ | Uncertain _ ->
1945              t, t, [], ugraph
1946          in
1947          insert_coercions := old_insert_coercions;
1948          if metasenv <> [] || menv = [] then
1949            newt
1950          else
1951            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1952        else
1953          t
1954    | C.Var (uri,exp_named_subst) ->
1955        let exp_named_subst = List.map aux exp_named_subst in
1956        C.Var (uri, exp_named_subst)
1957    | C.Const (uri,exp_named_subst) ->
1958        let exp_named_subst = List.map aux exp_named_subst in
1959        C.Const (uri, exp_named_subst)
1960    | C.MutInd (uri,tyno,exp_named_subst) ->
1961        let exp_named_subst = List.map aux exp_named_subst in
1962        C.MutInd (uri,tyno,exp_named_subst)
1963    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1964        let exp_named_subst = List.map aux exp_named_subst in
1965        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1966    | C.MutCase (uri,tyno,out,te,pl) ->
1967        let pl = List.map (merge_coercions ctx) pl in
1968        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1969    | C.Fix (fno, fl) ->
1970        let ctx' =
1971          List.fold_left
1972            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1973            ctx fl
1974        in
1975        let fl =
1976          List.map
1977            (fun (name,idx,ty,bo) ->
1978              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1979          fl
1980        in
1981        C.Fix (fno, fl)
1982    | C.CoFix (fno, fl) ->
1983        let ctx' =
1984          List.fold_left
1985            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1986            ctx fl
1987        in
1988        let fl =
1989          List.map
1990            (fun (name,ty,bo) ->
1991              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1992          fl
1993        in
1994        C.CoFix (fno, fl)
1995  in
1996   merge_coercions ctx t
1997 ;;
1998
1999 let pack_coercion_metasenv conjectures = conjectures (*
2000
2001   TASSI: this code war written when coercions were a toy,
2002          now packing coercions involves unification thus
2003          the metasenv may change, and this pack coercion
2004          does not handle that.
2005
2006   let module C = Cic in
2007   List.map
2008     (fun (i, ctx, ty) ->
2009        let ctx =
2010          List.fold_right
2011            (fun item ctx ->
2012               let item' =
2013                 match item with
2014                     Some (name, C.Decl t) ->
2015                       Some (name, C.Decl (pack_coercion conjectures ctx t))
2016                   | Some (name, C.Def (t,None)) ->
2017                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
2018                   | Some (name, C.Def (t,Some ty)) ->
2019                       Some (name, C.Def (pack_coercion conjectures ctx t,
2020                                          Some (pack_coercion conjectures ctx ty)))
2021                   | None -> None
2022               in
2023                 item'::ctx
2024            ) ctx []
2025        in
2026          ((i,ctx,pack_coercion conjectures ctx ty))
2027     ) conjectures
2028     *)
2029 ;;
2030
2031 let pack_coercion_obj obj = obj (*
2032
2033   TASSI: this code war written when coercions were a toy,
2034          now packing coercions involves unification thus
2035          the metasenv may change, and this pack coercion
2036          does not handle that.
2037
2038   let module C = Cic in
2039   match obj with
2040   | C.Constant (id, body, ty, params, attrs) ->
2041       let body =
2042         match body with
2043         | None -> None
2044         | Some body -> Some (pack_coercion [] [] body)
2045       in
2046       let ty = pack_coercion [] [] ty in
2047         C.Constant (id, body, ty, params, attrs)
2048   | C.Variable (name, body, ty, params, attrs) ->
2049       let body =
2050         match body with
2051         | None -> None
2052         | Some body -> Some (pack_coercion [] [] body)
2053       in
2054       let ty = pack_coercion [] [] ty in
2055         C.Variable (name, body, ty, params, attrs)
2056   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2057       let conjectures = pack_coercion_metasenv conjectures in
2058       let body = pack_coercion conjectures [] body in
2059       let ty = pack_coercion conjectures [] ty in
2060       C.CurrentProof (name, conjectures, body, ty, params, attrs)
2061   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2062       let indtys =
2063         List.map
2064           (fun (name, ind, arity, cl) ->
2065             let arity = pack_coercion [] [] arity in
2066             let cl =
2067               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2068             in
2069             (name, ind, arity, cl))
2070           indtys
2071       in
2072         C.InductiveDefinition (indtys, params, leftno, attrs) *)
2073 ;;
2074
2075
2076 (* DEBUGGING ONLY
2077 let type_of_aux' metasenv context term =
2078  try
2079   let (t,ty,m) =
2080       type_of_aux' metasenv context term in
2081     debug_print (lazy
2082      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2083    debug_print (lazy
2084     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2085    (t,ty,m)
2086  with
2087  | RefineFailure msg as e ->
2088      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2089      raise e
2090  | Uncertain msg as e ->
2091      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2092      raise e
2093 ;; *)
2094
2095 let profiler2 = HExtlib.profile "CicRefine"
2096
2097 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2098  profiler2.HExtlib.profile
2099   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2100
2101 let typecheck ~localization_tbl metasenv uri obj =
2102  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2103
2104 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2105 (* vim:set foldmethod=marker: *)