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