helm/software/components/ng_refiner/nCicRefiner.ml

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