helm/software/components/cic_unification/cicRefine.ml

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