helm/software/components/ng_refiner/nCicRefiner.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 let exp_implicit metasenv subst context expty =
  15  function
  16   | Some `Closed -> NCicMetaSubst.mk_meta metasenv [] expty
  17   | Some `Type | None -> NCicMetaSubst.mk_meta metasenv context expty
  18   | _ -> assert false
  19 ;;
  20
  21 let sort_of_prod localise metasenv subst context (name,s) t (t1, t2) =
  22    let restrict metasenv subst = function
  23      | NCic.Meta (i,(_,(NCic.Irl 0 | NCic.Ctx []))) as t ->
  24         metasenv, subst, t
  25      | NCic.Meta (i,(_,lc)) as t ->
  26         let len = match lc with NCic.Irl len->len | NCic.Ctx l->List.lenght l in
  27         let metasenv, subst, _ =
  28           NCicMetaSubst.restrict metasenv subst i (HExtlib.seq 1 len)
  29         in
  30         metasenv, subst, t
  31      | t -> metasenv, subst, t
  32    in
  33    let t1 = R.whd ~subst context t1 in
  34    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
  35    let metasenv, subst, t1 = restrict metasenv subst t1 in
  36    let metasenv, subst, t2 = restrict metasenv subst t2 in
  37    match t1, t2 with
  38    | C.Sort _, C.Sort C.Prop -> metasenv, subst, t2
  39    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
  40         metasenv, subst, C.Sort (C.Type (u1@u2))
  41    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2
  42    | C.Meta _, C.Sort _
  43    | C.Meta _, C.Meta _
  44    | C.Sort _, C.Meta  _ -> metasenv, subst, t2
  45    | x, _ | _, x ->
  46       let y, context =
  47         if x == t1 then s, context else t, ((name,C.Decl s)::context)
  48       in
  49       raise (TypeCheckerFailure (lazy (Printf.sprintf
  50         "%s is expected to be a type, but its type is %s that is not a sort"
  51          (PP.ppterm ~subst ~metasenv ~context y)
  52          (PP.ppterm ~subst ~metasenv ~context x))))
  53 ;;
  54
  55 let rec typeof
  56   ?(localize=fun _ -> Stdpp.dummy) metasenv subst context term expty
  57 =
  58   let force_ty metasenv subst context t infty = function
  59     | Some expty ->
  60        (match t with
  61        | NCic.Implicit _ -> metasenv, subst, t, expty
  62        | _ ->
  63          let metasenv, subst =
  64            NCicUnification.unify metasenv subst context infty expty in
  65          metasenv, subst, t, expty)
  66     | None -> metasenv, subst, t, infty
  67   in
  68   let rec typeof_aux metasenv subst context expty =
  69     fun t -> (*prerr_endline (PP.ppterm ~metasenv ~subst ~context t);*)
  70     let metasenv, subst, t, infty =
  71     match t with
  72     | C.Rel n ->
  73         let infty =
  74          (try
  75            match List.nth context (n - 1) with
  76            | (_,C.Decl ty) -> S.lift n ty
  77            | (_,C.Def (_,ty)) -> S.lift n ty
  78          with Failure _ ->
  79            raise (RefineFailure (lazy (localize t,"unbound variable"))))
  80         in
  81         metasenv, subst, t, infty
  82     | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
  83     | C.Sort (C.Type _) ->
  84         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
  85           NCicPp.ppterm ~subst ~metasenv ~context t)))
  86     | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
  87     | C.Implicit infos ->
  88          let metasenv,t,ty = exp_implicit metasenv subst context infos expty in
  89          metasenv, subst, t, ty
  90     | C.Meta (n,l) as t ->
  91        let ty =
  92         try
  93          let _,_,_,ty = U.lookup_subst n subst in
  94         with U.Subst_not_found _ -> try
  95          let _,_,ty = U.lookup_meta n metasenv in
  96          match ty with C.Implicit _ -> assert false | _ -> c,ty
  97         with U.Meta_not_found _ ->
  98          raise (AssertFailure (lazy (Printf.sprintf
  99           "%s not found" (PP.ppterm ~subst ~metasenv ~context t))))
 100        in
 101        metasenv, subst, t, S.subst_meta l ty
 102     | C.Const _ ->
 103        metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
 104     | C.Prod (name,s,t) as orig ->
 105        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
 106        let context = (name,(NCic.Decl s))::context in
 107        let metasenv, subst, t, s2 = typeof_aux metasenv subst context None t in
 108        let metasenv, subst, ty =
 109          sort_of_prod localize metasenv subst context (name,s) t (s1,s2)
 110        in
 111        metasenv, subst, orig, ty
 112     | C.Lambda (n,s,t) ->
 113        let sort = typeof_aux context s in
 114        (match R.whd ~subst context sort with
 115        | C.Meta _ | C.Sort _ -> ()
 116        | _ ->
 117          raise
 118            (TypeCheckerFailure (lazy (Printf.sprintf
 119              ("Not well-typed lambda-abstraction: " ^^
 120              "the source %s should be a type; instead it is a term " ^^
 121              "of type %s") (PP.ppterm ~subst ~metasenv ~context s)
 122              (PP.ppterm ~subst ~metasenv ~context sort)))));
 123        let ty = typeof_aux ((n,(C.Decl s))::context) t in
 124          C.Prod (n,s,ty)
 125     | C.LetIn (n,ty,t,bo) ->
 126        let ty_t = typeof_aux context t in
 127        let _ = typeof_aux context ty in
 128        if not (R.are_convertible ~subst context ty_t ty) then
 129          raise
 130           (TypeCheckerFailure
 131             (lazy (Printf.sprintf
 132               "The type of %s is %s but it is expected to be %s"
 133                 (PP.ppterm ~subst ~metasenv ~context t)
 134                 (PP.ppterm ~subst ~metasenv ~context ty_t)
 135                 (PP.ppterm ~subst ~metasenv ~context ty))))
 136        else
 137          let ty_bo = typeof_aux  ((n,C.Def (t,ty))::context) bo in
 138          S.subst ~avoid_beta_redexes:true t ty_bo
 139     | C.Appl (he::(_::_ as args)) ->
 140        let ty_he = typeof_aux context he in
 141        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 142        eat_prods ~subst ~metasenv context he ty_he args_with_ty
 143    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
 144    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,outtype,term,pl) ->
 145       let outsort = typeof_aux context outtype in
 146       let _,leftno,itl,_,_ = E.get_checked_indtys r in
 147       let constructorsno =
 148         let _,_,_,cl = List.nth itl tyno in List.length cl
 149       in
 150       let parameters, arguments =
 151         let ty = R.whd ~subst context (typeof_aux context term) in
 152         let r',tl =
 153          match ty with
 154             C.Const (Ref.Ref (_,Ref.Ind _) as r') -> r',[]
 155           | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as r') :: tl) -> r',tl
 156           | _ ->
 157              raise
 158                (TypeCheckerFailure (lazy (Printf.sprintf
 159                  "Case analysis: analysed term %s is not an inductive one"
 160                  (PP.ppterm ~subst ~metasenv ~context term)))) in
 161         if not (Ref.eq r r') then
 162          raise
 163           (TypeCheckerFailure (lazy (Printf.sprintf
 164             ("Case analysys: analysed term type is %s, but is expected " ^^
 165              "to be (an application of) %s")
 166             (PP.ppterm ~subst ~metasenv ~context ty)
 167             (PP.ppterm ~subst ~metasenv ~context (C.Const r')))))
 168         else
 169          try HExtlib.split_nth leftno tl
 170          with
 171           Failure _ ->
 172            raise (TypeCheckerFailure (lazy (Printf.sprintf
 173            "%s is partially applied"
 174            (PP.ppterm  ~subst ~metasenv ~context ty)))) in
 175       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 176       let sort_of_ind_type =
 177         if parameters = [] then C.Const r
 178         else C.Appl ((C.Const r)::parameters) in
 179       let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
 180       check_allowed_sort_elimination ~subst ~metasenv r context
 181        sort_of_ind_type type_of_sort_of_ind_ty outsort;
 182       (* let's check if the type of branches are right *)
 183       if List.length pl <> constructorsno then
 184        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
 185       let j,branches_ok,p_ty, exp_p_ty =
 186         List.fold_left
 187           (fun (j,b,old_p_ty,old_exp_p_ty) p ->
 188             if b then
 189               let cons =
 190                 let cons = Ref.mk_constructor j r in
 191                 if parameters = [] then C.Const cons
 192                 else C.Appl (C.Const cons::parameters)
 193               in
 194               let ty_p = typeof_aux context p in
 195               let ty_cons = typeof_aux context cons in
 196               let ty_branch =
 197                 type_of_branch ~subst context leftno outtype cons ty_cons 0
 198               in
 199               j+1, R.are_convertible ~subst context ty_p ty_branch,
 200               ty_p, ty_branch
 201             else
 202               j,false,old_p_ty,old_exp_p_ty
 203           ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
 204       in
 205       if not branches_ok then
 206         raise
 207          (TypeCheckerFailure
 208           (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
 209           "has type %s\nnot convertible with %s")
 210           (PP.ppterm  ~subst ~metasenv ~context
 211             (C.Const (Ref.mk_constructor (j-1) r)))
 212           (PP.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
 213           (PP.ppterm ~metasenv ~subst ~context p_ty)
 214           (PP.ppterm ~metasenv ~subst ~context exp_p_ty))));
 215       let res = outtype::arguments@[term] in
 216       R.head_beta_reduce (C.Appl res)
 217     | C.Match _ -> assert false
 218
 219   and type_of_branch ~subst context leftno outty cons tycons liftno =
 220     match R.whd ~subst context tycons with
 221     | C.Const (Ref.Ref (_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
 222     | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _))::tl) ->
 223         let _,arguments = HExtlib.split_nth leftno tl in
 224         C.Appl (S.lift liftno outty::arguments@[cons])
 225     | C.Prod (name,so,de) ->
 226         let cons =
 227          match S.lift 1 cons with
 228          | C.Appl l -> C.Appl (l@[C.Rel 1])
 229          | t -> C.Appl [t ; C.Rel 1]
 230         in
 231          C.Prod (name,so,
 232            type_of_branch ~subst ((name,(C.Decl so))::context)
 233             leftno outty cons de (liftno+1))
 234     | _ -> raise (AssertFailure (lazy "type_of_branch"))
 235
 236   (* check_metasenv_consistency checks that the "canonical" context of a
 237      metavariable is consitent - up to relocation via the relocation list l -
 238      with the actual context *)
 239   and check_metasenv_consistency
 240     ~subst ~metasenv term context canonical_context l
 241   =
 242    match l with
 243     | shift, C.Irl n ->
 244        let context = snd (HExtlib.split_nth shift context) in
 245         let rec compare = function
 246          | 0,_,[] -> ()
 247          | 0,_,_::_
 248          | _,_,[] ->
 249             raise (AssertFailure (lazy (Printf.sprintf
 250              "Local and canonical context %s have different lengths"
 251              (PP.ppterm ~subst ~context ~metasenv term))))
 252          | m,[],_::_ ->
 253             raise (TypeCheckerFailure (lazy (Printf.sprintf
 254              "Unbound variable -%d in %s" m
 255              (PP.ppterm ~subst ~metasenv ~context term))))
 256          | m,t::tl,ct::ctl ->
 257             (match t,ct with
 258                 (_,C.Decl t1), (_,C.Decl t2)
 259               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
 260               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
 261                  if not (R.are_convertible ~subst tl t1 t2) then
 262                   raise
 263                       (TypeCheckerFailure
 264                         (lazy (Printf.sprintf
 265                       ("Not well typed metavariable local context for %s: " ^^
 266                        "%s expected, which is not convertible with %s")
 267                       (PP.ppterm ~subst ~metasenv ~context term)
 268                       (PP.ppterm ~subst ~metasenv ~context t2)
 269                       (PP.ppterm ~subst ~metasenv ~context t1))))
 270               | _,_ ->
 271                raise
 272                    (TypeCheckerFailure (lazy (Printf.sprintf
 273                     ("Not well typed metavariable local context for %s: " ^^
 274                      "a definition expected, but a declaration found")
 275                     (PP.ppterm ~subst ~metasenv ~context term)))));
 276             compare (m - 1,tl,ctl)
 277         in
 278          compare (n,context,canonical_context)
 279     | shift, lc_kind ->
 280        (* we avoid useless lifting by shortening the context*)
 281        let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in
 282        let lifted_canonical_context =
 283          let rec lift_metas i = function
 284            | [] -> []
 285            | (n,C.Decl t)::tl ->
 286                (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
 287            | (n,C.Def (t,ty))::tl ->
 288                (n,C.Def ((S.subst_meta l (S.lift i t)),
 289                           S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
 290          in
 291           lift_metas 1 canonical_context in
 292        let l = U.expand_local_context lc_kind in
 293        try
 294         List.iter2
 295         (fun t ct ->
 296           match (t,ct) with
 297           | t, (_,C.Def (ct,_)) ->
 298              (*CSC: the following optimization is to avoid a possibly expensive
 299                     reduction that can be easily avoided and that is quite
 300                     frequent. However, this is better handled using levels to
 301                     control reduction *)
 302              let optimized_t =
 303               match t with
 304               | C.Rel n ->
 305                   (try
 306                     match List.nth context (n - 1) with
 307                     | (_,C.Def (te,_)) -> S.lift n te
 308                     | _ -> t
 309                     with Failure _ -> t)
 310               | _ -> t
 311              in
 312              if not (R.are_convertible ~subst context optimized_t ct)
 313              then
 314                raise
 315                  (TypeCheckerFailure
 316                    (lazy (Printf.sprintf
 317                      ("Not well typed metavariable local context: " ^^
 318                       "expected a term convertible with %s, found %s")
 319                      (PP.ppterm ~subst ~metasenv ~context ct)
 320                      (PP.ppterm ~subst ~metasenv ~context t))))
 321           | t, (_,C.Decl ct) ->
 322               let type_t = typeof_aux context t in
 323               if not (R.are_convertible ~subst context type_t ct) then
 324                 raise (TypeCheckerFailure
 325                  (lazy (Printf.sprintf
 326                   ("Not well typed metavariable local context: "^^
 327                   "expected a term of type %s, found %s of type %s")
 328                   (PP.ppterm ~subst ~metasenv ~context ct)
 329                   (PP.ppterm ~subst ~metasenv ~context t)
 330                   (PP.ppterm ~subst ~metasenv ~context type_t))))
 331         ) l lifted_canonical_context
 332        with
 333         Invalid_argument _ ->
 334           raise (AssertFailure (lazy (Printf.sprintf
 335            "Local and canonical context %s have different lengths"
 336            (PP.ppterm ~subst ~metasenv ~context term))))
 337
 338   and check_allowed_sort_elimination ~subst ~metasenv r =
 339    let mkapp he arg =
 340      match he with
 341      | C.Appl l -> C.Appl (l @ [arg])
 342      | t -> C.Appl [t;arg] in
 343    let rec aux context ind arity1 arity2 =
 344     let arity1 = R.whd ~subst context arity1 in
 345     let arity2 = R.whd ~subst context arity2 in
 346       match arity1,arity2 with
 347        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
 348           if not (R.are_convertible ~subst context so1 so2) then
 349            raise (TypeCheckerFailure (lazy (Printf.sprintf
 350             "In outtype: expected %s, found %s"
 351             (PP.ppterm ~subst ~metasenv ~context so1)
 352             (PP.ppterm ~subst ~metasenv ~context so2)
 353             )));
 354           aux ((name, C.Decl so1)::context)
 355            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
 356        | C.Sort _, C.Prod (name,so,ta) ->
 357           if not (R.are_convertible ~subst context so ind) then
 358            raise (TypeCheckerFailure (lazy (Printf.sprintf
 359             "In outtype: expected %s, found %s"
 360             (PP.ppterm ~subst ~metasenv ~context ind)
 361             (PP.ppterm ~subst ~metasenv ~context so)
 362             )));
 363           (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
 364             | (C.Sort C.Type _, C.Sort _)
 365             | (C.Sort C.Prop, C.Sort C.Prop) -> ()
 366             | (C.Sort C.Prop, C.Sort C.Type _) ->
 367         (* TODO: we should pass all these parameters since we
 368          * have them already *)
 369                 let _,leftno,itl,_,i = E.get_checked_indtys r in
 370                 let itl_len = List.length itl in
 371                 let _,itname,ittype,cl = List.nth itl i in
 372                 let cl_len = List.length cl in
 373                  (* is it a singleton, non recursive and non informative
 374                     definition or an empty one? *)
 375                  if not
 376                   (cl_len = 0 ||
 377                    (itl_len = 1 && cl_len = 1 &&
 378                     let _,_,constrty = List.hd cl in
 379                       is_non_recursive_singleton r itname ittype constrty &&
 380                       is_non_informative leftno constrty))
 381                  then
 382                   raise (TypeCheckerFailure (lazy
 383                    ("Sort elimination not allowed")));
 384           | _,_ -> ())
 385        | _,_ -> ()
 386    in
 387     aux
 388
 389  in
 390    typeof_aux context term
 391
 392 and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
 393   let rec aux ty_he = function
 394   | [] -> ty_he
 395   | (arg, ty_arg)::tl ->
 396       match R.whd ~subst context ty_he with
 397       | C.Prod (_,s,t) ->
 398           if R.are_convertible ~subst context ty_arg s then
 399             aux (S.subst ~avoid_beta_redexes:true arg t) tl
 400           else
 401             raise
 402               (TypeCheckerFailure
 403                 (lazy (Printf.sprintf
 404                   ("Appl: wrong application of %s: the parameter %s has type"^^
 405                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
 406                   (PP.ppterm ~subst ~metasenv ~context he)
 407                   (PP.ppterm ~subst ~metasenv ~context arg)
 408                   (PP.ppterm ~subst ~metasenv ~context ty_arg)
 409                   (PP.ppterm ~subst ~metasenv ~context s)
 410                   (PP.ppcontext ~subst ~metasenv context))))
 411        | _ ->
 412           raise
 413             (TypeCheckerFailure
 414               (lazy (Printf.sprintf
 415                 "Appl: %s is not a function, it cannot be applied"
 416                 (PP.ppterm ~subst ~metasenv ~context
 417                  (let res = List.length tl in
 418                   let eaten = List.length args_with_ty - res in
 419                    (C.Appl
 420                     (he::List.map fst
 421                      (fst (HExtlib.split_nth eaten args_with_ty)))))))))
 422   in
 423     aux ty_he args_with_ty
 424
 425
 426 (*
 427 open Printf
 428
 429 exception RefineFailure of string Lazy.t;;
 430 exception Uncertain of string Lazy.t;;
 431 exception AssertFailure of string Lazy.t;;
 432
 433 (* for internal use only; the integer is the number of surplus arguments *)
 434 exception MoreArgsThanExpected of int * exn;;
 435
 436 let insert_coercions = ref true
 437 let pack_coercions = ref true
 438
 439 let debug = false;;
 440
 441 let debug_print =
 442   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
 443
 444 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
 445
 446 let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
 447   try
 448 let foo () =
 449     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
 450 in profiler_eat_prods2.HExtlib.profile foo ()
 451   with
 452       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
 453     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 454 ;;
 455
 456 let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
 457
 458 let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
 459   try
 460 let foo () =
 461     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
 462 in profiler_eat_prods.HExtlib.profile foo ()
 463   with
 464       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
 465     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 466 ;;
 467
 468 let profiler = HExtlib.profile "CicRefine.fo_unif"
 469
 470 let fo_unif_subst subst context metasenv t1 t2 ugraph =
 471   try
 472 let foo () =
 473     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
 474 in profiler.HExtlib.profile foo ()
 475   with
 476       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
 477     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 478 ;;
 479
 480 let enrich localization_tbl t ?(f = fun msg -> msg) exn =
 481  let exn' =
 482   match exn with
 483      RefineFailure msg -> RefineFailure (f msg)
 484    | Uncertain msg -> Uncertain (f msg)
 485    | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
 486    | Sys.Break -> raise exn
 487    | _ -> prerr_endline (Printexc.to_string exn); assert false
 488  in
 489  let loc =
 490   try
 491    Cic.CicHash.find localization_tbl t
 492   with Not_found ->
 493    HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
 494    raise exn'
 495  in
 496   raise (HExtlib.Localized (loc,exn'))
 497
 498 let relocalize localization_tbl oldt newt =
 499  try
 500   let infos = Cic.CicHash.find localization_tbl oldt in
 501    Cic.CicHash.remove localization_tbl oldt;
 502    Cic.CicHash.add localization_tbl newt infos;
 503  with
 504   Not_found -> ()
 505 ;;
 506
 507 let rec split l n =
 508  match (l,n) with
 509     (l,0) -> ([], l)
 510   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
 511   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
 512 ;;
 513
 514 let exp_impl metasenv subst context =
 515  function
 516   | Some `Type ->
 517       let (metasenv', idx) =
 518         CicMkImplicit.mk_implicit_type metasenv subst context in
 519       let irl =
 520         CicMkImplicit.identity_relocation_list_for_metavariable context in
 521       metasenv', Cic.Meta (idx, irl)
 522   | Some `Closed ->
 523       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
 524       metasenv', Cic.Meta (idx, [])
 525   | None ->
 526       let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
 527       let irl =
 528         CicMkImplicit.identity_relocation_list_for_metavariable context in
 529       metasenv', Cic.Meta (idx, irl)
 530   | _ -> assert false
 531 ;;
 532
 533 let is_a_double_coercion t =
 534   let rec subst_nth n x l =
 535     match n,l with
 536     | _, [] -> []
 537     | 0, _::tl -> x :: tl
 538     | n, hd::tl -> hd :: subst_nth (n-1) x tl
 539   in
 540   let imp = Cic.Implicit None in
 541   let dummyres = false,imp, imp,imp,imp in
 542   match t with
 543   | Cic.Appl l1 ->
 544      (match CoercGraph.coerced_arg l1 with
 545      | Some (Cic.Appl l2, pos1) ->
 546          (match CoercGraph.coerced_arg l2 with
 547          | Some (x, pos2) ->
 548              true, List.hd l1, List.hd l2, x,
 549               Cic.Appl (subst_nth (pos1 + 1)
 550                 (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
 551          | _ -> dummyres)
 552       | _ -> dummyres)
 553   | _ -> dummyres
 554 ;;
 555
 556 let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
 557 =
 558   let len = List.length tlbody_and_type in
 559   let msg =
 560     lazy ("The term " ^
 561       CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
 562       " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
 563       ") is here applied to " ^ string_of_int len ^
 564       " arguments but here it can handle only up to " ^
 565       string_of_int (len - residuals) ^ " arguments")
 566   in
 567   enrich localization_tbl he ~f:(fun _-> msg) exn
 568 ;;
 569
 570 let mk_prod_of_metas metasenv context subst args =
 571   let rec mk_prod metasenv context' = function
 572     | [] ->
 573         let (metasenv, idx) =
 574           CicMkImplicit.mk_implicit_type metasenv subst context'
 575         in
 576         let irl =
 577           CicMkImplicit.identity_relocation_list_for_metavariable context'
 578         in
 579           metasenv,Cic.Meta (idx, irl)
 580     | (_,argty)::tl ->
 581         let (metasenv, idx) =
 582           CicMkImplicit.mk_implicit_type metasenv subst context'
 583         in
 584         let irl =
 585           CicMkImplicit.identity_relocation_list_for_metavariable context'
 586         in
 587         let meta = Cic.Meta (idx,irl) in
 588         let name =
 589           (* The name must be fresh for context.                 *)
 590           (* Nevertheless, argty is well-typed only in context.  *)
 591           (* Thus I generate a name (name_hint) in context and   *)
 592           (* then I generate a name --- using the hint name_hint *)
 593           (* --- that is fresh in context'.                      *)
 594           let name_hint =
 595             FreshNamesGenerator.mk_fresh_name ~subst metasenv
 596               (CicMetaSubst.apply_subst_context subst context)
 597               Cic.Anonymous
 598               ~typ:(CicMetaSubst.apply_subst subst argty)
 599           in
 600             FreshNamesGenerator.mk_fresh_name ~subst
 601               [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
 602         in
 603         let metasenv,target =
 604           mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
 605         in
 606           metasenv,Cic.Prod (name,meta,target)
 607   in
 608   mk_prod metasenv context args
 609 ;;
 610
 611 let rec type_of_constant uri ugraph =
 612  let module C = Cic in
 613  let module R = CicReduction in
 614  let module U = UriManager in
 615   let _ = CicTypeChecker.typecheck uri in
 616   let obj,u =
 617    try
 618     CicEnvironment.get_cooked_obj ugraph uri
 619    with Not_found -> assert false
 620   in
 621    match obj with
 622       C.Constant (_,_,ty,_,_) -> ty,u
 623     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
 624     | _ ->
 625        raise
 626         (RefineFailure
 627           (lazy ("Unknown constant definition " ^  U.string_of_uri uri)))
 628
 629 and type_of_variable uri ugraph =
 630   let module C = Cic in
 631   let module R = CicReduction in
 632   let module U = UriManager in
 633   let _ = CicTypeChecker.typecheck uri in
 634   let obj,u =
 635    try
 636     CicEnvironment.get_cooked_obj ugraph uri
 637     with Not_found -> assert false
 638   in
 639    match obj with
 640       C.Variable (_,_,ty,_,_) -> ty,u
 641     | _ ->
 642         raise
 643          (RefineFailure
 644           (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
 645
 646 and type_of_mutual_inductive_defs uri i ugraph =
 647   let module C = Cic in
 648   let module R = CicReduction in
 649   let module U = UriManager in
 650   let _ = CicTypeChecker.typecheck uri in
 651   let obj,u =
 652    try
 653     CicEnvironment.get_cooked_obj ugraph uri
 654    with Not_found -> assert false
 655   in
 656    match obj with
 657       C.InductiveDefinition (dl,_,_,_) ->
 658         let (_,_,arity,_) = List.nth dl i in
 659          arity,u
 660     | _ ->
 661        raise
 662         (RefineFailure
 663          (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
 664
 665 and type_of_mutual_inductive_constr uri i j ugraph =
 666   let module C = Cic in
 667   let module R = CicReduction in
 668   let module U = UriManager in
 669   let _ = CicTypeChecker.typecheck uri in
 670    let obj,u =
 671     try
 672      CicEnvironment.get_cooked_obj ugraph uri
 673     with Not_found -> assert false
 674    in
 675     match obj with
 676         C.InductiveDefinition (dl,_,_,_) ->
 677           let (_,_,_,cl) = List.nth dl i in
 678           let (_,ty) = List.nth cl (j-1) in
 679             ty,u
 680       | _ ->
 681           raise
 682                   (RefineFailure
 683               (lazy
 684                 ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
 685
 686
 687 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 688
 689 (* the check_branch function checks if a branch of a case is refinable.
 690    It returns a pair (outype_instance,args), a subst and a metasenv.
 691    outype_instance is the expected result of applying the case outtype
 692    to args.
 693    The problem is that outype is in general unknown, and we should
 694    try to synthesize it from the above information, that is in general
 695    a second order unification problem. *)
 696
 697 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 698   let module C = Cic in
 699   let module R = CicReduction in
 700     match R.whd ~subst context expectedtype with
 701         C.MutInd (_,_,_) ->
 702           (n,context,actualtype, [term]), subst, metasenv, ugraph
 703       | C.Appl (C.MutInd (_,_,_)::tl) ->
 704           let (_,arguments) = split tl left_args_no in
 705             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 706       | C.Prod (_,so,de) ->
 707           (* we expect that the actual type of the branch has the due
 708              number of Prod *)
 709           (match R.whd ~subst context actualtype with
 710                C.Prod (name',so',de') ->
 711                  let subst, metasenv, ugraph1 =
 712                    fo_unif_subst subst context metasenv so so' ugraph in
 713                  let term' =
 714                    (match CicSubstitution.lift 1 term with
 715                         C.Appl l -> C.Appl (l@[C.Rel 1])
 716                       | t -> C.Appl [t ; C.Rel 1]) in
 717                    (* we should also check that the name variable is anonymous in
 718                       the actual type de' ?? *)
 719                    check_branch (n+1)
 720                      ((Some (name',(C.Decl so)))::context)
 721                        metasenv subst left_args_no de' term' de ugraph1
 722              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
 723       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 724
 725 and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 726      ugraph
 727 =
 728   let rec type_of_aux subst metasenv context t ugraph =
 729     let module C = Cic in
 730     let module S = CicSubstitution in
 731     let module U = UriManager in
 732      let (t',_,_,_,_) as res =
 733       match t with
 734           (*    function *)
 735           C.Rel n ->
 736             (try
 737                match List.nth context (n - 1) with
 738                    Some (_,C.Decl ty) ->
 739                      t,S.lift n ty,subst,metasenv, ugraph
 740                  | Some (_,C.Def (_,ty)) ->
 741                      t,S.lift n ty,subst,metasenv, ugraph
 742                  | None ->
 743                     enrich localization_tbl t
 744                      (RefineFailure (lazy "Rel to hidden hypothesis"))
 745              with
 746               Failure _ ->
 747                enrich localization_tbl t
 748                 (RefineFailure (lazy "Not a closed term")))
 749         | C.Var (uri,exp_named_subst) ->
 750             let exp_named_subst',subst',metasenv',ugraph1 =
 751               check_exp_named_subst
 752                 subst metasenv context exp_named_subst ugraph
 753             in
 754             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 755             let ty =
 756               CicSubstitution.subst_vars exp_named_subst' ty_uri
 757             in
 758               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 759         | C.Meta (n,l) ->
 760             (try
 761                let (canonical_context, term,ty) =
 762                  CicUtil.lookup_subst n subst
 763                in
 764                let l',subst',metasenv',ugraph1 =
 765                  check_metasenv_consistency n subst metasenv context
 766                    canonical_context l ugraph
 767                in
 768                  (* trust or check ??? *)
 769                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 770                    subst', metasenv', ugraph1
 771                    (* type_of_aux subst metasenv
 772                       context (CicSubstitution.subst_meta l term) *)
 773              with CicUtil.Subst_not_found _ ->
 774                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 775                let l',subst',metasenv', ugraph1 =
 776                  check_metasenv_consistency n subst metasenv context
 777                    canonical_context l ugraph
 778                in
 779                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 780                    subst', metasenv',ugraph1)
 781         | C.Sort (C.Type tno) ->
 782             let tno' = CicUniv.fresh() in
 783              (try
 784                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 785                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 786               with
 787                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
 788         | C.Sort (C.CProp tno) ->
 789             let tno' = CicUniv.fresh() in
 790              (try
 791                let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 792                  t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 793               with
 794                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
 795         | C.Sort (C.Prop|C.Set) ->
 796             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 797         | C.Implicit infos ->
 798            let metasenv',t' = exp_impl metasenv subst context infos in
 799             type_of_aux subst metasenv' context t' ugraph
 800         | C.Cast (te,ty) ->
 801             let ty',_,subst',metasenv',ugraph1 =
 802               type_of_aux subst metasenv context ty ugraph
 803             in
 804             let te',inferredty,subst'',metasenv'',ugraph2 =
 805               type_of_aux subst' metasenv' context te ugraph1
 806             in
 807             let (te', ty'), subst''',metasenv''',ugraph3 =
 808               coerce_to_something true localization_tbl te' inferredty ty'
 809                 subst'' metasenv'' context ugraph2
 810             in
 811              C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 812         | C.Prod (name,s,t) ->
 813             let s',sort1,subst',metasenv',ugraph1 =
 814               type_of_aux subst metasenv context s ugraph
 815             in
 816             let s',sort1,subst', metasenv',ugraph1 =
 817               coerce_to_sort localization_tbl
 818               s' sort1 subst' context metasenv' ugraph1
 819             in
 820             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 821             let t',sort2,subst'',metasenv'',ugraph2 =
 822               type_of_aux subst' metasenv'
 823                 context_for_t t ugraph1
 824             in
 825             let t',sort2,subst'',metasenv'',ugraph2 =
 826               coerce_to_sort localization_tbl
 827               t' sort2 subst'' context_for_t metasenv'' ugraph2
 828             in
 829               let sop,subst''',metasenv''',ugraph3 =
 830                 sort_of_prod localization_tbl subst'' metasenv''
 831                   context (name,s') t' (sort1,sort2) ugraph2
 832               in
 833                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 834         | C.Lambda (n,s,t) ->
 835             let s',sort1,subst',metasenv',ugraph1 =
 836               type_of_aux subst metasenv context s ugraph
 837             in
 838             let s',sort1,subst',metasenv',ugraph1 =
 839               coerce_to_sort localization_tbl
 840               s' sort1 subst' context metasenv' ugraph1
 841             in
 842             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 843             let t',type2,subst'',metasenv'',ugraph2 =
 844               type_of_aux subst' metasenv' context_for_t t ugraph1
 845             in
 846               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 847                 subst'',metasenv'',ugraph2
 848         | C.LetIn (n,s,ty,t) ->
 849            (* only to check if s is well-typed *)
 850            let s',ty',subst',metasenv',ugraph1 =
 851              type_of_aux subst metasenv context s ugraph in
 852            let ty,_,subst',metasenv',ugraph1 =
 853              type_of_aux subst' metasenv' context ty ugraph1 in
 854            let subst',metasenv',ugraph1 =
 855             try
 856              fo_unif_subst subst' context metasenv'
 857                ty ty' ugraph1
 858             with
 859              exn ->
 860               enrich localization_tbl s' exn
 861                ~f:(function _ ->
 862                  lazy ("The term " ^
 863                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
 864                    context ^ " has type " ^
 865                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
 866                    context ^ " but is here used with type " ^
 867                   CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
 868                    context))
 869            in
 870            let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
 871
 872             let t',inferredty,subst'',metasenv'',ugraph2 =
 873               type_of_aux subst' metasenv'
 874                 context_for_t t ugraph1
 875             in
 876               (* One-step LetIn reduction.
 877                * Even faster than the previous solution.
 878                * Moreover the inferred type is closer to the expected one.
 879                *)
 880               C.LetIn (n,s',ty,t'),
 881                CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
 882                subst'',metasenv'',ugraph2
 883         | C.Appl (he::((_::_) as tl)) ->
 884             let he',hetype,subst',metasenv',ugraph1 =
 885               type_of_aux subst metasenv context he ugraph
 886             in
 887             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 888                typeof_list subst' metasenv' context ugraph1 tl
 889             in
 890             let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
 891               eat_prods true subst'' metasenv'' context
 892                 he' hetype tlbody_and_type ugraph2
 893             in
 894             let newappl = (C.Appl (coerced_he::coerced_args)) in
 895             avoid_double_coercion
 896               context subst''' metasenv''' ugraph3 newappl applty
 897         | C.Appl _ -> assert false
 898         | C.Const (uri,exp_named_subst) ->
 899             let exp_named_subst',subst',metasenv',ugraph1 =
 900               check_exp_named_subst subst metasenv context
 901                 exp_named_subst ugraph in
 902             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 903             let cty =
 904               CicSubstitution.subst_vars exp_named_subst' ty_uri
 905             in
 906               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 907         | C.MutInd (uri,i,exp_named_subst) ->
 908             let exp_named_subst',subst',metasenv',ugraph1 =
 909               check_exp_named_subst subst metasenv context
 910                 exp_named_subst ugraph
 911             in
 912             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 913             let cty =
 914               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 915               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 916         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 917             let exp_named_subst',subst',metasenv',ugraph1 =
 918               check_exp_named_subst subst metasenv context
 919                 exp_named_subst ugraph
 920             in
 921             let ty_uri,ugraph2 =
 922               type_of_mutual_inductive_constr uri i j ugraph1
 923             in
 924             let cty =
 925               CicSubstitution.subst_vars exp_named_subst' ty_uri
 926             in
 927               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 928                 metasenv',ugraph2
 929         | C.MutCase (uri, i, outtype, term, pl) ->
 930             (* first, get the inductive type (and noparams)
 931              * in the environment  *)
 932             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 933               let _ = CicTypeChecker.typecheck uri in
 934               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 935               match obj with
 936                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 937                     List.nth l i , expl_params, parsno, u
 938                 | _ ->
 939                     enrich localization_tbl t
 940                      (RefineFailure
 941                        (lazy ("Unkown mutual inductive definition " ^
 942                          U.string_of_uri uri)))
 943            in
 944            if List.length constructors <> List.length pl then
 945             enrich localization_tbl t
 946              (RefineFailure
 947                (lazy "Wrong number of cases")) ;
 948            let rec count_prod t =
 949              match CicReduction.whd ~subst context t with
 950                  C.Prod (_, _, t) -> 1 + (count_prod t)
 951                | _ -> 0
 952            in
 953            let no_args = count_prod arity in
 954              (* now, create a "generic" MutInd *)
 955            let metasenv,left_args =
 956              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 957            in
 958            let metasenv,right_args =
 959              let no_right_params = no_args - no_left_params in
 960                if no_right_params < 0 then assert false
 961                else CicMkImplicit.n_fresh_metas
 962                       metasenv subst context no_right_params
 963            in
 964            let metasenv,exp_named_subst =
 965              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 966            let expected_type =
 967              if no_args = 0 then
 968                C.MutInd (uri,i,exp_named_subst)
 969              else
 970                C.Appl
 971                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 972            in
 973              (* check consistency with the actual type of term *)
 974            let term',actual_type,subst,metasenv,ugraph1 =
 975              type_of_aux subst metasenv context term ugraph in
 976            let expected_type',_, subst, metasenv,ugraph2 =
 977              type_of_aux subst metasenv context expected_type ugraph1
 978            in
 979            let actual_type = CicReduction.whd ~subst context actual_type in
 980            let subst,metasenv,ugraph3 =
 981             try
 982              fo_unif_subst subst context metasenv
 983                expected_type' actual_type ugraph2
 984             with
 985              exn ->
 986               enrich localization_tbl term' exn
 987                ~f:(function _ ->
 988                  lazy ("The term " ^
 989                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
 990                    context ^ " has type " ^
 991                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
 992                    context ^ " but is here used with type " ^
 993                   CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
 994                   context))
 995            in
 996            let rec instantiate_prod t =
 997             function
 998                [] -> t
 999              | he::tl ->
1000                 match CicReduction.whd ~subst context t with
1001                    C.Prod (_,_,t') ->
1002                     instantiate_prod (CicSubstitution.subst he t') tl
1003                  | _ -> assert false
1004            in
1005            let arity_instantiated_with_left_args =
1006             instantiate_prod arity left_args in
1007              (* TODO: check if the sort elimination
1008               * is allowed: [(I q1 ... qr)|B] *)
1009            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
1010              List.fold_right
1011                (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
1012                   let constructor =
1013                     if left_args = [] then
1014                       (C.MutConstruct (uri,i,j,exp_named_subst))
1015                     else
1016                       (C.Appl
1017                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
1018                   in
1019                   let p',actual_type,subst,metasenv,ugraph1 =
1020                     type_of_aux subst metasenv context p ugraph
1021                   in
1022                   let constructor',expected_type, subst, metasenv,ugraph2 =
1023                     type_of_aux subst metasenv context constructor ugraph1
1024                   in
1025                   let outtypeinstance,subst,metasenv,ugraph3 =
1026                    try
1027                     check_branch 0 context metasenv subst
1028                      no_left_params actual_type constructor' expected_type
1029                      ugraph2
1030                    with
1031                     exn ->
1032                      enrich localization_tbl constructor'
1033                       ~f:(fun _ ->
1034                         lazy ("The term " ^
1035                          CicMetaSubst.ppterm_in_context metasenv subst p'
1036                           context ^ " has type " ^
1037                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
1038                           context ^ " but is here used with type " ^
1039                          CicMetaSubst.ppterm_in_context metasenv subst expected_type
1040                           context)) exn
1041                   in
1042                     (p'::pl,j-1,
1043                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
1044                pl ([],List.length pl,[],subst,metasenv,ugraph3)
1045            in
1046
1047              (* we are left to check that the outype matches his instances.
1048                 The easy case is when the outype is specified, that amount
1049                 to a trivial check. Otherwise, we should guess a type from
1050                 its instances
1051              *)
1052
1053            let outtype,outtypety, subst, metasenv,ugraph4 =
1054              type_of_aux subst metasenv context outtype ugraph4 in
1055            (match outtype with
1056            | C.Meta (n,l) ->
1057                (let candidate,ugraph5,metasenv,subst =
1058                  let exp_name_subst, metasenv =
1059                     let o,_ =
1060                       CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
1061                     in
1062                     let uris = CicUtil.params_of_obj o in
1063                     List.fold_right (
1064                       fun uri (acc,metasenv) ->
1065                         let metasenv',new_meta =
1066                            CicMkImplicit.mk_implicit metasenv subst context
1067                         in
1068                         let irl =
1069                           CicMkImplicit.identity_relocation_list_for_metavariable
1070                             context
1071                         in
1072                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
1073                     ) uris ([],metasenv)
1074                  in
1075                  let ty =
1076                   match left_args,right_args with
1077                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
1078                    | _,_ ->
1079                       let rec mk_right_args =
1080                        function
1081                           0 -> []
1082                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
1083                       in
1084                       let right_args_no = List.length right_args in
1085                       let lifted_left_args =
1086                        List.map (CicSubstitution.lift right_args_no) left_args
1087                       in
1088                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
1089                         (lifted_left_args @ mk_right_args right_args_no))
1090                  in
1091                  let fresh_name =
1092                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
1093                      context Cic.Anonymous ~typ:ty
1094                  in
1095                  match outtypeinstances with
1096                  | [] ->
1097                      let extended_context =
1098                       let rec add_right_args =
1099                        function
1100                           Cic.Prod (name,ty,t) ->
1101                            Some (name,Cic.Decl ty)::(add_right_args t)
1102                         | _ -> []
1103                       in
1104                        (Some (fresh_name,Cic.Decl ty))::
1105                        (List.rev
1106                         (add_right_args arity_instantiated_with_left_args))@
1107                        context
1108                      in
1109                      let metasenv,new_meta =
1110                        CicMkImplicit.mk_implicit metasenv subst extended_context
1111                      in
1112                        let irl =
1113                        CicMkImplicit.identity_relocation_list_for_metavariable
1114                          extended_context
1115                      in
1116                      let rec add_lambdas b =
1117                       function
1118                          Cic.Prod (name,ty,t) ->
1119                           Cic.Lambda (name,ty,(add_lambdas b t))
1120                        | _ -> Cic.Lambda (fresh_name, ty, b)
1121                      in
1122                      let candidate =
1123                       add_lambdas (Cic.Meta (new_meta,irl))
1124                        arity_instantiated_with_left_args
1125                      in
1126                      (Some candidate),ugraph4,metasenv,subst
1127                  | (constructor_args_no,_,instance,_)::tl ->
1128                      try
1129                        let instance',subst,metasenv =
1130                          CicMetaSubst.delift_rels subst metasenv
1131                           constructor_args_no instance
1132                        in
1133                        let candidate,ugraph,metasenv,subst =
1134                          List.fold_left (
1135                            fun (candidate_oty,ugraph,metasenv,subst)
1136                              (constructor_args_no,_,instance,_) ->
1137                                match candidate_oty with
1138                                | None -> None,ugraph,metasenv,subst
1139                                | Some ty ->
1140                                  try
1141                                    let instance',subst,metasenv =
1142                                      CicMetaSubst.delift_rels subst metasenv
1143                                       constructor_args_no instance
1144                                    in
1145                                    let subst,metasenv,ugraph =
1146                                     fo_unif_subst subst context metasenv
1147                                       instance' ty ugraph
1148                                    in
1149                                     candidate_oty,ugraph,metasenv,subst
1150                                  with
1151                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
1152                                   | RefineFailure _ | Uncertain _ ->
1153                                      None,ugraph,metasenv,subst
1154                          ) (Some instance',ugraph4,metasenv,subst) tl
1155                        in
1156                        match candidate with
1157                        | None -> None, ugraph,metasenv,subst
1158                        | Some t ->
1159                           let rec add_lambdas n b =
1160                            function
1161                               Cic.Prod (name,ty,t) ->
1162                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
1163                             | _ ->
1164                               Cic.Lambda (fresh_name, ty,
1165                                CicSubstitution.lift (n + 1) t)
1166                           in
1167                            Some
1168                             (add_lambdas 0 t arity_instantiated_with_left_args),
1169                            ugraph,metasenv,subst
1170                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
1171                        None,ugraph4,metasenv,subst
1172                in
1173                match candidate with
1174                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
1175                | Some candidate ->
1176                    let subst,metasenv,ugraph =
1177                     try
1178                      fo_unif_subst subst context metasenv
1179                        candidate outtype ugraph5
1180                     with
1181                      exn -> assert false(* unification against a metavariable *)
1182                    in
1183                      C.MutCase (uri, i, outtype, term', pl'),
1184                       CicReduction.head_beta_reduce
1185                        (CicMetaSubst.apply_subst subst
1186                         (Cic.Appl (outtype::right_args@[term']))),
1187                      subst,metasenv,ugraph)
1188            | _ ->    (* easy case *)
1189              let tlbody_and_type,subst,metasenv,ugraph4 =
1190                typeof_list subst metasenv context ugraph4 (right_args @ [term'])
1191              in
1192              let _,_,_,subst,metasenv,ugraph4 =
1193                eat_prods false subst metasenv context
1194                  outtype outtypety tlbody_and_type ugraph4
1195              in
1196              let _,_, subst, metasenv,ugraph5 =
1197                type_of_aux subst metasenv context
1198                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
1199              in
1200              let (subst,metasenv,ugraph6) =
1201                List.fold_left2
1202                  (fun (subst,metasenv,ugraph)
1203                    p (constructor_args_no,context,instance,args)
1204                   ->
1205                     let instance' =
1206                       let appl =
1207                         let outtype' =
1208                           CicSubstitution.lift constructor_args_no outtype
1209                         in
1210                           C.Appl (outtype'::args)
1211                       in
1212                         CicReduction.head_beta_reduce ~delta:false
1213                           ~upto:(List.length args) appl
1214                     in
1215                      try
1216                       fo_unif_subst subst context metasenv instance instance'
1217                        ugraph
1218                      with
1219                       exn ->
1220                        enrich localization_tbl p exn
1221                         ~f:(function _ ->
1222                           lazy ("The term " ^
1223                            CicMetaSubst.ppterm_in_context ~metasenv subst p
1224                             context ^ " has type " ^
1225                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
1226                             context ^ " but is here used with type " ^
1227                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
1228                             context)))
1229                  (subst,metasenv,ugraph5) pl' outtypeinstances
1230              in
1231                C.MutCase (uri, i, outtype, term', pl'),
1232                  CicReduction.head_beta_reduce
1233                   (CicMetaSubst.apply_subst subst
1234                    (C.Appl(outtype::right_args@[term']))),
1235                  subst,metasenv,ugraph6)
1236         | C.Fix (i,fl) ->
1237             let fl_ty',subst,metasenv,types,ugraph1,len =
1238               List.fold_left
1239                 (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
1240                    let ty',_,subst',metasenv',ugraph1 =
1241                       type_of_aux subst metasenv context ty ugraph
1242                    in
1243                      fl @ [ty'],subst',metasenv',
1244                        Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
1245                         :: types, ugraph, len+1
1246                 ) ([],subst,metasenv,[],ugraph,0) fl
1247             in
1248             let context' = types@context in
1249             let fl_bo',subst,metasenv,ugraph2 =
1250               List.fold_left
1251                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
1252                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
1253                      type_of_aux subst metasenv context' bo ugraph in
1254                    let expected_ty = CicSubstitution.lift len ty in
1255                    let subst',metasenv',ugraph' =
1256                     try
1257                      fo_unif_subst subst context' metasenv
1258                        ty_of_bo expected_ty ugraph1
1259                     with
1260                      exn ->
1261                       enrich localization_tbl bo exn
1262                        ~f:(function _ ->
1263                          lazy ("The term " ^
1264                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
1265                            context' ^ " has type " ^
1266                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1267                            context' ^ " but is here used with type " ^
1268                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1269                            context'))
1270                    in
1271                      fl @ [bo'] , subst',metasenv',ugraph'
1272                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1273             in
1274             let ty = List.nth fl_ty' i in
1275             (* now we have the new ty in fl_ty', the new bo in fl_bo',
1276              * and we want the new fl with bo' and ty' injected in the right
1277              * place.
1278              *)
1279             let rec map3 f l1 l2 l3 =
1280               match l1,l2,l3 with
1281               | [],[],[] -> []
1282               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1283               | _ -> assert false
1284             in
1285             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
1286               fl_ty' fl_bo' fl
1287             in
1288               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
1289         | C.CoFix (i,fl) ->
1290             let fl_ty',subst,metasenv,types,ugraph1,len =
1291               List.fold_left
1292                 (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
1293                    let ty',_,subst',metasenv',ugraph1 =
1294                      type_of_aux subst metasenv context ty ugraph
1295                    in
1296                      fl @ [ty'],subst',metasenv',
1297                       Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
1298                         types, ugraph1, len+1
1299                 ) ([],subst,metasenv,[],ugraph,0) fl
1300             in
1301             let context' = types@context in
1302             let fl_bo',subst,metasenv,ugraph2 =
1303               List.fold_left
1304                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
1305                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
1306                      type_of_aux subst metasenv context' bo ugraph in
1307                    let expected_ty = CicSubstitution.lift len ty in
1308                    let subst',metasenv',ugraph' =
1309                     try
1310                      fo_unif_subst subst context' metasenv
1311                        ty_of_bo expected_ty ugraph1
1312                     with
1313                      exn ->
1314                       enrich localization_tbl bo exn
1315                        ~f:(function _ ->
1316                          lazy ("The term " ^
1317                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
1318                            context' ^ " has type " ^
1319                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
1320                            context' ^ " but is here used with type " ^
1321                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
1322                            context))
1323                    in
1324                      fl @ [bo'],subst',metasenv',ugraph'
1325                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
1326             in
1327             let ty = List.nth fl_ty' i in
1328             (* now we have the new ty in fl_ty', the new bo in fl_bo',
1329              * and we want the new fl with bo' and ty' injected in the right
1330              * place.
1331              *)
1332             let rec map3 f l1 l2 l3 =
1333               match l1,l2,l3 with
1334               | [],[],[] -> []
1335               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
1336               | _ -> assert false
1337             in
1338             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
1339               fl_ty' fl_bo' fl
1340             in
1341               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
1342      in
1343       relocalize localization_tbl t t';
1344       res
1345
1346   (* check_metasenv_consistency checks that the "canonical" context of a
1347      metavariable is consitent - up to relocation via the relocation list l -
1348      with the actual context *)
1349   and check_metasenv_consistency
1350     metano subst metasenv context canonical_context l ugraph
1351     =
1352     let module C = Cic in
1353     let module R = CicReduction in
1354     let module S = CicSubstitution in
1355     let lifted_canonical_context =
1356       let rec aux i =
1357         function
1358             [] -> []
1359           | (Some (n,C.Decl t))::tl ->
1360               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1361           | None::tl -> None::(aux (i+1) tl)
1362           | (Some (n,C.Def (t,ty)))::tl ->
1363               (Some
1364                (n,
1365                 C.Def
1366                  (S.subst_meta l (S.lift i t),
1367                   S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
1368       in
1369         aux 1 canonical_context
1370     in
1371       try
1372         List.fold_left2
1373           (fun (l,subst,metasenv,ugraph) t ct ->
1374              match (t,ct) with
1375                  _,None ->
1376                    l @ [None],subst,metasenv,ugraph
1377                | Some t,Some (_,C.Def (ct,_)) ->
1378                   (*CSC: the following optimization is to avoid a possibly
1379                          expensive reduction that can be easily avoided and
1380                          that is quite frequent. However, this is better
1381                          handled using levels to control reduction *)
1382                   let optimized_t =
1383                    match t with
1384                       Cic.Rel n ->
1385                        (try
1386                          match List.nth context (n - 1) with
1387                             Some (_,C.Def (te,_)) -> S.lift n te
1388                           | _ -> t
1389                         with
1390                          Failure _ -> t)
1391                     | _ -> t
1392                   in
1393                    let subst',metasenv',ugraph' =
1394                    (try
1395 (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
1396  * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
1397                       fo_unif_subst subst context metasenv optimized_t ct ugraph
1398                     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 optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
1399                    in
1400                      l @ [Some t],subst',metasenv',ugraph'
1401                | Some t,Some (_,C.Decl ct) ->
1402                    let t',inferredty,subst',metasenv',ugraph1 =
1403                      type_of_aux subst metasenv context t ugraph
1404                    in
1405                    let subst'',metasenv'',ugraph2 =
1406                      (try
1407                         fo_unif_subst
1408                           subst' context metasenv' inferredty ct ugraph1
1409                       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))))))
1410                    in
1411                      l @ [Some t'], subst'',metasenv'',ugraph2
1412                | None, Some _  ->
1413                    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
1414       with
1415           Invalid_argument _ ->
1416             raise
1417             (RefineFailure
1418                (lazy (sprintf
1419                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
1420                   (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
1421                   (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
1422
1423   and check_exp_named_subst metasubst metasenv context tl ugraph =
1424     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
1425       match tl with
1426           [] -> [],metasubst,metasenv,ugraph
1427         | (uri,t)::tl ->
1428             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
1429             let typeofvar =
1430               CicSubstitution.subst_vars substs ty_uri in
1431               (* CSC: why was this code here? it is wrong
1432                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
1433                  Cic.Variable (_,Some bo,_,_) ->
1434                  raise
1435                  (RefineFailure (lazy
1436                  "A variable with a body can not be explicit substituted"))
1437                  | Cic.Variable (_,None,_,_) -> ()
1438                  | _ ->
1439                  raise
1440                  (RefineFailure (lazy
1441                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
1442                  ) ;
1443               *)
1444             let t',typeoft,metasubst',metasenv',ugraph2 =
1445               type_of_aux metasubst metasenv context t ugraph1 in
1446             let subst = uri,t' in
1447             let metasubst'',metasenv'',ugraph3 =
1448               try
1449                 fo_unif_subst
1450                   metasubst' context metasenv' typeoft typeofvar ugraph2
1451               with _ ->
1452                 raise (RefineFailure (lazy
1453                          ("Wrong Explicit Named Substitution: " ^
1454                            CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
1455                           " not unifiable with " ^
1456                           CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
1457             in
1458             (* FIXME: no mere tail recursive! *)
1459             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
1460               check_exp_named_subst_aux
1461                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
1462             in
1463               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
1464     in
1465       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
1466
1467
1468   and sort_of_prod localize subst metasenv context (name,s) t (t1, t2)
1469    ugraph
1470   =
1471     let module C = Cic in
1472     let context_for_t2 = (Some (name,C.Decl s))::context in
1473     let t1'' = CicReduction.whd ~subst context t1 in
1474     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
1475       match (t1'', t2'') with
1476         | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
1477               (* different than Coq manual!!! *)
1478               C.Sort s2,subst,metasenv,ugraph
1479         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1480             let t' = CicUniv.fresh() in
1481              (try
1482               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1483               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1484                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1485               with
1486                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1487         | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
1488             let t' = CicUniv.fresh() in
1489              (try
1490               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1491               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1492                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1493               with
1494                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1495         | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
1496             let t' = CicUniv.fresh() in
1497              (try
1498               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1499               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1500                 C.Sort (C.CProp t'),subst,metasenv,ugraph2
1501               with
1502                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1503         | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
1504             let t' = CicUniv.fresh() in
1505              (try
1506               let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1507               let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1508                 C.Sort (C.Type t'),subst,metasenv,ugraph2
1509               with
1510                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
1511         | (C.Sort _,C.Sort (C.Type t1)) ->
1512             C.Sort (C.Type t1),subst,metasenv,ugraph
1513         | (C.Sort _,C.Sort (C.CProp t1)) ->
1514             C.Sort (C.CProp t1),subst,metasenv,ugraph
1515         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
1516         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
1517             (* TODO how can we force the meta to become a sort? If we don't we
1518              * break the invariant that refine produce only well typed terms *)
1519             (* TODO if we check the non meta term and if it is a sort then we
1520              * are likely to know the exact value of the result e.g. if the rhs
1521              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1522             let (metasenv,idx) =
1523               CicMkImplicit.mk_implicit_sort metasenv subst in
1524             let (subst, metasenv,ugraph1) =
1525              try
1526               fo_unif_subst subst context_for_t2 metasenv
1527                 (C.Meta (idx,[])) t2'' ugraph
1528              with _ -> assert false (* unification against a metavariable *)
1529             in
1530               t2'',subst,metasenv,ugraph1
1531         | (C.Sort _,_)
1532         | (C.Meta _,_) ->
1533             enrich localization_tbl s
1534              (RefineFailure
1535                (lazy
1536                  (sprintf
1537                    "%s is supposed to be a type, but its type is %s"
1538                (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
1539                (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
1540         | _,_ ->
1541             enrich localization_tbl t
1542              (RefineFailure
1543                (lazy
1544                  (sprintf
1545                    "%s is supposed to be a type, but its type is %s"
1546                (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
1547                (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
1548
1549   and avoid_double_coercion context subst metasenv ugraph t ty =
1550    if not !pack_coercions then
1551     t,ty,subst,metasenv,ugraph
1552    else
1553     let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
1554     if b then
1555       let source_carr = CoercGraph.source_of c2 in
1556       let tgt_carr = CicMetaSubst.apply_subst subst ty in
1557       (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
1558       with
1559       | CoercGraph.SomeCoercion candidates ->
1560          let selected =
1561            HExtlib.list_findopt
1562              (function (metasenv,last,c) ->
1563                match c with
1564                | c when not (CoercGraph.is_composite c) ->
1565                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
1566                    None
1567                | c ->
1568                let subst,metasenv,ugraph =
1569                 fo_unif_subst subst context metasenv last head ugraph in
1570                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
1571                (try
1572                  debug_print
1573                    (lazy
1574                      ("packing: " ^
1575                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
1576                  let newt,_,subst,metasenv,ugraph =
1577                    type_of_aux subst metasenv context c ugraph in
1578                  debug_print (lazy "tipa...");
1579                  let subst, metasenv, ugraph =
1580                    (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
1581                     fo_unif_subst subst context metasenv newt t ugraph
1582                  in
1583                  debug_print (lazy "unifica...");
1584                  Some (newt, ty, subst, metasenv, ugraph)
1585                with
1586                | RefineFailure s | Uncertain s when not !pack_coercions->
1587                    debug_print s; debug_print (lazy "stop\n");None
1588                | RefineFailure s | Uncertain s ->
1589                    debug_print s;debug_print (lazy "goon\n");
1590                    try
1591                      let old_pack_coercions = !pack_coercions in
1592                      pack_coercions := false; (* to avoid diverging *)
1593                      let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
1594                        type_of_aux subst metasenv context c1_c2_implicit ugraph
1595                      in
1596                      pack_coercions := old_pack_coercions;
1597                      let b, _, _, _, _ =
1598                        is_a_double_coercion refined_c1_c2_implicit
1599                      in
1600                      if b then
1601                        None
1602                      else
1603                        let head' =
1604                          match refined_c1_c2_implicit with
1605                          | Cic.Appl l -> HExtlib.list_last l
1606                          | _ -> assert false
1607                        in
1608                        let subst, metasenv, ugraph =
1609                         try fo_unif_subst subst context metasenv
1610                           head head' ugraph
1611                         with RefineFailure s| Uncertain s->
1612                           debug_print s;assert false
1613                        in
1614                        let subst, metasenv, ugraph =
1615                          fo_unif_subst subst context metasenv
1616                           refined_c1_c2_implicit t ugraph
1617                        in
1618                        Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
1619                    with
1620                    | RefineFailure s | Uncertain s ->
1621                        pack_coercions := true;debug_print s;None
1622                    | exn -> pack_coercions := true; raise exn))
1623              candidates
1624          in
1625          (match selected with
1626          | Some x -> x
1627          | None ->
1628               debug_print
1629                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
1630               t, ty, subst, metasenv, ugraph)
1631       | _ -> t, ty, subst, metasenv, ugraph)
1632     else
1633       t, ty, subst, metasenv, ugraph
1634
1635   and typeof_list subst metasenv context ugraph l =
1636     let tlbody_and_type,subst,metasenv,ugraph =
1637       List.fold_right
1638         (fun x (res,subst,metasenv,ugraph) ->
1639            let x',ty,subst',metasenv',ugraph1 =
1640              type_of_aux subst metasenv context x ugraph
1641            in
1642             (x', ty)::res,subst',metasenv',ugraph1
1643         ) l ([],subst,metasenv,ugraph)
1644     in
1645       tlbody_and_type,subst,metasenv,ugraph
1646
1647   and eat_prods
1648     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
1649   =
1650     (* given he:hety, gives beack all (c he) such that (c e):?->? *)
1651     let fix_arity n metasenv context subst he hetype ugraph =
1652       let hetype = CicMetaSubst.apply_subst subst hetype in
1653       (* instead of a dummy functional type we may create the real product
1654        * using args_bo_and_ty, but since coercions lookup ignores the
1655        * actual ariety we opt for the simple solution *)
1656       let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
1657       match CoercGraph.look_for_coercion metasenv subst context hetype fty with
1658       | CoercGraph.NoCoercion -> []
1659       | CoercGraph.NotHandled ->
1660          raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
1661       | CoercGraph.SomeCoercionToTgt candidates
1662       | CoercGraph.SomeCoercion candidates ->
1663           HExtlib.filter_map
1664             (fun (metasenv,last,coerc) ->
1665               let pp t =
1666                 CicMetaSubst.ppterm_in_context ~metasenv subst t context in
1667               try
1668                let subst,metasenv,ugraph =
1669                 fo_unif_subst subst context metasenv last he ugraph in
1670                 debug_print (lazy ("New head: "^ pp coerc));
1671                 let tty,ugraph =
1672                  CicTypeChecker.type_of_aux' ~subst metasenv context coerc
1673                   ugraph
1674                 in
1675                  debug_print (lazy (" has type: "^ pp tty));
1676                  Some (coerc,tty,subst,metasenv,ugraph)
1677               with
1678               | Uncertain _ | RefineFailure _
1679               | HExtlib.Localized (_,Uncertain _)
1680               | HExtlib.Localized (_,RefineFailure _) -> None
1681               | exn -> assert false)
1682             candidates
1683     in
1684     (* aux function to process the type of the head and the args in parallel *)
1685     let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
1686       function
1687       | [] -> newargs,subst,metasenv,he,hetype,ugraph
1688       | (hete, hety)::tl as args ->
1689           match (CicReduction.whd ~subst context hetype) with
1690           | Cic.Prod (n,s,t) ->
1691               let arg,subst,metasenv,ugraph =
1692                 coerce_to_something allow_coercions localization_tbl
1693                   hete hety s subst metasenv context ugraph in
1694               eat_prods_and_args
1695                 metasenv subst context he (CicSubstitution.subst (fst arg) t)
1696                 ugraph (newargs@[arg]) tl
1697           | _ ->
1698               let he =
1699                 match he, newargs with
1700                 | _, [] -> he
1701                 | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
1702                 | _ -> Cic.Appl (he::List.map fst newargs)
1703               in
1704               (*{{{*) debug_print (lazy
1705                let pp x =
1706                 CicMetaSubst.ppterm_in_context ~metasenv subst x context in
1707                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
1708                "\n but is applyed to: " ^ String.concat ";"
1709                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
1710               let possible_fixes =
1711                fix_arity (List.length args) metasenv context subst he hetype
1712                 ugraph in
1713               match
1714                 HExtlib.list_findopt
1715                  (fun (he,hetype,subst,metasenv,ugraph) ->
1716                    (* {{{ *)debug_print (lazy ("Try fix: "^
1717                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
1718                    debug_print (lazy (" of type: "^
1719                     CicMetaSubst.ppterm_in_context
1720                     ~metasenv subst hetype context)); (* }}} *)
1721                    try
1722                     Some (eat_prods_and_args
1723                       metasenv subst context he hetype ugraph [] args)
1724                    with
1725                     | RefineFailure _ | Uncertain _
1726                     | HExtlib.Localized (_,RefineFailure _)
1727                     | HExtlib.Localized (_,Uncertain _) -> None)
1728                 possible_fixes
1729               with
1730               | Some x -> x
1731               | None ->
1732                  raise
1733                   (MoreArgsThanExpected
1734                     (List.length args, RefineFailure (lazy "")))
1735     in
1736     (* first we check if we are in the simple case of a meta closed term *)
1737     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
1738      if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
1739       (* this optimization is to postpone fix_arity (the most common case)*)
1740       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
1741      else
1742        (* this (says CSC) is also useful to infer dependent types *)
1743         let pristinemenv = metasenv in
1744         let metasenv,hetype' =
1745           mk_prod_of_metas metasenv context subst args_bo_and_ty
1746         in
1747         try
1748           let subst,metasenv,ugraph =
1749            fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
1750           in
1751           subst,metasenv,ugraph,hetype',he,args_bo_and_ty
1752         with RefineFailure _ | Uncertain _ ->
1753           subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
1754     in
1755     let coerced_args,subst,metasenv,he,t,ugraph =
1756      try
1757       eat_prods_and_args
1758         metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
1759      with
1760       MoreArgsThanExpected (residuals,exn) ->
1761         more_args_than_expected localization_tbl metasenv
1762          subst he context hetype' residuals args_bo_and_ty exn
1763     in
1764     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
1765
1766   and coerce_to_something
1767     allow_coercions localization_tbl t infty expty subst metasenv context ugraph
1768   =
1769     let module CS = CicSubstitution in
1770     let module CR = CicReduction in
1771     let cs_subst = CS.subst ~avoid_beta_redexes:true in
1772     let coerce_atom_to_something t infty expty subst metasenv context ugraph =
1773       debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
1774       let coer =
1775         CoercGraph.look_for_coercion metasenv subst context infty expty
1776       in
1777       match coer with
1778       | CoercGraph.NoCoercion
1779       | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
1780           "coerce_atom_to_something fails since no coercions found"))
1781       | CoercGraph.NotHandled when
1782           not (CicUtil.is_meta_closed infty) ||
1783           not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
1784           "coerce_atom_to_something fails since carriers have metas"))
1785       | CoercGraph.NotHandled -> raise (RefineFailure (lazy
1786           "coerce_atom_to_something fails since no coercions found"))
1787       | CoercGraph.SomeCoercion candidates ->
1788           debug_print (lazy (string_of_int (List.length candidates) ^
1789             " candidates found"));
1790           let uncertain = ref false in
1791           let selected =
1792             let posibilities =
1793               HExtlib.filter_map
1794               (fun (metasenv,last,c) ->
1795                try
1796                 (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
1797                 CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
1798                 " <==> " ^
1799                 CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
1800                 "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
1801                 context));
1802                 debug_print (lazy ("FO_UNIF_SUBST: " ^
1803                 CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
1804                 let subst,metasenv,ugraph =
1805                  fo_unif_subst subst context metasenv last t ugraph
1806                 in
1807                 let newt,newhety,subst,metasenv,ugraph =
1808                  type_of_aux subst metasenv context c ugraph in
1809                 let newt, newty, subst, metasenv, ugraph =
1810                  avoid_double_coercion context subst metasenv ugraph newt expty
1811                 in
1812                 let subst,metasenv,ugraph =
1813                   fo_unif_subst subst context metasenv newhety expty ugraph in
1814                  Some ((newt,newty), subst, metasenv, ugraph)
1815                with
1816                | Uncertain _ -> uncertain := true; None
1817                | RefineFailure _ -> None)
1818               candidates
1819             in
1820             match
1821               List.fast_sort
1822                 (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
1823                 posibilities
1824             with
1825             | [] -> None
1826             | x::_ -> Some x
1827           in
1828           match selected with
1829           | Some x -> x
1830           | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
1831           | None -> raise (RefineFailure (lazy "coerce_atom fails"))
1832     in
1833     let rec coerce_to_something_aux
1834       t infty expty subst metasenv context ugraph
1835     =
1836       try
1837         let subst, metasenv, ugraph =
1838           fo_unif_subst subst context metasenv infty expty ugraph
1839         in
1840         (t, expty), subst, metasenv, ugraph
1841       with (Uncertain _ | RefineFailure _ as exn)
1842         when allow_coercions && !insert_coercions ->
1843           let whd = CicReduction.whd ~delta:false in
1844           let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
1845           let infty = clean infty subst context in
1846           let expty = clean expty subst context in
1847           let t = clean t subst context in
1848           (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
1849           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
1850           CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
1851           CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
1852           let (coerced,_),subst,metasenv,_ as result =
1853            match infty, expty, t with
1854            | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
1855               (*{{{*) debug_print (lazy "FIX");
1856               (match fl with
1857                   [name,i,_(* infty *),bo] ->
1858                     let context_bo =
1859                      Some (Cic.Name name,Cic.Decl expty)::context in
1860                     let (rel1, _), subst, metasenv, ugraph =
1861                      coerce_to_something_aux (Cic.Rel 1)
1862                        (CS.lift 1 expty) (CS.lift 1 infty) subst
1863                       metasenv context_bo ugraph in
1864                     let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
1865                     let (bo,_), subst, metasenv, ugraph =
1866                      coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
1867                      expty) subst
1868                       metasenv context_bo ugraph
1869                     in
1870                      (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
1871                 | _ -> assert false (* not implemented yet *)) (*}}}*)
1872            | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
1873                (*{{{*) debug_print (lazy "CASE");
1874                (* {{{ helper functions *)
1875                let get_cl_and_left_p uri tyno outty ugraph =
1876                  match CicEnvironment.get_obj ugraph uri with
1877                  | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
1878                      let count_pis t =
1879                        let rec aux ctx t =
1880                          match CicReduction.whd ~delta:false ctx t with
1881                          | Cic.Prod (name,src,tgt) ->
1882                              let ctx = Some (name, Cic.Decl src) :: ctx in
1883                              1 + aux ctx tgt
1884                          | _ -> 0
1885                        in
1886                          aux [] t
1887                      in
1888                      let rec skip_lambda_delifting t n =
1889                        match t,n with
1890                        | _,0 -> t
1891                        | Cic.Lambda (_,_,t),n ->
1892                            skip_lambda_delifting
1893                              (CS.subst (Cic.Implicit None) t) (n - 1)
1894                        | _ -> assert false
1895                      in
1896                      let get_l_r_p n = function
1897                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
1898                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
1899                            HExtlib.split_nth n args
1900                        | _ -> assert false
1901                      in
1902                      let _, _, ty, cl = List.nth tl tyno in
1903                      let pis = count_pis ty in
1904                      let rno = pis - leftno in
1905                      let t = skip_lambda_delifting outty rno in
1906                      let left_p, _ = get_l_r_p leftno t in
1907                      let instantiale_with_left cl =
1908                        List.map
1909                          (fun ty ->
1910                            List.fold_left
1911                              (fun t p -> match t with
1912                                | Cic.Prod (_,_,t) ->
1913                                    cs_subst p t
1914                                | _-> assert false)
1915                              ty left_p)
1916                          cl
1917                      in
1918                      let cl = instantiale_with_left (List.map snd cl) in
1919                      cl, left_p, leftno, rno, ugraph
1920                  | _ -> raise exn
1921                in
1922                let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
1923                  match t,n with
1924                  | _,0 ->
1925                    let rec mkr n = function
1926                      | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
1927                    in
1928                    let bo =
1929                    CicReplace.replace_lifting
1930                      ~equality:(fun _ -> CicUtil.alpha_equivalence)
1931                      ~context:ctx
1932                      ~what:(matched::right_p)
1933                      ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
1934                      ~where:bo
1935                    in
1936                    bo
1937                  | Cic.Lambda (name, src, tgt),_ ->
1938                      Cic.Lambda (name, src,
1939                       keep_lambdas_and_put_expty
1940                        (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
1941                        (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
1942                  | _ -> assert false
1943                in
1944                let eq_uri, eq, eq_refl =
1945                  match LibraryObjects.eq_URI () with
1946                  | None -> HLog.warn "no default equality"; raise exn
1947                  | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
1948                in
1949                let add_params
1950                  metasenv subst context uri tyno cty outty mty m leftno i
1951                =
1952                  let rec aux context outty par k mty m = function
1953                    | Cic.Prod (name, src, tgt) ->
1954                        let t,k =
1955                          aux
1956                            (Some (name, Cic.Decl src) :: context)
1957                            (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
1958                            (CS.lift 1 mty) (CS.lift 1 m) tgt
1959                        in
1960                        Cic.Prod (name, src, t), k
1961                    | Cic.MutInd _ ->
1962                        let k =
1963                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1964                          if par <> [] then Cic.Appl (k::par) else k
1965                        in
1966                        Cic.Prod (Cic.Name "p",
1967                         Cic.Appl [eq; mty; m; k],
1968                         (CS.lift 1
1969                          (CR.head_beta_reduce ~delta:false
1970                           (Cic.Appl [outty;k])))),k
1971                    | Cic.Appl (Cic.MutInd _::pl) ->
1972                        let left_p,right_p = HExtlib.split_nth leftno pl in
1973                        let has_rights = right_p <> [] in
1974                        let k =
1975                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
1976                          Cic.Appl (k::left_p@par)
1977                        in
1978                        let right_p =
1979                          try match
1980                            CicTypeChecker.type_of_aux' ~subst metasenv context k
1981                              CicUniv.oblivion_ugraph
1982                          with
1983                          | Cic.Appl (Cic.MutInd _::args),_ ->
1984                              snd (HExtlib.split_nth leftno args)
1985                          | _ -> assert false
1986                          with CicTypeChecker.TypeCheckerFailure _-> assert false
1987                        in
1988                        if has_rights then
1989                          CR.head_beta_reduce ~delta:false
1990                            (Cic.Appl (outty ::right_p @ [k])),k
1991                        else
1992                          Cic.Prod (Cic.Name "p",
1993                           Cic.Appl [eq; mty; m; k],
1994                           (CS.lift 1
1995                            (CR.head_beta_reduce ~delta:false
1996                             (Cic.Appl (outty ::right_p @ [k]))))),k
1997                    | _ -> assert false
1998                  in
1999                    aux context outty [] 1 mty m cty
2000                in
2001                let add_lambda_for_refl_m pbo rno mty m k cty =
2002                  (* k lives in the right context *)
2003                  if rno <> 0 then pbo else
2004                  let rec aux mty m = function
2005                    | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
2006                       Cic.Lambda (name,src,
2007                        (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
2008                    | t,_ ->
2009                        Cic.Lambda (Cic.Name "p",
2010                          Cic.Appl [eq; mty; m; k],CS.lift 1 t)
2011                  in
2012                  aux mty m (pbo,cty)
2013                in
2014                let add_pi_for_refl_m new_outty mty m rno =
2015                  if rno <> 0 then new_outty else
2016                    let rec aux m mty = function
2017                      | Cic.Lambda (name, src, tgt) ->
2018                          Cic.Lambda (name, src,
2019                            aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
2020                      | t ->
2021                          Cic.Prod
2022                            (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
2023                            CS.lift 1 t)
2024                    in
2025                      aux m mty new_outty
2026                in (* }}} end helper functions *)
2027                (* constructors types with left params already instantiated *)
2028                let outty = CicMetaSubst.apply_subst subst outty in
2029                let cl, left_p, leftno,rno,ugraph =
2030                  get_cl_and_left_p uri tyno outty ugraph
2031                in
2032                let right_p, mty =
2033                  try
2034                    match
2035                      CicTypeChecker.type_of_aux' ~subst metasenv context m
2036                        CicUniv.oblivion_ugraph
2037                    with
2038                    | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
2039                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
2040                        snd (HExtlib.split_nth leftno args), mty
2041                    | _ -> assert false
2042                  with CicTypeChecker.TypeCheckerFailure _ ->
2043                     raise (AssertFailure(lazy "already ill-typed matched term"))
2044                in
2045                let new_outty =
2046                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
2047                in
2048                debug_print
2049                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
2050                   ~metasenv subst new_outty context));
2051                let _,pl,subst,metasenv,ugraph =
2052                  List.fold_right2
2053                    (fun cty pbo (i, acc, s, menv, ugraph) ->
2054                      (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
2055                       *   (new_)outty right_par (K_i left_par k_par) *)
2056                       let infty_pbo, _ =
2057                         add_params menv s context uri tyno
2058                           cty outty mty m leftno i in
2059                       debug_print
2060                        (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
2061                         ~metasenv subst infty_pbo context));
2062                       let expty_pbo, k = (* k is (K_i left_par k_par) *)
2063                         add_params menv s context uri tyno
2064                           cty new_outty mty m leftno i in
2065                       debug_print
2066                        (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
2067                         ~metasenv subst expty_pbo context));
2068                       let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
2069                       debug_print
2070                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
2071                         ~metasenv subst pbo context));
2072                       let (pbo, _), subst, metasenv, ugraph =
2073                         coerce_to_something_aux pbo infty_pbo expty_pbo
2074                           s menv context ugraph
2075                       in
2076                       debug_print
2077                         (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
2078                         ~metasenv subst pbo context));
2079                       (i-1, pbo::acc, subst, metasenv, ugraph))
2080                    cl pl (List.length pl, [], subst, metasenv, ugraph)
2081                in
2082                let new_outty = add_pi_for_refl_m new_outty mty m rno in
2083                debug_print
2084                  (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
2085                   ~metasenv subst new_outty context));
2086                let t =
2087                  if rno = 0 then
2088                    let refl_m=Cic.Appl[eq_refl;mty;m]in
2089                    Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
2090                  else
2091                    Cic.MutCase(uri,tyno,new_outty,m,pl)
2092                in
2093                (t, expty), subst, metasenv, ugraph (*}}}*)
2094            | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
2095                (*{{{*) debug_print (lazy "LAM");
2096                let name_con =
2097                  FreshNamesGenerator.mk_fresh_name
2098                    ~subst metasenv context ~typ:src2 Cic.Anonymous
2099                in
2100                let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
2101                (* contravariant part: the argument of f:src->ty *)
2102                let (rel1, _), subst, metasenv, ugraph =
2103                  coerce_to_something_aux
2104                   (Cic.Rel 1) (CS.lift 1 src2)
2105                   (CS.lift 1 src) subst metasenv context_src2 ugraph
2106                in
2107                (* covariant part: the result of f(c x); x:src2; (c x):src *)
2108                let name_t, bo =
2109                  match t with
2110                  | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
2111                  | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
2112                in
2113                (* we fix the possible dependency problem in the source ty *)
2114                let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
2115                let (bo, _), subst, metasenv, ugraph =
2116                  coerce_to_something_aux
2117                    bo ty ty2 subst metasenv context_src2 ugraph
2118                in
2119                let coerced = Cic.Lambda (name_t,src2, bo) in
2120                (coerced, expty), subst, metasenv, ugraph (*}}}*)
2121            | _ ->
2122                (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
2123                 ~metasenv subst infty context ^ " ==> " ^
2124                 CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
2125                coerce_atom_to_something
2126                t infty expty subst metasenv context ugraph (*}}}*)
2127           in
2128           debug_print (lazy ("COERCE TO SOMETHING END: "^
2129             CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
2130           result
2131     in
2132     try
2133       coerce_to_something_aux t infty expty subst metasenv context ugraph
2134     with Uncertain _ | RefineFailure _ as exn ->
2135       let f _ =
2136         lazy ("The term " ^
2137           CicMetaSubst.ppterm_in_context metasenv subst t context ^
2138           " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
2139           infty context ^ " but is here used with type " ^
2140           CicMetaSubst.ppterm_in_context metasenv subst expty context)
2141       in
2142         enrich localization_tbl ~f t exn
2143
2144   and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
2145     match CicReduction.whd ~delta:false ~subst context infty with
2146     | Cic.Meta _ | Cic.Sort _ ->
2147         t,infty, subst, metasenv, ugraph
2148     | src ->
2149        debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
2150          ~metasenv subst src context));
2151        let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
2152        try
2153          let (t, ty_t), subst, metasenv, ugraph =
2154            coerce_to_something true
2155              localization_tbl t src tgt subst metasenv context ugraph
2156          in
2157          debug_print (lazy ("COERCE TO SORT END: "^
2158            CicMetaSubst.ppterm_in_context ~metasenv subst t context));
2159          t, ty_t, subst, metasenv, ugraph
2160        with HExtlib.Localized (_, exn) ->
2161          let f _ =
2162            lazy ("(7)The term " ^
2163             CicMetaSubst.ppterm_in_context ~metasenv subst t context
2164             ^ " is not a type since it has type " ^
2165             CicMetaSubst.ppterm_in_context ~metasenv subst src context
2166             ^ " that is not a sort")
2167          in
2168            enrich localization_tbl ~f t exn
2169   in
2170
2171   (* eat prods ends here! *)
2172
2173   let t',ty,subst',metasenv',ugraph1 =
2174    type_of_aux [] metasenv context t ugraph
2175   in
2176   let substituted_t = CicMetaSubst.apply_subst subst' t' in
2177   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
2178     (* Andrea: ho rimesso qui l'applicazione della subst al
2179        metasenv dopo che ho droppato l'invariante che il metsaenv
2180        e' sempre istanziato *)
2181   let substituted_metasenv =
2182     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
2183     (* metasenv' *)
2184     (*  substituted_t,substituted_ty,substituted_metasenv *)
2185     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
2186   let cleaned_t =
2187    if clean_dummy_dependent_types then
2188     FreshNamesGenerator.clean_dummy_dependent_types substituted_t
2189    else substituted_t in
2190   let cleaned_ty =
2191    if clean_dummy_dependent_types then
2192     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
2193    else substituted_ty in
2194   let cleaned_metasenv =
2195    if clean_dummy_dependent_types then
2196     List.map
2197       (function (n,context,ty) ->
2198          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
2199          let context' =
2200            List.map
2201              (function
2202                   None -> None
2203                 | Some (n, Cic.Decl t) ->
2204                     Some (n,
2205                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
2206                 | Some (n, Cic.Def (bo,ty)) ->
2207                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
2208                     let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
2209                     in
2210                       Some (n, Cic.Def (bo',ty'))
2211              ) context
2212          in
2213            (n,context',ty')
2214       ) substituted_metasenv
2215    else
2216     substituted_metasenv
2217   in
2218     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
2219 ;;
2220
2221 let undebrujin uri typesno tys t =
2222   snd
2223    (List.fold_right
2224      (fun (name,_,_,_) (i,t) ->
2225        (* here the explicit_named_substituion is assumed to be *)
2226        (* of length 0 *)
2227        let t' = Cic.MutInd (uri,i,[])  in
2228        let t = CicSubstitution.subst t' t in
2229         i - 1,t
2230      ) tys (typesno - 1,t))
2231
2232 let map_first_n n start f g l =
2233   let rec aux acc k l =
2234     if k < n then
2235       match l with
2236       | [] -> raise (Invalid_argument "map_first_n")
2237       | hd :: tl -> f hd k (aux acc (k+1) tl)
2238     else
2239       g acc l
2240   in
2241   aux start 0 l
2242
2243 (*CSC: this is a very rough approximation; to be finished *)
2244 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
2245   let subst,metasenv,ugraph,tys =
2246     List.fold_right
2247       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
2248         let subst,metasenv,ugraph,cl =
2249           List.fold_right
2250             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
2251                let rec aux ctx k subst = function
2252                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
2253                      let subst,metasenv,ugraph,tl =
2254                        map_first_n leftno
2255                          (subst,metasenv,ugraph,[])
2256                          (fun t n (subst,metasenv,ugraph,acc) ->
2257                            let subst,metasenv,ugraph =
2258                              fo_unif_subst
2259                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
2260                            in
2261                            subst,metasenv,ugraph,(t::acc))
2262                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
2263                          tl
2264                      in
2265                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
2266                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
2267                      subst,metasenv,ugraph,t
2268                  | Cic.Prod (name,s,t) ->
2269                      let ctx = (Some (name,Cic.Decl s))::ctx in
2270                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
2271                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
2272                  | _ ->
2273                      raise
2274                       (RefineFailure
2275                         (lazy "not well formed constructor type"))
2276                in
2277                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
2278                subst,metasenv,ugraph,(name,ty) :: acc)
2279           cl (subst,metasenv,ugraph,[])
2280         in
2281         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
2282       tys ([],metasenv,ugraph,[])
2283   in
2284   let substituted_tys =
2285     List.map
2286       (fun (name,ind,arity,cl) ->
2287         let cl =
2288           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
2289         in
2290         name,ind,CicMetaSubst.apply_subst subst arity,cl)
2291       tys
2292   in
2293   metasenv,ugraph,substituted_tys
2294
2295 let typecheck metasenv uri obj ~localization_tbl =
2296  let ugraph = CicUniv.oblivion_ugraph in
2297  match obj with
2298     Cic.Constant (name,Some bo,ty,args,attrs) ->
2299      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
2300         since type_of_aux' destroys localization information (which are
2301         preserved by type_of_aux *)
2302      let loc exn' =
2303       try
2304        Cic.CicHash.find localization_tbl bo
2305       with Not_found ->
2306        HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
2307        raise exn' in
2308      let bo',boty,metasenv,ugraph =
2309       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
2310      let ty',_,metasenv,ugraph =
2311       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
2312      let subst,metasenv,ugraph =
2313       try
2314        fo_unif_subst [] [] metasenv boty ty' ugraph
2315       with
2316          RefineFailure _
2317        | Uncertain _ as exn ->
2318           let msg =
2319             lazy ("The term " ^
2320              CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
2321              " has type " ^
2322              CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
2323              " but is here used with type " ^
2324              CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
2325           in
2326            let exn' =
2327             match exn with
2328                RefineFailure _ -> RefineFailure msg
2329              | Uncertain _ -> Uncertain msg
2330              | _ -> assert false
2331            in
2332             raise (HExtlib.Localized (loc exn',exn'))
2333      in
2334      let bo' = CicMetaSubst.apply_subst subst bo' in
2335      let ty' = CicMetaSubst.apply_subst subst ty' in
2336      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
2337       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
2338   | Cic.Constant (name,None,ty,args,attrs) ->
2339      let ty',_,metasenv,ugraph =
2340       type_of_aux' ~localization_tbl metasenv [] ty ugraph
2341      in
2342       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
2343   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
2344      assert (metasenv' = metasenv);
2345      (* Here we do not check the metasenv for correctness *)
2346      let bo',boty,metasenv,ugraph =
2347       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
2348      let ty',sort,metasenv,ugraph =
2349       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
2350      begin
2351       match sort with
2352          Cic.Sort _
2353        (* instead of raising Uncertain, let's hope that the meta will become
2354           a sort *)
2355        | Cic.Meta _ -> ()
2356        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
2357      end;
2358      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
2359      let bo' = CicMetaSubst.apply_subst subst bo' in
2360      let ty' = CicMetaSubst.apply_subst subst ty' in
2361      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
2362       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
2363   | Cic.Variable _ -> assert false (* not implemented *)
2364   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
2365      (*CSC: this code is greately simplified and many many checks are missing *)
2366      (*CSC: e.g. the constructors are not required to build their own types,  *)
2367      (*CSC: the arities are not required to have as type a sort, etc.         *)
2368      let uri = match uri with Some uri -> uri | None -> assert false in
2369      let typesno = List.length tys in
2370      (* first phase: we fix only the types *)
2371      let metasenv,ugraph,tys =
2372       List.fold_right
2373        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
2374          let ty',_,metasenv,ugraph =
2375           (* clean_dummy_dependent_types: false to avoid cleaning the names
2376              of the left products, that must be identical to those of the
2377              constructors; however, non-left products should probably be
2378              cleaned *)
2379           type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
2380            metasenv [] ty ugraph
2381          in
2382           metasenv,ugraph,(name,b,ty',cl)::res
2383        ) tys (metasenv,ugraph,[]) in
2384      let con_context =
2385       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
2386      (* second phase: we fix only the constructors *)
2387      let saved_menv = metasenv in
2388      let metasenv,ugraph,tys =
2389       List.fold_right
2390        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
2391          let metasenv,ugraph,cl' =
2392           List.fold_right
2393            (fun (name,ty) (metasenv,ugraph,res) ->
2394              let ty =
2395               CicTypeChecker.debrujin_constructor
2396               ~cb:(relocalize localization_tbl) uri typesno [] ty in
2397              let ty',_,metasenv,ugraph =
2398               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
2399              let ty' = undebrujin uri typesno tys ty' in
2400               metasenv@saved_menv,ugraph,(name,ty')::res
2401            ) cl (metasenv,ugraph,[])
2402          in
2403           metasenv,ugraph,(name,b,ty,cl')::res
2404        ) tys (metasenv,ugraph,[]) in
2405      (* third phase: we check the positivity condition *)
2406      let metasenv,ugraph,tys =
2407        are_all_occurrences_positive metasenv ugraph uri tys paramsno
2408      in
2409      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
2410 ;;
2411
2412 (* sara' piu' veloce che raffinare da zero? mah.... *)
2413 let pack_coercion metasenv ctx t =
2414  let module C = Cic in
2415  let rec merge_coercions ctx =
2416    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
2417    function
2418    | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
2419    | C.Meta (n,subst) ->
2420       let subst' =
2421        List.map
2422         (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
2423       in
2424        C.Meta (n,subst')
2425    | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
2426    | C.Prod (name,so,dest) ->
2427        let ctx' = (Some (name,C.Decl so))::ctx in
2428        C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
2429    | C.Lambda (name,so,dest) ->
2430        let ctx' = (Some (name,C.Decl so))::ctx in
2431        C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
2432    | C.LetIn (name,so,ty,dest) ->
2433        let ctx' = Some (name,(C.Def (so,ty)))::ctx in
2434        C.LetIn
2435         (name, merge_coercions ctx so, merge_coercions ctx ty,
2436          merge_coercions ctx' dest)
2437    | C.Appl l ->
2438       let l = List.map (merge_coercions ctx) l in
2439       let t = C.Appl l in
2440        let b,_,_,_,_ = is_a_double_coercion t in
2441        if b then
2442          let ugraph = CicUniv.oblivion_ugraph in
2443          let old_insert_coercions = !insert_coercions in
2444          insert_coercions := false;
2445          let newt, _, menv, _ =
2446            try
2447              type_of_aux' metasenv ctx t ugraph
2448            with RefineFailure _ | Uncertain _ ->
2449              t, t, [], ugraph
2450          in
2451          insert_coercions := old_insert_coercions;
2452          if metasenv <> [] || menv = [] then
2453            newt
2454          else
2455            (prerr_endline "PUO' SUCCEDERE!!!!!";t)
2456        else
2457          t
2458    | C.Var (uri,exp_named_subst) ->
2459        let exp_named_subst = List.map aux exp_named_subst in
2460        C.Var (uri, exp_named_subst)
2461    | C.Const (uri,exp_named_subst) ->
2462        let exp_named_subst = List.map aux exp_named_subst in
2463        C.Const (uri, exp_named_subst)
2464    | C.MutInd (uri,tyno,exp_named_subst) ->
2465        let exp_named_subst = List.map aux exp_named_subst in
2466        C.MutInd (uri,tyno,exp_named_subst)
2467    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
2468        let exp_named_subst = List.map aux exp_named_subst in
2469        C.MutConstruct (uri,tyno,consno,exp_named_subst)
2470    | C.MutCase (uri,tyno,out,te,pl) ->
2471        let pl = List.map (merge_coercions ctx) pl in
2472        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
2473    | C.Fix (fno, fl) ->
2474        let ctx' =
2475          List.fold_left
2476            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2477            ctx fl
2478        in
2479        let fl =
2480          List.map
2481            (fun (name,idx,ty,bo) ->
2482              (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
2483          fl
2484        in
2485        C.Fix (fno, fl)
2486    | C.CoFix (fno, fl) ->
2487        let ctx' =
2488          List.fold_left
2489            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
2490            ctx fl
2491        in
2492        let fl =
2493          List.map
2494            (fun (name,ty,bo) ->
2495              (name, merge_coercions ctx ty, merge_coercions ctx' bo))
2496          fl
2497        in
2498        C.CoFix (fno, fl)
2499  in
2500   merge_coercions ctx t
2501 ;;
2502
2503 let pack_coercion_metasenv conjectures = conjectures (*
2504
2505   TASSI: this code war written when coercions were a toy,
2506          now packing coercions involves unification thus
2507          the metasenv may change, and this pack coercion
2508          does not handle that.
2509
2510   let module C = Cic in
2511   List.map
2512     (fun (i, ctx, ty) ->
2513        let ctx =
2514          List.fold_right
2515            (fun item ctx ->
2516               let item' =
2517                 match item with
2518                     Some (name, C.Decl t) ->
2519                       Some (name, C.Decl (pack_coercion conjectures ctx t))
2520                   | Some (name, C.Def (t,None)) ->
2521                       Some (name,C.Def (pack_coercion conjectures ctx t,None))
2522                   | Some (name, C.Def (t,Some ty)) ->
2523                       Some (name, C.Def (pack_coercion conjectures ctx t,
2524                                          Some (pack_coercion conjectures ctx ty)))
2525                   | None -> None
2526               in
2527                 item'::ctx
2528            ) ctx []
2529        in
2530          ((i,ctx,pack_coercion conjectures ctx ty))
2531     ) conjectures
2532     *)
2533 ;;
2534
2535 let pack_coercion_obj obj = obj (*
2536
2537   TASSI: this code war written when coercions were a toy,
2538          now packing coercions involves unification thus
2539          the metasenv may change, and this pack coercion
2540          does not handle that.
2541
2542   let module C = Cic in
2543   match obj with
2544   | C.Constant (id, body, ty, params, attrs) ->
2545       let body =
2546         match body with
2547         | None -> None
2548         | Some body -> Some (pack_coercion [] [] body)
2549       in
2550       let ty = pack_coercion [] [] ty in
2551         C.Constant (id, body, ty, params, attrs)
2552   | C.Variable (name, body, ty, params, attrs) ->
2553       let body =
2554         match body with
2555         | None -> None
2556         | Some body -> Some (pack_coercion [] [] body)
2557       in
2558       let ty = pack_coercion [] [] ty in
2559         C.Variable (name, body, ty, params, attrs)
2560   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
2561       let conjectures = pack_coercion_metasenv conjectures in
2562       let body = pack_coercion conjectures [] body in
2563       let ty = pack_coercion conjectures [] ty in
2564       C.CurrentProof (name, conjectures, body, ty, params, attrs)
2565   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
2566       let indtys =
2567         List.map
2568           (fun (name, ind, arity, cl) ->
2569             let arity = pack_coercion [] [] arity in
2570             let cl =
2571               List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
2572             in
2573             (name, ind, arity, cl))
2574           indtys
2575       in
2576         C.InductiveDefinition (indtys, params, leftno, attrs) *)
2577 ;;
2578
2579
2580 (* DEBUGGING ONLY
2581 let type_of_aux' metasenv context term =
2582  try
2583   let (t,ty,m) =
2584       type_of_aux' metasenv context term in
2585     debug_print (lazy
2586      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
2587    debug_print (lazy
2588     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
2589    (t,ty,m)
2590  with
2591  | RefineFailure msg as e ->
2592      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
2593      raise e
2594  | Uncertain msg as e ->
2595      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
2596      raise e
2597 ;; *)
2598
2599 let profiler2 = HExtlib.profile "CicRefine"
2600
2601 let type_of_aux' ?localization_tbl metasenv context term ugraph =
2602  profiler2.HExtlib.profile
2603   (type_of_aux' ?localization_tbl metasenv context term) ugraph
2604
2605 let typecheck ~localization_tbl metasenv uri obj =
2606  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
2607
2608 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
2609 (* vim:set foldmethod=marker: *)
2610 *)