helm/software/components/cic_unification/cicRefine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 exception RefineFailure of string Lazy.t;;
  31 exception Uncertain of string Lazy.t;;
  32 exception AssertFailure of string Lazy.t;;
  33
  34 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              (try
 420                let subst''',metasenv''',ugraph3 =
 421                  fo_unif_subst subst'' context metasenv''
 422                    inferredty ty' ugraph2
 423                in
 424                 C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 425               with
 426               | Uncertain _ | RefineFailure _ ->
 427                   let exn =
 428                     RefineFailure (lazy ("(3)The term " ^
 429                       CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
 430                        context ^ " has type " ^
 431                       CicMetaSubst.ppterm_in_context metasenv''
 432                         subst'' inferredty context ^
 433                       " but is here used with type " ^
 434                       CicMetaSubst.ppterm_in_context
 435                         metasenv'' subst'' ty' context))
 436                   in
 437                   try
 438                     let (te, ty), subst, metasenv, ugraph =
 439                       coerce_to_something te' inferredty ty'
 440                         subst'' metasenv'' context exn ugraph2
 441                     in
 442                     C.Cast (te, ty'), ty', subst, metasenv, ugraph
 443                   with exn -> enrich localization_tbl te' exn)
 444         | C.Prod (name,s,t) ->
 445             let s',sort1,subst',metasenv',ugraph1 =
 446               type_of_aux subst metasenv context s ugraph
 447             in
 448             let s',sort1,subst', metasenv',ugraph1 =
 449               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 450               s' sort1 subst' context metasenv' ugraph1
 451             in
 452             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 453             let t',sort2,subst'',metasenv'',ugraph2 =
 454               type_of_aux subst' metasenv'
 455                 context_for_t t ugraph1
 456             in
 457             let t',sort2,subst'',metasenv'',ugraph2 =
 458               coerce_to_sort false (Cic.Type(CicUniv.fresh()))
 459               t' sort2 subst'' context_for_t metasenv'' ugraph2
 460             in
 461               let sop,subst''',metasenv''',ugraph3 =
 462                 sort_of_prod localization_tbl subst'' metasenv''
 463                   context (name,s') t' (sort1,sort2) ugraph2
 464               in
 465                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 466         | C.Lambda (n,s,t) ->
 467             let s',sort1,subst',metasenv',ugraph1 =
 468               type_of_aux subst metasenv context s ugraph
 469             in
 470             let s',sort1,subst',metasenv',ugraph1 =
 471               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 472               s' sort1 subst' context metasenv' ugraph1
 473             in
 474             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 475             let t',type2,subst'',metasenv'',ugraph2 =
 476               type_of_aux subst' metasenv' context_for_t t ugraph1
 477             in
 478               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 479                 subst'',metasenv'',ugraph2
 480         | C.LetIn (n,s,t) ->
 481             (* only to check if s is well-typed *)
 482             let s',ty,subst',metasenv',ugraph1 =
 483               type_of_aux subst metasenv context s ugraph
 484             in
 485            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 486
 487             let t',inferredty,subst'',metasenv'',ugraph2 =
 488               type_of_aux subst' metasenv'
 489                 context_for_t t ugraph1
 490             in
 491               (* One-step LetIn reduction.
 492                * Even faster than the previous solution.
 493                * Moreover the inferred type is closer to the expected one.
 494                *)
 495               C.LetIn (n,s',t'),
 496                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
 497                subst'',metasenv'',ugraph2
 498         | C.Appl (he::((_::_) as tl)) ->
 499             let he',hetype,subst',metasenv',ugraph1 =
 500               type_of_aux subst metasenv context he ugraph
 501             in
 502             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 503                typeof_list subst' metasenv' context ugraph1 tl
 504             in
 505             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
 506               eat_prods true subst'' metasenv'' context
 507                 he' hetype tlbody_and_type ugraph2
 508             in
 509             let newappl = (C.Appl (coerced_he::coerced_args)) in
 510             avoid_double_coercion
 511               context subst''' metasenv''' ugraph3 newappl applty
 512         | C.Appl _ -> assert false
 513         | C.Const (uri,exp_named_subst) ->
 514             let exp_named_subst',subst',metasenv',ugraph1 =
 515               check_exp_named_subst subst metasenv context
 516                 exp_named_subst ugraph in
 517             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 518             let cty =
 519               CicSubstitution.subst_vars exp_named_subst' ty_uri
 520             in
 521               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 522         | C.MutInd (uri,i,exp_named_subst) ->
 523             let exp_named_subst',subst',metasenv',ugraph1 =
 524               check_exp_named_subst subst metasenv context
 525                 exp_named_subst ugraph
 526             in
 527             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 528             let cty =
 529               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 530               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 531         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 532             let exp_named_subst',subst',metasenv',ugraph1 =
 533               check_exp_named_subst subst metasenv context
 534                 exp_named_subst ugraph
 535             in
 536             let ty_uri,ugraph2 =
 537               type_of_mutual_inductive_constr uri i j ugraph1
 538             in
 539             let cty =
 540               CicSubstitution.subst_vars exp_named_subst' ty_uri
 541             in
 542               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 543                 metasenv',ugraph2
 544         | C.MutCase (uri, i, outtype, term, pl) ->
 545             (* first, get the inductive type (and noparams)
 546              * in the environment  *)
 547             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 548               let _ = CicTypeChecker.typecheck uri in
 549               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 550               match obj with
 551                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 552                     List.nth l i , expl_params, parsno, u
 553                 | _ ->
 554                     enrich localization_tbl t
 555                      (RefineFailure
 556                        (lazy ("Unkown mutual inductive definition " ^
 557                          U.string_of_uri uri)))
 558            in
 559            let rec count_prod t =
 560              match CicReduction.whd ~subst context t with
 561                  C.Prod (_, _, t) -> 1 + (count_prod t)
 562                | _ -> 0
 563            in
 564            let no_args = count_prod arity in
 565              (* now, create a "generic" MutInd *)
 566            let metasenv,left_args =
 567              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 568            in
 569            let metasenv,right_args =
 570              let no_right_params = no_args - no_left_params in
 571                if no_right_params < 0 then assert false
 572                else CicMkImplicit.n_fresh_metas
 573                       metasenv subst context no_right_params
 574            in
 575            let metasenv,exp_named_subst =
 576              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 577            let expected_type =
 578              if no_args = 0 then
 579                C.MutInd (uri,i,exp_named_subst)
 580              else
 581                C.Appl
 582                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 583            in
 584              (* check consistency with the actual type of term *)
 585            let term',actual_type,subst,metasenv,ugraph1 =
 586              type_of_aux subst metasenv context term ugraph in
 587            let expected_type',_, subst, metasenv,ugraph2 =
 588              type_of_aux subst metasenv context expected_type ugraph1
 589            in
 590            let actual_type = CicReduction.whd ~subst context actual_type in
 591            let subst,metasenv,ugraph3 =
 592             try
 593              fo_unif_subst subst context metasenv
 594                expected_type' actual_type ugraph2
 595             with
 596              exn ->
 597               enrich localization_tbl term' exn
 598                ~f:(function _ ->
 599                  lazy ("(10)The term " ^
 600                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
 601                    context ^ " has type " ^
 602                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
 603                    context ^ " but is here used with type " ^
 604                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
 605            in
 606            let rec instantiate_prod t =
 607             function
 608                [] -> t
 609              | he::tl ->
 610                 match CicReduction.whd ~subst context t with
 611                    C.Prod (_,_,t') ->
 612                     instantiate_prod (CicSubstitution.subst he t') tl
 613                  | _ -> assert false
 614            in
 615            let arity_instantiated_with_left_args =
 616             instantiate_prod arity left_args in
 617              (* TODO: check if the sort elimination
 618               * is allowed: [(I q1 ... qr)|B] *)
 619            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 620              List.fold_right
 621                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
 622                   let constructor =
 623                     if left_args = [] then
 624                       (C.MutConstruct (uri,i,j,exp_named_subst))
 625                     else
 626                       (C.Appl
 627                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 628                   in
 629                   let p',actual_type,subst,metasenv,ugraph1 =
 630                     type_of_aux subst metasenv context p ugraph
 631                   in
 632                   let constructor',expected_type, subst, metasenv,ugraph2 =
 633                     type_of_aux subst metasenv context constructor ugraph1
 634                   in
 635                   let outtypeinstance,subst,metasenv,ugraph3 =
 636                    try
 637                     check_branch 0 context metasenv subst
 638                      no_left_params actual_type constructor' expected_type
 639                      ugraph2
 640                    with
 641                     exn ->
 642                      enrich localization_tbl constructor'
 643                       ~f:(fun _ ->
 644                         lazy ("(11)The term " ^
 645                          CicMetaSubst.ppterm_in_context metasenv subst p'
 646                           context ^ " has type " ^
 647                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
 648                           context ^ " but is here used with type " ^
 649                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
 650                           context)) exn
 651                   in
 652                     (p'::pl,j-1,
 653                      outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
 654                pl ([],List.length pl,[],subst,metasenv,ugraph3)
 655            in
 656
 657              (* we are left to check that the outype matches his instances.
 658                 The easy case is when the outype is specified, that amount
 659                 to a trivial check. Otherwise, we should guess a type from
 660                 its instances
 661              *)
 662
 663            let outtype,outtypety, subst, metasenv,ugraph4 =
 664              type_of_aux subst metasenv context outtype ugraph4 in
 665            (match outtype with
 666            | C.Meta (n,l) ->
 667                (let candidate,ugraph5,metasenv,subst =
 668                  let exp_name_subst, metasenv =
 669                     let o,_ =
 670                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 671                     in
 672                     let uris = CicUtil.params_of_obj o in
 673                     List.fold_right (
 674                       fun uri (acc,metasenv) ->
 675                         let metasenv',new_meta =
 676                            CicMkImplicit.mk_implicit metasenv subst context
 677                         in
 678                         let irl =
 679                           CicMkImplicit.identity_relocation_list_for_metavariable
 680                             context
 681                         in
 682                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 683                     ) uris ([],metasenv)
 684                  in
 685                  let ty =
 686                   match left_args,right_args with
 687                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 688                    | _,_ ->
 689                       let rec mk_right_args =
 690                        function
 691                           0 -> []
 692                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 693                       in
 694                       let right_args_no = List.length right_args in
 695                       let lifted_left_args =
 696                        List.map (CicSubstitution.lift right_args_no) left_args
 697                       in
 698                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 699                         (lifted_left_args @ mk_right_args right_args_no))
 700                  in
 701                  let fresh_name =
 702                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 703                      context Cic.Anonymous ~typ:ty
 704                  in
 705                  match outtypeinstances with
 706                  | [] ->
 707                      let extended_context =
 708                       let rec add_right_args =
 709                        function
 710                           Cic.Prod (name,ty,t) ->
 711                            Some (name,Cic.Decl ty)::(add_right_args t)
 712                         | _ -> []
 713                       in
 714                        (Some (fresh_name,Cic.Decl ty))::
 715                        (List.rev
 716                         (add_right_args arity_instantiated_with_left_args))@
 717                        context
 718                      in
 719                      let metasenv,new_meta =
 720                        CicMkImplicit.mk_implicit metasenv subst extended_context
 721                      in
 722                        let irl =
 723                        CicMkImplicit.identity_relocation_list_for_metavariable
 724                          extended_context
 725                      in
 726                      let rec add_lambdas b =
 727                       function
 728                          Cic.Prod (name,ty,t) ->
 729                           Cic.Lambda (name,ty,(add_lambdas b t))
 730                        | _ -> Cic.Lambda (fresh_name, ty, b)
 731                      in
 732                      let candidate =
 733                       add_lambdas (Cic.Meta (new_meta,irl))
 734                        arity_instantiated_with_left_args
 735                      in
 736                      (Some candidate),ugraph4,metasenv,subst
 737                  | (constructor_args_no,_,instance,_)::tl ->
 738                      try
 739                        let instance',subst,metasenv =
 740                          CicMetaSubst.delift_rels subst metasenv
 741                           constructor_args_no instance
 742                        in
 743                        let candidate,ugraph,metasenv,subst =
 744                          List.fold_left (
 745                            fun (candidate_oty,ugraph,metasenv,subst)
 746                              (constructor_args_no,_,instance,_) ->
 747                                match candidate_oty with
 748                                | None -> None,ugraph,metasenv,subst
 749                                | Some ty ->
 750                                  try
 751                                    let instance',subst,metasenv =
 752                                      CicMetaSubst.delift_rels subst metasenv
 753                                       constructor_args_no instance
 754                                    in
 755                                    let subst,metasenv,ugraph =
 756                                     fo_unif_subst subst context metasenv
 757                                       instance' ty ugraph
 758                                    in
 759                                     candidate_oty,ugraph,metasenv,subst
 760                                  with
 761                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 762                                   | RefineFailure _ | Uncertain _ ->
 763                                      None,ugraph,metasenv,subst
 764                          ) (Some instance',ugraph4,metasenv,subst) tl
 765                        in
 766                        match candidate with
 767                        | None -> None, ugraph,metasenv,subst
 768                        | Some t ->
 769                           let rec add_lambdas n b =
 770                            function
 771                               Cic.Prod (name,ty,t) ->
 772                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 773                             | _ ->
 774                               Cic.Lambda (fresh_name, ty,
 775                                CicSubstitution.lift (n + 1) t)
 776                           in
 777                            Some
 778                             (add_lambdas 0 t arity_instantiated_with_left_args),
 779                            ugraph,metasenv,subst
 780                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 781                        None,ugraph4,metasenv,subst
 782                in
 783                match candidate with
 784                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 785                | Some candidate ->
 786                    let subst,metasenv,ugraph =
 787                     try
 788                      fo_unif_subst subst context metasenv
 789                        candidate outtype ugraph5
 790                     with
 791                      exn -> assert false(* unification against a metavariable *)
 792                    in
 793                      C.MutCase (uri, i, outtype, term', pl'),
 794                       CicReduction.head_beta_reduce
 795                        (CicMetaSubst.apply_subst subst
 796                         (Cic.Appl (outtype::right_args@[term']))),
 797                      subst,metasenv,ugraph)
 798            | _ ->    (* easy case *)
 799              let tlbody_and_type,subst,metasenv,ugraph4 =
 800                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
 801              in
 802              let _,_,_,subst,metasenv,ugraph4 =
 803                eat_prods false subst metasenv context
 804                  outtype outtypety tlbody_and_type ugraph4
 805              in
 806              let _,_, subst, metasenv,ugraph5 =
 807                type_of_aux subst metasenv context
 808                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 809              in
 810              let (subst,metasenv,ugraph6) =
 811                List.fold_left2
 812                  (fun (subst,metasenv,ugraph)
 813                    p (constructor_args_no,context,instance,args)
 814                   ->
 815                     let instance' =
 816                       let appl =
 817                         let outtype' =
 818                           CicSubstitution.lift constructor_args_no outtype
 819                         in
 820                           C.Appl (outtype'::args)
 821                       in
 822                         CicReduction.whd ~subst context appl
 823                     in
 824                      try
 825                       fo_unif_subst subst context metasenv instance instance'
 826                        ugraph
 827                      with
 828                       exn ->
 829                        enrich localization_tbl p exn
 830                         ~f:(function _ ->
 831                           lazy ("(12)The term " ^
 832                            CicMetaSubst.ppterm_in_context ~metasenv subst p
 833                             context ^ " has type " ^
 834                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
 835                             context ^ " but is here used with type " ^
 836                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
 837                             context)))
 838                  (subst,metasenv,ugraph5) pl' outtypeinstances
 839              in
 840                C.MutCase (uri, i, outtype, term', pl'),
 841                  CicReduction.head_beta_reduce
 842                   (CicMetaSubst.apply_subst subst
 843                    (C.Appl(outtype::right_args@[term]))),
 844                  subst,metasenv,ugraph6)
 845         | C.Fix (i,fl) ->
 846             let fl_ty',subst,metasenv,types,ugraph1,len =
 847               List.fold_left
 848                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
 849                    let ty',_,subst',metasenv',ugraph1 =
 850                       type_of_aux subst metasenv context ty ugraph
 851                    in
 852                      fl @ [ty'],subst',metasenv',
 853                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
 854                         :: types, ugraph, len+1
 855                 ) ([],subst,metasenv,[],ugraph,0) fl
 856             in
 857             let context' = types@context in
 858             let fl_bo',subst,metasenv,ugraph2 =
 859               List.fold_left
 860                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 861                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 862                      type_of_aux subst metasenv context' bo ugraph in
 863                    let expected_ty = CicSubstitution.lift len ty in
 864                    let subst',metasenv',ugraph' =
 865                     try
 866                      fo_unif_subst subst context' metasenv
 867                        ty_of_bo expected_ty ugraph1
 868                     with
 869                      exn ->
 870                       enrich localization_tbl bo exn
 871                        ~f:(function _ ->
 872                          lazy ("(13)The term " ^
 873                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 874                            context' ^ " has type " ^
 875                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 876                            context' ^ " but is here used with type " ^
 877                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 878                            context))
 879                    in
 880                      fl @ [bo'] , subst',metasenv',ugraph'
 881                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 882             in
 883             let ty = List.nth fl_ty' i in
 884             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 885              * and we want the new fl with bo' and ty' injected in the right
 886              * place.
 887              *)
 888             let rec map3 f l1 l2 l3 =
 889               match l1,l2,l3 with
 890               | [],[],[] -> []
 891               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 892               | _ -> assert false
 893             in
 894             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 895               fl_ty' fl_bo' fl
 896             in
 897               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 898         | C.CoFix (i,fl) ->
 899             let fl_ty',subst,metasenv,types,ugraph1,len =
 900               List.fold_left
 901                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
 902                    let ty',_,subst',metasenv',ugraph1 =
 903                      type_of_aux subst metasenv context ty ugraph
 904                    in
 905                      fl @ [ty'],subst',metasenv',
 906                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
 907                         types, ugraph1, len+1
 908                 ) ([],subst,metasenv,[],ugraph,0) fl
 909             in
 910             let context' = types@context in
 911             let fl_bo',subst,metasenv,ugraph2 =
 912               List.fold_left
 913                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 914                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 915                      type_of_aux subst metasenv context' bo ugraph in
 916                    let expected_ty = CicSubstitution.lift len ty in
 917                    let subst',metasenv',ugraph' =
 918                     try
 919                      fo_unif_subst subst context' metasenv
 920                        ty_of_bo expected_ty ugraph1
 921                     with
 922                      exn ->
 923                       enrich localization_tbl bo exn
 924                        ~f:(function _ ->
 925                          lazy ("(14)The term " ^
 926                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
 927                            context' ^ " has type " ^
 928                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
 929                            context' ^ " but is here used with type " ^
 930                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
 931                            context))
 932                    in
 933                      fl @ [bo'],subst',metasenv',ugraph'
 934                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 935             in
 936             let ty = List.nth fl_ty' i in
 937             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 938              * and we want the new fl with bo' and ty' injected in the right
 939              * place.
 940              *)
 941             let rec map3 f l1 l2 l3 =
 942               match l1,l2,l3 with
 943               | [],[],[] -> []
 944               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 945               | _ -> assert false
 946             in
 947             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 948               fl_ty' fl_bo' fl
 949             in
 950               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 951      in
 952       relocalize localization_tbl t t';
 953       res
 954
 955   (* check_metasenv_consistency checks that the "canonical" context of a
 956      metavariable is consitent - up to relocation via the relocation list l -
 957      with the actual context *)
 958   and check_metasenv_consistency
 959     metano subst metasenv context canonical_context l ugraph
 960     =
 961     let module C = Cic in
 962     let module R = CicReduction in
 963     let module S = CicSubstitution in
 964     let lifted_canonical_context =
 965       let rec aux i =
 966         function
 967             [] -> []
 968           | (Some (n,C.Decl t))::tl ->
 969               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 970           | (Some (n,C.Def (t,None)))::tl ->
 971               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 972           | None::tl -> None::(aux (i+1) tl)
 973           | (Some (n,C.Def (t,Some ty)))::tl ->
 974               (Some (n,
 975                      C.Def ((S.subst_meta l (S.lift i t)),
 976                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 977       in
 978         aux 1 canonical_context
 979     in
 980       try
 981         List.fold_left2
 982           (fun (l,subst,metasenv,ugraph) t ct ->
 983              match (t,ct) with
 984                  _,None ->
 985                    l @ [None],subst,metasenv,ugraph
 986                | Some t,Some (_,C.Def (ct,_)) ->
 987                    let subst',metasenv',ugraph' =
 988                    (try
 989 prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
 990                       fo_unif_subst subst context metasenv t ct ugraph
 991                     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))))))
 992                    in
 993                      l @ [Some t],subst',metasenv',ugraph'
 994                | Some t,Some (_,C.Decl ct) ->
 995                    let t',inferredty,subst',metasenv',ugraph1 =
 996                      type_of_aux subst metasenv context t ugraph
 997                    in
 998                    let subst'',metasenv'',ugraph2 =
 999                      (try
1000                         fo_unif_subst
1001                           subst' context metasenv' inferredty ct ugraph1
1002                       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))))))
1003                    in
1004                      l @ [Some t'], subst'',metasenv'',ugraph2
1005                | None, Some _  ->
1006                    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
1007       with
1008           Invalid_argument _ ->
1009             raise
1010             (RefineFailure
1011                (lazy (sprintf
1012                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1013                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1014                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1015
1016   and check_exp_named_subst metasubst metasenv context tl ugraph =
1017     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
1018       match tl with
1019           [] -> [],metasubst,metasenv,ugraph
1020         | (uri,t)::tl ->
1021             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
1022             let typeofvar =
1023               CicSubstitution.subst_vars substs ty_uri in
1024               (* CSC: why was this code here? it is wrong
1025                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1026                  Cic.Variable (_,Some bo,_,_) ->
1027                  raise
1028                  (RefineFailure (lazy
1029                  "A variable with a body can not be explicit substituted"))
1030                  | Cic.Variable (_,None,_,_) -> ()
1031                  | _ ->
1032                  raise
1033                  (RefineFailure (lazy
1034                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1035                  ) ;
1036               *)
1037             let t',typeoft,metasubst',metasenv',ugraph2 =
1038               type_of_aux metasubst metasenv context t ugraph1 in
1039             let subst = uri,t' in
1040             let metasubst'',metasenv'',ugraph3 =
1041               try
1042                 fo_unif_subst
1043                   metasubst' context metasenv' typeoft typeofvar ugraph2
1044               with _ ->
1045                 raise (RefineFailure (lazy
1046                          ("Wrong Explicit Named Substitution: " ^
1047                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1048                           " not unifiable with " ^
1049                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1050             in
1051             (* FIXME: no mere tail recursive! *)
1052             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1053               check_exp_named_subst_aux
1054                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1055             in
1056               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1057     in
1058       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1059
1060
1061   and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
1062    ugraph
1063   =
1064     let module C = Cic in
1065     let context_for_t2 = (Some (name,C.Decl s))::context in
1066     let t1'' = CicReduction.whd ~subst context t1 in
1067     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1068       match (t1'', t2'') with
1069           (C.Sort s1, C.Sort s2)
1070             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1071               (* different than Coq manual!!! *)
1072               C.Sort s2,subst,metasenv,ugraph
1073         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1074             let t' = CicUniv.fresh() in
1075              (try
1076               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1077               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1078                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1079               with
1080                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1081         | (C.Sort _,C.Sort (C.Type t1)) ->
1082             C.Sort (C.Type t1),subst,metasenv,ugraph
1083         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1084         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1085             (* TODO how can we force the meta to become a sort? If we don't we
1086              * break the invariant that refine produce only well typed terms *)
1087             (* TODO if we check the non meta term and if it is a sort then we
1088              * are likely to know the exact value of the result e.g. if the rhs
1089              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1090             let (metasenv,idx) =
1091               CicMkImplicit.mk_implicit_sort metasenv subst in
1092             let (subst, metasenv,ugraph1) =
1093              try
1094               fo_unif_subst subst context_for_t2 metasenv
1095                 (C.Meta (idx,[])) t2'' ugraph
1096              with _ -> assert false (* unification against a metavariable *)
1097             in
1098               t2'',subst,metasenv,ugraph1
1099         | (C.Sort _,_)
1100         | (C.Meta _,_) ->
1101             enrich localization_tbl s
1102              (RefineFailure
1103                (lazy
1104                  (sprintf
1105                    "%s is supposed to be a type, but its type is %s"
1106                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1107                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1108         | _,_ ->
1109             enrich localization_tbl t
1110              (RefineFailure
1111                (lazy
1112                  (sprintf
1113                    "%s is supposed to be a type, but its type is %s"
1114                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1115                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1116
1117   and avoid_double_coercion context subst metasenv ugraph t ty =
1118    if not !pack_coercions then
1119     t,ty,subst,metasenv,ugraph
1120    else
1121     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1122     if b then
1123       let source_carr = CoercGraph.source_of c2 in
1124       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1125       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1126       with
1127       | CoercGraph.SomeCoercion candidates ->
1128          let selected =
1129            HExtlib.list_findopt
1130              (function (metasenv,last,c) ->
1131                match c with
1132                | c when not (CoercGraph.is_composite c) ->
1133                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1134                    None
1135                | c ->
1136                let subst,metasenv,ugraph =
1137                 fo_unif_subst subst context metasenv last head ugraph in
1138                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1139                (try
1140                  debug_print
1141                    (lazy
1142                      ("packing: " ^
1143                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1144                  let newt,_,subst,metasenv,ugraph =
1145                    type_of_aux subst metasenv context c ugraph in
1146                  debug_print (lazy "tipa...");
1147                  let subst, metasenv, ugraph =
1148                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1149                     fo_unif_subst subst context metasenv newt t ugraph
1150                  in
1151                  debug_print (lazy "unifica...");
1152                  Some (newt, ty, subst, metasenv, ugraph)
1153                with
1154                | RefineFailure s | Uncertain s when not !pack_coercions->
1155                    debug_print s; debug_print (lazy "stop\n");None
1156                | RefineFailure s | Uncertain s ->
1157                    debug_print s;debug_print (lazy "goon\n");
1158                    try
1159                      let old_pack_coercions = !pack_coercions in
1160                      pack_coercions := false; (* to avoid diverging *)
1161                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1162                        type_of_aux subst metasenv context c1_c2_implicit ugraph
1163                      in
1164                      pack_coercions := old_pack_coercions;
1165                      let b, _, _, _, _ =
1166                        is_a_double_coercion refined_c1_c2_implicit
1167                      in
1168                      if b then
1169                        None
1170                      else
1171                        let head' =
1172                          match refined_c1_c2_implicit with
1173                          | Cic.Appl l -> HExtlib.list_last l
1174                          | _ -> assert false
1175                        in
1176                        let subst, metasenv, ugraph =
1177                         try fo_unif_subst subst context metasenv
1178                           head head' ugraph
1179                         with RefineFailure s| Uncertain s->
1180                           debug_print s;assert false
1181                        in
1182                        let subst, metasenv, ugraph =
1183                          fo_unif_subst subst context metasenv
1184                           refined_c1_c2_implicit t ugraph
1185                        in
1186                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1187                    with
1188                    | RefineFailure s | Uncertain s ->
1189                        pack_coercions := true;debug_print s;None
1190                    | exn -> pack_coercions := true; raise exn))
1191              candidates
1192          in
1193          (match selected with
1194          | Some x -> x
1195          | None ->
1196               debug_print
1197                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1198               t, ty, subst, metasenv, ugraph)
1199       | _ -> t, ty, subst, metasenv, ugraph)
1200     else
1201       t, ty, subst, metasenv, ugraph
1202
1203   and typeof_list subst metasenv context ugraph l =
1204     let tlbody_and_type,subst,metasenv,ugraph =
1205       List.fold_right
1206         (fun x (res,subst,metasenv,ugraph) ->
1207            let x',ty,subst',metasenv',ugraph1 =
1208              type_of_aux subst metasenv context x ugraph
1209            in
1210             (x', ty)::res,subst',metasenv',ugraph1
1211         ) l ([],subst,metasenv,ugraph)
1212     in
1213       tlbody_and_type,subst,metasenv,ugraph
1214
1215   and eat_prods
1216     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1217   =
1218     (* aux function to add coercions to funclass *)
1219     let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
1220       (* {{{ body *)
1221       let pristinemenv = metasenv in
1222       let metasenv,hetype' =
1223         mk_prod_of_metas metasenv context subst args_bo_and_ty
1224       in
1225       try
1226         let subst,metasenv,ugraph =
1227           fo_unif_subst_eat_prods
1228             subst context metasenv hetype hetype' ugraph
1229         in
1230         subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1231       with RefineFailure s | Uncertain s as exn
1232       when allow_coercions && !insert_coercions ->
1233         (* {{{ we search a coercion of the head (saturated) to funclass *)
1234         let metasenv = pristinemenv in
1235         debug_print (lazy
1236           ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
1237            " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype'
1238            (* ^ " cause: " ^ Lazy.force s *)));
1239         let how_many_args_are_needed =
1240           let rec aux n = function
1241             | Cic.Prod(_,_,t) -> aux (n+1) t
1242             | _ -> n
1243           in
1244           aux 0 (CicMetaSubst.apply_subst subst hetype)
1245         in
1246         let args, remainder =
1247           HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
1248         in
1249         let args = List.map fst args in
1250         let x =
1251           if args <> [] then
1252             match he with
1253             | Cic.Appl l -> Cic.Appl (l@args)
1254             | _ -> Cic.Appl (he::args)
1255           else
1256             he
1257         in
1258         let x,xty,subst,metasenv,ugraph =
1259          (*CSC: here unsharing is necessary to avoid an unwanted
1260            relocalization. However, this also shows a great source of
1261            inefficiency: "x" is refined twice (once now and once in the
1262            subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
1263          *)
1264          type_of_aux subst metasenv context (Unshare.unshare x) ugraph
1265         in
1266         let carr_src =
1267           CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
1268         in
1269         let carr_tgt = CoercDb.Fun 0 in
1270         match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
1271         | CoercGraph.NoCoercion
1272         | CoercGraph.NotMetaClosed
1273         | CoercGraph.NotHandled _ -> raise exn
1274         | CoercGraph.SomeCoercionToTgt candidates
1275         | CoercGraph.SomeCoercion candidates ->
1276             match
1277             HExtlib.list_findopt
1278               (fun (metasenv,last,coerc) ->
1279                 let subst,metasenv,ugraph =
1280                  fo_unif_subst subst context metasenv last x ugraph in
1281                 debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
1282                 try
1283                   (* we want this to be available in the error handler fo the
1284                    * following (so it has its own try. *)
1285                   let t,tty,subst,metasenv,ugraph =
1286                     type_of_aux subst metasenv context coerc ugraph
1287                   in
1288                   try
1289                     let metasenv, hetype' =
1290                       mk_prod_of_metas metasenv context subst remainder
1291                     in
1292                     debug_print (lazy
1293                       ("  unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^
1294                        CicMetaSubst.ppterm ~metasenv subst hetype'));
1295                     let subst,metasenv,ugraph =
1296                       fo_unif_subst_eat_prods
1297                         subst context metasenv tty hetype' ugraph
1298                     in
1299                     debug_print (lazy " success!");
1300                     Some (subst,metasenv,ugraph,tty,t,remainder)
1301                   with
1302                   | Uncertain _ | RefineFailure _ ->
1303                       try
1304                         let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
1305                           fix_arity
1306                             metasenv context subst t tty remainder ugraph
1307                         in
1308                         Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
1309                       with Uncertain _ | RefineFailure _ -> None
1310                 with
1311                    Uncertain _
1312                  | RefineFailure _
1313                  | HExtlib.Localized (_,Uncertain _)
1314                  | HExtlib.Localized (_,RefineFailure _) -> None
1315                  | exn -> assert false) (* ritornare None, e' un localized *)
1316               candidates
1317            with
1318            | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
1319                subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1320            | None ->
1321                more_args_than_expected localization_tbl metasenv
1322                  subst he context hetype args_bo_and_ty exn
1323       (* }}} end coercion to funclass stuff *)
1324       (* }}} end fix_arity *)
1325     in
1326     (* aux function to process the type of the head and the args in parallel *)
1327     let rec eat_prods_and_args
1328       pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
1329     =
1330       (* {{{ body *)
1331       function
1332         | [] -> newargs,subst,metasenv,he,hetype,ugraph
1333         | (hete, hety)::tl ->
1334             match (CicReduction.whd ~subst context hetype) with
1335             | Cic.Prod (n,s,t) ->
1336                 let arg,subst,metasenv,ugraph1 =
1337                  try
1338                   (try
1339                     let subst,metasenv,ugraph1 =
1340                       fo_unif_subst_eat_prods2
1341                         subst context metasenv hety s ugraph
1342                     in
1343                       (hete,hety),subst,metasenv,ugraph1
1344                   with RefineFailure _ | Uncertain _ as exn
1345                   when allow_coercions && !insert_coercions ->
1346                      coerce_to_something
1347                        hete hety s subst metasenv context exn ugraph)
1348                  with exn ->
1349                      enrich localization_tbl hete
1350                       ~f:(fun _ ->
1351                         (lazy ("(2)The term " ^
1352                           CicMetaSubst.ppterm_in_context ~metasenv subst hete
1353                            context ^ " has type " ^
1354                           CicMetaSubst.ppterm_in_context ~metasenv subst hety
1355                            context ^ " but is here used with type " ^
1356                           CicMetaSubst.ppterm_in_context
1357                             ~metasenv subst s context
1358                            (* "\nReason: " ^ Printexc.to_string exn*)))) exn
1359                 in
1360                   eat_prods_and_args pristinemenv metasenv subst context pristinehe he
1361                     (CicSubstitution.subst (fst arg) t)
1362                     ugraph1 (newargs@[arg]) tl
1363             | _ ->
1364                 try
1365                   let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1366                     fix_arity
1367                       pristinemenv context subst he hetype
1368                        (newargs@[hete,hety]@tl) ugraph
1369                   in
1370                   eat_prods_and_args metasenv
1371                     metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
1372                 with RefineFailure _ | Uncertain _ as exn ->
1373                   (* unable to fix arity *)
1374                    more_args_than_expected localization_tbl metasenv
1375                      subst he context hetype args_bo_and_ty exn
1376       (* }}} *)
1377     in
1378     (* first we check if we are in the simple case of a meta closed term *)
1379     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1380      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1381       (* this optimization is to postpone fix_arity (the most common case)*)
1382       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1383      else
1384        (* this (says CSC) is also useful to infer dependent types *)
1385        try
1386         fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
1387        with RefineFailure _ | Uncertain _ as exn ->
1388          (* unable to fix arity *)
1389           more_args_than_expected localization_tbl metasenv
1390             subst he context hetype args_bo_and_ty exn
1391     in
1392     let coerced_args,subst,metasenv,he,t,ugraph =
1393       eat_prods_and_args
1394         metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
1395     in
1396     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1397
1398   and coerce_to_something t infty expty subst metasenv context exn ugraph =
1399     if not !insert_coercions then
1400       raise exn
1401     else
1402     let clean t subst context =
1403       CicReduction.whd ~delta:false context (CicMetaSubst.apply_subst subst t)
1404     in
1405     let infty = clean infty subst context in
1406     let expty = clean expty subst context in
1407     match infty, expty with
1408     | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) ->
1409         (* covariant part *)
1410         let name_con = Cic.Name "name_con" in
1411         let name_t, ty_s_bo, bo =
1412           match t with
1413           | Cic.Lambda (name, src, bo) -> name, src, bo
1414           | _ -> name_con, src, Cic.Appl [CicSubstitution.lift 1 t ; Cic.Rel 1]
1415         in
1416         let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in
1417         let (bo, _), subst, metasenv, ugraph =
1418           coerce_to_something bo ty ty2 subst metasenv context_bo exn ugraph
1419         in
1420         (* contravariant part *)
1421         let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in
1422         let (rel1, _), subst, metasenv, ugraph =
1423           coerce_to_something (Cic.Rel 1) (CicSubstitution.lift 1 src2)
1424             (CicSubstitution.lift 1 src) subst metasenv context_rel1 exn
1425             ugraph
1426         in
1427         let coerced =
1428           Cic.Lambda (name_t,src2,
1429             CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo))
1430         in
1431           (coerced, expty), subst, metasenv, ugraph
1432     | _ ->
1433        coerce_atom_to_something t infty expty subst metasenv context exn ugraph
1434
1435   and coerce_atom_to_something t infty expty subst metasenv context exn ugraph =
1436     let coer =
1437       CoercGraph.look_for_coercion metasenv subst context infty expty
1438     in
1439       match coer with
1440       | CoercGraph.NotMetaClosed ->
1441           (match exn with
1442           | RefineFailure s -> raise (Uncertain s)
1443           | HExtlib.Localized _ -> assert false
1444           | _ -> raise exn)
1445       | CoercGraph.NoCoercion
1446       | CoercGraph.SomeCoercionToTgt _
1447       | CoercGraph.NotHandled _ ->
1448                       raise exn
1449       | CoercGraph.SomeCoercion candidates ->
1450           let selected =
1451             HExtlib.list_findopt
1452               (fun (metasenv,last,c) ->
1453                try
1454                 let subst,metasenv,ugraph =
1455                  fo_unif_subst subst context metasenv last t
1456                   ugraph in
1457                 let newt,newhety,subst,metasenv,ugraph =
1458                  type_of_aux subst metasenv context
1459                   c ugraph
1460                 in
1461                 let newt, newty, subst, metasenv, ugraph =
1462                  avoid_double_coercion context subst metasenv
1463                   ugraph newt expty
1464                 in
1465                 let subst,metasenv,ugraph1 =
1466                   fo_unif_subst subst context metasenv
1467                      newhety expty ugraph
1468                 in
1469                  Some ((newt,newty), subst, metasenv, ugraph)
1470                with Uncertain _ | RefineFailure _ -> None)
1471               candidates
1472           in
1473           match selected with
1474           | Some x -> x
1475           | None -> raise exn
1476
1477   and coerce_to_sort
1478         in_source tgt_sort t type_to_coerce subst context metasenv uragph =
1479       match CicReduction.whd ~subst:subst context type_to_coerce with
1480       | Cic.Meta _ | Cic.Sort _ ->
1481           t,type_to_coerce, subst, metasenv, ugraph
1482       | src ->
1483          let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
1484          let exn =
1485            RefineFailure (lazy ("(7)The term " ^
1486             CicMetaSubst.ppterm_in_context ~metasenv subst t context
1487             ^ " is not a type since it has type " ^
1488             CicMetaSubst.ppterm_in_context ~metasenv subst src context
1489             ^ " that is not a sort"))
1490          in
1491          try
1492            let (t, ty_t), subst, metasenv, ugraph =
1493              coerce_to_something t src tgt
1494                subst metasenv context exn ugraph
1495            in
1496            t, ty_t, subst, metasenv, ugraph
1497          with exn -> enrich localization_tbl t exn
1498   in
1499
1500   (* eat prods ends here! *)
1501
1502   let t',ty,subst',metasenv',ugraph1 =
1503    type_of_aux [] metasenv context t ugraph
1504   in
1505   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1506   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1507     (* Andrea: ho rimesso qui l'applicazione della subst al
1508        metasenv dopo che ho droppato l'invariante che il metsaenv
1509        e' sempre istanziato *)
1510   let substituted_metasenv =
1511     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1512     (* metasenv' *)
1513     (*  substituted_t,substituted_ty,substituted_metasenv *)
1514     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1515   let cleaned_t =
1516     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1517   let cleaned_ty =
1518     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1519   let cleaned_metasenv =
1520     List.map
1521       (function (n,context,ty) ->
1522          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1523          let context' =
1524            List.map
1525              (function
1526                   None -> None
1527                 | Some (n, Cic.Decl t) ->
1528                     Some (n,
1529                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1530                 | Some (n, Cic.Def (bo,ty)) ->
1531                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1532                     let ty' =
1533                       match ty with
1534                           None -> None
1535                         | Some ty ->
1536                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1537                     in
1538                       Some (n, Cic.Def (bo',ty'))
1539              ) context
1540          in
1541            (n,context',ty')
1542       ) substituted_metasenv
1543   in
1544     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1545 ;;
1546
1547 let undebrujin uri typesno tys t =
1548   snd
1549    (List.fold_right
1550      (fun (name,_,_,_) (i,t) ->
1551        (* here the explicit_named_substituion is assumed to be *)
1552        (* of length 0 *)
1553        let t' = Cic.MutInd (uri,i,[])  in
1554        let t = CicSubstitution.subst t' t in
1555         i - 1,t
1556      ) tys (typesno - 1,t))
1557
1558 let map_first_n n start f g l =
1559   let rec aux acc k l =
1560     if k < n then
1561       match l with
1562       | [] -> raise (Invalid_argument "map_first_n")
1563       | hd :: tl -> f hd k (aux acc (k+1) tl)
1564     else
1565       g acc l
1566   in
1567   aux start 0 l
1568
1569 (*CSC: this is a very rough approximation; to be finished *)
1570 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1571   let subst,metasenv,ugraph,tys =
1572     List.fold_right
1573       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1574         let subst,metasenv,ugraph,cl =
1575           List.fold_right
1576             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1577                let rec aux ctx k subst = function
1578                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1579                      let subst,metasenv,ugraph,tl =
1580                        map_first_n leftno
1581                          (subst,metasenv,ugraph,[])
1582                          (fun t n (subst,metasenv,ugraph,acc) ->
1583                            let subst,metasenv,ugraph =
1584                              fo_unif_subst
1585                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1586                            in
1587                            subst,metasenv,ugraph,(t::acc))
1588                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1589                          tl
1590                      in
1591                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1592                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1593                      subst,metasenv,ugraph,t
1594                  | Cic.Prod (name,s,t) ->
1595                      let ctx = (Some (name,Cic.Decl s))::ctx in
1596                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1597                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1598                  | _ ->
1599                      raise
1600                       (RefineFailure
1601                         (lazy "not well formed constructor type"))
1602                in
1603                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1604                subst,metasenv,ugraph,(name,ty) :: acc)
1605           cl (subst,metasenv,ugraph,[])
1606         in
1607         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1608       tys ([],metasenv,ugraph,[])
1609   in
1610   let substituted_tys =
1611     List.map
1612       (fun (name,ind,arity,cl) ->
1613         let cl =
1614           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1615         in
1616         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1617       tys
1618   in
1619   metasenv,ugraph,substituted_tys
1620
1621 let typecheck metasenv uri obj ~localization_tbl =
1622  let ugraph = CicUniv.empty_ugraph in
1623  match obj with
1624     Cic.Constant (name,Some bo,ty,args,attrs) ->
1625      let bo',boty,metasenv,ugraph =
1626       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1627      let ty',_,metasenv,ugraph =
1628       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1629      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1630      let bo' = CicMetaSubst.apply_subst subst bo' in
1631      let ty' = CicMetaSubst.apply_subst subst ty' in
1632      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1633       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1634   | Cic.Constant (name,None,ty,args,attrs) ->
1635      let ty',_,metasenv,ugraph =
1636       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1637      in
1638       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1639   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1640      assert (metasenv' = metasenv);
1641      (* Here we do not check the metasenv for correctness *)
1642      let bo',boty,metasenv,ugraph =
1643       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1644      let ty',sort,metasenv,ugraph =
1645       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1646      begin
1647       match sort with
1648          Cic.Sort _
1649        (* instead of raising Uncertain, let's hope that the meta will become
1650           a sort *)
1651        | Cic.Meta _ -> ()
1652        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1653      end;
1654      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1655      let bo' = CicMetaSubst.apply_subst subst bo' in
1656      let ty' = CicMetaSubst.apply_subst subst ty' in
1657      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1658       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1659   | Cic.Variable _ -> assert false (* not implemented *)
1660   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1661      (*CSC: this code is greately simplified and many many checks are missing *)
1662      (*CSC: e.g. the constructors are not required to build their own types,  *)
1663      (*CSC: the arities are not required to have as type a sort, etc.         *)
1664      let uri = match uri with Some uri -> uri | None -> assert false in
1665      let typesno = List.length tys in
1666      (* first phase: we fix only the types *)
1667      let metasenv,ugraph,tys =
1668       List.fold_right
1669        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1670          let ty',_,metasenv,ugraph =
1671           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1672          in
1673           metasenv,ugraph,(name,b,ty',cl)::res
1674        ) tys (metasenv,ugraph,[]) in
1675      let con_context =
1676       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1677      (* second phase: we fix only the constructors *)
1678      let saved_menv = metasenv in
1679      let metasenv,ugraph,tys =
1680       List.fold_right
1681        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1682          let metasenv,ugraph,cl' =
1683           List.fold_right
1684            (fun (name,ty) (metasenv,ugraph,res) ->
1685              let ty =
1686               CicTypeChecker.debrujin_constructor
1687                ~cb:(relocalize localization_tbl) uri typesno ty in
1688              let ty',_,metasenv,ugraph =
1689               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1690              let ty' = undebrujin uri typesno tys ty' in
1691               metasenv@saved_menv,ugraph,(name,ty')::res
1692            ) cl (metasenv,ugraph,[])
1693          in
1694           metasenv,ugraph,(name,b,ty,cl')::res
1695        ) tys (metasenv,ugraph,[]) in
1696      (* third phase: we check the positivity condition *)
1697      let metasenv,ugraph,tys =
1698        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1699      in
1700      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1701 ;;
1702
1703 (* sara' piu' veloce che raffinare da zero? mah.... *)
1704 let pack_coercion metasenv ctx t =
1705  let module C = Cic in
1706  let rec merge_coercions ctx =
1707    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
1708    function
1709    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
1710    | C.Meta (n,subst) ->
1711       let subst' =
1712        List.map
1713         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
1714       in
1715        C.Meta (n,subst')
1716    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
1717    | C.Prod (name,so,dest) ->
1718        let ctx' = (Some (name,C.Decl so))::ctx in
1719        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
1720    | C.Lambda (name,so,dest) ->
1721        let ctx' = (Some (name,C.Decl so))::ctx in
1722        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
1723    | C.LetIn (name,so,dest) ->
1724        let _,ty,metasenv,ugraph =
1725         pack_coercions := false;
1726         type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
1727         pack_coercions := true;
1728        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
1729        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
1730    | C.Appl l ->
1731       let l = List.map (merge_coercions ctx) l in
1732       let t = C.Appl l in
1733        let b,_,_,_,_ = is_a_double_coercion t in
1734        if b then
1735          let ugraph = CicUniv.oblivion_ugraph in
1736          let old_insert_coercions = !insert_coercions in
1737          insert_coercions := false;
1738          let newt, _, menv, _ =
1739            try
1740              type_of_aux' metasenv ctx t ugraph
1741            with RefineFailure _ | Uncertain _ ->
1742              t, t, [], ugraph
1743          in
1744          insert_coercions := old_insert_coercions;
1745          if metasenv <> [] || menv = [] then
1746            newt
1747          else
1748            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
1749        else
1750          t
1751    | C.Var (uri,exp_named_subst) ->
1752        let exp_named_subst = List.map aux exp_named_subst in
1753        C.Var (uri, exp_named_subst)
1754    | C.Const (uri,exp_named_subst) ->
1755        let exp_named_subst = List.map aux exp_named_subst in
1756        C.Const (uri, exp_named_subst)
1757    | C.MutInd (uri,tyno,exp_named_subst) ->
1758        let exp_named_subst = List.map aux exp_named_subst in
1759        C.MutInd (uri,tyno,exp_named_subst)
1760    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
1761        let exp_named_subst = List.map aux exp_named_subst in
1762        C.MutConstruct (uri,tyno,consno,exp_named_subst)
1763    | C.MutCase (uri,tyno,out,te,pl) ->
1764        let pl = List.map (merge_coercions ctx) pl in
1765        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
1766    | C.Fix (fno, fl) ->
1767        let ctx' =
1768          List.fold_left
1769            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1770            ctx fl
1771        in
1772        let fl =
1773          List.map
1774            (fun (name,idx,ty,bo) ->
1775              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
1776          fl
1777        in
1778        C.Fix (fno, fl)
1779    | C.CoFix (fno, fl) ->
1780        let ctx' =
1781          List.fold_left
1782            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
1783            ctx fl
1784        in
1785        let fl =
1786          List.map
1787            (fun (name,ty,bo) ->
1788              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
1789          fl
1790        in
1791        C.CoFix (fno, fl)
1792  in
1793   merge_coercions ctx t
1794 ;;
1795
1796 let pack_coercion_metasenv conjectures =
1797   let module C = Cic in
1798   List.map
1799     (fun (i, ctx, ty) ->
1800        let ctx =
1801          List.fold_right
1802            (fun item ctx ->
1803               let item' =
1804                 match item with
1805                     Some (name, C.Decl t) ->
1806                       Some (name, C.Decl (pack_coercion conjectures ctx t))
1807                   | Some (name, C.Def (t,None)) ->
1808                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
1809                   | Some (name, C.Def (t,Some ty)) ->
1810                       Some (name, C.Def (pack_coercion conjectures ctx t,
1811                                          Some (pack_coercion conjectures ctx ty)))
1812                   | None -> None
1813               in
1814                 item'::ctx
1815            ) ctx []
1816        in
1817          ((i,ctx,pack_coercion conjectures ctx ty))
1818     ) conjectures
1819 ;;
1820
1821 let pack_coercion_obj obj =
1822   let module C = Cic in
1823   match obj with
1824   | C.Constant (id, body, ty, params, attrs) ->
1825       let body =
1826         match body with
1827         | None -> None
1828         | Some body -> Some (pack_coercion [] [] body)
1829       in
1830       let ty = pack_coercion [] [] ty in
1831         C.Constant (id, body, ty, params, attrs)
1832   | C.Variable (name, body, ty, params, attrs) ->
1833       let body =
1834         match body with
1835         | None -> None
1836         | Some body -> Some (pack_coercion [] [] body)
1837       in
1838       let ty = pack_coercion [] [] ty in
1839         C.Variable (name, body, ty, params, attrs)
1840   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
1841       let conjectures = pack_coercion_metasenv conjectures in
1842       let body = pack_coercion conjectures [] body in
1843       let ty = pack_coercion conjectures [] ty in
1844       C.CurrentProof (name, conjectures, body, ty, params, attrs)
1845   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
1846       let indtys =
1847         List.map
1848           (fun (name, ind, arity, cl) ->
1849             let arity = pack_coercion [] [] arity in
1850             let cl =
1851               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
1852             in
1853             (name, ind, arity, cl))
1854           indtys
1855       in
1856         C.InductiveDefinition (indtys, params, leftno, attrs)
1857 ;;
1858
1859
1860 (* DEBUGGING ONLY
1861 let type_of_aux' metasenv context term =
1862  try
1863   let (t,ty,m) =
1864       type_of_aux' metasenv context term in
1865     debug_print (lazy
1866      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1867    debug_print (lazy
1868     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1869    (t,ty,m)
1870  with
1871  | RefineFailure msg as e ->
1872      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1873      raise e
1874  | Uncertain msg as e ->
1875      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1876      raise e
1877 ;; *)
1878
1879 let profiler2 = HExtlib.profile "CicRefine"
1880
1881 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1882  profiler2.HExtlib.profile
1883   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1884
1885 let typecheck ~localization_tbl metasenv uri obj =
1886  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
1887
1888 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
1889 (* vim:set foldmethod=marker: *)