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