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 coerce_atom_to_something t infty expty subst metasenv context ugraph =
1365       let coer =
1366         CoercGraph.look_for_coercion metasenv subst context infty expty
1367       in
1368       match coer with
1369       | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
1370           "coerce_atom_to_something fails since not meta closed"))
1371       | CoercGraph.NoCoercion
1372       | CoercGraph.SomeCoercionToTgt _
1373       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
1374           "coerce_atom_to_something fails since no coercions found"))
1375       | CoercGraph.SomeCoercion candidates ->
1376           let uncertain = ref false in
1377           let selected =
1378             HExtlib.list_findopt
1379               (fun (metasenv,last,c) ->
1380                try
1381                 let subst,metasenv,ugraph =
1382                  fo_unif_subst subst context metasenv last t ugraph in
1383                 let newt,newhety,subst,metasenv,ugraph =
1384                  type_of_aux subst metasenv context c ugraph in
1385                 let newt, newty, subst, metasenv, ugraph =
1386                  avoid_double_coercion context subst metasenv ugraph newt expty
1387                 in
1388                 let subst,metasenv,ugraph =
1389                   fo_unif_subst subst context metasenv newhety expty ugraph in
1390                  Some ((newt,newty), subst, metasenv, ugraph)
1391                with
1392                | Uncertain _ -> uncertain := true; None
1393                | RefineFailure _ -> None)
1394               candidates
1395           in
1396           match selected with
1397           | Some x -> x
1398           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1399           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1400     in
1401     let rec coerce_to_something_aux
1402       t infty expty subst metasenv context ugraph
1403     =
1404       try
1405         let subst, metasenv, ugraph =
1406           fo_unif_subst subst context metasenv infty expty ugraph
1407         in
1408         (t, expty), subst, metasenv, ugraph
1409       with Uncertain _ | RefineFailure _ as exn ->
1410         if not allow_coercions || not !insert_coercions then
1411           enrich localization_tbl t exn
1412         else
1413           let whd = CicReduction.whd ~delta:false in
1414           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1415           let infty = clean infty subst context in
1416           let expty = clean expty subst context in
1417           match infty, expty, t with
1418           | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
1419              (match fl with
1420                  [name,i,_(* infty *),bo] ->
1421                    let context_bo =
1422                     Some (Cic.Name name,Cic.Decl expty)::context in
1423                    let (rel1, _), subst, metasenv, ugraph =
1424                     coerce_to_something_aux (Cic.Rel 1)
1425                       (CS.lift 1 expty) (CS.lift 1 infty) subst
1426                      metasenv context_bo ugraph in
1427                    let bo =
1428                     CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
1429                    in
1430                    let (bo,_), subst, metasenv, ugraph =
1431                     coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1432                     expty) subst
1433                      metasenv context_bo ugraph
1434                    in
1435                     (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1436                | _ -> assert false (* not implemented yet *))
1437           | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1438               (* move this stuff away *)
1439               let get_cl_and_left_p uri tyno outty ugraph =
1440                 match CicEnvironment.get_obj ugraph uri with
1441                 | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1442                     let count_pis t =
1443                       let rec aux ctx t =
1444                         match CicReduction.whd ~delta:false ctx t with
1445                         | Cic.Prod (name,src,tgt) ->
1446                             let ctx = Some (name, Cic.Decl src) :: ctx in
1447                             1 + aux ctx tgt
1448                         | _ -> 0
1449                       in
1450                         aux [] t
1451                     in
1452                     let rec skip_lambda_delifting t n =
1453                       match t,n with
1454                       | _,0 -> t
1455                       | Cic.Lambda (_,_,t),n ->
1456                           skip_lambda_delifting
1457                             (CS.subst (Cic.Implicit None) t) (n - 1)
1458                       | _ -> assert false
1459                     in
1460                     let get_l_r_p n = function
1461                             | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1462                       | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1463                           HExtlib.split_nth n args
1464                       | _ -> assert false
1465                     in
1466                     let _, _, ty, cl = List.nth tl tyno in
1467                     let pis = count_pis ty in
1468                     let rno = pis - leftno in
1469                     let t = skip_lambda_delifting outty rno in
1470                     let left_p, _ = get_l_r_p leftno t in
1471                     let instantiale_with_left cl =
1472                       List.map
1473                         (fun ty ->
1474                           List.fold_left
1475                             (fun t p -> CS.subst ~avoid_beta_redexes:true p t)
1476                             ty left_p)
1477                         cl
1478                     in
1479                     let cl = instantiale_with_left (List.map snd cl) in
1480                     cl, left_p, leftno, rno, ugraph
1481                 | _ -> raise exn
1482               in
1483               let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1484                 match t,n with
1485                 | _,0 ->
1486                   let rec mkr n = function
1487                     | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1488                   in
1489                   let bo =
1490                   CicReplace.replace_lifting
1491                     ~equality:(fun _ -> CicUtil.alpha_equivalence)
1492                     ~context:ctx
1493                     ~what:(matched::right_p)
1494                     ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1495                     ~where:bo
1496                   in
1497                   bo
1498                 | Cic.Lambda (name, src, tgt),_ ->
1499                     Cic.Lambda (name, src,
1500                       keep_lambdas_and_put_expty
1501                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1502                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1503                 | _ -> assert false
1504               in
1505               let add_params uri tyno cty outty leftno i =
1506                 let mytl = function [] -> [] | _::tl -> tl in
1507                 let rec aux outty par k = function
1508                   | Cic.Prod (name, src, tgt) ->
1509                       Cic.Prod (name, src,
1510                         aux (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
1511                   | Cic.MutInd _ ->
1512                       let par = mytl par in
1513                       let k =
1514                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
1515                         if par <> [] then Cic.Appl (k::par) else k
1516                       in
1517                       CR.head_beta_reduce ~delta:false
1518                         (Cic.Appl [outty;k])
1519                   | Cic.Appl (Cic.MutInd _::pl) ->
1520                       let par = mytl par in
1521                       let left_p,right_p = HExtlib.split_nth leftno pl in
1522                       let k =
1523                         let k = Cic.MutConstruct (uri,tyno,i,[]) in
1524                         Cic.Appl (k::left_p@par)
1525                       in
1526                       CR.head_beta_reduce ~delta:false
1527                         (Cic.Appl (outty ::right_p @ [k]))
1528                   | _ -> assert false
1529                 in
1530                   aux outty [] 1 cty
1531               in
1532               let rec add_params2 expty = function
1533                 | Cic.Prod (name, src, tgt) ->
1534                     Cic.Prod (name, src, add_params2 (CS.lift 1 expty) tgt)
1535                 | Cic.MutInd _ | Cic.Appl (Cic.MutInd _::_) -> expty
1536                 | _ -> assert false
1537               in
1538               (* constructors types with left params already instantiated *)
1539               let outty = CicMetaSubst.apply_subst subst outty in
1540               let cl, left_p, leftno,rno,ugraph =
1541                 get_cl_and_left_p uri tyno outty ugraph
1542               in
1543               let right_p =
1544                 try
1545                   match
1546                     CicTypeChecker.type_of_aux' ~subst metasenv context m
1547                       CicUniv.oblivion_ugraph
1548                   with
1549                   | Cic.MutInd _,_ -> []
1550                   | Cic.Appl (Cic.MutInd _::args),_ ->
1551                       snd (HExtlib.split_nth leftno args)
1552                   | _ -> assert false
1553                 with CicTypeChecker.TypeCheckerFailure _ ->
1554                   let rec foo =
1555                     function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
1556                   in
1557                    foo rno
1558               in
1559               let new_outty =
1560                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
1561               in
1562               let _,pl,subst,metasenv,ugraph =
1563                 List.fold_right2
1564                   (fun cty pbo (i, acc, subst, metasenv, ugraph) ->
1565                      (* Pi k_par, outty right_par (K_i left_par k_par)*)
1566                      let infty_pbo = add_params uri tyno cty outty leftno i in
1567                      (* Pi k_par, expty *)
1568                      let expty_pbo = add_params2 expty cty in
1569                      let (pbo, _), subst, metasenv, ugraph =
1570                        coerce_to_something_aux pbo infty_pbo expty_pbo
1571                          subst metasenv context ugraph
1572                      in
1573                      (i-1, pbo::acc, subst, metasenv, ugraph))
1574                   cl pl (List.length pl, [], subst, metasenv, ugraph)
1575               in
1576               let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
1577               (t, expty), subst, metasenv, ugraph
1578           | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
1579               let name_con = Cic.Name "name_con" in
1580               let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
1581               (* contravariant part: the argument of f:src->ty *)
1582               let (rel1, _), subst, metasenv, ugraph =
1583                 coerce_to_something_aux
1584                  (Cic.Rel 1) (CS.lift 1 src2)
1585                  (CS.lift 1 src) subst metasenv context_src2 ugraph
1586               in
1587               (* covariant part: the result of f(c x); x:src2; (c x):src *)
1588               let name_t, bo =
1589                 match t with
1590                 | Cic.Lambda (n,_,bo) -> n, CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
1591                 | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
1592               in
1593               (* we fix the possible dependency problem in the source ty *)
1594               let ty = CS.subst ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 ty) in
1595               let (bo, _), subst, metasenv, ugraph =
1596                 coerce_to_something_aux
1597                   bo ty ty2 subst metasenv context_src2 ugraph
1598               in
1599               let coerced = Cic.Lambda (name_t,src2, bo) in
1600                 (coerced, expty), subst, metasenv, ugraph
1601           | _ ->
1602             coerce_atom_to_something t infty expty subst metasenv context ugraph
1603     in
1604     try
1605       coerce_to_something_aux t infty expty subst metasenv context ugraph
1606     with Uncertain _ | RefineFailure _ as exn ->
1607       let f _ =
1608         lazy ("The term " ^
1609           CicMetaSubst.ppterm_in_context metasenv subst t context ^
1610           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
1611           infty context ^ " but is here used with type " ^
1612           CicMetaSubst.ppterm_in_context metasenv subst expty context)
1613       in
1614         enrich localization_tbl ~f t exn
1615
1616   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
1617     match CicReduction.whd ~subst:subst context infty with
1618     | Cic.Meta _ | Cic.Sort _ ->
1619         t,infty, subst, metasenv, ugraph
1620     | src ->
1621        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1622        try
1623          let (t, ty_t), subst, metasenv, ugraph =
1624            coerce_to_something true
1625              localization_tbl t src tgt subst metasenv context ugraph
1626          in
1627          t, ty_t, subst, metasenv, ugraph
1628        with HExtlib.Localized (_, exn) ->
1629          let f _ =
1630            lazy ("(7)The term " ^
1631             CicMetaSubst.ppterm_in_context ~metasenv subst t context
1632             ^ " is not a type since it has type " ^
1633             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1634             ^ " that is not a sort")
1635          in
1636            enrich localization_tbl ~f t exn
1637   in
1638
1639   (* eat prods ends here! *)
1640
1641   let t',ty,subst',metasenv',ugraph1 =
1642    type_of_aux [] metasenv context t ugraph
1643   in
1644   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1645   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1646     (* Andrea: ho rimesso qui l'applicazione della subst al
1647        metasenv dopo che ho droppato l'invariante che il metsaenv
1648        e' sempre istanziato *)
1649   let substituted_metasenv =
1650     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1651     (* metasenv' *)
1652     (*  substituted_t,substituted_ty,substituted_metasenv *)
1653     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1654   let cleaned_t =
1655     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1656   let cleaned_ty =
1657     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1658   let cleaned_metasenv =
1659     List.map
1660       (function (n,context,ty) ->
1661          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1662          let context' =
1663            List.map
1664              (function
1665                   None -> None
1666                 | Some (n, Cic.Decl t) ->
1667                     Some (n,
1668                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1669                 | Some (n, Cic.Def (bo,ty)) ->
1670                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1671                     let ty' =
1672                       match ty with
1673                           None -> None
1674                         | Some ty ->
1675                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1676                     in
1677                       Some (n, Cic.Def (bo',ty'))
1678              ) context
1679          in
1680            (n,context',ty')
1681       ) substituted_metasenv
1682   in
1683     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1684 ;;
1685
1686 let undebrujin uri typesno tys t =
1687   snd
1688    (List.fold_right
1689      (fun (name,_,_,_) (i,t) ->
1690        (* here the explicit_named_substituion is assumed to be *)
1691        (* of length 0 *)
1692        let t' = Cic.MutInd (uri,i,[])  in
1693        let t = CicSubstitution.subst t' t in
1694         i - 1,t
1695      ) tys (typesno - 1,t))
1696
1697 let map_first_n n start f g l =
1698   let rec aux acc k l =
1699     if k < n then
1700       match l with
1701       | [] -> raise (Invalid_argument "map_first_n")
1702       | hd :: tl -> f hd k (aux acc (k+1) tl)
1703     else
1704       g acc l
1705   in
1706   aux start 0 l
1707
1708 (*CSC: this is a very rough approximation; to be finished *)
1709 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1710   let subst,metasenv,ugraph,tys =
1711     List.fold_right
1712       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1713         let subst,metasenv,ugraph,cl =
1714           List.fold_right
1715             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1716                let rec aux ctx k subst = function
1717                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1718                      let subst,metasenv,ugraph,tl =
1719                        map_first_n leftno
1720                          (subst,metasenv,ugraph,[])
1721                          (fun t n (subst,metasenv,ugraph,acc) ->
1722                            let subst,metasenv,ugraph =
1723                              fo_unif_subst
1724                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1725                            in
1726                            subst,metasenv,ugraph,(t::acc))
1727                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1728                          tl
1729                      in
1730                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1731                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1732                      subst,metasenv,ugraph,t
1733                  | Cic.Prod (name,s,t) ->
1734                      let ctx = (Some (name,Cic.Decl s))::ctx in
1735                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1736                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1737                  | _ ->
1738                      raise
1739                       (RefineFailure
1740                         (lazy "not well formed constructor type"))
1741                in
1742                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1743                subst,metasenv,ugraph,(name,ty) :: acc)
1744           cl (subst,metasenv,ugraph,[])
1745         in
1746         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1747       tys ([],metasenv,ugraph,[])
1748   in
1749   let substituted_tys =
1750     List.map
1751       (fun (name,ind,arity,cl) ->
1752         let cl =
1753           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1754         in
1755         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1756       tys
1757   in
1758   metasenv,ugraph,substituted_tys
1759
1760 let typecheck metasenv uri obj ~localization_tbl =
1761  let ugraph = CicUniv.empty_ugraph in
1762  match obj with
1763     Cic.Constant (name,Some bo,ty,args,attrs) ->
1764      let bo',boty,metasenv,ugraph =
1765       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1766      let ty',_,metasenv,ugraph =
1767       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1768      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1769      let bo' = CicMetaSubst.apply_subst subst bo' in
1770      let ty' = CicMetaSubst.apply_subst subst ty' in
1771      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1772       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1773   | Cic.Constant (name,None,ty,args,attrs) ->
1774      let ty',_,metasenv,ugraph =
1775       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1776      in
1777       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1778   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1779      assert (metasenv' = metasenv);
1780      (* Here we do not check the metasenv for correctness *)
1781      let bo',boty,metasenv,ugraph =
1782       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1783      let ty',sort,metasenv,ugraph =
1784       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1785      begin
1786       match sort with
1787          Cic.Sort _
1788        (* instead of raising Uncertain, let's hope that the meta will become
1789           a sort *)
1790        | Cic.Meta _ -> ()
1791        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1792      end;
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.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1798   | Cic.Variable _ -> assert false (* not implemented *)
1799   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1800      (*CSC: this code is greately simplified and many many checks are missing *)
1801      (*CSC: e.g. the constructors are not required to build their own types,  *)
1802      (*CSC: the arities are not required to have as type a sort, etc.         *)
1803      let uri = match uri with Some uri -> uri | None -> assert false in
1804      let typesno = List.length tys in
1805      (* first phase: we fix only the types *)
1806      let metasenv,ugraph,tys =
1807       List.fold_right
1808        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1809          let ty',_,metasenv,ugraph =
1810           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1811          in
1812           metasenv,ugraph,(name,b,ty',cl)::res
1813        ) tys (metasenv,ugraph,[]) in
1814      let con_context =
1815       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1816      (* second phase: we fix only the constructors *)
1817      let saved_menv = metasenv in
1818      let metasenv,ugraph,tys =
1819       List.fold_right
1820        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1821          let metasenv,ugraph,cl' =
1822           List.fold_right
1823            (fun (name,ty) (metasenv,ugraph,res) ->
1824              let ty =
1825               CicTypeChecker.debrujin_constructor
1826                ~cb:(relocalize localization_tbl) uri typesno ty in
1827              let ty',_,metasenv,ugraph =
1828               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1829              let ty' = undebrujin uri typesno tys ty' in
1830               metasenv@saved_menv,ugraph,(name,ty')::res
1831            ) cl (metasenv,ugraph,[])
1832          in
1833           metasenv,ugraph,(name,b,ty,cl')::res
1834        ) tys (metasenv,ugraph,[]) in
1835      (* third phase: we check the positivity condition *)
1836      let metasenv,ugraph,tys =
1837        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1838      in
1839      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1840 ;;
1841
1842 (* sara' piu' veloce che raffinare da zero? mah.... *)
1843 let pack_coercion metasenv ctx t =
1844  let module C = Cic in
1845  let rec merge_coercions ctx =
1846    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1847    function
1848    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1849    | C.Meta (n,subst) ->
1850       let subst' =
1851        List.map
1852         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1853       in
1854        C.Meta (n,subst')
1855    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1856    | C.Prod (name,so,dest) ->
1857        let ctx' = (Some (name,C.Decl so))::ctx in
1858        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1859    | C.Lambda (name,so,dest) ->
1860        let ctx' = (Some (name,C.Decl so))::ctx in
1861        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1862    | C.LetIn (name,so,dest) ->
1863        let _,ty,metasenv,ugraph =
1864         pack_coercions := false;
1865         type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1866         pack_coercions := true;
1867        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1868        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1869    | C.Appl l ->
1870       let l = List.map (merge_coercions ctx) l in
1871       let t = C.Appl l in
1872        let b,_,_,_,_ = is_a_double_coercion t in
1873        if b then
1874          let ugraph = CicUniv.oblivion_ugraph in
1875          let old_insert_coercions = !insert_coercions in
1876          insert_coercions := false;
1877          let newt, _, menv, _ =
1878            try
1879              type_of_aux' metasenv ctx t ugraph
1880            with RefineFailure _ | Uncertain _ ->
1881              t, t, [], ugraph
1882          in
1883          insert_coercions := old_insert_coercions;
1884          if metasenv <> [] || menv = [] then
1885            newt
1886          else
1887            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1888        else
1889          t
1890    | C.Var (uri,exp_named_subst) ->
1891        let exp_named_subst = List.map aux exp_named_subst in
1892        C.Var (uri, exp_named_subst)
1893    | C.Const (uri,exp_named_subst) ->
1894        let exp_named_subst = List.map aux exp_named_subst in
1895        C.Const (uri, exp_named_subst)
1896    | C.MutInd (uri,tyno,exp_named_subst) ->
1897        let exp_named_subst = List.map aux exp_named_subst in
1898        C.MutInd (uri,tyno,exp_named_subst)
1899    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1900        let exp_named_subst = List.map aux exp_named_subst in
1901        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1902    | C.MutCase (uri,tyno,out,te,pl) ->
1903        let pl = List.map (merge_coercions ctx) pl in
1904        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1905    | C.Fix (fno, fl) ->
1906        let ctx' =
1907          List.fold_left
1908            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1909            ctx fl
1910        in
1911        let fl =
1912          List.map
1913            (fun (name,idx,ty,bo) ->
1914              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1915          fl
1916        in
1917        C.Fix (fno, fl)
1918    | C.CoFix (fno, fl) ->
1919        let ctx' =
1920          List.fold_left
1921            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1922            ctx fl
1923        in
1924        let fl =
1925          List.map
1926            (fun (name,ty,bo) ->
1927              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1928          fl
1929        in
1930        C.CoFix (fno, fl)
1931  in
1932   merge_coercions ctx t
1933 ;;
1934
1935 let pack_coercion_metasenv conjectures =
1936   let module C = Cic in
1937   List.map
1938     (fun (i, ctx, ty) ->
1939        let ctx =
1940          List.fold_right
1941            (fun item ctx ->
1942               let item' =
1943                 match item with
1944                     Some (name, C.Decl t) ->
1945                       Some (name, C.Decl (pack_coercion conjectures ctx t))
1946                   | Some (name, C.Def (t,None)) ->
1947                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
1948                   | Some (name, C.Def (t,Some ty)) ->
1949                       Some (name, C.Def (pack_coercion conjectures ctx t,
1950                                          Some (pack_coercion conjectures ctx ty)))
1951                   | None -> None
1952               in
1953                 item'::ctx
1954            ) ctx []
1955        in
1956          ((i,ctx,pack_coercion conjectures ctx ty))
1957     ) conjectures
1958 ;;
1959
1960 let pack_coercion_obj obj =
1961   let module C = Cic in
1962   match obj with
1963   | C.Constant (id, body, ty, params, attrs) ->
1964       let body =
1965         match body with
1966         | None -> None
1967         | Some body -> Some (pack_coercion [] [] body)
1968       in
1969       let ty = pack_coercion [] [] ty in
1970         C.Constant (id, body, ty, params, attrs)
1971   | C.Variable (name, body, ty, params, attrs) ->
1972       let body =
1973         match body with
1974         | None -> None
1975         | Some body -> Some (pack_coercion [] [] body)
1976       in
1977       let ty = pack_coercion [] [] ty in
1978         C.Variable (name, body, ty, params, attrs)
1979   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1980       let conjectures = pack_coercion_metasenv conjectures in
1981       let body = pack_coercion conjectures [] body in
1982       let ty = pack_coercion conjectures [] ty in
1983       C.CurrentProof (name, conjectures, body, ty, params, attrs)
1984   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1985       let indtys =
1986         List.map
1987           (fun (name, ind, arity, cl) ->
1988             let arity = pack_coercion [] [] arity in
1989             let cl =
1990               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1991             in
1992             (name, ind, arity, cl))
1993           indtys
1994       in
1995         C.InductiveDefinition (indtys, params, leftno, attrs)
1996 ;;
1997
1998
1999 (* DEBUGGING ONLY
2000 let type_of_aux' metasenv context term =
2001  try
2002   let (t,ty,m) =
2003       type_of_aux' metasenv context term in
2004     debug_print (lazy
2005      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2006    debug_print (lazy
2007     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2008    (t,ty,m)
2009  with
2010  | RefineFailure msg as e ->
2011      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2012      raise e
2013  | Uncertain msg as e ->
2014      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2015      raise e
2016 ;; *)
2017
2018 let profiler2 = HExtlib.profile "CicRefine"
2019
2020 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2021  profiler2.HExtlib.profile
2022   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2023
2024 let typecheck ~localization_tbl metasenv uri obj =
2025  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2026
2027 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2028 (* vim:set foldmethod=marker: *)