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