matita/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 exception RefineFailure of (Stdpp.location * string) Lazy.t;;
  15 exception Uncertain of (Stdpp.location * string) Lazy.t;;
  16 exception AssertFailure of string Lazy.t;;
  17
  18 module C = NCic
  19 module Ref = NReference
  20
  21 type 'a expected_type = [ `XTNone       (* unknown *)
  22                         | `XTSome of 'a (* the given term *)
  23                         | `XTSort       (* any sort *)
  24                         | `XTInd        (* any (co)inductive type *)
  25                         ]
  26
  27 let debug = ref false;;
  28 let indent = ref "";;
  29 let times = ref [];;
  30 let pp s =
  31  if !debug then
  32   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  33 ;;
  34 let inside c =
  35  if !debug then
  36   begin
  37    let time1 = Unix.gettimeofday () in
  38    indent := !indent ^ String.make 1 c;
  39    times := time1 :: !times;
  40    prerr_endline ("{{{" ^ !indent ^ " ")
  41   end
  42 ;;
  43 let outside ok =
  44  if !debug then
  45   begin
  46    let time2 = Unix.gettimeofday () in
  47    let time1 =
  48     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
  49    prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
  50    if not ok then prerr_endline "exception raised!";
  51    try
  52     indent := String.sub !indent 0 (String.length !indent -1)
  53    with
  54     Invalid_argument _ -> indent := "??"; ()
  55  end
  56 ;;
  57
  58
  59 let wrap_exc msg = function
  60   | NCicUnification.Uncertain _ -> Uncertain msg
  61   | NCicUnification.UnificationFailure _ -> RefineFailure msg
  62   | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
  63   | e -> raise e
  64 ;;
  65
  66 let exp_implicit status ~localise metasenv subst context with_type t =
  67  function
  68   | `Closed ->
  69       let metasenv,subst,expty =
  70        match with_type with
  71           `XTSort
  72         | `XTInd
  73         | `XTNone -> metasenv,subst,None
  74         | `XTSome typ ->
  75            let (metasenv,subst),typ =
  76             try
  77              NCicMetaSubst.delift status
  78               ~unify:(fun m s c t1 t2 ->
  79                 try Some (NCicUnification.unify status m s c t1 t2)
  80                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
  81               metasenv subst context (-1) (0,C.Irl 0) typ
  82             with
  83               NCicMetaSubst.MetaSubstFailure _
  84             | NCicMetaSubst.Uncertain _ ->
  85                raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type: " ^ status#ppterm ~metasenv ~subst ~context typ)))
  86
  87            in
  88             metasenv,subst,Some typ
  89       in
  90        NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst
  91   | `Type ->
  92       let with_type = match with_type with `XTSome t -> Some t | _ -> None in
  93       NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
  94   | `Term ->
  95       let with_type = match with_type with `XTSome t -> Some t | _ -> None in
  96       NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
  97   | `Tagged s ->
  98       let with_type = match with_type with `XTSome t -> Some t | _ -> None in
  99       NCicMetaSubst.mk_meta
 100         ~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst
 101   | `Vector ->
 102       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
 103        "can only be used in argument position")))
 104   | _ -> assert false
 105 ;;
 106
 107 let check_allowed_sort_elimination status localise r orig =
 108    let mkapp he arg =
 109      match he with
 110      | C.Appl l -> C.Appl (l @ [arg])
 111      | t -> C.Appl [t;arg] in
 112    (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
 113    let rec aux metasenv subst context ind arity1 arity2 =
 114      (*D*)inside 'S'; try let rc =
 115      let arity1 = NCicReduction.whd status ~subst context arity1 in
 116      pp (lazy(status#ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
 117         status#ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
 118         status#ppmetasenv ~subst metasenv));
 119      match arity1 with
 120      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
 121         let metasenv, _, meta, _ =
 122           NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `IsType
 123         in
 124         let metasenv, subst =
 125           try NCicUnification.unify status metasenv subst context
 126                 arity2 (C.Prod (name, so1, meta))
 127           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
 128             "expected %s, found %s" (* XXX localizzare meglio *)
 129             (status#ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
 130             (status#ppterm ~subst ~metasenv ~context arity2))) exc)
 131         in
 132         aux metasenv subst ((name, C.Decl so1)::context)
 133          (mkapp (NCicSubstitution.lift status 1 ind) (C.Rel 1)) de1 meta
 134      | C.Sort _ (* , t ==?== C.Prod _ *) ->
 135         let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `IsSort in
 136         let metasenv, subst =
 137           try NCicUnification.unify status metasenv subst context
 138                 arity2 (C.Prod ("_", ind, meta))
 139           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
 140             "expected %s, found %s" (* XXX localizzare meglio *)
 141             (status#ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
 142             (status#ppterm ~subst ~metasenv ~context arity2))) exc)
 143         in
 144         (try NCicTypeChecker.check_allowed_sort_elimination status
 145             ~metasenv ~subst r context ind arity1 arity2;
 146             metasenv, subst
 147         with exc -> raise (wrap_exc (lazy (localise orig,
 148           "Sort elimination not allowed ")) exc))
 149      | _ -> assert false
 150      (*D*)in outside true; rc with exc -> outside false; raise exc
 151    in
 152     aux
 153 ;;
 154
 155 (* CSC: temporary thing, waiting for better times *)
 156 let mk_fresh_name context name =
 157 try
 158  let rex = Str.regexp "[0-9']*$" in
 159  let rex2 = Str.regexp "'*$" in
 160  let basename = Str.global_replace rex "" in
 161  let suffix name =
 162   ignore (Str.search_forward rex name 0);
 163   let n = Str.matched_string name in
 164   let n = Str.global_replace rex2 "" n in
 165    if n = "" then 0 else int_of_string n
 166 in
 167  let name' = basename name in
 168  let name' = if name' = "_" then "H" else name' in
 169  let last =
 170   List.fold_left
 171    (fun last (name,_) ->
 172      if basename name = name' then
 173       max last (suffix name)
 174      else
 175       last
 176    ) (-1) context
 177  in
 178   name' ^ (if last = -1 then "" else string_of_int (last + 1))
 179 with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
 180
 181 (* let eq, eq_refl =
 182     let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
 183     C.Const (Ref.reference_of_spec uri (Ref.Ind (true,0,2))),
 184     C.Const (Ref.reference_of_spec uri Ref.Con (0,1,2))
 185 *)
 186 let eq, eq_refl =
 187  let uri = NUri.uri_of_string "cic:/matita/basics/jmeq/jmeq.ind" in
 188  C.Const (Ref.reference_of_spec uri (Ref.Ind(true,0,2))),
 189  C.Const (Ref.reference_of_spec uri (Ref.Con(0,1,2)))
 190
 191 let rec typeof (status:#NCicCoercion.status)
 192   ?(localise=fun _ -> Stdpp.dummy_loc)
 193   metasenv subst context term expty
 194 =
 195   let force_ty skip_lambda skip_appl metasenv subst context orig t infty expty =
 196     (*D*)inside 'F'; try let rc =
 197     match expty with
 198     | `XTSome expty ->
 199        (match t with
 200        | C.Implicit _ -> assert false
 201        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
 202        | C.Appl _ when skip_appl -> metasenv, subst, t, expty
 203        | _ ->
 204           pp (lazy ("forcing infty=expty: "^
 205           (status#ppterm ~metasenv ~subst ~context infty) ^  " === " ^
 206           (status#ppterm ~metasenv ~subst:[] ~context expty)));
 207            try
 208              let metasenv, subst =
 209     (*D*)inside 'U'; try let rc =
 210                NCicUnification.unify status metasenv subst context infty expty
 211     (*D*)in outside true; rc with exc -> outside false; raise exc
 212              in
 213              metasenv, subst, t, expty
 214            with
 215            | NCicUnification.Uncertain _
 216            | NCicUnification.UnificationFailure _ as exc ->
 217              try_coercions status ~localise
 218                metasenv subst context t orig infty (`XTSome expty) exc)
 219     | `XTNone -> metasenv, subst, t, infty
 220     | `XTSort ->
 221        (match t with
 222        | C.Implicit _ -> assert false
 223        | _ ->
 224           pp (lazy ("forcing infty=any sort: "^
 225           (status#ppterm ~metasenv ~subst ~context infty) ^  " === any sort"));
 226           force_to_sort status metasenv subst context t orig localise infty)
 227     | `XTInd ->
 228        (match t with
 229        | C.Implicit _ -> assert false
 230        | _ ->
 231           pp (lazy ("forcing infty=any (co)inductive type: "^
 232           (status#ppterm ~metasenv ~subst ~context infty) ^  " === any (co)inductive type"));
 233           force_to_inductive status metasenv subst context t orig localise infty)
 234     (*D*)in outside true; rc with exc -> outside false; raise exc
 235   in
 236   let rec typeof_aux metasenv subst context expty =
 237     fun t as orig ->
 238     (*D*)inside 'R'; try let rc =
 239     pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
 240        match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
 241                       | `XTNone -> "None" | `XTSome e ->
 242        status#ppterm ~metasenv ~subst ~context e));
 243     let metasenv, subst, t, infty =
 244     match t with
 245     | C.Rel n ->
 246         let infty =
 247          (try
 248            match List.nth context (n - 1) with
 249            | (_,C.Decl ty) -> NCicSubstitution.lift status n ty
 250            | (_,C.Def (_,ty)) -> NCicSubstitution.lift status n ty
 251          with Failure _ ->
 252            raise (RefineFailure (lazy (localise t,"unbound variable"))))
 253         in
 254         metasenv, subst, t, infty
 255     | C.Sort s ->
 256          (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
 257          with
 258          | NCicEnvironment.UntypableSort msg ->
 259               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
 260          | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
 261     | C.Implicit infos ->
 262          let (metasenv,_,t,ty),subst =
 263            exp_implicit status ~localise metasenv subst context expty t infos
 264          in
 265          (match expty with
 266             | `XTSome _ -> metasenv, subst, t, ty
 267             | _         -> typeof_aux metasenv subst context expty t)
 268     | C.Meta (n,l) as t ->
 269        let metasenv, ty =
 270         try
 271          let _,_,_,ty = NCicUtils.lookup_subst n subst in metasenv, ty
 272         with NCicUtils.Subst_not_found _ ->
 273          NCicMetaSubst.extend_meta metasenv n
 274        in
 275        metasenv, subst, t, NCicSubstitution.subst_meta status l ty
 276     | C.Const _ ->
 277        metasenv, subst, t, NCicTypeChecker.typeof status ~subst ~metasenv context t
 278     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
 279        let metasenv, subst, s, s1 = typeof_aux metasenv subst context `XTSort s in
 280        let metasenv, subst, s, s1 =
 281          force_to_sort status
 282            metasenv subst context s orig_s localise s1 in
 283        let context1 = (name,(C.Decl s))::context in
 284        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 `XTSort t in
 285        let metasenv, subst, t, s2 =
 286          force_to_sort status
 287            metasenv subst context1 t orig_t localise s2 in
 288        let metasenv, subst, s, t, ty =
 289          sort_of_prod status localise metasenv subst
 290            context orig_s orig_t (name,s) t (s1,s2)
 291        in
 292        metasenv, subst, C.Prod(name,s,t), ty
 293     | C.Lambda (n,(s as orig_s),t) as orig ->
 294        let exp_s, exp_ty_t, force_after =
 295          match expty with
 296          | `XTSort
 297          | `XTInd
 298          | `XTNone -> `XTNone, `XTNone, false
 299          | `XTSome expty ->
 300              match NCicReduction.whd status ~subst context expty with
 301              | C.Prod (_,s,t) -> `XTSome s, `XTSome t, false
 302              | _ -> `XTNone, `XTNone, true
 303        in
 304        let (metasenv,subst), s =
 305          match exp_s with
 306          | `XTSome exp_s ->
 307              (* optimized case: implicit and implicitly typed meta
 308               * the optimization prevents proliferation of metas  *)
 309              (match s with
 310               | C.Implicit _ -> (metasenv,subst),exp_s
 311               | _ ->
 312                   let metasenv, subst, s = match s with
 313                     | C.Meta (n,_)
 314                         when (try (match NCicUtils.lookup_meta n metasenv with
 315                               | _,_,C.Implicit (`Typeof _) -> true
 316                               | _ -> false)
 317                         with
 318                           | _ -> false) -> metasenv, subst, s
 319                     | _ ->  check_type status ~localise metasenv subst context s in
 320                   (try
 321                     pp(lazy("Force source to: "^status#ppterm ~metasenv ~subst
 322                        ~context exp_s));
 323                     NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s, s
 324                   with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
 325                     "Source type %s was expected to be %s" (status#ppterm ~metasenv
 326                     ~subst ~context s) (status#ppterm ~metasenv ~subst ~context
 327                     exp_s))) exc)))
 328          | `XTNone
 329          | `XTSort
 330          | `XTInd  ->
 331              let metasenv, subst, s =
 332                check_type status ~localise metasenv subst context s in
 333              (metasenv, subst), s
 334        in
 335        let context_for_t = (n,C.Decl s) :: context in
 336        let metasenv, subst, t, ty_t =
 337          typeof_aux metasenv subst context_for_t exp_ty_t t
 338        in
 339        if force_after then
 340          force_ty false true metasenv subst context orig
 341            (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
 342        else
 343          metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
 344     | C.LetIn (n,ty,t,bo) ->
 345        let metasenv, subst, ty =
 346          check_type status ~localise metasenv subst context ty in
 347        let metasenv, subst, t, _ =
 348          typeof_aux metasenv subst context (`XTSome ty) t in
 349        let context1 = (n, C.Def (t,ty)) :: context in
 350        let metasenv, subst, expty1 =
 351          match expty with
 352          | `XTSome x ->
 353              let m, s, x =
 354                NCicUnification.delift_type_wrt_terms
 355                 status metasenv subst context1 (NCicSubstitution.lift status 1 x)
 356                 [NCicSubstitution.lift status 1 t]
 357              in
 358                m, s, `XTSome x
 359          | _ -> metasenv, subst, expty
 360        in
 361        let metasenv, subst, bo, bo_ty =
 362          typeof_aux metasenv subst context1 expty1 bo
 363        in
 364        let bo_ty = NCicSubstitution.subst status ~avoid_beta_redexes:true t bo_ty in
 365        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
 366     | C.Appl ((he as orig_he)::(_::_ as args)) ->
 367        let upto = match orig_he with C.Meta _ -> List.length args | _ -> 0 in
 368        let hbr t =
 369          if upto > 0 then NCicReduction.head_beta_reduce status ~upto t else t
 370        in
 371        let refine_appl metasenv subst args =
 372          let metasenv, subst, he, ty_he =
 373             typeof_aux metasenv subst context `XTNone he in
 374          let metasenv, subst, t, ty =
 375            eat_prods status ~localise force_ty metasenv subst context expty t
 376             orig_he he ty_he args in
 377          metasenv, subst, hbr t, ty
 378        in
 379        if args = [C.Implicit `Vector] && expty <> `XTNone then
 380          (* we try here to expand the vector a 0 implicits, but we use
 381           * the expected type *)
 382          try
 383            let metasenv, subst, he, ty_he =
 384               typeof_aux metasenv subst context expty he in
 385            metasenv, subst, hbr he, ty_he
 386          with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
 387        else
 388         (* CSC: whd can be useful on he too... *)
 389         (match he with
 390             C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
 391              match expty with
 392              | `XTSome expty -> (
 393                match NCicReduction.whd status ~subst context expty with
 394                 C.Appl (C.Const (Ref.Ref (uri2,Ref.Ind _) as ref)::expargs)
 395                 when NUri.eq uri1 uri2 ->
 396                 (try
 397                  let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
 398                  let leftexpargs,_ = HExtlib.split_nth leftno expargs in
 399                   let rec instantiate metasenv subst revargs args =
 400                    function
 401                      [] ->
 402                       (* some checks are re-done here, but it would be complex
 403                          to avoid them (e.g. we did not check yet that the
 404                          constructor is a constructor for that inductive type)*)
 405                       refine_appl metasenv subst ((List.rev revargs)@args)
 406                    | (exparg::expargs) as allexpargs ->
 407                       match args with
 408                          [] -> raise (Failure "Not enough args")
 409                        | (C.Implicit `Vector::args) as allargs ->
 410                           (try
 411                             instantiate metasenv subst revargs args allexpargs
 412                            with
 413                               Sys.Break as exn -> raise exn
 414                             | _ ->
 415                              instantiate metasenv subst revargs
 416                               (C.Implicit `Term :: allargs) allexpargs)
 417                        | arg::args ->
 418                           let metasenv,subst,arg,_ =
 419                            typeof_aux metasenv subst context `XTNone arg in
 420                           let metasenv,subst =
 421                            NCicUnification.unify status metasenv subst context
 422                             arg exparg
 423                           in
 424                            instantiate metasenv subst(arg::revargs) args expargs
 425                   in
 426                    instantiate metasenv subst [] args leftexpargs
 427                 with
 428                  | Sys.Break as exn -> raise exn
 429                  | _ ->
 430                     refine_appl metasenv subst args (* to try coercions *))
 431                | _ -> refine_appl metasenv subst args)
 432              | `XTNone
 433              | `XTSort
 434              | `XTInd  -> refine_appl metasenv subst args)
 435           | _ -> refine_appl metasenv subst args)
 436    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
 437    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
 438           outtype,(term as orig_term),pl) as orig ->
 439       let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
 440       let _, _, arity, cl = List.nth itl tyno in
 441       let constructorsno = List.length cl in
 442       let _, metasenv, args =
 443         NCicMetaSubst.saturate status metasenv subst context arity 0 in
 444       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
 445       let metasenv, subst, term, _ =
 446         typeof_aux metasenv subst context (`XTSome ind) term in
 447       let parameters, arguments = HExtlib.split_nth leftno args in
 448       let outtype =
 449         match outtype with
 450         | C.Implicit _ as ot ->
 451              let rec aux = function
 452                | [] -> C.Lambda ("_",C.Implicit `Type,ot)
 453                | _::tl -> C.Lambda ("_",C.Implicit `Type,aux tl)
 454              in
 455                aux arguments
 456         | _ -> outtype
 457       in
 458       let metasenv, subst, outtype, outsort =
 459         typeof_aux metasenv subst context `XTNone outtype in (* this cannot be `XTSort *)
 460
 461       (* next lines are to do a subst-expansion of the outtype, so
 462          that when it becomes a beta-abstraction, the beta-redex is
 463          fired during substitution *)
 464       let _,fresh_metanoouttype,newouttype,_ =
 465        NCicMetaSubst.mk_meta metasenv context `IsTerm in
 466       let subst =
 467        (fresh_metanoouttype,([`Name "outtype"],context,outtype,outsort))
 468          ::subst in
 469       let outtype = newouttype in
 470
 471       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 472       let ind =
 473         if parameters = [] then C.Const r
 474         else C.Appl ((C.Const r)::parameters) in
 475       let metasenv, subst, ind, ind_ty =
 476         typeof_aux metasenv subst context `XTNone ind in (* FG: this cannot be `XTSort *)
 477       let metasenv, subst =
 478          check_allowed_sort_elimination status localise r orig_term metasenv subst
 479            context ind ind_ty outsort
 480       in
 481       (* let's check if the type of branches are right *)
 482       if List.length pl <> constructorsno then
 483        raise (RefineFailure (lazy (localise orig,
 484          "Wrong number of cases in a match")));
 485 (*
 486       let metasenv, subst =
 487         match expty with
 488         | None -> metasenv, subst
 489         | Some expty ->
 490            NCicUnification.unify status metasenv subst context resty expty
 491       in
 492 *)
 493       let _, metasenv, subst, pl =
 494         List.fold_right
 495           (fun p (j, metasenv, subst, branches) ->
 496               let cons =
 497                 let cons = Ref.mk_constructor j r in
 498                 if parameters = [] then C.Const cons
 499                 else C.Appl (C.Const cons::parameters)
 500               in
 501               let metasenv, subst, cons, ty_cons =
 502                 typeof_aux metasenv subst context `XTNone cons in (* FG: this cannot be `XTInd *)
 503               let ty_branch =
 504                 NCicTypeChecker.type_of_branch status
 505                   ~subst context leftno outtype cons ty_cons in
 506               pp (lazy ("TYPEOFBRANCH: " ^
 507                status#ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
 508                status#ppterm ~metasenv ~subst ~context ty_branch ));
 509               let metasenv, subst, p, _ =
 510                 typeof_aux metasenv subst context (`XTSome ty_branch) p in
 511               j-1, metasenv, subst, p :: branches)
 512           pl (List.length pl, metasenv, subst, [])
 513       in
 514       let resty = C.Appl (outtype::arguments@[term]) in
 515       let resty = NCicReduction.head_beta_reduce status ~subst resty in
 516       metasenv, subst, C.Match (r, outtype, term, pl),resty
 517     | C.Match _ -> assert false
 518     in
 519     pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
 520          status#ppterm ~metasenv ~subst ~context infty ));
 521       force_ty true true metasenv subst context orig t infty expty
 522     (*D*)in outside true; rc with exc -> outside false; raise exc
 523   in
 524     typeof_aux metasenv subst context expty term
 525
 526 and check_type status ~localise metasenv subst context (ty as orig_ty) =
 527   let metasenv, subst, ty, sort =
 528     typeof status ~localise metasenv subst context ty `XTSort
 529   in
 530   let metasenv, subst, ty, _ =
 531     force_to_sort status metasenv subst context ty orig_ty localise sort
 532   in
 533     metasenv, subst, ty
 534
 535 and try_coercions status
 536   ~localise metasenv subst context t orig_t infty expty exc
 537 =
 538   let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in
 539   try
 540    (match expty with
 541        `XTSome expty ->
 542          pp (lazy "WWW: trying coercions -- preliminary unification");
 543          let metasenv, subst =
 544            NCicUnification.unify status metasenv subst context infty expty
 545          in metasenv, subst, t, expty
 546      | _ -> raise (Failure "Special case XTProd, XTSort or XTInd"))
 547   with
 548   | exn ->
 549   (* we try with a coercion *)
 550   let rec first exc = function
 551   | [] ->
 552       pp (lazy "WWW: no more coercions!");
 553       raise (wrap_exc (lazy
 554        let expty =
 555         match expty with
 556            `XTSome expty -> status#ppterm ~metasenv ~subst ~context expty
 557          | `XTSort -> "[[sort]]"
 558          | `XTProd -> "[[prod]]"
 559          | `XTInd  -> "[[ind]]"  in
 560          (localise orig_t, Printf.sprintf
 561         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
 562         (status#ppterm ~metasenv ~subst ~context t)
 563         (status#ppterm ~metasenv ~subst ~context infty)
 564         expty)) exc)
 565   | (_,metasenv, newterm, newtype, meta)::tl ->
 566       try
 567           pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));
 568           pp (lazy ( "UNIFICATION in CTX:\n"^
 569             status#ppcontext ~metasenv ~subst context
 570             ^ "\nMENV: " ^
 571             status#ppmetasenv metasenv ~subst
 572             ^ "\nOF: " ^
 573             status#ppterm ~metasenv ~subst ~context t ^  " === " ^
 574             status#ppterm ~metasenv ~subst ~context meta ^ "\n"));
 575         let metasenv, subst =
 576           NCicUnification.unify status metasenv subst context t meta in
 577         match expty with
 578            `XTSome expty ->
 579              pp (lazy ( "UNIFICATION in CTX:\n"^
 580                status#ppcontext ~metasenv ~subst context
 581                ^ "\nMENV: " ^
 582                status#ppmetasenv metasenv ~subst
 583                ^ "\nOF: " ^
 584                status#ppterm ~metasenv ~subst ~context newtype ^  " === " ^
 585                status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
 586              let metasenv,subst =
 587                NCicUnification.unify status metasenv subst context newtype expty
 588              in
 589               metasenv, subst, newterm, newtype
 590          | `XTSort ->
 591              (match NCicReduction.whd status ~subst context newtype with
 592                  C.Sort _ -> metasenv,subst,newterm,newtype
 593                | _ -> first exc tl)
 594          | `XTInd ->
 595              (match NCicReduction.whd status ~subst context newtype with
 596                  C.Const (Ref.Ref (_, Ref.Ind _)) -> metasenv,subst,newterm,newtype
 597                | _ -> first exc tl)
 598          | `XTProd ->
 599              (match NCicReduction.whd status ~subst context newtype with
 600                  C.Prod _ -> metasenv,subst,newterm,newtype
 601                | _ -> first exc tl)
 602       with
 603       | NCicUnification.UnificationFailure _ -> first exc tl
 604       | NCicUnification.Uncertain _ as exc -> first exc tl
 605   in
 606
 607   try
 608     pp (lazy "WWW: trying coercions -- inner check");
 609     match infty, expty, t with
 610     (* `XTSort|`XTProd|`XTInd + Match not implemented *)
 611     | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,_tyno,_leftno)) as r,outty,m,pl) ->
 612         (*{{{*) pp (lazy "CASE");
 613         (* {{{ helper functions *)
 614         let get_cl_and_left_p refit outty =
 615           match refit with
 616           | Ref.Ref (_uri, Ref.Ind (_,tyno,_leftno)) ->
 617              let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
 618              let _, _, ty, cl = List.nth itl tyno in
 619              (*let constructorsno = List.length cl in*)
 620               let count_pis t =
 621                 let rec aux ctx t =
 622                   match NCicReduction.whd status ~subst ~delta:max_int ctx t with
 623                   | C.Prod (name,src,tgt) ->
 624                       let ctx = (name, (C.Decl src)) :: ctx in
 625                       1 + aux ctx tgt
 626                   | _ -> 0
 627                 in
 628                   aux [] t
 629               in
 630               let rec skip_lambda_delifting t n =
 631                 match t,n with
 632                 | _,0 -> t
 633                 | C.Lambda (_,_,t),n ->
 634                     pp (lazy ("WWW: failing term? "^ status#ppterm ~subst:[] ~metasenv:[] ~context:[] t));
 635                     skip_lambda_delifting
 636                       (* substitute dangling indices with a dummy *)
 637                       (NCicSubstitution.subst status (C.Sort C.Prop) t) (n - 1)
 638                 | _ -> assert false
 639               in
 640               let get_l_r_p n = function
 641                 | C.Lambda (_,C.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
 642                 | C.Lambda (_,C.Appl
 643                     (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
 644                     HExtlib.split_nth n args
 645                 | _ -> assert false
 646               in
 647               let pis = count_pis ty in
 648               let rno = pis - leftno in
 649               let t = skip_lambda_delifting outty rno in
 650               let left_p, _ = get_l_r_p leftno t in
 651               let instantiate_with_left cl =
 652                 List.map
 653                   (fun ty ->
 654                     List.fold_left
 655                       (fun t p -> match t with
 656                         | C.Prod (_,_,t) ->
 657                             cs_subst p t
 658                         | _-> assert false)
 659                       ty left_p)
 660                   cl
 661               in
 662               let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
 663               cl, left_p, leftno, rno
 664           | _ -> raise exn
 665         in
 666         (*{{{*) pp (lazy "CASE");
 667         let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
 668           match t,n with
 669           | _,0 ->
 670             let rec mkr n = function
 671               | [] -> [] | _::tl -> C.Rel n :: mkr (n+1) tl
 672             in
 673             pp (lazy ("input replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
 674             let bo =
 675             NCicRefineUtil.replace_lifting status
 676               ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence status)
 677               ~context:ctx
 678               ~what:(matched::right_p)
 679               ~with_what:(C.Rel 1::List.rev (mkr 2 right_p))
 680               ~where:bo
 681             in
 682             pp (lazy ("output replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
 683             bo
 684           | C.Lambda (name, src, tgt),_ ->
 685               C.Lambda (name, src,
 686                keep_lambdas_and_put_expty
 687                 ((name, C.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo)
 688                 (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
 689           | _ -> assert false
 690         in
 691         let add_params
 692           metasenv subst context cty outty mty m i
 693         =
 694           let rec aux context outty par j mty m = function
 695             | C.Prod (name, src, tgt) ->
 696                 let t,k =
 697                   aux
 698                     ((name, C.Decl src) :: context)
 699                     (NCicSubstitution.lift status 1 outty) (C.Rel j::par) (j+1)
 700                     (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
 701                 in
 702                 C.Prod (name, src, t), k
 703             | C.Const (Ref.Ref (_,Ref.Ind (_,_,_leftno)) as r) ->
 704                 let k =
 705                   let k = C.Const(Ref.mk_constructor i r) in
 706                   NCicUntrusted.mk_appl k par
 707                 in
 708                 (* the type has no parameters, so kty = mty
 709                 let kty =
 710                   try NCicTypechecker.typeof ~subst ~metasenv context k
 711                   with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 712                 in *)
 713                 C.Prod ("p",
 714                  C.Appl [eq; mty; m; mty; k],
 715                  (NCicSubstitution.lift status 1
 716                   (NCicReduction.head_beta_reduce status ~delta:max_int
 717                    (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
 718             | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
 719                 let left_p,_right_p = HExtlib.split_nth leftno pl in
 720                 (*let has_rights = right_p <> [] in*)
 721                 let k =
 722                   let k = C.Const(Ref.mk_constructor i r) in
 723                   NCicUntrusted.mk_appl k (left_p@par)
 724                 in
 725                 let right_p =
 726                   try match
 727                     NCicTypeChecker.typeof status ~subst ~metasenv context k
 728                   with
 729                   | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
 730                       snd (HExtlib.split_nth leftno args)
 731                   | _ -> assert false
 732                   with NCicTypeChecker.TypeCheckerFailure _-> assert false
 733                 in
 734                 let orig_right_p =
 735                   match mty with
 736                   | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
 737                       snd (HExtlib.split_nth leftno args)
 738                   | _ -> assert false
 739                 in
 740                 List.fold_right2
 741                   (fun x y (tacc,pacc) ->
 742                     let xty =
 743                     try NCicTypeChecker.typeof status ~subst ~metasenv context x
 744                       with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 745                     in
 746                     let yty =
 747                     try NCicTypeChecker.typeof status ~subst ~metasenv context y
 748                       with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 749                     in
 750                     C.Prod ("_", C.Appl [eq;xty;x;yty;y],
 751                      NCicSubstitution.lift status 1 tacc), (xty,x,yty,y)::pacc)
 752                   (orig_right_p @ [m]) (right_p @ [k])
 753                   (NCicReduction.head_beta_reduce status ~delta:max_int
 754                       (NCicUntrusted.mk_appl outty (right_p@[k])), [])
 755
 756   (*              if has_rights then
 757                   NCicReduction.head_beta_reduce status ~delta:max_int
 758                     (C.Appl (outty ::right_p @ [k])),k
 759                 else
 760                   C.Prod ("p",
 761                    C.Appl [eq; mty; m; k],
 762                    (NCicSubstitution.lift status 1
 763                     (NCicReduction.head_beta_reduce status ~delta:max_int
 764                      (C.Appl (outty ::right_p @ [k]))))),k*)
 765             | _ -> assert false
 766           in
 767             aux context outty [] 1 mty m cty
 768         in
 769         let add_lambda_for_refl_m pbo eqs cty =
 770           (* k lives in the right context *)
 771           (* if rno <> 0 then pbo else *)
 772           let rec aux = function
 773             | C.Lambda (name,src,bo), C.Prod (_,_,ty) ->
 774                 C.Lambda (name,src,
 775                 (aux (bo,ty)))
 776             | t,_ -> snd (List.fold_right
 777                 (fun (xty,x,yty,y) (n,acc) -> n+1, C.Lambda ("p" ^ string_of_int n,
 778                   C.Appl [eq; xty; x; yty; y],
 779                   NCicSubstitution.lift status 1 acc)) eqs (1,t))
 780                 (*C.Lambda ("p",
 781                   C.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*)
 782           in
 783           aux (pbo,cty)
 784         in
 785         let add_pi_for_refl_m context new_outty mty m lno rno =
 786           (*if rno <> 0 then new_outty else*)
 787             let rec aux context mty m = function
 788               | C.Lambda (name, src, tgt) ->
 789                   let context = (name, C.Decl src)::context in
 790                   C.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt)
 791               | t ->
 792                   let lhs =
 793                     match mty with
 794                     | C.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
 795                     | _ -> [m]
 796                   in
 797                   let rhs =
 798                     List.map (fun x -> C.Rel x)
 799                       (List.rev (HExtlib.list_seq 1 (rno+2))) in
 800                   List.fold_right2
 801                     (fun x y acc ->
 802                       let xty =
 803                     try NCicTypeChecker.typeof status ~subst ~metasenv context x
 804                         with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 805                       in
 806                       let yty =
 807                     try NCicTypeChecker.typeof status ~subst ~metasenv context y
 808                         with NCicTypeChecker.TypeCheckerFailure _ -> assert false
 809                       in
 810                       C.Prod
 811                       ("_", C.Appl [eq;xty;x;yty;y],
 812                        (NCicSubstitution.lift status 1 acc)))
 813                     lhs rhs t
 814   (*                C.Prod
 815                     ("_", C.Appl [eq;mty;m;C.Rel 1],
 816                     NCicSubstitution.lift status 1 t)*)
 817             in
 818               aux context mty m new_outty
 819         in (* }}} end helper functions *)
 820         (* constructors types with left params already instantiated *)
 821         let outty = NCicUntrusted.apply_subst status subst context outty in
 822         let cl, _left_p, leftno,rno =
 823           get_cl_and_left_p r outty
 824         in
 825         let right_p, mty =
 826           try
 827             match
 828               NCicTypeChecker.typeof status ~subst ~metasenv context m
 829             with
 830             | (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | C.Meta _) as mty -> [], mty
 831             | C.Appl ((C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|C.Meta _)::args) as mty ->
 832                 snd (HExtlib.split_nth leftno args), mty
 833             | _ -> assert false
 834           with NCicTypeChecker.TypeCheckerFailure _ ->
 835              raise (AssertFailure(lazy "already ill-typed matched term"))
 836         in
 837         let mty = NCicUntrusted.apply_subst status subst context mty in
 838         let outty = NCicUntrusted.apply_subst status subst context outty in
 839         let expty = NCicUntrusted.apply_subst status subst context expty in
 840         let new_outty =
 841          keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
 842         in
 843         pp
 844           (lazy ("CASE: new_outty: " ^ status#ppterm
 845            ~context ~metasenv ~subst new_outty));
 846         let _,pl,subst,metasenv =
 847           List.fold_right2
 848             (fun cty pbo (i, acc, s, menv) ->
 849                pp (lazy ("begin iteration"));
 850               (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
 851                *   (new_)outty right_par (K_i left_par k_par) *)
 852                let infty_pbo, _ =
 853                  add_params menv s context cty outty mty m i in
 854                pp
 855                 (lazy ("CASE: infty_pbo: "^ status#ppterm
 856                  ~context ~metasenv ~subst infty_pbo));
 857                let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
 858                  add_params menv s context cty new_outty mty m i in
 859                pp
 860                 (lazy ("CASE: expty_pbo: "^ status#ppterm
 861                  ~context ~metasenv ~subst expty_pbo));
 862                let pbo = add_lambda_for_refl_m pbo eqs cty in
 863                pp
 864                  (lazy ("CASE: pbo: " ^ status#ppterm
 865                  ~context ~metasenv ~subst pbo));
 866                let metasenv, subst, pbo, _ =
 867                  try_coercions status ~localise menv s context pbo
 868                  orig_t (*??*) infty_pbo (`XTSome expty_pbo) exc
 869                in
 870                pp
 871                  (lazy ("CASE: pbo2: " ^ status#ppterm
 872                  ~context ~metasenv ~subst pbo));
 873                (i-1, pbo::acc, subst, metasenv))
 874             cl pl (List.length pl, [], subst, metasenv)
 875         in
 876         (*let metasenv, subst =
 877           try
 878             NCicUnification.unify status metasenv subst context outty new_outty
 879           with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
 880         in*)
 881         let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
 882         pp (lazy ("CASE: new_outty: " ^ (status#ppterm
 883            ~metasenv ~subst ~context new_outty)));
 884         let right_tys =
 885           List.map
 886             (fun t -> NCicTypeChecker.typeof status ~subst ~metasenv context t) right_p in
 887         let eqs =
 888           List.map2 (fun x y -> C.Appl[eq_refl;x;y]) (right_tys@[mty])
 889             (right_p@[m]) in
 890         let t = C.Appl (C.Match(r,new_outty,m,pl) :: eqs)
 891         in
 892         metasenv, subst, t, expty (*}}}*)
 893     | _,`XTSome expty,C.LetIn(name,ty,t,bo) ->
 894         pp (lazy "LETIN");
 895         let name' = mk_fresh_name context name in
 896         let context_bo = (name', C.Def (t,ty)) :: context in
 897         let metasenv, subst, bo2, _ =
 898           try_coercions status ~localise metasenv subst context_bo
 899            bo orig_t (NCicSubstitution.lift status 1 infty)
 900            (`XTSome (NCicSubstitution.lift status 1 expty)) exc
 901         in
 902         let coerced = C.LetIn (name',ty,t,bo2) in
 903         pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
 904         metasenv, subst, coerced, expty
 905     | C.Prod (nameprod, src, ty),`XTSome (C.Prod (_, src2, ty2) as expty), _ ->
 906         (*{{{*) pp (lazy "LAM");
 907         pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
 908         let namename = match t with C.Lambda (n,_,_) -> n | _ -> nameprod in
 909         let name_con = mk_fresh_name context namename in
 910         let context_src2 = ((name_con, C.Decl src2) :: context) in
 911         (* contravariant part: the argument of f:src->ty *)
 912         let metasenv, subst, rel1, _ =
 913           try_coercions status ~localise metasenv subst context_src2
 914            (C.Rel 1) orig_t (NCicSubstitution.lift status 1 src2)
 915            (`XTSome (NCicSubstitution.lift status 1 src)) exc
 916         in
 917         (* covariant part: the result of f(c x); x:src2; (c x):src *)
 918         let name_t, bo =
 919           match t with
 920           | C.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo)
 921           | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift status 1 t) [rel1]
 922         in
 923         (* we fix the possible dependency problem in the source ty *)
 924         let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in
 925         let metasenv, subst, bo, _ =
 926           try_coercions status ~localise metasenv subst context_src2
 927             bo orig_t ty (`XTSome ty2) exc
 928         in
 929         let coerced = C.Lambda (name_t,src2, bo) in
 930         pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
 931         metasenv, subst, coerced, expty (*}}}*)
 932     | _ -> raise exc
 933   with _ ->
 934   let expty =
 935    match expty with
 936       `XTSome expty -> expty
 937     | `XTSort ->
 938         C.Sort (C.Type
 939          (match NCicEnvironment.get_universes () with
 940            | x::_ -> x
 941            | _ -> assert false))
 942     | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
 943     | `XTInd -> assert false(*CSC: was not handled, OCaml 4.0 complains. ??? *)
 944   in
 945   pp(lazy("try_coercion " ^
 946     status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
 947     status#ppterm ~metasenv ~subst ~context expty));
 948     first exc
 949       (NCicCoercion.look_for_coercion
 950         status metasenv subst context infty expty)
 951
 952 and force_to_sort status metasenv subst context t orig_t localise ty =
 953   try
 954     let metasenv, subst, ty =
 955       NCicUnification.sortfy status (Failure "sortfy") metasenv subst context ty in
 956       metasenv, subst, t, ty
 957   with
 958       Failure _ ->
 959         let msg =
 960          (lazy (localise orig_t,
 961            "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
 962            " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
 963         let ty = NCicReduction.whd status ~subst context ty in
 964         let exn =
 965          if NCicUnification.could_reduce status ~subst context ty then
 966           Uncertain msg
 967          else
 968           RefineFailure msg
 969         in
 970           try_coercions status ~localise metasenv subst context
 971             t orig_t ty `XTSort exn
 972
 973 and force_to_inductive status metasenv subst context t orig_t localise ty =
 974   try
 975     let metasenv, subst, ty =
 976       NCicUnification.indfy status (Failure "indfy") metasenv subst context ty in
 977       metasenv, subst, t, ty
 978   with
 979       Failure _ ->
 980         let msg =
 981          (lazy (localise orig_t,
 982            "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
 983            " is not a (co)inductive type: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
 984         let ty = NCicReduction.whd status ~subst context ty in
 985 (* prerr_endline ("#### " ^ status#ppterm ~metasenv ~subst ~context ty); *)
 986         let exn =
 987          if NCicUnification.could_reduce status ~subst context ty then
 988           Uncertain msg
 989          else
 990           RefineFailure msg
 991         in
 992           raise exn
 993 (* FG: this should be as follows but the case `XTInd is not imp;emented yet
 994           try_coercions status ~localise metasenv subst context
 995             t orig_t ty `XTInd exn
 996 *)
 997
 998 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
 999  t (t1, t2)
1000 =
1001    (* force to sort is done in the Prod case in typeof *)
1002    match t1, t2 with
1003    | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
1004    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
1005         metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2))
1006    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
1007    | C.Meta _, C.Sort _
1008    | C.Meta _, C.Meta (_,(_,_))
1009    | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2
1010    | x, (C.Sort _ | C.Meta _) | _, x ->
1011       let y, context, orig =
1012         if x == t1 then s, context, orig_s
1013         else t, ((name,C.Decl s)::context), orig_t
1014       in
1015       raise (RefineFailure (lazy (localise orig,Printf.sprintf
1016         "%s is expected to be a type, but its type is %s that is not a sort"
1017          (status#ppterm ~subst ~metasenv ~context y)
1018          (status#ppterm ~subst ~metasenv ~context x))))
1019
1020 and guess_name status subst ctx ty =
1021   let aux initial = "#" ^ String.make 1 initial in
1022   match ty with
1023   | C.Const (Ref.Ref (u,_))
1024   | C.Appl (C.Const (Ref.Ref (u,_)) :: _) ->
1025       aux (String.sub (NUri.name_of_uri u) 0 1).[0]
1026   | C.Prod _ -> aux 'f'
1027   | C.Meta (n,lc) ->
1028       (try
1029          let _,_,t,_ = NCicUtils.lookup_subst n subst in
1030          guess_name status subst ctx (NCicSubstitution.subst_meta status lc t)
1031       with NCicUtils.Subst_not_found _ -> aux 'M')
1032   | _ -> aux 'H'
1033
1034 and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
1035   (*D*)inside 'E'; try let rc =
1036   let rec aux metasenv subst args_so_far he ty_he xxx =
1037   (*D*)inside 'V'; try let rc =
1038    match xxx with
1039   | [] ->
1040      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
1041      pp(lazy("FORCE FINAL APPL: " ^
1042        status#ppterm ~metasenv ~subst ~context res ^
1043        " of type " ^ status#ppterm ~metasenv ~subst ~context ty_he
1044        ^ " to type " ^ match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
1045                                       | `XTNone -> "None" | `XTSome x ->
1046        status#ppterm ~metasenv ~subst ~context x));
1047      (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
1048       * the application may also be a lambda! *)
1049      force_ty false false metasenv subst context orig_t res ty_he expty
1050   | C.Implicit `Vector::tl ->
1051       let has_some_more_pis x =
1052         match NCicReduction.whd status ~subst context x with
1053         |  C.Meta _ | C.Appl (C.Meta _::_) -> false
1054         | _ -> true
1055       in
1056      (try
1057        aux metasenv subst args_so_far he ty_he tl
1058       with
1059       | Uncertain _
1060       | RefineFailure _ as exc when has_some_more_pis ty_he ->
1061           (try
1062            aux metasenv subst args_so_far he ty_he
1063             (C.Implicit `Term :: C.Implicit `Vector :: tl)
1064           with
1065            Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
1066      | RefineFailure msg when not (has_some_more_pis ty_he) ->
1067         (* instantiating the head could change the has_some_more_pis flag *)
1068         raise (Uncertain msg))
1069   | arg::tl ->
1070       match NCicReduction.whd status ~subst context ty_he with
1071       | C.Prod (_,s,t) ->
1072           let metasenv, subst, arg, _ =
1073             typeof status ~localise metasenv subst context arg (`XTSome s) in
1074           let t = NCicSubstitution.subst status ~avoid_beta_redexes:true arg t in
1075           aux metasenv subst (arg :: args_so_far) he t tl
1076       | C.Meta _
1077       | C.Appl (C.Meta _ :: _) as t ->
1078           let metasenv, subst, arg, ty_arg =
1079             typeof status ~localise metasenv subst context arg `XTNone in
1080           let name = guess_name status subst context ty_arg in
1081           let metasenv, _, meta, _ =
1082             NCicMetaSubst.mk_meta metasenv
1083               ((name,C.Decl ty_arg) :: context) `IsType
1084           in
1085           let flex_prod = C.Prod (name, ty_arg, meta) in
1086           (* next line grants that ty_args is a type *)
1087           let metasenv,subst, flex_prod, _ =
1088            typeof status ~localise metasenv subst context flex_prod `XTSort in
1089 (*
1090           pp (lazy ( "UNIFICATION in CTX:\n"^
1091             status#ppcontext ~metasenv ~subst context
1092             ^ "\nOF: " ^
1093             status#ppterm ~metasenv ~subst ~context t ^  " === " ^
1094             status#ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
1095 *)
1096           let metasenv, subst =
1097              try NCicUnification.unify status metasenv subst context t flex_prod
1098              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
1099               ("The term %s has an inferred type %s, but is applied to the" ^^
1100                " argument %s of type %s")
1101               (status#ppterm ~metasenv ~subst ~context he)
1102               (status#ppterm ~metasenv ~subst ~context t)
1103               (status#ppterm ~metasenv ~subst ~context arg)
1104               (status#ppterm ~metasenv ~subst ~context ty_arg)))
1105                  (match exc with
1106                  | NCicUnification.UnificationFailure m ->
1107                      NCicUnification.Uncertain m
1108                  | x -> x))
1109               (* XXX coerce to funclass *)
1110           in
1111           let meta = NCicSubstitution.subst status ~avoid_beta_redexes:true arg meta in
1112           aux metasenv subst (arg :: args_so_far) he meta tl
1113       | C.Match (_,_,C.Meta _,_)
1114       | C.Match (_,_,C.Appl (C.Meta _ :: _),_)
1115       | C.Appl (C.Const (Ref.Ref (_, Ref.Fix _)) :: _) ->
1116           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
1117             ("The term %s is here applied to %d arguments but expects " ^^
1118             "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
1119             (List.length args) (List.length args_so_far))))
1120       | ty ->
1121           let metasenv, subst, newhead, newheadty =
1122             try_coercions status ~localise metasenv subst context
1123               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
1124               `XTProd
1125               (RefineFailure (lazy (localise orig_he, Printf.sprintf
1126                ("The term %s is here applied to %d arguments but expects " ^^
1127                "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
1128                (List.length args) (List.length args_so_far))))
1129           in
1130            aux metasenv subst [] newhead newheadty (arg :: tl)
1131   (*D*)in outside true; rc with exc -> outside false; raise exc
1132   in
1133    (* We need to reverse the order of the new created metas since they
1134       are pushed on top of the metasenv in the wrong order *)
1135    let highest_meta = NCicMetaSubst.maxmeta () in
1136    let metasenv, subst, newhead, newheadty =
1137     aux metasenv subst [] he ty_he args in
1138    let metasenv_old,metasenv_new =
1139     List.partition (fun (i,_) -> i <= highest_meta) metasenv
1140    in
1141     (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
1142   (*D*)in outside true; rc with exc -> outside false; raise exc
1143 ;;
1144
1145 let rec first f l1 l2 =
1146   match l1,l2 with
1147   | x1::tl1, x2::tl2 ->
1148       (try f x1 x2 with Not_found -> first f tl1 tl2)
1149   | _ -> raise Not_found
1150 ;;
1151
1152 let rec find add dt t =
1153   if dt == add then t
1154   else
1155     let dl, l =
1156       match dt, t with
1157       | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
1158       | C.Appl dl,C.Appl l -> dl,l
1159       | C.Lambda (_,ds,dt), C.Lambda (_,s,t)
1160       | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
1161       | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t]
1162       | C.Match (_,dot,dt,dl),  C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
1163       | _ -> raise Not_found
1164     in
1165       first (find add) dl l
1166 ;;
1167
1168 let relocalise old_localise dt t add =
1169   old_localise
1170     (try find add dt t with Not_found -> assert false)
1171 ;;
1172
1173 let undebruijnate status inductive ref t rev_fl =
1174   let len = List.length rev_fl in
1175   NCicSubstitution.psubst status (fun x -> x)
1176    (HExtlib.list_mapi
1177       (fun (_,_,rno,_,_,_) i ->
1178          let i = len - i - 1 in
1179          C.Const
1180            (if inductive then Ref.mk_fix i rno ref
1181             else Ref.mk_cofix i ref))
1182       rev_fl)
1183     t
1184 ;;
1185
1186
1187 let typeof_obj
1188   status ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
1189 =
1190   match obj with
1191   | C.Constant (relevance, name, bo, ty, attr) ->
1192        let metasenv, subst, ty =
1193          check_type status ~localise metasenv subst [] ty in
1194        let metasenv, subst, bo, ty, height =
1195          match bo with
1196          | Some bo ->
1197              let metasenv, subst, bo, ty =
1198                typeof status ~localise metasenv subst [] bo (`XTSome ty) in
1199              let height = (* XXX recalculate *) height in
1200                metasenv, subst, Some bo, ty, height
1201          | None -> metasenv, subst, None, ty, 0
1202        in
1203        uri, height, metasenv, subst,
1204          C.Constant (relevance, name, bo, ty, attr)
1205   | C.Fixpoint (inductive, fl, attr) ->
1206       let len = List.length fl in
1207       let types, metasenv, subst, rev_fl =
1208         List.fold_left
1209          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
1210            let metasenv, subst, ty =
1211              check_type status ~localise metasenv subst [] ty in
1212            let dbo = NCicTypeChecker.debruijn status uri len [] ~subst bo in
1213            let localise = relocalise localise dbo bo in
1214             (name,C.Decl ty)::types,
1215               metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
1216          ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
1217       in
1218       let metasenv, subst, fl =
1219         List.fold_left
1220           (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
1221             let metasenv, subst, dbo, ty =
1222               typeof status ~localise metasenv subst types dbo (`XTSome ty)
1223             in
1224             metasenv, subst, (relevance,name,k,ty,dbo)::fl)
1225           (metasenv, subst, []) rev_fl
1226       in
1227       let height = (* XXX recalculate *) height in
1228       let fl =
1229         List.map
1230           (fun (relevance,name,k,ty,dbo) ->
1231             let bo =
1232               undebruijnate status inductive
1233                (Ref.reference_of_spec uri
1234                  (if inductive then Ref.Fix (0,k,0)
1235                   else Ref.CoFix 0)) dbo rev_fl
1236             in
1237               relevance,name,k,ty,bo)
1238           fl
1239       in
1240        uri, height, metasenv, subst,
1241          C.Fixpoint (inductive, fl, attr)
1242   | C.Inductive (ind, leftno, itl, attr) ->
1243      let len = List.length itl in
1244      let metasenv,subst,rev_itl,tys =
1245       List.fold_left
1246        (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
1247           let metasenv, subst, ty =
1248             check_type status ~localise metasenv subst [] ty in
1249           metasenv,subst,(relevance,n,ty,cl)::res,(n,C.Decl ty)::ctx
1250        ) (metasenv,subst,[],[]) itl in
1251      let metasenv,subst,itl,_ =
1252       List.fold_left
1253        (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
1254          let context,ty_sort = NCicReduction.split_prods status ~subst [] ~-1 ty in
1255          let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
1256          let metasenv,subst,cl =
1257           List.fold_right
1258            (fun (k_relev,n,te) (metasenv,subst,res) ->
1259              let k_relev =
1260               try snd (HExtlib.split_nth leftno k_relev)
1261               with Failure _ -> k_relev in
1262              let te = NCicTypeChecker.debruijn status uri len [] ~subst te in
1263              let metasenv, subst, te =
1264                check_type status ~localise metasenv subst tys te in
1265              let context,te = NCicReduction.split_prods status ~subst tys leftno te in
1266              let _,chopped_context_rev =
1267               HExtlib.split_nth (List.length tys) (List.rev context) in
1268              let sx_context_te_rev,_ =
1269               HExtlib.split_nth leftno chopped_context_rev in
1270              let metasenv,subst,_ =
1271               try
1272                List.fold_left2
1273                 (fun (metasenv,subst,context) item1 item2 ->
1274                   let (metasenv,subst),convertible =
1275                    try
1276                     match item1,item2 with
1277                       (n1,C.Decl ty1),(n2,C.Decl ty2) ->
1278                         if n1 = n2 then
1279                          NCicUnification.unify status ~test_eq_only:true metasenv
1280                           subst context ty1 ty2,true
1281                         else
1282                          (metasenv,subst),false
1283                     | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
1284                         if n1 = n2 then
1285                          let metasenv,subst =
1286                           NCicUnification.unify status ~test_eq_only:true metasenv
1287                            subst context ty1 ty2
1288                          in
1289                           NCicUnification.unify status ~test_eq_only:true metasenv
1290                            subst context bo1 bo2,true
1291                         else
1292                          (metasenv,subst),false
1293                     | _,_ -> (metasenv,subst),false
1294                    with
1295                    | NCicUnification.Uncertain _
1296                    | NCicUnification.UnificationFailure _ ->
1297                       (metasenv,subst),false
1298                   in
1299                    let term2 =
1300                     match item2 with
1301                        _,C.Decl t -> t
1302                      | _,C.Def (b,_) -> b in
1303                    if not convertible then
1304                     raise (RefineFailure (lazy (localise term2,
1305                      ("Mismatch between the left parameters of the constructor " ^
1306                       "and those of its inductive type"))))
1307                    else
1308                     metasenv,subst,item1::context
1309                 ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
1310               with Invalid_argument "List.fold_left2" -> assert false in
1311              let metasenv, subst =
1312                 let rec aux context (metasenv,subst) = function
1313                   | C.Meta _ -> metasenv, subst
1314                   | C.Implicit _ -> metasenv, subst
1315                   | C.Appl (C.Rel i :: args)
1316                       when i > List.length context - len ->
1317                       let lefts, _ = HExtlib.split_nth leftno args in
1318                       let ctxlen = List.length context in
1319                       let (metasenv, subst), _ =
1320                         List.fold_left
1321                         (fun ((metasenv, subst),l) arg ->
1322                           NCicUnification.unify status
1323                            ~test_eq_only:true metasenv subst context arg
1324                              (C.Rel (ctxlen - len - l)), l+1
1325                           )
1326                         ((metasenv, subst), 0) lefts
1327                       in
1328                       metasenv, subst
1329                   | t -> NCicUtils.fold (fun e c -> e::c) context aux
1330                   (metasenv,subst) t
1331                 in
1332                aux context (metasenv,subst) te
1333              in
1334              let con_sort= NCicTypeChecker.typeof status ~subst ~metasenv context te in
1335               (match
1336                 NCicReduction.whd status ~subst context con_sort,
1337                 NCicReduction.whd status ~subst [] ty_sort
1338                with
1339                   (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
1340                    if not (NCicEnvironment.universe_leq u1 u2) then
1341                     raise
1342                      (RefineFailure
1343                        (lazy(localise te, "The type " ^
1344                          status#ppterm ~metasenv ~subst ~context s1 ^
1345                          " of the constructor is not included in the inductive"^
1346                          " type sort " ^
1347                          status#ppterm ~metasenv ~subst ~context s2)))
1348                 | C.Sort _, C.Sort C.Prop
1349                 | C.Sort _, C.Sort C.Type _ -> ()
1350                 | _, _ ->
1351                    raise
1352                     (RefineFailure
1353                       (lazy (localise te,
1354                         "Wrong constructor or inductive arity shape"))));
1355               (* let's check also the positivity conditions *)
1356               if
1357                not
1358                (NCicTypeChecker.are_all_occurrences_positive status
1359                  ~subst context uri leftno (i+leftno) leftno (len+leftno) te)
1360               then
1361                 raise
1362                   (RefineFailure
1363                     (lazy (localise te,
1364                       "Non positive occurence in " ^
1365                         status#ppterm ~metasenv ~subst ~context te)))
1366               else
1367                let relsno = List.length itl + leftno in
1368                let te =
1369                  NCicSubstitution.psubst status
1370                   (fun i ->
1371                     if i <= leftno  then
1372                      C.Rel i
1373                     else
1374                      C.Const (Ref.reference_of_spec uri
1375                       (Ref.Ind (ind,relsno - i,leftno))))
1376                   (HExtlib.list_seq 1 (relsno+1))
1377                    te in
1378                let te =
1379                 List.fold_right
1380                  (fun (name,decl) te ->
1381                    match decl with
1382                       C.Decl ty -> C.Prod (name,ty,te)
1383                     | C.Def (bo,ty) -> C.LetIn (name,ty,bo,te)
1384                  ) sx_context_te_rev te
1385                in
1386                 metasenv,subst,(k_relev,n,te)::res
1387               ) cl (metasenv,subst,[])
1388          in
1389           metasenv,subst,(it_relev,n,ty,cl)::res,i+1
1390        ) (metasenv,subst,[],1) rev_itl
1391      in
1392       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
1393 ;;
1394
1395 (* vim:set foldmethod=marker: *)