helm/software/components/cic_unification/cicRefine.ml

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