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