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