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